From 90f4acb3f6f07aad5c76d88c2cce3355169a4bad Mon Sep 17 00:00:00 2001 From: Floris van Doorn Date: Fri, 7 Jul 2017 22:32:57 +0100 Subject: [PATCH] fix definition of atiyah-hirzebruch spectral sequence, define serre spectral sequence The construction of the Serre spectral sequence is done up to 11 sorry's, all which are marked with 'TODO FOR SSS'. 8 of them are equivalences related to cohomology (6 of which are corollaries of the other 2), 2 of them are calculations on int, and the last is in the definition of a spectrum map. --- archive/smash_assoc.hlean | 1 + homotopy/cohomology.hlean | 34 +++++++--- homotopy/serre.hlean | 132 ++++++++++++++++-------------------- homotopy/spectrum.hlean | 48 +++++++++++-- homotopy/strunc.hlean | 12 +++- move_to_lib.hlean | 10 +++ pointed.hlean | 8 +++ pointed_pi.hlean | 137 +++++++++++++++++++++++++++++++++++--- 8 files changed, 284 insertions(+), 98 deletions(-) diff --git a/archive/smash_assoc.hlean b/archive/smash_assoc.hlean index 772bd3d..1741bf9 100644 --- a/archive/smash_assoc.hlean +++ b/archive/smash_assoc.hlean @@ -6,6 +6,7 @@ import ..homotopy.smash open bool pointed eq equiv is_equiv sum bool prod unit circle cofiber prod.ops wedge is_trunc function red_susp unit sigma +exit namespace smash variables {A B C : Type*} diff --git a/homotopy/cohomology.hlean b/homotopy/cohomology.hlean index efd2a32..9949e34 100644 --- a/homotopy/cohomology.hlean +++ b/homotopy/cohomology.hlean @@ -43,7 +43,7 @@ definition ordinary_parametrized_cohomology [reducible] {X : Type*} (G : X → A parametrized_cohomology (λx, EM_spectrum (G x)) n definition unreduced_parametrized_cohomology {X : Type} (Y : X → spectrum) (n : ℤ) : AbGroup := -@parametrized_cohomology X₊ (add_point_spectrum Y) n +parametrized_cohomology (add_point_spectrum Y) n definition unreduced_ordinary_parametrized_cohomology [reducible] {X : Type} (G : X → AbGroup) (n : ℤ) : AbGroup := @@ -72,11 +72,19 @@ trunc_equiv_trunc 0 (!pfunext ⬝e loop_pequiv_loop !pfunext ⬝e loopn_pequiv_l 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 +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) := -sorry +sorry /- TODO FOR SSS -/ + +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) := +sorry /- TODO FOR SSS -/ /- functoriality -/ @@ -113,14 +121,22 @@ definition cohomology_isomorphism_refl (X : Type*) (Y : spectrum) (n : ℤ) (x : cohomology_isomorphism (pequiv.refl X) Y n x = x := !Group_trunc_pmap_isomorphism_refl -definition cohomology_isomorphism_right (X : Type*) {Y Y' : spectrum} (e : Πn, Y n ≃* Y' n) (n : ℤ) - : H^n[X, Y] ≃g H^n[X, Y'] := -sorry +definition cohomology_isomorphism_right (X : Type*) {Y Y' : spectrum} (e : Πn, Y n ≃* Y' n) + (n : ℤ) : H^n[X, Y] ≃g H^n[X, Y'] := +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 + (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 -/ + +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] := +sorry /- TODO FOR SSS -/ + +definition unreduced_ordinary_parametrized_cohomology_isomorphism_right {X : Type} + {G G' : X → AbGroup} (e : Πx, G x ≃g G' x) (n : ℤ) : + uopH^n[(x : X), G x] ≃g uopH^n[(x : X), G' x] := +sorry /- TODO FOR SSS -/ definition ordinary_cohomology_isomorphism_right (X : Type*) {G G' : AbGroup} (e : G ≃g G') (n : ℤ) : oH^n[X, G] ≃g oH^n[X, G'] := diff --git a/homotopy/serre.hlean b/homotopy/serre.hlean index cef85d5..dfef176 100644 --- a/homotopy/serre.hlean +++ b/homotopy/serre.hlean @@ -151,79 +151,73 @@ begin { apply phomotopy_of_is_contr_cod, apply is_trunc_trunc } end -definition pfiber_postnikov_smap (A : spectrum) (n : ℤ) (k : ℤ) : - sfiber (postnikov_smap A n) k ≃* EM_spectrum (πₛ[n] A) (n + k) := +definition sfiber_postnikov_smap_pequiv (A : spectrum) (n : ℤ) (k : ℤ) : + sfiber (postnikov_smap A n) k ≃* ssuspn n (EM_spectrum (πₛ[n] A)) k := proof pfiber_pequiv_of_square _ _ (postnikov_smap_postnikov_map A n k (n + k) idp) ⬝e* -pfiber_postnikov_map_pred' A n k _ idp +pfiber_postnikov_map_pred' A n k _ idp ⬝e* +pequiv_ap (EM_spectrum (πₛ[n] A)) (add.comm n k) qed section atiyah_hirzebruch parameters {X : Type*} (Y : X → spectrum) (s₀ : ℤ) (H : Πx, is_strunc s₀ (Y x)) definition atiyah_hirzebruch_exact_couple : exact_couple rℤ Z2 := - @exact_couple_sequence (λs, strunc s (spi X Y)) (postnikov_smap (spi X Y)) - - definition atiyah_hirzebruch_ub ⦃s n : ℤ⦄ (Hs : s ≤ n - 1) : - is_contr (πₛ[n] (strunc s (spi X Y))) := - begin - apply trivial_shomotopy_group_of_is_strunc, - apply is_strunc_strunc, - exact lt_of_le_sub_one Hs - end + @exact_couple_sequence (λs, spi X (λx, strunc s (Y x))) + (λs, spi_compose_left (λx, postnikov_smap (Y x) s)) include H - definition atiyah_hirzebruch_lb ⦃s n : ℤ⦄ (Hs : s ≥ s₀ + 1) : - is_equiv (postnikov_smap (spi X Y) s n) := + definition atiyah_hirzebruch_ub ⦃s n : ℤ⦄ (Hs : s ≤ n - 1) : + is_contr (πₛ[n] (spi X (λx, strunc s (Y x)))) := + begin + refine trivial_shomotopy_group_of_is_strunc _ _ (lt_of_le_sub_one Hs), + apply is_strunc_spi, intro x, exact is_strunc_strunc _ _ + end + + definition atiyah_hirzebruch_lb ⦃s n : ℤ⦄ (Hs : s ≥ s₀ + 1) : + is_equiv (spi_compose_left (λx, postnikov_smap (Y x) s) n) := begin - have H2 : is_strunc s₀ (spi X Y), from is_strunc_spi _ _ H, refine is_equiv_of_equiv_of_homotopy - (ptrunc_pequiv_ptrunc_of_is_trunc _ _ (H2 n)) _, - { apply maxm2_monotone, apply add_le_add_right, exact le.trans !le_add_one Hs }, - { apply maxm2_monotone, apply add_le_add_right, exact le_sub_one_of_lt Hs }, - refine @trunc.rec _ _ _ _ _, - { intro x, apply is_trunc_eq, - assert H3 : maxm2 (s - 1 + n) ≤ (maxm2 (s + n)).+1, - { refine trunc_index.le_succ (maxm2_monotone (le.trans (le_of_eq !add.right_comm) - !sub_one_le)) }, - exact @is_trunc_of_le _ _ _ H3 !is_trunc_trunc }, - intro a, reflexivity + (ppi_pequiv_right (λx, ptrunc_pequiv_ptrunc_of_is_trunc _ _ (H x n))) _, + { intro x, apply maxm2_monotone, apply add_le_add_right, exact le.trans !le_add_one Hs }, + { intro x, apply maxm2_monotone, apply add_le_add_right, exact le_sub_one_of_lt Hs }, + intro f, apply eq_of_ppi_homotopy, + apply pmap_compose_ppi_phomotopy_left, intro x, + fapply phomotopy.mk, + { refine @trunc.rec _ _ _ _ _, + { intro x, apply is_trunc_eq, + assert H3 : maxm2 (s - 1 + n) ≤ (maxm2 (s + n)).+1, + { refine trunc_index.le_succ (maxm2_monotone (le.trans (le_of_eq !add.right_comm) + !sub_one_le)) }, + exact @is_trunc_of_le _ _ _ H3 !is_trunc_trunc }, + intro a, reflexivity }, + reflexivity end definition is_bounded_atiyah_hirzebruch : is_bounded atiyah_hirzebruch_exact_couple := is_bounded_sequence _ s₀ (λn, n - 1) atiyah_hirzebruch_lb atiyah_hirzebruch_ub definition atiyah_hirzebruch_convergence' : - (λn s, πₛ[n] (sfiber (postnikov_smap (spi X Y) s))) ⟹ᵍ (λn, πₛ[n] (strunc s₀ (spi X Y))) := + (λn s, πₛ[n] (sfiber (spi_compose_left (λx, postnikov_smap (Y x) s)))) ⟹ᵍ + (λn, πₛ[n] (spi X (λx, strunc s₀ (Y x)))) := converges_to_sequence _ s₀ (λn, n - 1) atiyah_hirzebruch_lb atiyah_hirzebruch_ub - lemma spi_EM_spectrum (n : ℤ) : Π(k : ℤ), - EM_spectrum (πₛ[n] (spi X Y)) (n + k) ≃* spi X (λx, EM_spectrum (πₛ[n] (Y x))) k := - begin - exact sorry - -- apply spectrum_pequiv_of_nat_add 2, intro k, - -- fapply EMadd1_pequiv (k+1), - -- { exact sorry }, - -- { exact sorry }, - -- { apply is_trunc_ppi, rotate 1, intro x, }, - end - -set_option formatter.hide_full_terms false definition atiyah_hirzebruch_convergence : - (λn s, opH^-n[(x : X), πₛ[s] (Y x)]) ⟹ᵍ (λn, pH^-n[(x : X), Y x]) := + (λn s, opH^-(n-s)[(x : X), πₛ[s] (Y x)]) ⟹ᵍ (λn, pH^-n[(x : X), Y x]) := converges_to_g_isomorphism atiyah_hirzebruch_convergence' begin intro n s, refine _ ⬝g (parametrized_cohomology_isomorphism_shomotopy_group_spi _ idp)⁻¹ᵍ, - apply shomotopy_group_isomorphism_of_pequiv, intro k, - refine pfiber_postnikov_smap (spi X Y) s k ⬝e* _, - apply spi_EM_spectrum + refine _ ⬝g !shomotopy_group_ssuspn, + apply shomotopy_group_isomorphism_of_pequiv n, intro k, + refine !pfiber_ppi_compose_left ⬝e* _, + exact ppi_pequiv_right (λx, sfiber_postnikov_smap_pequiv (Y x) s k) end begin intro n, refine _ ⬝g (parametrized_cohomology_isomorphism_shomotopy_group_spi _ idp)⁻¹ᵍ, apply shomotopy_group_isomorphism_of_pequiv, intro k, - apply ptrunc_pequiv, exact is_strunc_spi s₀ Y H k, + exact ppi_pequiv_right (λx, ptrunc_pequiv (maxm2 (s₀ + k)) (Y x k)), end end atiyah_hirzebruch @@ -232,7 +226,7 @@ section unreduced_atiyah_hirzebruch definition unreduced_atiyah_hirzebruch_convergence {X : Type} (Y : X → spectrum) (s₀ : ℤ) (H : Πx, is_strunc s₀ (Y x)) : - (λn s, uopH^-n[(x : X), πₛ[s] (Y x)]) ⟹ᵍ (λn, upH^-n[(x : X), Y x]) := + (λn s, uopH^-(n-s)[(x : X), πₛ[s] (Y x)]) ⟹ᵍ (λn, upH^-n[(x : X), Y x]) := converges_to_g_isomorphism (@atiyah_hirzebruch_convergence X₊ (add_point_spectrum Y) s₀ (is_strunc_add_point_spectrum H)) begin @@ -249,36 +243,28 @@ end unreduced_atiyah_hirzebruch section serre variables {X : Type} (F : X → Type) (Y : spectrum) (s₀ : ℤ) (H : is_strunc s₀ Y) - open option - definition add_point_over {X : Type} (F : X → Type) (x : option X) : Type* := - (option.cases_on x (lift empty) F)₊ - - postfix `₊ₒ`:(max+1) := add_point_over - include H - -- definition serre_convergence : - -- (λn s, uopH^-n[(x : X), uH^-s[F x, Y]]) ⟹ᵍ (λn, uH^-n[Σ(x : X), F x, Y]) := - -- proof - -- converges_to_g_isomorphism - -- (unreduced_atiyah_hirzebruch_convergence - -- (λx, sp_cotensor (F x) Y) s₀ - -- (λx, is_strunc_sp_cotensor s₀ (F x) H)) - -- begin - -- exact sorry - -- -- intro n s, - -- -- apply ordinary_parametrized_cohomology_isomorphism_right, - -- -- intro x, - -- -- exact (cohomology_isomorphism_shomotopy_group_sp_cotensor _ _ idp)⁻¹ᵍ, - -- end - -- begin - -- intro n, exact sorry - -- -- refine parametrized_cohomology_isomorphism_shomotopy_group_spi _ idp ⬝g _, - -- -- refine _ ⬝g (cohomology_isomorphism_shomotopy_group_sp_cotensor _ _ idp)⁻¹ᵍ, - -- -- apply shomotopy_group_isomorphism_of_pequiv, intro k, - -- end - -- qed + definition serre_convergence : + (λn s, uopH^-(n-s)[(x : X), uH^-s[F x, Y]]) ⟹ᵍ (λn, uH^-n[Σ(x : X), F x, Y]) := + proof + converges_to_g_isomorphism + (unreduced_atiyah_hirzebruch_convergence + (λx, sp_ucotensor (F x) Y) s₀ + (λx, is_strunc_sp_ucotensor s₀ (F x) H)) + begin + intro n s, + refine unreduced_ordinary_parametrized_cohomology_isomorphism_right _ (-(n-s)), + intro x, + exact (unreduced_cohomology_isomorphism_shomotopy_group_sp_ucotensor _ _ idp)⁻¹ᵍ + end + begin + intro n, + refine unreduced_parametrized_cohomology_isomorphism_shomotopy_group_supi _ idp ⬝g _, + refine _ ⬝g (unreduced_cohomology_isomorphism_shomotopy_group_sp_ucotensor _ _ idp)⁻¹ᵍ, + apply shomotopy_group_isomorphism_of_pequiv, intro k, + exact (sigma_pumap F (Y k))⁻¹ᵉ* + end + qed end serre -/- TODO: πₛ[n] (strunc 0 (spi X Y)) ≃g H^n[X, λx, Y x] -/ - end spectrum diff --git a/homotopy/spectrum.hlean b/homotopy/spectrum.hlean index 24446cd..c2ab845 100644 --- a/homotopy/spectrum.hlean +++ b/homotopy/spectrum.hlean @@ -639,17 +639,35 @@ set_option pp.coercions true -- Makes sense for any indexing succ_str. Could be done for -- prespectra too, but as with truncation, why bother? - definition sp_cotensor [constructor] {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_ppmap_commute A (B (S n)))⁻¹ᵉ* ∘*ᵉ (pequiv_ppcompose_left (equiv_glue B n))) + /- unpointed cotensor -/ + definition sp_ucotensor [constructor] {N : succ_str} (A : Type) (B : gen_spectrum N) : + gen_spectrum N := + spectrum.MK (λn, A →ᵘ* B n) + (λn, pumap_pequiv_right A (equiv_glue B n) ⬝e* (loop_pumap A (B (S n)))⁻¹ᵉ*) + ---------------------------------------- -- Sections of parametrized spectra ---------------------------------------- - 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)) + 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)) + + definition spi_compose_left [constructor] {N : succ_str} {A : Type*} {E F : A -> gen_spectrum N} + (f : Πa, E a →ₛ F a) : spi A E →ₛ spi A F := + smap.mk (λn, ppi_compose_left (λa, f a n)) sorry /- TODO FOR SSS -/ + + -- unpointed spi + definition supi [constructor] {N : succ_str} (A : Type) (E : A → gen_spectrum N) : + gen_spectrum N := + spectrum.MK (λn, Πᵘ*a, E a n) + (λn, pupi_pequiv_right (λa, equiv_glue (E a) n) ⬝e* (loop_pupi (λa, E a (S n)))⁻¹ᵉ*) /----------------------------------------- Fibers and long exact sequences @@ -1064,6 +1082,28 @@ set_option pp.coercions true definition spectrify_fun {N : succ_str} {X Y : gen_prespectrum N} (f : X →ₛ Y) : spectrify X →ₛ spectrify Y := spectrify.elim ((@spectrify_map _ Y) ∘ₛ f) + /- + suspension of a spectrum + + this is just a shift. A shift in the other direction is loopn, + but we might not want to define that yet. + -/ + + definition ssusp [constructor] {N : succ_str} (X : gen_spectrum N) : gen_spectrum N := + spectrum.MK (λn, X (S n)) (λn, equiv_glue X (S n)) + + definition ssuspn [constructor] (k : ℤ) (X : spectrum) : spectrum := + spectrum.MK (λn, X (n + k)) + (λn, equiv_glue X (n + k) ⬝e* loop_pequiv_loop (pequiv_ap X !add.right_comm)) + + definition shomotopy_group_ssuspn (k : ℤ) (X : spectrum) (n : ℤ) : + πₛ[k] (ssuspn n X) ≃g πₛ[k - n] X := + have k - n + (2 - k + n) = 2, from + !add.comm ⬝ + ap (λx, x + (k - n)) (!add.assoc ⬝ ap (λx, 2 + x) (ap (λx, -k + x) !neg_neg⁻¹ ⬝ !neg_add⁻¹)) ⬝ + sub_add_cancel 2 (k - n), + (shomotopy_group_isomorphism_homotopy_group X this)⁻¹ᵍ + /- Tensor by spaces -/ /- Smash product of spectra -/ diff --git a/homotopy/strunc.hlean b/homotopy/strunc.hlean index 264dfc7..8355a43 100644 --- a/homotopy/strunc.hlean +++ b/homotopy/strunc.hlean @@ -8,12 +8,12 @@ namespace int private definition maxm2_le.lemma₁ {n k : ℕ} : n+(1:int) + -[1+ k] ≤ n := le.intro ( calc n + 1 + -[1+ k] + k = n + 1 - (k + 1) + k : by reflexivity - ... = n : sorry) + ... = n : sorry) /- TODO FOR SSS -/ private definition maxm2_le.lemma₂ {n : ℕ} {k : ℤ} : -[1+ n] + 1 + k ≤ k := le.intro ( calc -[1+ n] + 1 + k + n = - (n + 1) + 1 + k + n : by reflexivity - ... = k : sorry) + ... = k : sorry) /- TODO FOR SSS -/ definition maxm2_le (n k : ℤ) : maxm2 (n+1+k) ≤ (maxm1m1 n).+1+2+(maxm1m1 k) := begin @@ -142,6 +142,10 @@ definition is_strunc_strunc (k : ℤ) (E : spectrum) : is_strunc k (strunc k E) := λ n, is_trunc_trunc (maxm2 (k + n)) (E n) +definition is_strunc_strunc_of_is_strunc (k : ℤ) {l : ℤ} {E : spectrum} (H : is_strunc l E) + : is_strunc l (strunc k E) := +λ n, !is_trunc_trunc_of_is_trunc + definition str [constructor] (k : ℤ) (E : spectrum) : E →ₛ strunc k E := smap.mk (λ n, ptr (maxm2 (k + n)) (E n)) abstract begin @@ -283,4 +287,8 @@ definition is_strunc_sp_cotensor (n : ℤ) (A : Type*) {Y : spectrum} (H : is_st : is_strunc n (sp_cotensor A Y) := is_strunc_pequiv_closed (λn, !pppi_pequiv_ppmap) (is_strunc_spi n (λa, Y) (λa, H)) +definition is_strunc_sp_ucotensor (n : ℤ) (A : Type) {Y : spectrum} (H : is_strunc n Y) + : is_strunc n (sp_ucotensor A Y) := +λk, !pi.is_trunc_arrow + end spectrum diff --git a/move_to_lib.hlean b/move_to_lib.hlean index 3189251..05aa604 100644 --- a/move_to_lib.hlean +++ b/move_to_lib.hlean @@ -7,6 +7,16 @@ open eq nat int susp pointed pmap sigma is_equiv equiv fiber algebra trunc pi gr namespace eq + definition apd10_prepostcompose_nondep {A B C D : Type} (h : C → D) {g g' : B → C} (p : g = g') + (f : A → B) (a : A) : apd10 (ap (λg a, h (g (f a))) p) a = ap h (apd10 p (f a)) := + begin induction p, reflexivity end + + definition apd10_prepostcompose {A B : Type} {C : B → Type} {D : A → Type} + (f : A → B) (h : Πa, C (f a) → D a) {g g' : Πb, C b} + (p : g = g') (a : A) : + apd10 (ap (λg a, h a (g (f a))) p) a = ap (h a) (apd10 p (f a)) := + begin induction p, reflexivity end + definition eq.rec_to {A : Type} {a₀ : A} {P : Π⦃a₁⦄, a₀ = a₁ → Type} {a₁ : A} (p₀ : a₀ = a₁) (H : P p₀) ⦃a₂ : A⦄ (p : a₀ = a₂) : P p := begin diff --git a/pointed.hlean b/pointed.hlean index cb6bbac..fe5b507 100644 --- a/pointed.hlean +++ b/pointed.hlean @@ -157,6 +157,14 @@ namespace pointed h a' ∘* ptransport X (ap f p) ~* ptransport Y (ap g p) ∘* h a := by induction p; exact !pcompose_pid ⬝* !pid_pcompose⁻¹* + definition ptransport_ap {A B : Type} (X : B → Type*) (f : A → B) {a a' : A} (p : a = a') : + ptransport X (ap f p) ~* ptransport (X ∘ f) p := + by induction p; reflexivity + + definition ptransport_constant (A : Type) (B : Type*) {a a' : A} (p : a = a') : + ptransport (λ(a : A), B) p ~* pid B := + by induction p; reflexivity + definition ptransport_natural {A : Type} (X : A → Type*) (Y : A → Type*) (h : Πa, X a →* Y a) {a a' : A} (p : a = a') : h a' ∘* ptransport X p ~* ptransport Y p ∘* h a := diff --git a/pointed_pi.hlean b/pointed_pi.hlean index 6a35cea..233accc 100644 --- a/pointed_pi.hlean +++ b/pointed_pi.hlean @@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Ulrik Buchholtz, Floris van Doorn -/ -import homotopy.connectedness types.pointed2 .move_to_lib +import homotopy.connectedness types.pointed2 .move_to_lib .pointed open eq pointed equiv sigma is_equiv trunc @@ -173,7 +173,7 @@ namespace pointed definition eq_ppi_homotopy_refl_ppi_homotopy_of_eq_refl : ppi_homotopy.refl k = ppi_homotopy_of_eq (refl k) := begin induction k with k p, - induction p, reflexivity + induction p, reflexivity end variable {k} @@ -281,15 +281,15 @@ namespace pointed pequiv_of_equiv (fiber.sigma_char f pt) idp /- the pointed type of unpointed (nondependent) maps -/ - definition upmap [constructor] (A : Type) (B : Type*) : Type* := + definition pumap [constructor] (A : Type) (B : Type*) : Type* := pointed.MK (A → B) (const A pt) /- the pointed type of unpointed dependent maps -/ - definition uppi [constructor] {A : Type} (B : A → Type*) : Type* := + definition pupi [constructor] {A : Type} (B : A → Type*) : Type* := pointed.MK (Πa, B a) (λa, pt) - notation `Πᵘ*` binders `, ` r:(scoped P, uppi P) := r - infix ` →ᵘ* `:30 := upmap + notation `Πᵘ*` binders `, ` r:(scoped P, pupi P) := r + infix ` →ᵘ* `:30 := pumap definition ppmap.sigma_char [constructor] (A B : Type*) : ppmap A B ≃* @psigma_gen (A →ᵘ* B) (λf, f pt = pt) idp := @@ -377,12 +377,12 @@ namespace pointed open sigma.ops - definition psigma_gen_pi_pequiv_uppi_psigma_gen [constructor] {A : Type*} {B : A → Type*} + definition psigma_gen_pi_pequiv_pupi_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*} + definition pupi_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 @@ -408,7 +408,7 @@ namespace pointed ≃* @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) + by exact psigma_gen_pequiv_psigma_gen (pupi_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⟩ : @@ -456,7 +456,7 @@ namespace pointed ... ≃* ppmap A (pfiber f) : by exact pequiv_ppcompose_left !pfiber.sigma_char'⁻¹ᵉ* - definition pfiber_ppcompose_left_dep {B C : A → Type*} (f : Πa, B a →* C a) : + definition pfiber_ppi_compose_left {B C : A → Type*} (f : Πa, B a →* C a) : pfiber (ppi_compose_left f) ≃* Π*(a : A), pfiber (f a) := calc pfiber (ppi_compose_left f) ≃* @@ -485,6 +485,123 @@ namespace pointed -- definition pppi_ppmap {A C : Type*} {B : A → Type*} : -- ppmap (/- dependent smash of B -/) C ≃* Π*(a : A), ppmap (B a) C := + -- TODO: homotopy_of_eq and apd10 should be the same + -- TODO: there is also apd10_eq_of_homotopy in both pi and eq(?) + + /- stuff about the pointed type of unpointed maps (dependent and non-dependent) -/ + definition sigma_pumap {A : Type} (B : A → Type) (C : Type*) : + ((Σa, B a) →ᵘ* C) ≃* Πᵘ*a, B a →ᵘ* C := + pequiv_of_equiv (equiv_sigma_rec _)⁻¹ᵉ idp + + definition loop_pupi [constructor] {A : Type} (B : A → Type*) : Ω (Πᵘ*a, B a) ≃* Πᵘ*a, Ω (B a) := + pequiv_of_equiv eq_equiv_homotopy idp + + definition phomotopy_mk_pupi [constructor] {A : Type*} {B : Type} {C : B → Type*} + {f g : A →* (Πᵘ*b, C b)} (p : f ~2 g) + (q : p pt ⬝hty apd10 (respect_pt g) ~ apd10 (respect_pt f)) : f ~* g := + begin + apply phomotopy.mk (λa, eq_of_homotopy (p a)), + apply eq_of_fn_eq_fn eq_equiv_homotopy, + apply eq_of_homotopy, intro b, + refine !apd10_con ⬝ _, + refine whisker_right _ !pi.apd10_eq_of_homotopy ⬝ q b + end + + definition pupi_functor [constructor] {A A' : Type} {B : A → Type*} {B' : A' → Type*} + (f : A' → A) (g : Πa, B (f a) →* B' a) : (Πᵘ*a, B a) →* (Πᵘ*a', B' a') := + pmap.mk (λh a, g a (h (f a))) (eq_of_homotopy (λa, respect_pt (g a))) + + definition pupi_functor_compose {A A' A'' : Type} + {B : A → Type*} {B' : A' → Type*} {B'' : A'' → Type*} (f : A'' → A') (f' : A' → A) + (g' : Πa, B' (f a) →* B'' a) (g : Πa, B (f' a) →* B' a) : + pupi_functor (f' ∘ f) (λa, g' a ∘* g (f a)) ~* pupi_functor f g' ∘* pupi_functor f' g := + begin + fapply phomotopy_mk_pupi, + { intro h a, reflexivity }, + { intro a, refine !idp_con ⬝ _, refine !apd10_con ⬝ _ ⬝ !pi.apd10_eq_of_homotopy⁻¹, esimp, + refine (!apd10_prepostcompose ⬝ ap02 (g' a) !pi.apd10_eq_of_homotopy) ◾ + !pi.apd10_eq_of_homotopy } + end + + definition pupi_functor_pid (A : Type) (B : A → Type*) : + pupi_functor id (λa, pid (B a)) ~* pid (Πᵘ*a, B a) := + begin + fapply phomotopy_mk_pupi, + { intro h a, reflexivity }, + { intro a, refine !idp_con ⬝ !pi.apd10_eq_of_homotopy⁻¹ } + end + + definition pupi_functor_phomotopy {A A' : Type} {B : A → Type*} {B' : A' → Type*} + {f f' : A' → A} {g : Πa, B (f a) →* B' a} {g' : Πa, B (f' a) →* B' a} + (p : f ~ f') (q : Πa, g a ~* g' a ∘* ptransport B (p a)) : + pupi_functor f g ~* pupi_functor f' g' := + begin + fapply phomotopy_mk_pupi, + { intro h a, exact q a (h (f a)) ⬝ ap (g' a) (apdt h (p a)) }, + { intro a, esimp, + exact whisker_left _ !pi.apd10_eq_of_homotopy ⬝ !con.assoc ⬝ + to_homotopy_pt (q a) ⬝ !pi.apd10_eq_of_homotopy⁻¹ } + end + + definition pupi_pequiv [constructor] {A A' : Type} {B : A → Type*} {B' : A' → Type*} + (e : A' ≃ A) (f : Πa, B (e a) ≃* B' a) : + (Πᵘ*a, B a) ≃* (Πᵘ*a', B' a') := + pequiv.MK (pupi_functor e f) + (pupi_functor e⁻¹ᵉ (λa, ptransport B (right_inv e a) ∘* (f (e⁻¹ᵉ a))⁻¹ᵉ*)) + abstract begin + refine !pupi_functor_compose⁻¹* ⬝* pupi_functor_phomotopy (to_right_inv e) _ ⬝* + !pupi_functor_pid, + intro a, exact !pinv_pcompose_cancel_right ⬝* !pid_pcompose⁻¹* + end end + abstract begin + refine !pupi_functor_compose⁻¹* ⬝* pupi_functor_phomotopy (to_left_inv e) _ ⬝* + !pupi_functor_pid, + intro a, refine !passoc⁻¹* ⬝* pinv_right_phomotopy_of_phomotopy _ ⬝* !pid_pcompose⁻¹*, + refine pwhisker_left _ _ ⬝* !ptransport_natural, + exact ptransport_change_eq _ (adj e a) ⬝* ptransport_ap B e (to_left_inv e a) + end end + + definition pupi_pequiv_right [constructor] {A : Type} {B B' : A → Type*} (f : Πa, B a ≃* B' a) : + (Πᵘ*a, B a) ≃* (Πᵘ*a, B' a) := + pupi_pequiv erfl f + + definition loop_pumap [constructor] (A : Type) (B : Type*) : Ω (A →ᵘ* B) ≃* A →ᵘ* Ω B := + loop_pupi (λa, B) + + definition phomotopy_mk_pumap [constructor] {A C : Type*} {B : Type} {f g : A →* (B →ᵘ* C)} + (p : f ~2 g) (q : p pt ⬝hty apd10 (respect_pt g) ~ apd10 (respect_pt f)) + : f ~* g := + phomotopy_mk_pupi p q + + definition pumap_functor [constructor] {A A' : Type} {B B' : Type*} (f : A' → A) (g : B →* B') : + (A →ᵘ* B) →* (A' →ᵘ* B') := + pupi_functor f (λa, g) + + definition pumap_functor_compose {A A' A'' : Type} {B B' B'' : Type*} + (f : A'' → A') (f' : A' → A) (g' : B' →* B'') (g : B →* B') : + pumap_functor (f' ∘ f) (g' ∘* g) ~* pumap_functor f g' ∘* pumap_functor f' g := + pupi_functor_compose f f' (λa, g') (λa, g) + + definition pumap_functor_pid (A : Type) (B : Type*) : + pumap_functor id (pid B) ~* pid (A →ᵘ* B) := + pupi_functor_pid A (λa, B) + + definition pumap_functor_phomotopy {A A' : Type} {B B' : Type*} {f f' : A' → A} {g g' : B →* B'} + (p : f ~ f') (q : g ~* g') : pumap_functor f g ~* pumap_functor f' g' := + pupi_functor_phomotopy p (λa, q ⬝* !pcompose_pid⁻¹* ⬝* pwhisker_left _ !ptransport_constant⁻¹*) + + definition pumap_pequiv [constructor] {A A' : Type} {B B' : Type*} (e : A ≃ A') (f : B ≃* B') : + (A →ᵘ* B) ≃* (A' →ᵘ* B') := + pupi_pequiv e⁻¹ᵉ (λa, f) + + definition pumap_pequiv_right [constructor] (A : Type) {B B' : Type*} (f : B ≃* B') : + (A →ᵘ* B) ≃* (A →ᵘ* B') := + pumap_pequiv erfl f + + definition pumap_pequiv_left [constructor] {A A' : Type} (B : Type*) (f : A ≃ A') : + (A →ᵘ* B) ≃* (A' →ᵘ* B) := + pumap_pequiv f pequiv.rfl + end pointed open pointed open is_trunc is_conn