From 63ec1b8d37a41d9c95c0eff53b98dd470723506b Mon Sep 17 00:00:00 2001 From: Floris van Doorn Date: Sun, 2 Jul 2017 01:14:18 +0100 Subject: [PATCH] progress on atiyah-hirzebruch and serre spectral sequences Note: the Serre spectral sequence only works for unreduced cohomology, so we need some results for that For reduced homology we might get a similar result if we replace the sigma in the RHS by a dependent version of the smash product --- homotopy/EM.hlean | 7 +++ homotopy/cohomology.hlean | 71 ++++++++++++++++++++++--- homotopy/serre.hlean | 109 ++++++++++++++++++++++++++++++++++---- homotopy/spectrum.hlean | 36 ++++++++++++- homotopy/strunc.hlean | 14 ++++- move_to_lib.hlean | 14 +++++ pointed.hlean | 3 ++ pointed_pi.hlean | 7 ++- 8 files changed, 237 insertions(+), 24 deletions(-) diff --git a/homotopy/EM.hlean b/homotopy/EM.hlean index aa95281..03eb5c3 100644 --- a/homotopy/EM.hlean +++ b/homotopy/EM.hlean @@ -570,4 +570,11 @@ namespace EM abstract (EMadd1_functor_gcompose φ φ⁻¹ᵍ n)⁻¹* ⬝* EMadd1_functor_phomotopy proof right_inv φ qed n ⬝* EMadd1_functor_gid H n end + definition EM_pequiv_EM (n : ℕ) {G H : AbGroup} (φ : G ≃g H) : K G n ≃* K H n := + begin + cases n with n, + { exact pequiv_of_isomorphism φ }, + { exact EMadd1_pequiv_EMadd1 n φ } + end + end EM diff --git a/homotopy/cohomology.hlean b/homotopy/cohomology.hlean index 8c25b70..e1d9fdc 100644 --- a/homotopy/cohomology.hlean +++ b/homotopy/cohomology.hlean @@ -20,31 +20,64 @@ namespace cohomology 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 definition ordinary_cohomology_Z [reducible] (X : Type*) (n : ℤ) : AbGroup := 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 +definition unreduced_cohomology (X : Type) (Y : spectrum) (n : ℤ) : AbGroup := +cohomology X₊ Y n + +definition unreduced_ordinary_cohomology [reducible] (X : Type) (G : AbGroup) (n : ℤ) : AbGroup := +unreduced_cohomology X (EM_spectrum G) n + +definition unreduced_ordinary_cohomology_Z [reducible] (X : Type) (n : ℤ) : AbGroup := +unreduced_ordinary_cohomology X agℤ n + +definition parametrized_cohomology {X : Type*} (Y : X → spectrum) (n : ℤ) : AbGroup := +AbGroup_trunc_ppi (λx, Y x (n+2)) + +definition ordinary_parametrized_cohomology [reducible] {X : Type*} (G : X → AbGroup) (n : ℤ) : + AbGroup := +parametrized_cohomology (λx, EM_spectrum (G x)) n + +definition unreduced_parametrized_cohomology {X : Type} (Y : X → spectrum) (n : ℤ) : AbGroup := +@parametrized_cohomology X₊ (λx, option.cases_on x sunit Y) n + +definition unreduced_ordinary_parametrized_cohomology [reducible] {X : Type} (G : X → AbGroup) + (n : ℤ) : AbGroup := +unreduced_parametrized_cohomology (λx, EM_spectrum (G x)) n + +notation `H^` n `[`:0 X:0 `, ` Y:0 `]`:0 := cohomology X Y n +notation `oH^` n `[`:0 X:0 `, ` G:0 `]`:0 := ordinary_cohomology X G n +notation `H^` n `[`:0 X:0 `]`:0 := ordinary_cohomology_Z X n +notation `uH^` n `[`:0 X:0 `, ` Y:0 `]`:0 := unreduced_cohomology X Y n +notation `uoH^` n `[`:0 X:0 `, ` G:0 `]`:0 := unreduced_ordinary_cohomology X G n +notation `uH^` n `[`:0 X:0 `]`:0 := unreduced_ordinary_cohomology_Z X n notation `pH^` n `[`:0 binders `, ` r:(scoped Y, parametrized_cohomology Y n) `]`:0 := r +notation `opH^` n `[`:0 binders `, ` r:(scoped G, ordinary_parametrized_cohomology G n) `]`:0 := r +notation `upH^` n `[`:0 binders `, ` r:(scoped Y, unreduced_parametrized_cohomology Y n) `]`:0 := r +notation `uopH^` n `[`:0 binders `, ` r:(scoped G, unreduced_ordinary_parametrized_cohomology G 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 : ℤ) : +definition cohomology_equiv_shomotopy_group_sp_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 +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 + +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 + /- functoriality -/ @@ -81,6 +114,23 @@ 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 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 + +definition ordinary_cohomology_isomorphism_right (X : Type*) {G G' : AbGroup} (e : G ≃g G') + (n : ℤ) : oH^n[X, G] ≃g oH^n[X, G'] := +cohomology_isomorphism_right X (EM_spectrum_pequiv e) n + +definition ordinary_parametrized_cohomology_isomorphism_right (X : Type*) {G G' : X → AbGroup} + (e : Πx, G x ≃g G' x) (n : ℤ) : opH^n[(x : X), G x] ≃g opH^n[(x : X), G' x] := +parametrized_cohomology_isomorphism_right X (λx, EM_spectrum_pequiv (e x)) n + /- suspension axiom -/ definition cohomology_psusp_2 (Y : spectrum) (n : ℤ) : @@ -169,6 +219,11 @@ theorem EM_dimension (G : AbGroup) (n : ℤ) (H : n ≠ 0) : (equiv_of_isomorphism (cohomology_isomorphism (pequiv_plift pbool) _ _))) (EM_dimension' G n H) +open group algebra +theorem ordinary_cohomology_pbool (G : AbGroup) : ordinary_cohomology pbool G 0 ≃g G := +sorry +--isomorphism_of_equiv (trunc_equiv_trunc 0 (ppmap_pbool_pequiv _ ⬝e _) ⬝e !trunc_equiv) sorry + /- cohomology theory -/ structure cohomology_theory.{u} : Type.{u+1} := diff --git a/homotopy/serre.hlean b/homotopy/serre.hlean index eb19084..de278ea 100644 --- a/homotopy/serre.hlean +++ b/homotopy/serre.hlean @@ -1,9 +1,12 @@ -import ..algebra.module_exact_couple .strunc +import ..algebra.module_exact_couple .strunc .cohomology open eq spectrum trunc is_trunc pointed int EM algebra left_module fiber lift equiv is_equiv + cohomology group sigma unit +set_option pp.binder_types true /- Eilenberg MacLane spaces are the fibers of the Postnikov system of a type -/ +namespace pointed definition postnikov_map [constructor] (A : Type*) (n : ℕ₋₂) : ptrunc (n.+1) A →* ptrunc n A := ptrunc.elim (n.+1) !ptr @@ -62,6 +65,10 @@ begin end, this⁻¹ᵛ* +end pointed open pointed + +namespace spectrum + definition is_strunc_strunc_pred (X : spectrum) (k : ℤ) : is_strunc k (strunc (k - 1) X) := λn, @(is_trunc_of_le _ (maxm2_monotone (add_le_add_right (sub_one_le k) n))) !is_strunc_strunc @@ -69,10 +76,11 @@ definition postnikov_smap [constructor] (X : spectrum) (k : ℤ) : strunc k X →ₛ strunc (k - 1) X := strunc_elim (str (k - 1) X) (is_strunc_strunc_pred X k) -definition postnikov_smap_phomotopy [constructor] (X : spectrum) (k : ℤ) (n : ℤ) : - postnikov_smap X k n ~* postnikov_map (X n) (maxm2 (k - 1 + n)) ∘* - sorry := -sorry +definition pfiber_postnikov_smap (A : spectrum) (n : ℤ) (k : ℤ) : + pfiber (postnikov_smap A n k) ≃* EM_spectrum (πₛ[n] A) k := +begin + exact sorry +end section atiyah_hirzebruch parameters {X : Type*} (Y : X → spectrum) (s₀ : ℤ) (H : Πx, is_strunc s₀ (Y x)) @@ -80,16 +88,95 @@ section atiyah_hirzebruch 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 + + include H + definition atiyah_hirzebruch_lb ⦃s n : ℤ⦄ (Hs : s ≥ s₀ + 1) : + is_equiv (postnikov_smap (spi X Y) 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 + end + definition is_bounded_atiyah_hirzebruch : is_bounded atiyah_hirzebruch_exact_couple := - is_bounded_sequence _ s₀ (λn, n - 1) + 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))) := + converges_to_sequence _ s₀ (λn, n - 1) atiyah_hirzebruch_lb atiyah_hirzebruch_ub + + lemma spi_EM_spectrum (k s : ℤ) : + EM_spectrum (πₛ[s] (spi X Y)) k ≃* spi X (λx, EM_spectrum (πₛ[s] (Y x))) k := + sorry + + definition atiyah_hirzebruch_convergence : + (λn s, opH^-n[(x : X), πₛ[s] (Y x)]) ⟹ᵍ (λn, pH^-n[(x : X), Y x]) := + converges_to_g_isomorphism atiyah_hirzebruch_convergence' begin - intro s n H, - exact sorry + 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 end begin - intro s n H, apply trivial_shomotopy_group_of_is_strunc, - apply is_strunc_strunc, - exact lt_of_le_sub_one H, + 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, end end 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 + + /- NOTE: we need unreduced cohomology, maybe also define aityah_hirzebruch for unreduced cohomology -/ + include H + definition serre_convergence : + (λn s, opH^-n[(x : X₊), H^-s[F₊ₒ x, Y]]) ⟹ᵍ (λn, H^-n[(Σ(x : X), F x)₊, Y]) := + -- (λn s, uopH^-n[(x : X), uH^-s[F x, Y]]) ⟹ᵍ (λn, uH^-n[Σ(x : X), F x, Y]) := + proof + converges_to_g_isomorphism + (atiyah_hirzebruch_convergence (λx, sp_cotensor (F₊ₒ x) Y) s₀ + (λx, is_strunc_sp_cotensor s₀ (F₊ₒ x) H)) + begin + 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 +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 67049e7..6207293 100644 --- a/homotopy/spectrum.hlean +++ b/homotopy/spectrum.hlean @@ -8,7 +8,7 @@ Authors: Michael Shulman, Floris van Doorn, Egbert Rijke, Stefano Piceghello, Yu import homotopy.LES_of_homotopy_groups .splice ..colim types.pointed2 .EM ..pointed_pi .smash_adjoint ..algebra.seq_colim .fwedge .pointed_cubes open eq nat int susp pointed pmap sigma is_equiv equiv fiber algebra trunc trunc_index pi group - seq_colim succ_str EM EM.ops function + seq_colim succ_str EM EM.ops function unit lift is_trunc /--------------------- Basic definitions @@ -253,6 +253,18 @@ namespace spectrum -- Equivalences of prespectra ------------------------------ + definition spectrum_pequiv_of_nat {E F : spectrum} (e : Π(n : ℕ), E n ≃* F n) (n : ℤ) : + E n ≃* F n := + begin + have Πn, E (n + 1) ≃* F (n + 1) → E n ≃* F n, + from λk f, equiv_glue E k ⬝e* loop_pequiv_loop f ⬝e* (equiv_glue F k)⁻¹ᵉ*, + induction n with n n, + exact e n, + induction n with n IH, + { exact this -[1+0] (e 0) }, + { exact this -[1+succ n] IH } + end + structure is_sequiv {N : succ_str} {E F : gen_prespectrum N} (f : E →ₛ F) : Type := (to_linv : F →ₛ E) (is_retr : to_linv ∘ₛf ~ₛ sid E) @@ -326,6 +338,13 @@ namespace spectrum definition psp_sphere : gen_prespectrum +ℕ := psp_susp bool.pbool + ------------------------------ + -- Contractible spectrum + ------------------------------ + + definition sunit.{u} [constructor] : spectrum.{u} := + spectrum.MK (λn, plift punit) (λn, pequiv_of_is_contr _ _ _ _) + /--------------------- Homotopy groups ---------------------/ @@ -342,6 +361,14 @@ namespace spectrum πₛ[n] E →g πₛ[n] F := π→g[2] (f (2 - n)) + definition shomotopy_group_isomorphism_of_pequiv (n : ℤ) {E F : spectrum} (f : Πn, E n ≃* F n) : + πₛ[n] E ≃g πₛ[n] F := + homotopy_group_isomorphism_of_pequiv 1 (f (2 - n)) + + definition shomotopy_group_isomorphism_of_pequiv_nat (n : ℕ) {E F : spectrum} + (f : Πn, E n ≃* F n) : πₛ[n] E ≃g πₛ[n] F := + shomotopy_group_isomorphism_of_pequiv n (spectrum_pequiv_of_nat f) + notation `πₛ→[`:95 n:0 `]`:0 := shomotopy_group_fun n -- what an awful name @@ -405,7 +432,8 @@ namespace spectrum Fibers and long exact sequences -----------------------------------------/ - definition sfiber {N : succ_str} {X Y : gen_spectrum N} (f : X →ₛ Y) : gen_spectrum N := + definition sfiber [constructor] {N : succ_str} {X Y : gen_spectrum N} (f : X →ₛ Y) : + gen_spectrum N := spectrum.MK (λn, pfiber (f n)) (λn, (loop_pfiber (f (S n)))⁻¹ᵉ* ∘*ᵉ pfiber_pequiv_of_square _ _ (sglue_square f n)) @@ -728,6 +756,10 @@ spectrify_fun (smash_prespectrum_fun f g) definition EM_spectrum /-[constructor]-/ (G : AbGroup) : spectrum := spectrum.Mk (K G) (λn, (loop_EM G n)⁻¹ᵉ*) + definition EM_spectrum_pequiv {G H : AbGroup} (e : G ≃g H) (n : ℤ) : + EM_spectrum G n ≃* EM_spectrum H n := + spectrum_pequiv_of_nat (λk, EM_pequiv_EM k e) n + /- Wedge of prespectra -/ open fwedge diff --git a/homotopy/strunc.hlean b/homotopy/strunc.hlean index 0acf418..bbfec92 100644 --- a/homotopy/strunc.hlean +++ b/homotopy/strunc.hlean @@ -134,6 +134,10 @@ begin (maxm2_monotone (algebra.add_le_add_right H n)) end +definition is_strunc_pequiv_closed {k : ℤ} {E F : spectrum} (H : Πn, E n ≃* F n) + (H2 : is_strunc k E) : is_strunc k F := +λn, is_trunc_equiv_closed (maxm2 (k + n)) (H n) + definition is_strunc_strunc (k : ℤ) (E : spectrum) : is_strunc k (strunc k E) := λ n, is_trunc_trunc (maxm2 (k + n)) (E n) @@ -255,7 +259,7 @@ section end -definition is_strunc_spi (A : Type*) (k n : ℤ) (H : n ≤ k) (P : A → n-spectrum) +definition is_strunc_spi_of_le {A : Type*} (k n : ℤ) (H : n ≤ k) (P : A → n-spectrum) : is_strunc k (spi A P) := begin assert K : n ≤ -[1+ 0] + 1 + k, @@ -266,4 +270,12 @@ begin (truncspectrum.struct (P a)))) } end +definition is_strunc_spi {A : Type*} (n : ℤ) (P : A → spectrum) (H : Πa, is_strunc n (P a)) + : is_strunc n (spi A P) := +is_strunc_spi_of_le n n !le.refl (λa, truncspectrum.mk (P a) (H a)) + +definition is_strunc_sp_cotensor (n : ℤ) (A : Type*) {Y : spectrum} (H : is_strunc n Y) + : is_strunc n (sp_cotensor A Y) := +is_strunc_pequiv_closed (λn, !pppi_pequiv_ppmap) (is_strunc_spi n (λa, Y) (λa, H)) + end spectrum diff --git a/move_to_lib.hlean b/move_to_lib.hlean index dee29bd..9c2c4ee 100644 --- a/move_to_lib.hlean +++ b/move_to_lib.hlean @@ -227,6 +227,12 @@ namespace int definition sub_one_le (n : ℤ) : n - 1 ≤ n := sub_nat_le n 1 + definition le_add_nat (n : ℤ) (m : ℕ) : n ≤ n + m := + le.intro rfl + + definition le_add_one (n : ℤ) : n ≤ n + 1:= + le_add_nat n 1 + end int namespace pmap @@ -236,6 +242,14 @@ namespace pmap end pmap +namespace lift + + definition is_trunc_plift [instance] [priority 1450] (A : Type*) (n : ℕ₋₂) + [H : is_trunc n A] : is_trunc n (plift A) := + is_trunc_lift A n + +end lift + namespace trunc -- TODO: redefine loopn_ptrunc_pequiv diff --git a/pointed.hlean b/pointed.hlean index 355125e..cd3c1dc 100644 --- a/pointed.hlean +++ b/pointed.hlean @@ -195,6 +195,9 @@ namespace pointed definition is_contr_loop (A : Type*) [is_set A] : is_contr (Ω A) := is_contr.mk idp (λa, !is_prop.elim) + definition is_contr_punit [instance] : is_contr punit := + is_contr_unit + definition pequiv_of_is_contr (A B : Type*) (HA : is_contr A) (HB : is_contr B) : A ≃* B := pequiv_punit_of_is_contr A _ ⬝e* (pequiv_punit_of_is_contr B _)⁻¹ᵉ* diff --git a/pointed_pi.hlean b/pointed_pi.hlean index 5eaf6ea..49943d7 100644 --- a/pointed_pi.hlean +++ b/pointed_pi.hlean @@ -399,7 +399,7 @@ namespace pointed idpo)⁻¹ᵉ* qed - definition pmap_psigma {A B : Type*} (C : B → Type) (c : C pt) : + definition ppmap_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 _) := @@ -430,7 +430,7 @@ namespace pointed refine !idp_con ⬝ _, symmetry, refine !ap_id ◾ !idp_con ⬝ _, apply con.right_inv end ... ≃* ppmap A (psigma_gen (λb, f b = pt) (respect_pt f)) : - by exact (pmap_psigma _ _)⁻¹ᵉ* + by exact (ppmap_psigma _ _)⁻¹ᵉ* ... ≃* ppmap A (pfiber f) : by exact pequiv_ppcompose_left !pfiber.sigma_char'⁻¹ᵉ* @@ -460,6 +460,9 @@ namespace pointed by exact (ppi_psigma _ _)⁻¹ᵉ* ... ≃* Π*(a : A), pfiber (f a) : by exact ppi_pequiv_right (λa, !pfiber.sigma_char'⁻¹ᵉ*) + -- definition pppi_ppmap {A C : Type*} {B : A → Type*} : + -- ppmap (/- dependent smash of B -/) C ≃* Π*(a : A), ppmap (B a) C := + end pointed open pointed open is_trunc is_conn