From a7b746c8130fc28405984e3f7352cff7806185cf Mon Sep 17 00:00:00 2001 From: Floris van Doorn Date: Wed, 24 May 2017 08:25:58 -0400 Subject: [PATCH] define parametrized cohomology --- algebra/arrow_group.hlean | 163 ++++++++++++++++++++++++-------------- homotopy/cohomology.hlean | 88 ++++---------------- homotopy/spectrum.hlean | 38 +++++---- move_to_lib.hlean | 11 +++ pointed_pi.hlean | 84 ++++++++++++++++++-- 5 files changed, 228 insertions(+), 156 deletions(-) diff --git a/algebra/arrow_group.hlean b/algebra/arrow_group.hlean index 7cfa23d..eb8001f 100644 --- a/algebra/arrow_group.hlean +++ b/algebra/arrow_group.hlean @@ -1,14 +1,63 @@ -import algebra.group_theory ..pointed eq2 -open pi pointed algebra group eq equiv is_trunc trunc +/- various groups of maps. Most importantly we define a group structure on trunc 0 (A →* Ω B), + which is used in the definition of cohomology -/ +--author: Floris van Doorn + +import algebra.group_theory ..pointed ..pointed_pi eq2 +open pi pointed algebra group eq equiv is_trunc trunc susp namespace group + /- We first define the group structure on A →* Ω B (except for truncatedness). + Instead of Ω B, we could also choose any infinity group. However, we need various 2-coherences, + so it's easier to just do it for the loop space. -/ definition pmap_mul [constructor] {A B : Type*} (f g : A →* Ω B) : A →* Ω B := pmap.mk (λa, f a ⬝ g a) (respect_pt f ◾ respect_pt g ⬝ !idp_con) definition pmap_inv [constructor] {A B : Type*} (f : A →* Ω B) : A →* Ω B := pmap.mk (λa, (f a)⁻¹ᵖ) (respect_pt f)⁻² + /- we prove some coherences of the multiplication. We don't need them for the group structure, but they + are used to show that cohomology satisfies the Eilenberg-Steenrod axioms -/ + definition ap1_pmap_mul {X Y : Type*} (f g : X →* Ω Y) : + Ω→ (pmap_mul f g) ~* pmap_mul (Ω→ f) (Ω→ g) := + begin + fconstructor, + { intro p, esimp, + refine ap1_gen_con_left (respect_pt f) (respect_pt f) + (respect_pt g) (respect_pt g) p ⬝ _, + refine !whisker_right_idp ◾ !whisker_left_idp2, }, + { refine !con.assoc ⬝ _, + refine _ ◾ idp ⬝ _, rotate 1, + rexact ap1_gen_con_left_idp (respect_pt f) (respect_pt g), esimp, + refine !con.assoc ⬝ _, + apply whisker_left, apply inv_con_eq_idp, + refine !con2_con_con2 ⬝ ap011 concat2 _ _: + refine eq_of_square (!natural_square ⬝hp !ap_id) ⬝ !con_idp } + end + + definition pmap_mul_pcompose {A B C : Type*} (g h : B →* Ω C) (f : A →* B) : + pmap_mul g h ∘* f ~* pmap_mul (g ∘* f) (h ∘* f) := + begin + fconstructor, + { intro p, reflexivity }, + { esimp, refine !idp_con ⬝ _, refine !con2_con_con2⁻¹ ⬝ whisker_right _ _, + refine !ap_eq_ap011⁻¹ } + end + + definition pcompose_pmap_mul {A B C : Type*} (h : B →* C) (f g : A →* Ω B) : + Ω→ h ∘* pmap_mul f g ~* pmap_mul (Ω→ h ∘* f) (Ω→ h ∘* g) := + begin + fconstructor, + { intro p, exact ap1_con h (f p) (g p) }, + { refine whisker_left _ !con2_con_con2⁻¹ ⬝ _, refine !con.assoc⁻¹ ⬝ _, + refine whisker_right _ (eq_of_square !ap1_gen_con_natural) ⬝ _, + refine !con.assoc ⬝ whisker_left _ _, apply ap1_gen_con_idp } + end + + definition loop_psusp_intro_pmap_mul {X Y : Type*} (f g : psusp X →* Ω Y) : + loop_psusp_intro (pmap_mul f g) ~* pmap_mul (loop_psusp_intro f) (loop_psusp_intro g) := + pwhisker_right _ !ap1_pmap_mul ⬝* !pmap_mul_pcompose + definition inf_group_pmap [constructor] [instance] (A B : Type*) : inf_group (A →* Ω B) := begin fapply inf_group.mk, @@ -33,7 +82,7 @@ namespace group !trunc_group definition Group_trunc_pmap [reducible] [constructor] (A B : Type*) : Group := - Group.mk (trunc 0 (A →* Ω (Ω B))) _ + Group.mk (trunc 0 (A →* Ω B)) _ definition Group_trunc_pmap_homomorphism [constructor] {A A' B : Type*} (f : A' →* A) : Group_trunc_pmap A B →g Group_trunc_pmap A' B := @@ -73,15 +122,15 @@ namespace group induction f with f, apply ap tr, apply eq_of_phomotopy, apply pcompose_pconst end - definition Group_trunc_pmap_pcompose [constructor] {A A' A'' B : Type*} (f : A' →* A) (f' : A'' →* A') - (g : Group_trunc_pmap A B) : Group_trunc_pmap_homomorphism (f ∘* f') g = + definition Group_trunc_pmap_pcompose [constructor] {A A' A'' B : Type*} (f : A' →* A) + (f' : A'' →* A') (g : Group_trunc_pmap A B) : Group_trunc_pmap_homomorphism (f ∘* f') g = Group_trunc_pmap_homomorphism f' (Group_trunc_pmap_homomorphism f g) := begin induction g with g, apply ap tr, apply eq_of_phomotopy, exact !passoc⁻¹* end - definition Group_trunc_pmap_phomotopy [constructor] {A A' B : Type*} {f f' : A' →* A} (p : f ~* f') : - @Group_trunc_pmap_homomorphism _ _ B f ~ Group_trunc_pmap_homomorphism f' := + definition Group_trunc_pmap_phomotopy [constructor] {A A' B : Type*} {f f' : A' →* A} + (p : f ~* f') : @Group_trunc_pmap_homomorphism _ _ B f ~ Group_trunc_pmap_homomorphism f' := begin intro g, induction g, exact ap tr (eq_of_phomotopy (pwhisker_left a p)) end @@ -95,7 +144,8 @@ namespace group apply pwhisker_left_refl end - definition ab_inf_group_pmap [constructor] [instance] (A B : Type*) : ab_inf_group (A →* Ω (Ω B)) := + definition ab_inf_group_pmap [constructor] [instance] (A B : Type*) : + ab_inf_group (A →* Ω (Ω B)) := ⦃ab_inf_group, inf_group_pmap A (Ω B), mul_comm := begin intro f g, fapply pmap_eq, @@ -110,8 +160,9 @@ namespace group definition AbGroup_trunc_pmap [reducible] [constructor] (A B : Type*) : AbGroup := AbGroup.mk (trunc 0 (A →* Ω (Ω B))) _ - /- Group of functions whose codomain is a group -/ - definition group_pi [instance] [constructor] {A : Type} (P : A → Type) [Πa, group (P a)] : group (Πa, P a) := + /- Group of dependent functions whose codomain is a group -/ + definition group_pi [instance] [constructor] {A : Type} (P : A → Type) [Πa, group (P a)] : + group (Πa, P a) := begin fapply group.mk, { apply is_trunc_pi }, @@ -140,62 +191,56 @@ namespace group { intro g h, apply eq_of_homotopy, intro a, exact respect_mul (f a) g h } end - -- definition AbGroup_trunc_pmap_homomorphism [constructor] {A A' B : Type*} (f : A' →* A) : - -- AbGroup_trunc_pmap A B →g AbGroup_trunc_pmap A' B := - -- Group_trunc_pmap_homomorphism f + /- Group of dependent functions into a loop space -/ + definition ppi_mul [constructor] {A : Type*} {B : A → Type*} (f g : Π*a, Ω (B a)) : Π*a, Ω (B a) := + proof ppi.mk (λa, f a ⬝ g a) (ppi_resp_pt f ◾ ppi_resp_pt g ⬝ !idp_con) qed + definition ppi_inv [constructor] {A : Type*} {B : A → Type*} (f : Π*a, Ω (B a)) : Π*a, Ω (B a) := + proof ppi.mk (λa, (f a)⁻¹ᵖ) (ppi_resp_pt f)⁻² qed - /- Group of functions whose codomain is a group -/ - -- definition group_arrow [instance] (A B : Type) [group B] : group (A → B) := - -- begin - -- fapply group.mk, - -- { apply is_trunc_arrow }, - -- { intro f g a, exact f a * g a }, - -- { intros, apply eq_of_homotopy, intro a, apply mul.assoc }, - -- { intro a, exact 1 }, - -- { intros, apply eq_of_homotopy, intro a, apply one_mul }, - -- { intros, apply eq_of_homotopy, intro a, apply mul_one }, - -- { intro f a, exact (f a)⁻¹ }, - -- { intros, apply eq_of_homotopy, intro a, apply mul.left_inv } - -- end + definition inf_group_ppi [constructor] [instance] {A : Type*} (B : A → Type*) : + inf_group (Π*a, Ω (B a)) := + begin + fapply inf_group.mk, + { exact ppi_mul }, + { intro f g h, fapply ppi_eq, + { intro a, exact con.assoc (f a) (g a) (h a) }, + { rexact eq_of_square (con2_assoc (ppi_resp_pt f) (ppi_resp_pt g) (ppi_resp_pt h)) }}, + { apply ppi_const }, + { intros f, fapply ppi_eq, + { intro a, exact one_mul (f a) }, + { esimp, apply eq_of_square, refine _ ⬝vp !ap_id, apply natural_square_tr }}, + { intros f, fapply ppi_eq, + { intro a, exact mul_one (f a) }, + { reflexivity }}, + { exact ppi_inv }, + { intro f, fapply ppi_eq, + { intro a, exact con.left_inv (f a) }, + { exact !con_left_inv_idp⁻¹ }}, + end - -- definition Group_arrow (A : Type) (G : Group) : Group := - -- Group.mk (A → G) _ + definition group_trunc_ppi [constructor] [instance] {A : Type*} (B : A → Type*) : + group (trunc 0 (Π*a, Ω (B a))) := + !trunc_group - -- definition ab_group_arrow [instance] (A B : Type) [ab_group B] : ab_group (A → B) := - -- ⦃ab_group, group_arrow A B, - -- mul_comm := by intros; apply eq_of_homotopy; intro a; apply mul.comm⦄ + definition Group_trunc_ppi [reducible] [constructor] {A : Type*} (B : A → Type*) : Group := + Group.mk (trunc 0 (Π*a, Ω (B a))) _ - -- definition AbGroup_arrow (A : Type) (G : AbGroup) : AbGroup := - -- AbGroup.mk (A → G) _ + definition ab_inf_group_ppi [constructor] [instance] {A : Type*} (B : A → Type*) : + ab_inf_group (Π*a, Ω (Ω (B a))) := + ⦃ab_inf_group, inf_group_ppi (λa, Ω (B a)), mul_comm := + begin + intro f g, fapply ppi_eq, + { intro a, exact eckmann_hilton (f a) (g a) }, + { rexact eq_of_square (eckmann_hilton_con2 (ppi_resp_pt f) (ppi_resp_pt g)) } + end⦄ - -- definition pgroup_ppmap [instance] (A B : Type*) [pgroup B] : pgroup (ppmap A B) := - -- begin - -- fapply pgroup.mk, - -- { apply is_trunc_pmap }, - -- { intro f g, apply pmap.mk (λa, f a * g a), - -- exact ap011 mul (respect_pt f) (respect_pt g) ⬝ !one_mul }, - -- { intros, apply pmap_eq_of_homotopy, intro a, apply mul.assoc }, - -- { intro f, apply pmap.mk (λa, (f a)⁻¹), apply inv_eq_one, apply respect_pt }, - -- { intros, apply pmap_eq_of_homotopy, intro a, apply one_mul }, - -- { intros, apply pmap_eq_of_homotopy, intro a, apply mul_one }, - -- { intros, apply pmap_eq_of_homotopy, intro a, apply mul.left_inv } - -- end + definition ab_group_trunc_ppi [constructor] [instance] {A : Type*} (B : A → Type*) : + ab_group (trunc 0 (Π*a, Ω (Ω (B a)))) := + !trunc_ab_group - -- definition Group_pmap (A : Type*) (G : Group) : Group := - -- Group_of_pgroup (ppmap A (pType_of_Group G)) + definition AbGroup_trunc_ppi [reducible] [constructor] {A : Type*} (B : A → Type*) : AbGroup := + AbGroup.mk (trunc 0 (Π*a, Ω (Ω (B a)))) _ - -- definition AbGroup_pmap (A : Type*) (G : AbGroup) : AbGroup := - -- AbGroup.mk (A →* pType_of_Group G) - -- ⦃ ab_group, Group.struct (Group_pmap A G), - -- mul_comm := by intro f g; apply pmap_eq_of_homotopy; intro a; apply mul.comm ⦄ - - -- definition Group_pmap_homomorphism [constructor] {A A' : Type*} (f : A' →* A) (G : AbGroup) : - -- Group_pmap A G →g Group_pmap A' G := - -- begin - -- fapply homomorphism.mk, - -- { intro g, exact g ∘* f}, - -- { intro g h, apply pmap_eq_of_homotopy, intro a, reflexivity } - -- end end group diff --git a/homotopy/cohomology.hlean b/homotopy/cohomology.hlean index 5326a17..1baa8b8 100644 --- a/homotopy/cohomology.hlean +++ b/homotopy/cohomology.hlean @@ -6,87 +6,23 @@ Authors: Floris van Doorn Reduced cohomology of spectra and cohomology theories -/ -import .spectrum .EM ..algebra.arrow_group .fwedge ..choice .pushout ..move_to_lib ..algebra.product_group +import .spectrum ..algebra.arrow_group .fwedge ..choice .pushout ..algebra.product_group open eq spectrum int trunc pointed EM group algebra circle sphere nat EM.ops equiv susp is_trunc function fwedge cofiber bool lift sigma is_equiv choice pushout algebra unit pi -definition is_exact_trunc_functor {A B : Type} {C : Type*} {f : A → B} {g : B → C} - (H : is_exact_t f g) : @is_exact _ _ (ptrunc 0 C) (trunc_functor 0 f) (trunc_functor 0 g) := -begin - constructor, - { intro a, esimp, induction a with a, - exact ap tr (is_exact_t.im_in_ker H a) }, - { intro b p, induction b with b, note q := !tr_eq_tr_equiv p, induction q with q, - induction is_exact_t.ker_in_im H b q with a r, - exact image.mk (tr a) (ap tr r) } -end - -definition is_exact_homotopy {A B C : Type*} {f f' : A → B} {g g' : B → C} - (p : f ~ f') (q : g ~ g') (H : is_exact f g) : is_exact f' g' := -begin - induction p using homotopy.rec_on_idp, - induction q using homotopy.rec_on_idp, - assumption -end - --- move to arrow group - -definition ap1_pmap_mul {X Y : Type*} (f g : X →* Ω Y) : - Ω→ (pmap_mul f g) ~* pmap_mul (Ω→ f) (Ω→ g) := -begin - fconstructor, - { intro p, esimp, - refine ap1_gen_con_left (respect_pt f) (respect_pt f) - (respect_pt g) (respect_pt g) p ⬝ _, - refine !whisker_right_idp ◾ !whisker_left_idp2, }, - { refine !con.assoc ⬝ _, - refine _ ◾ idp ⬝ _, rotate 1, - rexact ap1_gen_con_left_idp (respect_pt f) (respect_pt g), esimp, - refine !con.assoc ⬝ _, - apply whisker_left, apply inv_con_eq_idp, - refine !con2_con_con2 ⬝ ap011 concat2 _ _: - refine eq_of_square (!natural_square ⬝hp !ap_id) ⬝ !con_idp } -end - -definition pmap_mul_pcompose {A B C : Type*} (g h : B →* Ω C) (f : A →* B) : - pmap_mul g h ∘* f ~* pmap_mul (g ∘* f) (h ∘* f) := -begin - fconstructor, - { intro p, reflexivity }, - { esimp, refine !idp_con ⬝ _, refine !con2_con_con2⁻¹ ⬝ whisker_right _ _, - refine !ap_eq_ap011⁻¹ } -end - -definition pcompose_pmap_mul {A B C : Type*} (h : B →* C) (f g : A →* Ω B) : - Ω→ h ∘* pmap_mul f g ~* pmap_mul (Ω→ h ∘* f) (Ω→ h ∘* g) := -begin - fconstructor, - { intro p, exact ap1_con h (f p) (g p) }, - { refine whisker_left _ !con2_con_con2⁻¹ ⬝ _, refine !con.assoc⁻¹ ⬝ _, - refine whisker_right _ (eq_of_square !ap1_gen_con_natural) ⬝ _, - refine !con.assoc ⬝ whisker_left _ _, apply ap1_gen_con_idp } -end - -definition loop_psusp_intro_pmap_mul {X Y : Type*} (f g : psusp X →* Ω Y) : - loop_psusp_intro (pmap_mul f g) ~* pmap_mul (loop_psusp_intro f) (loop_psusp_intro g) := -pwhisker_right _ !ap1_pmap_mul ⬝* !pmap_mul_pcompose - -definition equiv_glue2 (Y : spectrum) (n : ℤ) : Ω (Ω (Y (n+2))) ≃* Y n := -begin - refine (!equiv_glue ⬝e* loop_pequiv_loop (!equiv_glue ⬝e* loop_pequiv_loop _))⁻¹ᵉ*, - refine pequiv_of_eq (ap Y _), - exact add.assoc n 1 1 -end - namespace cohomology -definition EM_spectrum /-[constructor]-/ (G : AbGroup) : spectrum := -spectrum.Mk (K G) (λn, (loop_EM G n)⁻¹ᵉ*) - +/- The cohomology of X with coefficients in Y is + trunc 0 (A →* Ω[2] (Y (n+2))) + In the file arrow_group (in algebra) we construct the group structor on this type. +-/ definition cohomology (X : Type*) (Y : spectrum) (n : ℤ) : AbGroup := AbGroup_trunc_pmap X (Y (n+2)) +definition parametrized_cohomology {X : Type*} (Y : X → spectrum) (n : ℤ) : AbGroup := +AbGroup_trunc_ppi (λx, Y x (n+2)) + definition ordinary_cohomology [reducible] (X : Type*) (G : AbGroup) (n : ℤ) : AbGroup := cohomology X (EM_spectrum G) n @@ -95,9 +31,17 @@ ordinary_cohomology X agℤ n notation `H^` n `[`:0 X:0 `, ` Y:0 `]`:0 := cohomology X Y n notation `H^` n `[`:0 X:0 `]`:0 := ordinary_cohomology_Z X n +notation `pH^` n `[`:0 binders `, ` r:(scoped Y, parametrized_cohomology Y n) `]`:0 := r -- check H^3[S¹*,EM_spectrum agℤ] -- check H^3[S¹*] +-- check pH^3[(x : S¹*), EM_spectrum agℤ] + +/- an alternate definition of cohomology -/ +definition cohomology_equiv_shomotopy_group_cotensor (X : Type*) (Y : spectrum) (n : ℤ) : + H^n[X, Y] ≃ πₛ[-n] (sp_cotensor X Y) := +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 unpointed_cohomology (X : Type) (Y : spectrum) (n : ℤ) : AbGroup := cohomology X₊ Y n diff --git a/homotopy/spectrum.hlean b/homotopy/spectrum.hlean index 9e84cfa..e10fd82 100644 --- a/homotopy/spectrum.hlean +++ b/homotopy/spectrum.hlean @@ -5,9 +5,9 @@ Authors: Michael Shulman, Floris van Doorn -/ -import homotopy.LES_of_homotopy_groups .splice homotopy.susp ..colim ..pointed +import homotopy.LES_of_homotopy_groups .splice homotopy.susp ..colim ..pointed .EM ..pointed_pi open eq nat int susp pointed pmap sigma is_equiv equiv fiber algebra trunc trunc_index pi group - seq_colim succ_str + seq_colim succ_str EM EM.ops /--------------------- Basic definitions @@ -48,6 +48,13 @@ namespace spectrum definition equiv_glue {N : succ_str} (E : gen_prespectrum N) [H : is_spectrum E] (n:N) : (E n) ≃* (Ω (E (S n))) := pequiv_of_pmap (glue E n) (is_spectrum.is_equiv_glue E n) + definition equiv_glue2 (Y : spectrum) (n : ℤ) : Ω (Ω (Y (n+2))) ≃* Y n := + begin + refine (!equiv_glue ⬝e* loop_pequiv_loop (!equiv_glue ⬝e* loop_pequiv_loop _))⁻¹ᵉ*, + refine pequiv_of_eq (ap Y _), + exact add.assoc n 1 1 + end + -- a square when we compose glue with transporting over a path in N definition glue_ptransport {N : succ_str} (X : gen_prespectrum N) {n n' : N} (p : n = n') : glue X n' ∘* ptransport X p ~* Ω→ (ptransport X (ap S p)) ∘* glue X n := @@ -224,7 +231,8 @@ namespace spectrum -- Makes sense for any indexing succ_str. Could be done for -- prespectra too, but as with truncation, why bother? - definition sp_cotensor {N : succ_str} (A : Type*) (B : gen_spectrum N) : gen_spectrum N := + + definition sp_cotensor [constructor] {N : succ_str} (A : Type*) (B : gen_spectrum N) : gen_spectrum N := spectrum.MK (λn, ppmap A (B n)) (λn, (loop_pmap_commute A (B (S n)))⁻¹ᵉ* ∘*ᵉ (pequiv_ppcompose_left (equiv_glue B n))) @@ -232,10 +240,9 @@ namespace spectrum -- Sections of parametrized spectra ---------------------------------------- - -- this definition must be changed to use dependent maps respecting the basepoint, presumably - -- definition spi {N : succ_str} (A : Type) (E : A -> gen_spectrum N) : gen_spectrum N := - -- spectrum.MK (λn, ppi (λa, E a n)) - -- (λn, (loop_ppi_commute (λa, E a (S n)))⁻¹ᵉ* ∘*ᵉ equiv_ppi_right (λa, equiv_glue (E a) n)) + definition spi [constructor] {N : succ_str} (A : Type*) (E : A -> gen_spectrum N) : gen_spectrum N := + spectrum.MK (λn, Π*a, E a n) + (λn, !ppi_loop_pequiv⁻¹ᵉ* ∘*ᵉ ppi_pequiv_right (λa, equiv_glue (E a) n)) /----------------------------------------- Fibers and long exact sequences @@ -355,17 +362,8 @@ namespace spectrum end /- Mapping spectra -/ + -- note: see also cotensor above - definition mapping_prespectrum [constructor] {N : succ_str} (X : Type*) (Y : gen_prespectrum N) : - gen_prespectrum N := - gen_prespectrum.mk (λn, ppmap X (Y n)) (λn, pfunext X (Y (S n)) ∘* ppcompose_left (glue Y n)) - - definition mapping_spectrum [constructor] {N : succ_str} (X : Type*) (Y : gen_spectrum N) : - gen_spectrum N := - gen_spectrum.mk - (mapping_prespectrum X Y) - (is_spectrum.mk (λn, to_is_equiv (pequiv_ppcompose_left (equiv_glue Y n) ⬝e - pfunext X (Y (S n))))) /- Spectrification -/ @@ -446,4 +444,10 @@ namespace spectrum /- Cofibers and stability -/ + /- The Eilenberg-MacLane spectrum -/ + + definition EM_spectrum /-[constructor]-/ (G : AbGroup) : spectrum := + spectrum.Mk (K G) (λn, (loop_EM G n)⁻¹ᵉ*) + + end spectrum diff --git a/move_to_lib.hlean b/move_to_lib.hlean index 6327aef..de9ab2b 100644 --- a/move_to_lib.hlean +++ b/move_to_lib.hlean @@ -44,6 +44,17 @@ begin exact H end +definition is_exact_trunc_functor {A B : Type} {C : Type*} {f : A → B} {g : B → C} + (H : is_exact_t f g) : @is_exact _ _ (ptrunc 0 C) (trunc_functor 0 f) (trunc_functor 0 g) := +begin + constructor, + { intro a, esimp, induction a with a, + exact ap tr (is_exact_t.im_in_ker H a) }, + { intro b p, induction b with b, note q := !tr_eq_tr_equiv p, induction q with q, + induction is_exact_t.ker_in_im H b q with a r, + exact image.mk (tr a) (ap tr r) } +end + definition is_contr_middle_of_is_exact {A B : Type} {C : Type*} {f : A → B} {g : B → C} (H : is_exact f g) [is_contr A] [is_set B] [is_contr C] : is_contr B := begin diff --git a/pointed_pi.hlean b/pointed_pi.hlean index 6dfe10b..6f01e7e 100644 --- a/pointed_pi.hlean +++ b/pointed_pi.hlean @@ -6,7 +6,7 @@ Authors: Ulrik Buchholtz import .move_to_lib -open eq pointed equiv sigma +open eq pointed equiv sigma is_equiv /- The goal of this file is to give the truncation level @@ -18,17 +18,18 @@ open eq pointed equiv sigma as a tool, because these appear in the more general statement is_trunc_ppi (the generality needed for induction). - Unfortunately, some of these names (ppi) and notations (Π*) - clash with those in types.pi in the pi namespace. -/ namespace pointed abbreviation ppi_resp_pt [unfold 3] := @ppi.resp_pt + definition ppi_const [constructor] {A : Type*} (P : A → Type*) : Π*(a : A), P a := + ppi.mk (λa, pt) idp + definition pointed_ppi [instance] [constructor] {A : Type*} (P : A → Type*) : pointed (ppi A P) := - pointed.mk (ppi.mk (λ a, pt) idp) + pointed.mk (ppi_const P) definition pppi [constructor] {A : Type*} (P : A → Type*) : Type* := pointed.mk' (ppi A P) @@ -39,13 +40,29 @@ namespace pointed (homotopy : f ~ g) (homotopy_pt : homotopy pt ⬝ ppi_resp_pt g = ppi_resp_pt f) - variables {A : Type*} {P : A → Type*} {f g : Π*(a : A), P a} + variables {A : Type*} {P Q R : A → Type*} {f g h : Π*(a : A), P a} infix ` ~~* `:50 := ppi_homotopy abbreviation ppi_to_homotopy_pt [unfold 5] := @ppi_homotopy.homotopy_pt abbreviation ppi_to_homotopy [coercion] [unfold 5] (p : f ~~* g) : Πa, f a = g a := ppi_homotopy.homotopy p + variable (f) + protected definition ppi_homotopy.refl : f ~~* f := + sorry + variable {f} + protected definition ppi_homotopy.rfl [refl] : f ~~* f := + ppi_homotopy.refl f + + protected definition ppi_homotopy.symm [symm] (p : f ~~* g) : g ~~* f := + sorry + + protected definition ppi_homotopy.trans [trans] (p : f ~~* g) (q : g ~~* h) : f ~~* h := + sorry + + infix ` ⬝*' `:75 := ppi_homotopy.trans + postfix `⁻¹*'`:(max+1) := ppi_homotopy.symm + definition ppi_equiv_pmap (A B : Type*) : (Π*(a : A), B) ≃ (A →* B) := begin fapply equiv.MK, @@ -92,14 +109,14 @@ namespace pointed definition ppi_eq_equiv : (f = g) ≃ (f ~~* g) := calc (f = g) ≃ ppi.sigma_char P f = ppi.sigma_char P g : eq_equiv_fn_eq (ppi.sigma_char P) f g - ... ≃ Σ(p : ppi.to_fun f = ppi.to_fun g), + ... ≃ Σ(p : f = g), pathover (λh, h pt = pt) (ppi_resp_pt f) p (ppi_resp_pt g) : sigma_eq_equiv _ _ - ... ≃ Σ(p : ppi.to_fun f = ppi.to_fun g), + ... ≃ Σ(p : f = g), ppi_resp_pt f = ap (λh, h pt) p ⬝ ppi_resp_pt g : sigma_equiv_sigma_right (λp, eq_pathover_equiv_Fl p (ppi_resp_pt f) (ppi_resp_pt g)) - ... ≃ Σ(p : ppi.to_fun f = ppi.to_fun g), + ... ≃ Σ(p : f = g), ppi_resp_pt f = apd10 p pt ⬝ ppi_resp_pt g : sigma_equiv_sigma_right (λp, equiv_eq_closed_right _ (whisker_right _ (ap_eq_apd10 p _))) @@ -130,6 +147,57 @@ namespace pointed ... ≃ Π*(a : A), Ω (pType.mk (P a) (f a)) : erfl + variables {f g} + definition eq_of_ppi_homotopy (h : f ~~* g) : f = g := + (ppi_eq_equiv f g)⁻¹ᵉ h + + definition ppi_loop_pequiv : Ω (Π*(a : A), P a) ≃* Π*(a : A), Ω (P a) := + pequiv_of_equiv (ppi_loop_equiv pt) idp + + definition pmap_compose_ppi [constructor] (g : Π(a : A), ppmap (P a) (Q a)) + (f : Π*(a : A), P a) : Π*(a : A), Q a := + proof ppi.mk (λa, g a (f a)) (ap (g pt) (ppi.resp_pt f) ⬝ respect_pt (g pt)) qed + + definition pmap_compose_ppi_const_right (g : Π(a : A), ppmap (P a) (Q a)) : + pmap_compose_ppi g (ppi_const P) ~~* ppi_const Q := + proof ppi_homotopy.mk (λa, respect_pt (g a)) !idp_con⁻¹ qed + + 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 + + definition ppi_compose_left [constructor] (g : Π(a : A), ppmap (P a) (Q a)) : + (Π*(a : A), P a) →* Π*(a : A), Q a := + pmap.mk (pmap_compose_ppi g) (eq_of_ppi_homotopy (pmap_compose_ppi_const_right g)) + + 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 + + definition pmap_compose_ppi_pid_left [constructor] + (f : Π*(a : A), P a) : pmap_compose_ppi (λa, pid (P a)) f ~~* f := + sorry + + definition pmap_compose_pmap_compose_ppi [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 + + definition ppi_pequiv_right [constructor] (g : Π(a : A), P a ≃* Q a) : + (Π*(a : A), P a) ≃* Π*(a : A), Q a := + begin + apply pequiv_of_pmap (ppi_compose_left g), + apply adjointify _ (ppi_compose_left (λa, (g a)⁻¹ᵉ*)), + { intro f, apply eq_of_ppi_homotopy, + refine !pmap_compose_pmap_compose_ppi ⬝*' _, + refine pmap_compose_ppi_phomotopy_left _ (λa, !pright_inv) ⬝*' _, + apply pmap_compose_ppi_pid_left }, + { intro f, apply eq_of_ppi_homotopy, + refine !pmap_compose_pmap_compose_ppi ⬝*' _, + refine pmap_compose_ppi_phomotopy_left _ (λa, !pleft_inv) ⬝*' _, + apply pmap_compose_ppi_pid_left } + end + end pointed open pointed open is_trunc is_conn