From d814c472ab59f34e52a354498f3e87ef4096ce4b Mon Sep 17 00:00:00 2001 From: Floris van Doorn Date: Wed, 28 Jun 2017 13:14:48 +0100 Subject: [PATCH] add strunc file for truncatedness/truncations of spectra --- algebra/module_exact_couple.hlean | 14 ++-- homotopy/spectrum.hlean | 5 +- homotopy/strunc.hlean | 52 ++++++++++++ pointed.hlean | 21 +++++ pointed_pi.hlean | 133 +++++++++++++++++++++--------- 5 files changed, 177 insertions(+), 48 deletions(-) create mode 100644 homotopy/strunc.hlean diff --git a/algebra/module_exact_couple.hlean b/algebra/module_exact_couple.hlean index bde504c..80c4762 100644 --- a/algebra/module_exact_couple.hlean +++ b/algebra/module_exact_couple.hlean @@ -485,13 +485,14 @@ namespace pointed open prod prod.ops fiber parameters {A : ℤ → Type*[1]} (f : Π(n : ℤ), A n →* A (n - 1)) [Hf : Πn, is_conn_fun 1 (f n)] include Hf - definition I [constructor] : Set := trunctype.mk (ℤ × ℤ) !is_trunc_prod + protected definition I [constructor] : Set := trunctype.mk (gℤ ×g gℤ) !is_trunc_prod + local abbreviation I := @pointed.I - definition D_sequence : graded_module rℤ I := - λv, LeftModule_int_of_AbGroup (πc[v.2] (A (v.1))) + -- definition D_sequence : graded_module rℤ I := + -- λv, LeftModule_int_of_AbGroup (πc[v.2] (A (v.1))) - definition E_sequence : graded_module rℤ I := - λv, LeftModule_int_of_AbGroup (πc[v.2] (pconntype.mk (pfiber (f (v.1))) !Hf pt)) + -- definition E_sequence : graded_module rℤ I := + -- λv, LeftModule_int_of_AbGroup (πc[v.2] (pconntype.mk (pfiber (f (v.1))) !Hf pt)) /- first need LES of these connected homotopy groups -/ @@ -509,7 +510,8 @@ namespace spectrum parameters {A : ℤ → spectrum} (f : Π(s : ℤ), A s →ₛ A (s - 1)) - definition I [constructor] : Set := trunctype.mk (gℤ ×g gℤ) !is_trunc_prod + protected definition I [constructor] : Set := trunctype.mk (gℤ ×g gℤ) !is_trunc_prod + local abbreviation I := @spectrum.I definition D_sequence : graded_module rℤ I := λv, LeftModule_int_of_AbGroup (πₛ[v.1] (A (v.2))) diff --git a/homotopy/spectrum.hlean b/homotopy/spectrum.hlean index 4df2fbd..214e230 100644 --- a/homotopy/spectrum.hlean +++ b/homotopy/spectrum.hlean @@ -151,13 +151,14 @@ namespace spectrum -- I guess this manual eta-expansion is necessary because structures lack definitional eta? := phomotopy.mk (glue_square f n) (to_homotopy_pt (glue_square f n)) - definition sid {N : succ_str} (E : gen_prespectrum N) : E →ₛ E := + definition sid [constructor] [refl] {N : succ_str} (E : gen_prespectrum N) : E →ₛ E := smap.mk (λn, pid (E n)) (λn, calc glue E n ∘* pid (E n) ~* glue E n : pcompose_pid ... ~* pid (Ω(E (S n))) ∘* glue E n : pid_pcompose ... ~* Ω→(pid (E (S n))) ∘* glue E n : pwhisker_right (glue E n) ap1_pid⁻¹*) - definition scompose {N : succ_str} {X Y Z : gen_prespectrum N} (g : Y →ₛ Z) (f : X →ₛ Y) : X →ₛ Z := + definition scompose [trans] {N : succ_str} {X Y Z : gen_prespectrum N} + (g : Y →ₛ Z) (f : X →ₛ Y) : X →ₛ Z := smap.mk (λn, g n ∘* f n) (λn, calc glue Z n ∘* to_fun g n ∘* to_fun f n ~* (glue Z n ∘* to_fun g n) ∘* to_fun f n : passoc diff --git a/homotopy/strunc.hlean b/homotopy/strunc.hlean new file mode 100644 index 0000000..73ce3cf --- /dev/null +++ b/homotopy/strunc.hlean @@ -0,0 +1,52 @@ +import .spectrum .EM + +open int trunc eq is_trunc lift unit pointed equiv is_equiv algebra EM +namespace spectrum + +definition trunc_int.{u} (k : ℤ) (X : Type.{u}) : Type.{u} := +begin + induction k with k k, exact trunc k X, + cases k with k, exact trunc -1 X, + exact lift unit +end + +definition ptrunc_int.{u} (k : ℤ) (X : pType.{u}) : pType.{u} := +begin + induction k with k k, exact ptrunc k X, + exact plift punit +end + +definition ptrunc_int_pequiv_ptrunc_int (k : ℤ) {X Y : Type*} (e : X ≃* Y) : + ptrunc_int k X ≃* ptrunc_int k Y := +begin + induction k with k k, + exact ptrunc_pequiv_ptrunc k e, + exact !pequiv_plift⁻¹ᵉ* ⬝e* !pequiv_plift +end + +definition ptrunc_int_change_int {k l : ℤ} (X : Type*) (p : k = l) : + ptrunc_int k X ≃* ptrunc_int l X := +pequiv_ap (λn, ptrunc_int n X) p + +definition loop_ptrunc_int_pequiv (k : ℤ) (X : Type*) : + Ω (ptrunc_int (k+1) X) ≃* ptrunc_int k (Ω X) := +begin + induction k with k k, + exact loop_ptrunc_pequiv k X, + cases k with k, + change Ω (ptrunc 0 X) ≃* plift punit, + exact !loop_pequiv_punit_of_is_set ⬝e* !pequiv_plift, + exact loop_pequiv_loop !pequiv_plift⁻¹ᵉ* ⬝e* !loop_punit ⬝e* !pequiv_plift +end + +definition strunc_int [constructor] (k : ℤ) (E : spectrum) : spectrum := +spectrum.MK (λ(n : ℤ), ptrunc_int (k + n) (E n)) + (λ(n : ℤ), ptrunc_int_pequiv_ptrunc_int (k + n) (equiv_glue E n) ⬝e* + (loop_ptrunc_int_pequiv (k + n) (E (n+1)))⁻¹ᵉ* ⬝e* + loop_pequiv_loop (ptrunc_int_change_int _ (add.assoc k n 1))) + +definition strunc_int_change_int [constructor] {k l : ℤ} (E : spectrum) (p : k = l) : + strunc_int k E →ₛ strunc_int l E := +begin induction p, reflexivity end + +end spectrum diff --git a/pointed.hlean b/pointed.hlean index c71e2fc..62adf6c 100644 --- a/pointed.hlean +++ b/pointed.hlean @@ -182,4 +182,25 @@ namespace pointed sorry end psquare + + definition ap1_pequiv_ap {A : Type} (B : A → Type*) {a a' : A} (p : a = a') : + Ω→ (pequiv_ap B p) ~* pequiv_ap (Ω ∘ B) p := + begin induction p, apply ap1_pid end + + definition pequiv_ap_natural {A : Type} (B C : A → Type*) {a a' : A} (p : a = a') + (f : Πa, B a →* C a) : + psquare (pequiv_ap B p) (pequiv_ap C p) (f a) (f a') := + begin induction p, exact phrfl end + + definition pequiv_ap_natural2 {A : Type} (B C : A → Type*) {a a' : A} (p : a = a') + (f : Πa, B a →* C a) : + psquare (pequiv_ap B p) (pequiv_ap C p) (f a) (f a') := + begin induction p, exact phrfl end + + definition loop_pequiv_punit_of_is_set (X : Type*) [is_set X] : Ω X ≃* punit := + pequiv_punit_of_is_contr _ (is_contr_of_inhabited_prop pt) + + definition loop_punit : Ω punit ≃* punit := + loop_pequiv_punit_of_is_set punit + end pointed diff --git a/pointed_pi.hlean b/pointed_pi.hlean index 911de4a..1ddc00b 100644 --- a/pointed_pi.hlean +++ b/pointed_pi.hlean @@ -63,21 +63,21 @@ namespace pointed variable (k) protected definition ppi_homotopy.refl : k ~~* k := - sorry + ppi_homotopy.mk homotopy.rfl !idp_con variable {k} protected definition ppi_homotopy.rfl [refl] : k ~~* k := ppi_homotopy.refl k protected definition ppi_homotopy.symm [symm] (p : k ~~* l) : l ~~* k := - sorry + ppi_homotopy.mk p⁻¹ʰᵗʸ (inv_con_eq_of_eq_con (ppi_to_homotopy_pt p)⁻¹) protected definition ppi_homotopy.trans [trans] (p : k ~~* l) (q : l ~~* m) : k ~~* m := - sorry + ppi_homotopy.mk (λa, p a ⬝ q a) (!con.assoc ⬝ whisker_left (p pt) (ppi_to_homotopy_pt q) ⬝ ppi_to_homotopy_pt p) infix ` ⬝*' `:75 := ppi_homotopy.trans postfix `⁻¹*'`:(max+1) := ppi_homotopy.symm - definition ppi_equiv_pmap (A B : Type*) : (Π*(a : A), B) ≃ (A →* B) := + definition ppi_equiv_pmap [constructor] (A B : Type*) : (Π*(a : A), B) ≃ (A →* B) := begin fapply equiv.MK, { intro k, induction k with k p, exact pmap.mk k p }, @@ -86,9 +86,19 @@ namespace pointed { intro k, induction k with k p, reflexivity } end - definition pppi_pequiv_ppmap (A B : Type*) : (Π*(a : A), B) ≃* ppmap A B := + definition pppi_pequiv_ppmap [constructor] (A B : Type*) : (Π*(a : A), B) ≃* ppmap A B := pequiv_of_equiv (ppi_equiv_pmap A B) idp + protected definition ppi_gen.sigma_char [constructor] {A : Type*} (B : A → Type) (b₀ : B pt) : + ppi_gen B b₀ ≃ Σ(k : Πa, B a), k pt = b₀ := + begin + fapply equiv.MK: intro x, + { constructor, exact ppi_gen.resp_pt x }, + { induction x, constructor, assumption }, + { induction x, reflexivity }, + { induction x, reflexivity } + end + definition ppi.sigma_char [constructor] {A : Type*} (B : A → Type*) : (Π*(a : A), B a) ≃ Σ(k : (Π (a : A), B a)), k pt = pt := begin @@ -99,15 +109,6 @@ namespace pointed all_goals reflexivity end - protected definition ppi_gen.sigma_char [constructor] {A : Type*} (B : A → Type) (b₀ : B pt) : - ppi_gen B b₀ ≃ Σ(k : Πa, B a), k pt = b₀ := - begin - fapply equiv.MK: intro x, - { constructor, exact ppi_gen.resp_pt x }, - { induction x, constructor, assumption }, - { induction x, reflexivity }, - { induction x, reflexivity } - end variables (k l) @@ -206,7 +207,7 @@ namespace pointed definition pmap_compose_ppi_const_left (f : Π*(a : A), P a) : pmap_compose_ppi (λa, pconst (P a) (Q a)) f ~~* ppi_const Q := - sorry + ppi_homotopy.mk homotopy.rfl !ap_constant⁻¹ definition ppi_compose_left [constructor] (g : Π(a : A), ppmap (P a) (Q a)) : (Π*(a : A), P a) →* Π*(a : A), Q a := @@ -214,16 +215,19 @@ namespace pointed definition pmap_compose_ppi_phomotopy_left [constructor] {g g' : Π(a : A), ppmap (P a) (Q a)} (f : Π*(a : A), P a) (p : Πa, g a ~* g' a) : pmap_compose_ppi g f ~~* pmap_compose_ppi g' f := - sorry + ppi_homotopy.mk (λa, p a (f a)) + abstract !con.assoc⁻¹ ⬝ whisker_right _ !ap_con_eq_con_ap⁻¹ ⬝ !con.assoc ⬝ + whisker_left _ (to_homotopy_pt (p pt)) end definition pmap_compose_ppi_pid_left [constructor] (f : Π*(a : A), P a) : pmap_compose_ppi (λa, pid (P a)) f ~~* f := - sorry + ppi_homotopy.mk homotopy.rfl idp - definition pmap_compose_pmap_compose_ppi [constructor] (h : Π(a : A), ppmap (Q a) (R a)) + definition pmap_compose_ppi_pcompose [constructor] (h : Π(a : A), ppmap (Q a) (R a)) (g : Π(a : A), ppmap (P a) (Q a)) : - pmap_compose_ppi h (pmap_compose_ppi g f) ~~* pmap_compose_ppi (λa, h a ∘* g a) f := - sorry + pmap_compose_ppi (λa, h a ∘* g a) f ~~* pmap_compose_ppi h (pmap_compose_ppi g f) := + ppi_homotopy.mk homotopy.rfl + abstract !idp_con ⬝ whisker_right _ (!ap_con ⬝ whisker_right _ !ap_compose'⁻¹) ⬝ !con.assoc end definition ppi_pequiv_right [constructor] (g : Π(a : A), P a ≃* Q a) : (Π*(a : A), P a) ≃* Π*(a : A), Q a := @@ -231,11 +235,11 @@ namespace pointed apply pequiv_of_pmap (ppi_compose_left g), apply adjointify _ (ppi_compose_left (λa, (g a)⁻¹ᵉ*)), { intro f, apply ppi_eq, - refine !pmap_compose_pmap_compose_ppi ⬝*' _, + refine !pmap_compose_ppi_pcompose⁻¹*' ⬝*' _, refine pmap_compose_ppi_phomotopy_left _ (λa, !pright_inv) ⬝*' _, apply pmap_compose_ppi_pid_left }, { intro f, apply ppi_eq, - refine !pmap_compose_pmap_compose_ppi ⬝*' _, + refine !pmap_compose_ppi_pcompose⁻¹*' ⬝*' _, refine pmap_compose_ppi_phomotopy_left _ (λa, !pleft_inv) ⬝*' _, apply pmap_compose_ppi_pid_left } end @@ -255,28 +259,41 @@ namespace pointed pequiv_of_equiv (fiber.sigma_char f pt) idp /- the pointed type of unpointed (nondependent) maps -/ - definition parrow [constructor] (A : Type) (B : Type*) : Type* := + definition upmap [constructor] (A : Type) (B : Type*) : Type* := pointed.MK (A → B) (const A pt) /- the pointed type of unpointed dependent maps -/ - definition p_pi [constructor] {A : Type} (B : A → Type*) : Type* := + definition uppi [constructor] {A : Type} (B : A → Type*) : Type* := pointed.MK (Πa, B a) (λa, pt) - definition ppmap.sigma_char (A B : Type*) : - ppmap A B ≃* @psigma_gen (parrow A B) (λf, f pt = pt) idp := + notation `Πᵘ*` binders `, ` r:(scoped P, uppi P) := r + infix ` →ᵘ* `:30 := upmap + + definition ppmap.sigma_char [constructor] (A B : Type*) : + ppmap A B ≃* @psigma_gen (A →ᵘ* B) (λf, f pt = pt) idp := pequiv_of_equiv pmap.sigma_char idp - definition pppi.sigma_char {A : Type*} {B : A → Type*} : - (Π*(a : A), B a) ≃* @psigma_gen (p_pi B) (λf, f pt = pt) idp := + definition pppi.sigma_char [constructor] {A : Type*} (B : A → Type*) : + (Π*(a : A), B a) ≃* @psigma_gen (Πᵘ*a, B a) (λf, f pt = pt) idp := proof pequiv_of_equiv !ppi.sigma_char idp qed - definition psigma_gen_pequiv_psigma_gen_right {A : Type*} {B B' : A → Type} + definition psigma_gen_pequiv_psigma_gen [constructor] {A A' : Type*} {B : A → Type} + {B' : A' → Type} {b : B pt} {b' : B' pt} (f : A ≃* A') + (g : Πa, B a ≃ B' (f a)) (p : g pt b =[respect_pt f] b') : psigma_gen B b ≃* psigma_gen B' b' := + pequiv_of_equiv (sigma_equiv_sigma f g) (sigma_eq (respect_pt f) p) + + definition psigma_gen_pequiv_psigma_gen_left [constructor] {A A' : Type*} {B : A' → Type} + {b : B pt} (f : A ≃* A') {b' : B (f pt)} (q : b' =[respect_pt f] b) : + psigma_gen (B ∘ f) b' ≃* psigma_gen B b := + psigma_gen_pequiv_psigma_gen f (λa, erfl) q + + definition psigma_gen_pequiv_psigma_gen_right [constructor] {A : Type*} {B B' : A → Type} {b : B pt} {b' : B' pt} (f : Πa, B a ≃ B' a) (p : f pt b = b') : psigma_gen B b ≃* psigma_gen B' b' := - pequiv_of_equiv (sigma_equiv_sigma_right f) (ap (dpair pt) p) + psigma_gen_pequiv_psigma_gen pequiv.rfl f (pathover_idp_of_eq p) - definition psigma_gen_pequiv_psigma_gen_basepoint {A : Type*} {B : A → Type} {b b' : B pt} - (p : b = b') : psigma_gen B b ≃* psigma_gen B b' := + definition psigma_gen_pequiv_psigma_gen_basepoint [constructor] {A : Type*} {B : A → Type} + {b b' : B pt} (p : b = b') : psigma_gen B b ≃* psigma_gen B b' := psigma_gen_pequiv_psigma_gen_right (λa, erfl) p definition ppi_gen_functor_right [constructor] {A : Type*} {B B' : A → Type} @@ -336,23 +353,59 @@ namespace pointed (p : b = b') : ppi_gen B b ≃ ppi_gen B b' := ppi_gen_equiv_ppi_gen_right (λa, erfl) p - definition ppi_psigma {A : Type*} {B : A → Type*} (C : Πa, B a → Type) (c : Πa, C a pt) : - (Π*(a : A), (psigma_gen (C a) (c a))) ≃* + open sigma.ops + + definition psigma_gen_pi_pequiv_uppi_psigma_gen [constructor] {A : Type*} {B : A → Type*} + (C : Πa, B a → Type) (c : Πa, C a pt) : + @psigma_gen (Πᵘ*a, B a) (λf, Πa, C a (f a)) c ≃* Πᵘ*a, psigma_gen (C a) (c a) := + pequiv_of_equiv sigma_pi_equiv_pi_sigma idp + + definition uppi_psigma_gen_pequiv_psigma_gen_pi [constructor] {A : Type*} {B : A → Type*} + (C : Πa, B a → Type) (c : Πa, C a pt) : + (Πᵘ*a, psigma_gen (C a) (c a)) ≃* @psigma_gen (Πᵘ*a, B a) (λf, Πa, C a (f a)) c := + pequiv_of_equiv sigma_pi_equiv_pi_sigma⁻¹ᵉ idp + + definition psigma_gen_assoc [constructor] {A : Type*} {B : A → Type} (C : Πa, B a → Type) + (b₀ : B pt) (c₀ : C pt b₀) : + psigma_gen (λa, Σb, C a b) ⟨b₀, c₀⟩ ≃* @psigma_gen (psigma_gen B b₀) (λv, C v.1 v.2) c₀ := + pequiv_of_equiv !sigma_assoc_equiv idp + + definition psigma_gen_swap [constructor] {A : Type*} {B B' : A → Type} + (C : Π⦃a⦄, B a → B' a → Type) (b₀ : B pt) (b₀' : B' pt) (c₀ : C b₀ b₀') : + @psigma_gen (psigma_gen B b₀ ) (λv, Σb', C v.2 b') ⟨b₀', c₀⟩ ≃* + @psigma_gen (psigma_gen B' b₀') (λv, Σb , C b v.2) ⟨b₀ , c₀⟩ := + !psigma_gen_assoc⁻¹ᵉ* ⬝e* psigma_gen_pequiv_psigma_gen_right (λa, !sigma_comm_equiv) idp ⬝e* + !psigma_gen_assoc + + definition ppi_psigma.{u v w} {A : pType.{u}} {B : A → pType.{v}} (C : Πa, B a → Type.{w}) + (c : Πa, C a pt) : (Π*(a : A), (psigma_gen (C a) (c a))) ≃* psigma_gen (λ(f : Π*(a : A), B a), ppi_gen (λa, C a (f a)) - (transport (C pt) (ppi.resp_pt f)⁻¹ (c pt))) - (ppi_const _) := + (transport (C pt) (ppi.resp_pt f)⁻¹ (c pt))) (ppi_const _) := + proof calc (Π*(a : A), psigma_gen (C a) (c a)) - ≃* @psigma_gen (p_pi (λa, psigma_gen (C a) (c a))) (λf, f pt = pt) idp : pppi.sigma_char + ≃* @psigma_gen (Πᵘ*a, psigma_gen (C a) (c a)) (λf, f pt = pt) idp : pppi.sigma_char + ... ≃* @psigma_gen (@psigma_gen (Πᵘ*a, B a) (λf, Πa, C a (f a)) c) + (λv, Σ(p : v.1 pt = pt), v.2 pt =[p] c pt) ⟨idp, idpo⟩ : + by exact psigma_gen_pequiv_psigma_gen (uppi_psigma_gen_pequiv_psigma_gen_pi C c) + (λf, sigma_eq_equiv _ _) idpo + ... ≃* @psigma_gen (@psigma_gen (Πᵘ*a, B a) (λf, f pt = pt) idp) + (λv, Σ(g : Πa, C a (v.1 a)), g pt =[v.2] c pt) ⟨c, idpo⟩ : + by apply psigma_gen_swap ... ≃* psigma_gen (λ(f : Π*(a : A), B a), ppi_gen (λa, C a (f a)) (transport (C pt) (ppi.resp_pt f)⁻¹ (c pt))) - (ppi_const _) : sorry + (ppi_const _) : + by exact (psigma_gen_pequiv_psigma_gen (pppi.sigma_char B) + (λf, !ppi_gen.sigma_char ⬝e sigma_equiv_sigma_right (λg, !pathover_equiv_eq_tr⁻¹ᵉ)) + idpo)⁻¹ᵉ* + qed definition pmap_psigma {A B : Type*} (C : B → Type) (c : C pt) : ppmap A (psigma_gen C c) ≃* psigma_gen (λ(f : ppmap A B), ppi_gen (C ∘ f) (transport C (respect_pt f)⁻¹ c)) (ppi_const _) := - !pppi_pequiv_ppmap⁻¹ᵉ* ⬝e* !ppi_psigma ⬝e* sorry - + !pppi_pequiv_ppmap⁻¹ᵉ* ⬝e* !ppi_psigma ⬝e* + sorry +-- psigma_gen_pequiv_psigma_gen (pppi_pequiv_ppmap A B) (λf, begin esimp, exact ppi_gen_equiv_ppi_gen_right (λa, _) _ end) _ definition pfiber_ppcompose_left (f : B →* C) : pfiber (@ppcompose_left A B C f) ≃* ppmap A (pfiber f) :=