From e92fb0a4354a96a01c02fc0e4bb97fa931c5fe78 Mon Sep 17 00:00:00 2001 From: Floris van Doorn Date: Sat, 8 Jul 2017 15:11:11 +0100 Subject: [PATCH] prove two of the sorry's in cohomology --- homotopy/cohomology.hlean | 30 +++++++++---- homotopy/spectrum.hlean | 92 ++++++++++++++++++++------------------- pointed.hlean | 17 +++++++- pointed_pi.hlean | 26 +++++++++-- 4 files changed, 108 insertions(+), 57 deletions(-) diff --git a/homotopy/cohomology.hlean b/homotopy/cohomology.hlean index cb6e3c7..799aa8f 100644 --- a/homotopy/cohomology.hlean +++ b/homotopy/cohomology.hlean @@ -70,14 +70,6 @@ definition cohomology_equiv_shomotopy_group_sp_cotensor (X : Type*) (Y : spectru trunc_equiv_trunc 0 (!pfunext ⬝e loop_pequiv_loop !pfunext ⬝e loopn_pequiv_loopn 2 (pequiv_of_eq (ap (λn, ppmap X (Y n)) (add.comm n 2 ⬝ ap (add 2) !neg_neg⁻¹)))) -definition cohomology_isomorphism_shomotopy_group_sp_cotensor (X : Type*) (Y : spectrum) {n m : ℤ} - (p : -m = n) : H^n[X, Y] ≃g πₛ[m] (sp_cotensor X Y) := -sorry /- TODO FOR SSS -/ - -definition unreduced_cohomology_isomorphism_shomotopy_group_sp_ucotensor (X : Type) (Y : spectrum) - {n m : ℤ} (p : -m = n) : uH^n[X, Y] ≃g πₛ[m] (sp_ucotensor X Y) := -sorry /- TODO FOR SSS -/ - definition parametrized_cohomology_isomorphism_shomotopy_group_spi {X : Type*} (Y : X → spectrum) {n m : ℤ} (p : -m = n) : pH^n[(x : X), Y x] ≃g πₛ[m] (spi X Y) := begin @@ -90,8 +82,25 @@ end definition unreduced_parametrized_cohomology_isomorphism_shomotopy_group_supi {X : Type} (Y : X → spectrum) {n m : ℤ} (p : -m = n) : upH^n[(x : X), Y x] ≃g πₛ[m] (supi X Y) := +begin + refine parametrized_cohomology_isomorphism_shomotopy_group_spi (add_point_spectrum Y) p ⬝g _, + apply shomotopy_group_isomorphism_of_pequiv, intro k, + apply pppi_add_point_over +end + +definition cohomology_isomorphism_shomotopy_group_sp_cotensor (X : Type*) (Y : spectrum) {n m : ℤ} + (p : -m = n) : H^n[X, Y] ≃g πₛ[m] (sp_cotensor X Y) := sorry /- TODO FOR SSS -/ +definition unreduced_cohomology_isomorphism_shomotopy_group_sp_ucotensor (X : Type) (Y : spectrum) + {n m : ℤ} (p : -m = n) : uH^n[X, Y] ≃g πₛ[m] (sp_ucotensor X Y) := +begin + refine cohomology_isomorphism_shomotopy_group_sp_cotensor X₊ Y p ⬝g _, + apply shomotopy_group_isomorphism_of_pequiv, intro k, apply ppmap_add_point +end + + + /- functoriality -/ definition cohomology_functor [constructor] {X X' : Type*} (f : X' →* X) (Y : spectrum) @@ -133,7 +142,10 @@ sorry /- TODO FOR SSS -/ definition parametrized_cohomology_isomorphism_right {X : Type*} {Y Y' : X → spectrum} (e : Πx n, Y x n ≃* Y' x n) (n : ℤ) : pH^n[(x : X), Y x] ≃g pH^n[(x : X), Y' x] := -sorry /- TODO FOR SSS -/ +parametrized_cohomology_isomorphism_shomotopy_group_spi Y !neg_neg ⬝g +shomotopy_group_isomorphism_of_pequiv (-n) (λk, ppi_pequiv_right sorry) ⬝g +(parametrized_cohomology_isomorphism_shomotopy_group_spi Y' !neg_neg)⁻¹ᵍ +--sorry /- TODO FOR SSS -/ definition unreduced_parametrized_cohomology_isomorphism_right {X : Type} {Y Y' : X → spectrum} (e : Πx n, Y x n ≃* Y' x n) (n : ℤ) : upH^n[(x : X), Y x] ≃g upH^n[(x : X), Y' x] := diff --git a/homotopy/spectrum.hlean b/homotopy/spectrum.hlean index fa79d72..dee9f5d 100644 --- a/homotopy/spectrum.hlean +++ b/homotopy/spectrum.hlean @@ -191,7 +191,7 @@ namespace spectrum exact smap.mk f fsq, end - definition smap_to_sigma_isretr {N : succ_str} {X Y : gen_prespectrum N} (f : smap_sigma X Y) : + definition smap_to_sigma_isretr {N : succ_str} {X Y : gen_prespectrum N} (f : smap_sigma X Y) : smap_to_sigma (smap_to_struc f) = f := begin induction f, reflexivity @@ -472,7 +472,7 @@ namespace spectrum (phtpy n) (ap1_phomotopy (phtpy (S n))) (glue_square f n) - (glue_square g n) + (glue_square g n) definition shomotopy_to_sigma [unfold 6] {N : succ_str} {X Y : gen_prespectrum N} {f g : X →ₛ Y} (H : f ~ₛ g) : shomotopy_sigma f g := begin @@ -500,7 +500,7 @@ namespace spectrum induction H, reflexivity end - definition shomotopy_sigma_equiv [constructor] {N : succ_str} {X Y : gen_prespectrum N} (f g : X →ₛ Y) : + definition shomotopy_sigma_equiv [constructor] {N : succ_str} {X Y : gen_prespectrum N} (f g : X →ₛ Y) : shomotopy_sigma f g ≃ (f ~ₛ g) := begin fapply equiv.mk, @@ -524,17 +524,17 @@ namespace spectrum (eq.eq_equiv_homotopy) ⬝e pi_equiv_pi_right (λ n, pmap_eq_equiv (f n) (g n)) /- - definition ppi_homotopy_rec_on_eq [recursor] + definition ppi_homotopy_rec_on_eq [recursor] {k' : ppi_gen B x₀} - {Q : (k ~~* k') → Type} - (p : k ~~* k') - (H : Π(q : k = k'), Q (ppi_homotopy_of_eq q)) + {Q : (k ~~* k') → Type} + (p : k ~~* k') + (H : Π(q : k = k'), Q (ppi_homotopy_of_eq q)) : Q p := ppi_homotopy_of_eq_of_ppi_homotopy p ▸ H (eq_of_ppi_homotopy p) -/ definition fam_phomotopy_rec_on_eq {N : Type} {X Y : N → Type*} (f g : Π n, X n →* Y n) - {Q : (Π n, f n ~* g n) → Type} - (p : Π n, f n ~* g n) + {Q : (Π n, f n ~* g n) → Type} + (p : Π n, f n ~* g n) (H : Π (q : f = g), Q (fam_phomotopy_of_eq f g q)) : Q p := begin refine _ ▸ H ((fam_phomotopy_of_eq f g)⁻¹ᵉ p), @@ -557,7 +557,7 @@ set_option pp.coercions true definition fam_phomotopy_rec_on_idp {N : Type} {X Y : N → Type*} (f : Π n, X n →* Y n) (Q : Π (g : Π n, X n →* Y n) (H : Π n, f n ~* g n), Type) - (q : Q f (λ n, phomotopy.rfl)) + (q : Q f (λ n, phomotopy.rfl)) (g : Π n, X n →* Y n) (H : Π n, f n ~* g n) : Q g H := begin fapply fam_phomotopy_rec_on_eq, @@ -579,16 +579,16 @@ set_option pp.coercions true intro n, esimp at *, revert g H gsq Hsq n, - refine fam_phomotopy_rec_on_idp f _ _, + refine fam_phomotopy_rec_on_idp f _ _, intro gsq Hsq n, refine change_path _ _, -- have p : eq_of_homotopy (λ n, eq_of_phomotopy phomotopy.rfl) = refl f, reflexivity, refine (eq_of_homotopy_eta rfl)⁻¹ ⬝ _, fapply ap (eq_of_homotopy), fapply eq_of_homotopy, intro n, refine (eq_of_phomotopy_refl _)⁻¹, --- fapply eq_of_ppi_homotopy, +-- fapply eq_of_ppi_homotopy, fapply pathover_idp_of_eq, - note Hsq' := ptube_v_eq_bot phomotopy.rfl (ap1_phomotopy_refl _) (fsq n) (gsq n) (Hsq n), + note Hsq' := ptube_v_eq_bot phomotopy.rfl (ap1_phomotopy_refl _) (fsq n) (gsq n) (Hsq n), unfold ptube_v at *, unfold phsquare at *, refine _ ⬝ Hsq'⁻¹ ⬝ _, @@ -656,20 +656,20 @@ set_option pp.coercions true gen_spectrum N := spectrum.MK (λn, Π*a, E a n) (λn, !ppi_loop_pequiv⁻¹ᵉ* ∘*ᵉ ppi_pequiv_right (λa, equiv_glue (E a) n)) - + definition ppi_assoc_compose_left {A : Type*} {B C D : A → Type*} (f : Π (a : A), B a →* C a) (g : Π (a : A), C a →* D a) : (ppi_compose_left g ∘* ppi_compose_left f) ~* ppi_compose_left (λ a, g a ∘* f a) := begin - fapply phomotopy.mk, + fapply phomotopy.mk, intro h, fapply eq_of_ppi_homotopy, fapply ppi_homotopy.mk, -- intro a, reflexivity, --- esimp, +-- esimp, repeat exact sorry, end /- TODO FOR SSS -/ - definition psquare_of_ppi_compose_left {A : Type*} {B C D E : A → Type*} + definition psquare_of_ppi_compose_left {A : Type*} {B C D E : A → Type*} {ftop : Π (a : A), B a →* C a} {fbot : Π (a : A), D a →* E a} {fleft : Π (a : A), B a →* D a} {fright : Π (a : A), C a →* E a} (psq : Π (a :A), psquare (ftop a) (fbot a) (fleft a) (fright a)) @@ -681,15 +681,15 @@ set_option pp.coercions true := begin refine (ppi_assoc_compose_left ftop fright) ⬝* _ ⬝* (ppi_assoc_compose_left fleft fbot)⁻¹*, - refine eq_of_homotopy (λ a, eq_of_phomotopy (psq a)) ▸ phomotopy.rfl, + refine eq_of_homotopy (λ a, eq_of_phomotopy (psq a)) ▸ phomotopy.rfl, -- the last step is probably an unnecessary application of function extensionality. end - definition spi_compose_left_topsq - {N : succ_str} {A : Type*} {E F : A → gen_spectrum N} (f : Π a, (E a) →ₛ (F a)) (n : N) - : psquare - (ppi_compose_left (λ a, f a n)) - (ppi_compose_left (λ a, Ω→ (f a (S n)))) + definition spi_compose_left_topsq + {N : succ_str} {A : Type*} {E F : A → gen_spectrum N} (f : Π a, (E a) →ₛ (F a)) (n : N) + : psquare + (ppi_compose_left (λ a, f a n)) + (ppi_compose_left (λ a, Ω→ (f a (S n)))) (ppi_pequiv_right (λ a, equiv_glue (E a) n)) (ppi_pequiv_right (λ a, equiv_glue (F a) n)) := @@ -731,17 +731,17 @@ set_option pp.coercions true begin intro n, fapply psquare_of_phomotopy, - refine - (passoc _ _ (ppi_compose_left (λ a, to_fun (f a) n))) - ⬝* _ ⬝* - (passoc (!ppi_loop_pequiv⁻¹ᵉ*) - (ppi_compose_left (λ a, Ω→ (f a (S n)))) + refine + (passoc _ _ (ppi_compose_left (λ a, to_fun (f a) n))) + ⬝* _ ⬝* + (passoc (!ppi_loop_pequiv⁻¹ᵉ*) + (ppi_compose_left (λ a, Ω→ (f a (S n)))) (ppi_pequiv_right (λa, equiv_glue (E a) n)))⁻¹* - ⬝* _ ⬝* - (passoc (Ω→ (ppi_compose_left (λ a, to_fun (f a) (S n)))) _ _), - { refine (pwhisker_left (ppi_loop_pequiv⁻¹ᵉ*) _), + ⬝* _ ⬝* + (passoc (Ω→ (ppi_compose_left (λ a, to_fun (f a) (S n)))) _ _), + { refine (pwhisker_left (ppi_loop_pequiv⁻¹ᵉ*) _), fapply spi_compose_left_topsq}, - { refine (pwhisker_right (ppi_pequiv_right (λ a, equiv_glue (E a) n)) _), + { refine (pwhisker_right (ppi_pequiv_right (λ a, equiv_glue (E a) n)) _), fapply spi_compose_left_botsq}, end @@ -936,7 +936,7 @@ set_option pp.coercions true glue X n -- And similarly we need the pointed homotopies witnessing that the squares commute - definition to_prespectrification_psq {N : succ_str} (X : gen_prespectrum N) (n : N) : + definition to_prespectrification_psq {N : succ_str} (X : gen_prespectrum N) (n : N) : psquare (to_prespectrification_pfun X n) (Ω→ (to_prespectrification_pfun X (S n))) (glue X n) (glue (prespectrification X) n) := psquare_of_phomotopy phomotopy.rfl @@ -966,10 +966,10 @@ set_option pp.coercions true -- In the following we define the underlying family of pointed maps of such an extension definition is_sconnected_to_prespectrification_inv_pfun {N : succ_str} {X : gen_prespectrum N} {E : gen_spectrum N} : (X →ₛ E) → Π (n : N), prespectrification X n →* E n := - λ (f : X →ₛ E) n, (equiv_glue E n)⁻¹ᵉ* ∘* Ω→ (f (S n)) + λ (f : X →ₛ E) n, (equiv_glue E n)⁻¹ᵉ* ∘* Ω→ (f (S n)) -- In the following we define the commuting squares of the extension - definition is_sconnected_to_prespectrification_inv_psq {N : succ_str} {X : gen_prespectrum N} {E : gen_spectrum N} (f : X →ₛ E) (n : N) : + definition is_sconnected_to_prespectrification_inv_psq {N : succ_str} {X : gen_prespectrum N} {E : gen_spectrum N} (f : X →ₛ E) (n : N) : psquare (is_sconnected_to_prespectrification_inv_pfun f n) (Ω→ (is_sconnected_to_prespectrification_inv_pfun f (S n))) (glue (prespectrification X) n) @@ -986,7 +986,7 @@ set_option pp.coercions true end -- Now we bundle the definition into a map (X →ₛ E) → (prespectrification X →ₛ E) - definition is_sconnected_to_prespectrification_inv {N : succ_str} (X : gen_prespectrum N) (E : gen_spectrum N) + definition is_sconnected_to_prespectrification_inv {N : succ_str} (X : gen_prespectrum N) (E : gen_spectrum N) : (X →ₛ E) → (prespectrification X →ₛ E) := begin intro f, @@ -1235,19 +1235,23 @@ spectrify_fun (smash_prespectrum_fun f g) spectrum.MK (λn, plift punit) (λn, pequiv_of_is_contr _ _ _ _) definition shomotopy_group_sunit.{u} (n : ℤ) : πₛ[n] sunit.{u} ≃g trivial_ab_group_lift.{u} := - have H : 0 <[ℕ] 2, from !zero_lt_succ, - isomorphism_of_is_contr (@trivial_homotopy_group_of_is_trunc _ _ _ !is_trunc_lift H) - !is_trunc_lift + phomotopy_group_plift_punit 2 + + definition add_point_spectrum [constructor] {X : Type} (Y : X → spectrum) (x : X₊) : spectrum := + spectrum.MK (λn, add_point_over (λx, Y x n) x) + begin + intro n, induction x with x, + apply pequiv_of_is_contr, + apply is_trunc_lift, + apply is_contr_loop_of_is_contr, apply is_trunc_lift, + exact equiv_glue (Y x) n + end open option - definition add_point_spectrum [unfold 3] {X : Type} (Y : X → spectrum) : X₊ → spectrum - | (some x) := Y x - | none := sunit - definition shomotopy_group_add_point_spectrum {X : Type} (Y : X → spectrum) (n : ℤ) : Π(x : X₊), πₛ[n] (add_point_spectrum Y x) ≃g add_point_AbGroup (λ (x : X), πₛ[n] (Y x)) x | (some x) := by reflexivity - | none := shomotopy_group_sunit n + | none := proof phomotopy_group_plift_punit 2 qed /- The Eilenberg-MacLane spectrum -/ diff --git a/pointed.hlean b/pointed.hlean index fe5b507..a1ba9f8 100644 --- a/pointed.hlean +++ b/pointed.hlean @@ -4,7 +4,7 @@ import types.pointed2 .move_to_lib -open pointed eq equiv function is_equiv unit is_trunc trunc nat algebra sigma group +open pointed eq equiv function is_equiv unit is_trunc trunc nat algebra sigma group lift option namespace pointed @@ -227,5 +227,20 @@ namespace pointed phomotopy.mk (λa, ap f !is_prop.elim ⬝ respect_pt f ⬝ (respect_pt g)⁻¹ ⬝ ap g !is_prop.elim) begin rewrite [▸*, is_prop_elim_self, +ap_idp, idp_con, con_idp, inv_con_cancel_right] end + definition add_point_over [unfold 3] {A : Type} (B : A → Type*) : A₊ → Type* + | (some a) := B a + | none := plift punit + + definition phomotopy_group_plift_punit.{u} (n : ℕ) [H : is_at_least_two n] : + πag[n] (plift.{0 u} punit) ≃g trivial_ab_group_lift.{u} := + begin + induction H with n, + have H : 0 <[ℕ] n+2, from !zero_lt_succ, + have is_set unit, from _, + have is_trunc (trunc_index.of_nat 0) punit, from this, + exact isomorphism_of_is_contr (@trivial_homotopy_group_of_is_trunc _ _ _ !is_trunc_lift H) + !is_trunc_lift + end + end pointed diff --git a/pointed_pi.hlean b/pointed_pi.hlean index 4423012..8185b42 100644 --- a/pointed_pi.hlean +++ b/pointed_pi.hlean @@ -6,7 +6,7 @@ Authors: Ulrik Buchholtz, Floris van Doorn import homotopy.connectedness types.pointed2 .move_to_lib .pointed -open eq pointed equiv sigma is_equiv trunc +open eq pointed equiv sigma is_equiv trunc option /- In this file we define dependent pointed maps and properties of them. @@ -153,8 +153,6 @@ namespace pointed : sigma_equiv_sigma_right (λp, eq_equiv_eq_symm _ _) ... ≃ (k ~~* l) : ppi_homotopy.sigma_char k l - - variables -- the same as pmap_eq variables {k l} definition ppi_eq (h : k ~~* l) : k = l := @@ -471,6 +469,28 @@ namespace pointed -- definition pppi_ppmap {A C : Type*} {B : A → Type*} : -- ppmap (/- dependent smash of B -/) C ≃* Π*(a : A), ppmap (B a) C := + definition ppi_add_point_over {A : Type} (B : A → Type*) : + (Π*a, add_point_over B a) ≃ Πa, B a := + begin + fapply equiv.MK, + { intro f a, exact f (some a) }, + { intro f, fconstructor, + intro a, cases a, exact pt, exact f a, + reflexivity }, + { intro f, reflexivity }, + { intro f, cases f with f p, apply ppi_eq, fapply ppi_homotopy.mk, + { intro a, cases a, exact p⁻¹, reflexivity }, + { exact con.left_inv p }}, + end + + definition pppi_add_point_over {A : Type} (B : A → Type*) : + (Π*a, add_point_over B a) ≃* Πᵘ*a, B a := + pequiv_of_equiv (ppi_add_point_over B) idp + + definition ppmap_add_point {A : Type} (B : Type*) : + ppmap A₊ B ≃* A →ᵘ* B := + pequiv_of_equiv (pmap_equiv_left A B) idp + -- TODO: homotopy_of_eq and apd10 should be the same -- TODO: there is also apd10_eq_of_homotopy in both pi and eq(?)