From 2e55a4a4efe08ff0fb3ae015160943657dbcdd0f Mon Sep 17 00:00:00 2001 From: spiceghello Date: Fri, 9 Jun 2017 11:51:04 -0600 Subject: [PATCH] fwedge_prespectrum --- homotopy/spectrum.hlean | 14 +++++++++++++- 1 file changed, 13 insertions(+), 1 deletion(-) diff --git a/homotopy/spectrum.hlean b/homotopy/spectrum.hlean index ce7c8df..6e7b713 100644 --- a/homotopy/spectrum.hlean +++ b/homotopy/spectrum.hlean @@ -5,7 +5,7 @@ Authors: Michael Shulman, Floris van Doorn -/ -import homotopy.LES_of_homotopy_groups .splice ..colim types.pointed2 .EM ..pointed_pi .smash_adjoint ..algebra.seq_colim +import homotopy.LES_of_homotopy_groups .splice ..colim types.pointed2 .EM ..pointed_pi .smash_adjoint ..algebra.seq_colim .fwedge open eq nat int susp pointed pmap sigma is_equiv equiv fiber algebra trunc trunc_index pi group seq_colim succ_str EM EM.ops function @@ -593,5 +593,17 @@ spectrify_fun (smash_prespectrum_fun f g) definition EM_spectrum /-[constructor]-/ (G : AbGroup) : spectrum := spectrum.Mk (K G) (λn, (loop_EM G n)⁻¹ᵉ*) + /- Wedge of prespectra -/ + +open fwedge + + definition fwedge_prespectrum.{u v} {I : Type.{v}} (X : I -> prespectrum.{u}) : prespectrum.{max u v} := + begin + fconstructor, + { intro n, exact fwedge (λ i, X i n) }, + { intro n, fapply fwedge_pmap, + intro i, exact Ω→ !pinl ∘* !glue + } + end end spectrum