From 5e4c536d27ec0b9553fdbcd22bc8b2e9ff6041f1 Mon Sep 17 00:00:00 2001 From: Floris van Doorn Date: Tue, 6 Jun 2017 17:07:07 -0400 Subject: [PATCH] progress on spectrify --- colim.hlean | 50 ++++++++++++++++++++++++++++------------- homotopy/spectrum.hlean | 10 +++++++-- 2 files changed, 43 insertions(+), 17 deletions(-) diff --git a/colim.hlean b/colim.hlean index 5aaf1b5..feb238f 100644 --- a/colim.hlean +++ b/colim.hlean @@ -1,6 +1,6 @@ -- authors: Floris van Doorn, Egbert Rijke -import hit.colimit types.fin homotopy.chain_complex .move_to_lib +import hit.colimit types.fin homotopy.chain_complex types.pointed2 open seq_colim pointed algebra eq is_trunc nat is_equiv equiv sigma sigma.ops chain_complex namespace seq_colim @@ -8,7 +8,7 @@ namespace seq_colim definition pseq_colim [constructor] {X : ℕ → Type*} (f : Πn, X n →* X (n+1)) : Type* := pointed.MK (seq_colim f) (@sι _ _ 0 pt) - definition inclusion_pt [constructor] {X : ℕ → Type*} (f : Πn, X n →* X (n+1)) (n : ℕ) + definition inclusion_pt {X : ℕ → Type*} (f : Πn, X n →* X (n+1)) (n : ℕ) : inclusion f (Point (X n)) = Point (pseq_colim f) := begin induction n with n p, @@ -249,6 +249,10 @@ namespace seq_colim { exact ap (ι _) !respect_pt } end + definition pshift_equiv_pinclusion {A : ℕ → Type*} (f : Πn, A n →* A (succ n)) (n : ℕ) : + psquare (pinclusion f n) (pinclusion (λn, f (n+1)) n) (f n) (pshift_equiv f) := + phomotopy.mk homotopy.rfl begin refine !idp_con ⬝ _, esimp, exact sorry end + section functor variable {f} variables {A' : ℕ → Type} {f' : seq_diagram A'} @@ -305,6 +309,30 @@ namespace seq_colim : Π(x : seq_colim f), P x := by induction v with Pincl Pglue; exact seq_colim.rec f Pincl Pglue + definition pseq_colim_pequiv [constructor] {A A' : ℕ → Type*} {f : Π{n}, A n →* A (n+1)} + {f' : Π{n}, A' n →* A' (n+1)} (g : Π{n}, A n ≃* A' n) + (p : Π⦃n⦄, g ∘* f ~ f' ∘* g) : pseq_colim @f ≃* pseq_colim @f' := + pequiv_of_equiv (seq_colim_equiv @g p) (ap (ι _) (respect_pt g)) + + definition seq_colim_equiv_constant [constructor] {A : ℕ → Type*} {f f' : Π⦃n⦄, A n → A (n+1)} + (p : Π⦃n⦄ (a : A n), f a = f' a) : seq_colim f ≃ seq_colim f' := + seq_colim_equiv (λn, erfl) p + + definition pseq_colim_equiv_constant [constructor] {A : ℕ → Type*} {f f' : Π{n}, A n →* A (n+1)} + (p : Π⦃n⦄, f ~ f') : pseq_colim @f ≃* pseq_colim @f' := + pseq_colim_pequiv (λn, pequiv.rfl) p + + definition pseq_colim_pequiv_pinclusion {A A' : ℕ → Type*} {f : Π(n), A n →* A (n+1)} + {f' : Π(n), A' n →* A' (n+1)} (g : Π(n), A n ≃* A' n) + (p : Π⦃n⦄, g (n+1) ∘* f n ~ f' n ∘* g n) (n : ℕ) : + psquare (pinclusion f n) (pinclusion f' n) (g n) (pseq_colim_pequiv g p) := + sorry + + definition seq_colim_equiv_constant_pinclusion {A : ℕ → Type*} {f f' : Π⦃n⦄, A n →* A (n+1)} + (p : Π⦃n⦄ (a : A n), f a = f' a) (n : ℕ) : + pseq_colim_equiv_constant p ∘* pinclusion f n ~* pinclusion f' n := + sorry + definition is_equiv_seq_colim_rec (P : seq_colim f → Type) : is_equiv (seq_colim_rec_unc : (Σ(Pincl : Π ⦃n : ℕ⦄ (a : A n), P (ι f a)), @@ -327,19 +355,6 @@ namespace seq_colim equiv.mk _ !is_equiv_seq_colim_rec end functor - definition pseq_colim_pequiv [constructor] {A A' : ℕ → Type*} {f : Π{n}, A n →* A (n+1)} - {f' : Π{n}, A' n →* A' (n+1)} (g : Π{n}, A n ≃* A' n) - (p : Π⦃n⦄, g ∘* f ~ f' ∘* g) : pseq_colim @f ≃* pseq_colim @f' := - pequiv_of_equiv (seq_colim_equiv @g p) (ap (ι _) (respect_pt g)) - - definition seq_colim_equiv_constant [constructor] {A : ℕ → Type*} {f f' : Π⦃n⦄, A n → A (n+1)} - (p : Π⦃n⦄ (a : A n), f a = f' a) : seq_colim f ≃ seq_colim f' := - seq_colim_equiv (λn, erfl) p - - definition pseq_colim_equiv_constant [constructor] {A : ℕ → Type*} {f f' : Π{n}, A n →* A (n+1)} - (p : Π⦃n⦄, f ~ f') : pseq_colim @f ≃* pseq_colim @f' := - pseq_colim_pequiv (λn, pequiv.rfl) p - definition pseq_colim.elim [constructor] {A : ℕ → Type*} {B : Type*} {f : Π{n}, A n →* A (n+1)} (g : Πn, A n →* B) (p : Πn, g (n+1) ∘* f ~ g n) : pseq_colim @f →* B := begin @@ -361,6 +376,7 @@ namespace seq_colim theorem prep0_succ_lemma {A : ℕ → Type*} (f : pseq_diagram A) (n : ℕ) (p : rep0 (λn x, f x) n pt = rep0 (λn x, f x) n pt) (q : prep0 f n (Point (A 0)) = Point (A n)) + : loop_equiv_eq_closed (ap (@f n) q ⬝ respect_pt (@f n)) (ap (@f n) p) = Ω→(@f n) (loop_equiv_eq_closed q p) := by rewrite [▸*, con_inv, ↑ap1_gen, +ap_con, ap_inv, +con.assoc] @@ -466,6 +482,10 @@ namespace seq_colim { exact sorry } end + definition pseq_colim_loop_pinclusion {X : ℕ → Type*} (f : Πn, X n →* X (n+1)) (n : ℕ) : + pseq_colim_loop f ∘* Ω→ (pinclusion f n) ~* pinclusion (λn, Ω→(f n)) n := + sorry + -- open succ_str -- definition pseq_colim_succ_str_change_index' {N : succ_str} {B : N → Type*} (n : N) (m : ℕ) -- (h : Πn, B n →* B (S n)) : diff --git a/homotopy/spectrum.hlean b/homotopy/spectrum.hlean index 0cf3cf0..953faf3 100644 --- a/homotopy/spectrum.hlean +++ b/homotopy/spectrum.hlean @@ -396,8 +396,8 @@ namespace spectrum definition spectrify_pequiv {N : succ_str} (X : gen_prespectrum N) (n : N) : spectrify_type X n ≃* Ω (spectrify_type X (S n)) := begin - refine _ ⬝e* !pseq_colim_loop⁻¹ᵉ*, refine !pshift_equiv ⬝e* _, + refine _ ⬝e* !pseq_colim_loop⁻¹ᵉ*, transitivity pseq_colim (λk, spectrify_type_fun' X (succ k) (S n +' k)), rotate 1, refine pseq_colim_equiv_constant (λn, !ap1_pcompose⁻¹*), fapply pseq_colim_pequiv, @@ -426,7 +426,13 @@ namespace spectrum begin fapply smap.mk, { intro n, exact pinclusion _ 0 }, - { intro n, exact sorry } + { intro n, apply phomotopy_of_psquare, refine !pid_pcompose⁻¹* ⬝ph* _, + refine !pid_pcompose⁻¹* ⬝ph* _, + --pshift_equiv_pinclusion (spectrify_type_fun X n) 0 + refine _ ⬝v* _, + rotate 1, exact pshift_equiv_pinclusion (spectrify_type_fun X n) 0, + exact sorry +} end definition spectrify.elim {N : succ_str} {X : gen_prespectrum N} {Y : gen_spectrum N}