From d8c694e1136468eb26f66d68176b3188076946d8 Mon Sep 17 00:00:00 2001 From: Floris van Doorn Date: Thu, 22 Sep 2016 16:03:08 -0400 Subject: [PATCH] update after changes in the HoTT library. Mostly some naming and notation changes --- algebra/group_constructions.hlean | 16 ++++----- algebra/module.hlean | 19 +++++++++-- homotopy/EM.hlean | 25 +++++++-------- homotopy/cohomology.hlean | 4 +-- homotopy/degree.hlean | 44 ++++++++++++------------- homotopy/spectrum.hlean | 34 ++++++++++---------- homotopy/spherical_fibrations.hlean | 4 +-- move_to_lib.hlean | 50 ++++++++++++++--------------- 8 files changed, 103 insertions(+), 93 deletions(-) diff --git a/algebra/group_constructions.hlean b/algebra/group_constructions.hlean index 4485f17..753cb99 100644 --- a/algebra/group_constructions.hlean +++ b/algebra/group_constructions.hlean @@ -165,10 +165,10 @@ namespace group variable {N} definition gq_map_eq_one (g : G) (H : N g) : gq_map N g = 1 := - begin + begin apply eq_of_rel, have e : (g * 1⁻¹ = g), - from calc + from calc g * 1⁻¹ = g * 1 : one_inv ... = g : mul_one, unfold quotient_rel, rewrite e, exact H @@ -177,18 +177,18 @@ namespace group definition rel_of_gq_map_eq_one (g : G) (H : gq_map N g = 1) : N g := begin have e : (g * 1⁻¹ = g), - from calc + from calc g * 1⁻¹ = g * 1 : one_inv ... = g : mul_one, rewrite (inverse e), - apply rel_of_eq _ H - end + apply rel_of_eq _ H + end definition quotient_group_elim (f : G →g G') (H : Π⦃g⦄, N g → f g = 1) : quotient_group N →g G' := begin fapply homomorphism.mk, -- define function - { apply set_quotient.elim f, + { apply set_quotient.elim f, intro g h K, apply eq_of_mul_inv_eq_one, have e : f (g * h⁻¹) = f g * (f h)⁻¹, @@ -197,8 +197,8 @@ namespace group ... = f g * (f h)⁻¹ : to_respect_inv, rewrite (inverse e), apply H, exact K}, - { intro g h, induction g using set_quotient.rec_prop with g, - induction h using set_quotient.rec_prop with h, + { intro g h, induction g using set_quotient.rec_prop with g, + induction h using set_quotient.rec_prop with h, krewrite (inverse (to_respect_mul (gq_map N) g h)), unfold gq_map, esimp, exact to_respect_mul f g h } end diff --git a/algebra/module.hlean b/algebra/module.hlean index 2279517..f6496d2 100644 --- a/algebra/module.hlean +++ b/algebra/module.hlean @@ -17,13 +17,26 @@ infixl ` • `:73 := has_scalar.smul /- modules over a ring -/ -structure left_module [class] (R M : Type) [ringR : ring R] - extends has_scalar R M, add_comm_group M := +structure left_module (R M : Type) [ringR : ring R] extends has_scalar R M, comm_group M renaming + mul→add mul_assoc→add_assoc one→zero one_mul→zero_add mul_one→add_zero inv→neg + mul_left_inv→add_left_inv mul_comm→add_comm := (smul_left_distrib : Π (r : R) (x y : M), smul r (add x y) = (add (smul r x) (smul r y))) -(smul_right_distrib : Π (r s : R) (x : M), smul (ring.add r s) x = (add (smul r x) (smul s x))) +(smul_right_distrib : Π (r s : R) (x : M), smul (ring.add _ r s) x = (add (smul r x) (smul s x))) (mul_smul : Π r s x, smul (mul r s) x = smul r (smul s x)) (one_smul : Π x, smul one x = x) +/- we make it a class now (and not as part of the structure) to avoid + left_module.to_comm_group to be an instance -/ +attribute left_module [class] + +definition add_comm_group_of_left_module [reducible] [trans_instance] (R M : Type) [K : ring R] + [H : left_module R M] : add_comm_group M := +@left_module.to_comm_group R M K H + +definition has_scalar_of_left_module [reducible] [trans_instance] (R M : Type) [K : ring R] + [H : left_module R M] : has_scalar R M := +@left_module.to_has_scalar R M K H + section left_module variables {R M : Type} variable [ringR : ring R] diff --git a/homotopy/EM.hlean b/homotopy/EM.hlean index c5a38ae..075a5f7 100644 --- a/homotopy/EM.hlean +++ b/homotopy/EM.hlean @@ -10,7 +10,7 @@ Eilenberg MacLane spaces import homotopy.EM .spectrum open eq is_equiv equiv is_conn is_trunc unit function pointed nat group algebra trunc trunc_index - fiber prod fin pointed susp EM.ops + fiber prod pointed susp EM.ops namespace EM @@ -26,7 +26,7 @@ namespace EM induction n with n IH, { exact loop_pequiv_loop (loop_EM2 G)}, refine _ ⬝e* IH, - refine !phomotopy_group_pequiv_loop_ptrunc⁻¹ᵉ* ⬝e* _ ⬝e* !phomotopy_group_pequiv_loop_ptrunc, + refine !homotopy_group_pequiv_loop_ptrunc⁻¹ᵉ* ⬝e* _ ⬝e* !homotopy_group_pequiv_loop_ptrunc, apply iterate_psusp_stability_pequiv, rexact add_mul_le_mul_add n 1 1 end @@ -97,12 +97,12 @@ namespace EM { exact pt}, { exact pt}, change carrier (Ω X), refine f _ _ _ _ _ (tr x), - { refine _⁻¹ᵉ ⬝e e, apply equiv_of_pequiv, apply pequiv_of_eq, apply loop_space_succ_eq_in}, + { refine _⁻¹ᵉ ⬝e e, apply equiv_of_pequiv, apply loopn_succ_in}, exact abstract begin intro p q, refine _ ⬝ !r, apply ap e, esimp, - apply inv_tr_eq_of_eq_tr, symmetry, - rewrite [- + ap_inv, - + tr_compose], - refine !loop_space_succ_eq_in_concat ⬝ _, exact !tr_inv_tr ◾ !tr_inv_tr + apply inv_eq_of_eq, + refine _⁻¹ ⬝ !loopn_succ_in_con⁻¹, + exact to_right_inv (loopn_succ_in X (succ n)) p ◾ to_right_inv (loopn_succ_in X (succ n)) q end end end @@ -172,10 +172,10 @@ namespace EM -- definition freudenthal_homotopy_group_pequiv (A : Type*) {n k : ℕ} [is_conn n A] (H : k ≤ 2 * n) -- : π*[k + 1] (psusp A) ≃* π*[k] A := -- calc --- π*[k + 1] (psusp A) ≃* π*[k] (Ω (psusp A)) : pequiv_of_eq (phomotopy_group_succ_in (psusp A) k) --- ... ≃* Ω[k] (ptrunc k (Ω (psusp A))) : phomotopy_group_pequiv_loop_ptrunc k (Ω (psusp A)) +-- π*[k + 1] (psusp A) ≃* π*[k] (Ω (psusp A)) : pequiv_of_eq (homotopy_group_succ_in (psusp A) k) +-- ... ≃* Ω[k] (ptrunc k (Ω (psusp A))) : homotopy_group_pequiv_loop_ptrunc k (Ω (psusp A)) -- ... ≃* Ω[k] (ptrunc k A) : loopn_pequiv_loopn k (freudenthal_pequiv A H) --- ... ≃* π*[k] A : (phomotopy_group_pequiv_loop_ptrunc k A)⁻¹ᵉ* +-- ... ≃* π*[k] A : (homotopy_group_pequiv_loop_ptrunc k A)⁻¹ᵉ* definition iterate_psusp_succ_pequiv (n : ℕ) (A : Type*) : iterate_psusp (succ n) A ≃* iterate_psusp n (psusp A) := @@ -217,9 +217,9 @@ namespace EM { exact pcompose f}, { exact pcompose f⁻¹ᵉ*}, { intro f, apply pmap_eq_of_phomotopy, - exact !passoc⁻¹* ⬝* pwhisker_right _ !pright_inv ⬝* !pid_comp}, + exact !passoc⁻¹* ⬝* pwhisker_right _ !pright_inv ⬝* !pid_pcompose}, { intro f, apply pmap_eq_of_phomotopy, - exact !passoc⁻¹* ⬝* pwhisker_right _ !pleft_inv ⬝* !pid_comp} + exact !passoc⁻¹* ⬝* pwhisker_right _ !pleft_inv ⬝* !pid_pcompose} end definition iterate_psusp_adjoint_loopn [constructor] (X Y : Type*) (n : ℕ) : @@ -228,10 +228,9 @@ namespace EM revert X Y, induction n with n IH: intro X Y, { reflexivity}, { refine !susp_adjoint_loop ⬝e !IH ⬝e _, apply pmap_equiv_pmap_right, - symmetry, apply pequiv_of_eq, apply loop_space_succ_eq_in} + symmetry, apply loopn_succ_in} end - end EM -- cohomology ∥ X → K(G,n) ∥ -- reduced cohomology ∥ X →* K(G,n) ∥ diff --git a/homotopy/cohomology.hlean b/homotopy/cohomology.hlean index bd09458..98a140b 100644 --- a/homotopy/cohomology.hlean +++ b/homotopy/cohomology.hlean @@ -22,5 +22,5 @@ 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 -check H^3[S¹.,EM_spectrum agℤ] -check H^3[S¹.] +check H^3[S¹*,EM_spectrum agℤ] +check H^3[S¹*] diff --git a/homotopy/degree.hlean b/homotopy/degree.hlean index 847c79b..5d3d2e2 100644 --- a/homotopy/degree.hlean +++ b/homotopy/degree.hlean @@ -29,12 +29,12 @@ namespace sphere -- unfold [π2S2, chain_complex.LES_of_homotopy_groups], -- end -check (pmap.to_fun - (chain_complex.cc_to_fn - (chain_complex.LES_of_homotopy_groups - hopf.complex_phopf) - (pair 1 2)) - (tr surf)) +-- check (pmap.to_fun +-- (chain_complex.cc_to_fn +-- (chain_complex.LES_of_homotopy_groups +-- hopf.complex_phopf) +-- (pair 1 2)) +-- (tr surf)) -- eval (pmap.to_fun -- (chain_complex.cc_to_fn @@ -43,33 +43,31 @@ check (pmap.to_fun -- (pair 1 2)) -- (tr surf)) - -- definition πnSn_surf (n : ℕ) : πnSn n (tr surf) = 1 :> ℤ := - -- begin - -- cases n with n IH, - -- { refine ap (πnSn _ ∘ tr) surf_eq_loop ⬝ _, apply transport_code_loop }, - -- { unfold [πnSn], } - -- end --- set_option pp.all true + definition πnSn_surf (n : ℕ) : πnSn n (tr surf) = 1 :> ℤ := + begin + cases n with n IH, + { refine ap (πnSn _ ∘ tr) surf_eq_loop ⬝ _, apply transport_code_loop }, + { unfold [πnSn], exact sorry} + end -exit - definition deg {n : ℕ} [H : is_succ n] (f : S. n →* S. n) : ℤ := + definition deg {n : ℕ} [H : is_succ n] (f : S* n →* S* n) : ℤ := by induction H with n; exact πnSn n ((π→g[n+1] f) (tr surf)) - definition deg_id (n : ℕ) [H : is_succ n] : deg (pid (S. n)) = (1 : ℤ) := + definition deg_id (n : ℕ) [H : is_succ n] : deg (pid (S* n)) = (1 : ℤ) := by induction H with n; - exact ap (πnSn n) (phomotopy_group_functor_pid (succ n) (S. (succ n)) (tr surf)) ⬝ πnSn_surf n + exact ap (πnSn n) (phomotopy_group_functor_pid (succ n) (S* (succ n)) (tr surf)) ⬝ πnSn_surf n - definition deg_phomotopy {n : ℕ} [H : is_succ n] {f g : S. n →* S. n} (p : f ~* g) : + definition deg_phomotopy {n : ℕ} [H : is_succ n] {f g : S* n →* S* n} (p : f ~* g) : deg f = deg g := begin induction H with n, - exact ap (πnSn n) (phomotopy_group_functor_phomotopy (succ n) p (tr surf)), + exact ap (πnSn n) (homotopy_group_functor_phomotopy (succ n) p (tr surf)), end definition endomorphism_int (f : gℤ →g gℤ) (n : ℤ) : f n = f (1 : ℤ) *[ℤ] n := @endomorphism_int_unbundled f (homomorphism.addstruct f) n - definition endomorphism_equiv_Z {i : signature} {X : Group i} (e : X ≃g gℤ) {one : X} + definition endomorphism_equiv_Z {X : Group} (e : X ≃g gℤ) {one : X} (p : e one = 1 :> ℤ) (φ : X →g X) (x : X) : e (φ x) = e (φ one) *[ℤ] e x := begin revert x, refine equiv_rect' (equiv_of_isomorphism e) _ _, @@ -81,15 +79,15 @@ exit { symmetry, exact to_right_inv (equiv_of_isomorphism e) n} end - definition deg_compose {n : ℕ} [H : is_succ n] (f g : S. n →* S. n) : + definition deg_compose {n : ℕ} [H : is_succ n] (f g : S* n →* S* n) : deg (g ∘* f) = deg g *[ℤ] deg f := begin induction H with n, - refine ap (πnSn n) (phomotopy_group_functor_compose (succ n) g f (tr surf)) ⬝ _, + refine ap (πnSn n) (homotopy_group_functor_compose (succ n) g f (tr surf)) ⬝ _, apply endomorphism_equiv_Z !πnSn !πnSn_surf (π→g[n+1] g) end - definition deg_equiv {n : ℕ} [H : is_succ n] (f : S. n ≃* S. n) : + definition deg_equiv {n : ℕ} [H : is_succ n] (f : S* n ≃* S* n) : deg f = 1 ⊎ deg f = -1 := begin induction H with n, diff --git a/homotopy/spectrum.hlean b/homotopy/spectrum.hlean index 1650eb5..2d1631a 100644 --- a/homotopy/spectrum.hlean +++ b/homotopy/spectrum.hlean @@ -130,9 +130,9 @@ namespace spectrum definition sid {N : succ_str} (E : gen_spectrum N) : E →ₛ E := smap.mk (λn, pid (E n)) - (λn, calc glue E n ∘* pid (E n) ~* glue E n : comp_pid - ... ~* pid (Ω(E (S n))) ∘* glue E n : pid_comp - ... ~* Ω→(pid (E (S n))) ∘* glue E n : pwhisker_right (glue E n) ap1_id⁻¹*) + (λ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 := smap.mk (λn, g n ∘* f n) @@ -142,7 +142,7 @@ namespace spectrum ... ~* Ω→(to_fun g (S n)) ∘* (glue Y n ∘* to_fun f n) : passoc ... ~* Ω→(to_fun g (S n)) ∘* (Ω→ (f (S n)) ∘* glue X n) : pwhisker_left Ω→(to_fun g (S n)) (glue_square f n) ... ~* (Ω→(to_fun g (S n)) ∘* Ω→(f (S n))) ∘* glue X n : passoc - ... ~* Ω→(to_fun g (S n) ∘* to_fun f (S n)) ∘* glue X n : pwhisker_right (glue X n) (ap1_compose _ _)) + ... ~* Ω→(to_fun g (S n) ∘* to_fun f (S n)) ∘* glue X n : pwhisker_right (glue X n) (ap1_pcompose _ _)) infixr ` ∘ₛ `:60 := scompose @@ -209,7 +209,7 @@ namespace spectrum -- prespectra too, but as with truncation, why bother? definition sp_cotensor {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)))⁻¹ᵉ* ∘*ᵉ (equiv_ppcompose_left (equiv_glue B n))) + (λn, (loop_pmap_commute A (B (S n)))⁻¹ᵉ* ∘*ᵉ (pequiv_ppcompose_left (equiv_glue B n))) ---------------------------------------- -- Sections of parametrized spectra @@ -234,11 +234,11 @@ namespace spectrum intro n, exact sorry end - definition π_glue (X : spectrum) (n : ℤ) : π*[2] (X (2 - succ n)) ≃* π*[3] (X (2 - n)) := + definition π_glue (X : spectrum) (n : ℤ) : π[2] (X (2 - succ n)) ≃* π[3] (X (2 - n)) := begin - refine phomotopy_group_pequiv 2 (equiv_glue X (2 - succ n)) ⬝e* _, + refine homotopy_group_pequiv 2 (equiv_glue X (2 - succ n)) ⬝e* _, assert H : succ (2 - succ n) = 2 - n, exact ap succ !sub_sub⁻¹ ⬝ sub_add_cancel (2-n) 1, - exact pequiv_of_eq (ap (λn, π*[2] (Ω (X n))) H), + exact pequiv_of_eq (ap (λn, π[2] (Ω (X n))) H), end definition πg_glue (X : spectrum) (n : ℤ) : πg[1+1] (X (2 - succ n)) ≃g πg[2+1] (X (2 - n)) := @@ -257,14 +257,14 @@ namespace spectrum end definition π_glue_square {X Y : spectrum} (f : X →ₛ Y) (n : ℤ) : - π_glue Y n ∘* π→*[2] (f (2 - succ n)) ~* π→*[3] (f (2 - n)) ∘* π_glue X n := + π_glue Y n ∘* π→[2] (f (2 - succ n)) ~* π→[3] (f (2 - n)) ∘* π_glue X n := begin refine !passoc ⬝* _, - assert H1 : phomotopy_group_pequiv 2 (equiv_glue Y (2 - succ n)) ∘* π→*[2] (f (2 - succ n)) - ~* π→*[2] (Ω→ (f (succ (2 - succ n)))) ∘* phomotopy_group_pequiv 2 (equiv_glue X (2 - succ n)), - { refine !phomotopy_group_functor_compose⁻¹* ⬝* _, - refine phomotopy_group_functor_phomotopy 2 !sglue_square ⬝* _, - apply phomotopy_group_functor_compose }, + assert H1 : homotopy_group_pequiv 2 (equiv_glue Y (2 - succ n)) ∘* π→[2] (f (2 - succ n)) + ~* π→[2] (Ω→ (f (succ (2 - succ n)))) ∘* homotopy_group_pequiv 2 (equiv_glue X (2 - succ n)), + { refine !homotopy_group_functor_compose⁻¹* ⬝* _, + refine homotopy_group_functor_phomotopy 2 !sglue_square ⬝* _, + apply homotopy_group_functor_compose }, refine pwhisker_left _ H1 ⬝* _, clear H1, refine !passoc⁻¹* ⬝* _ ⬝* !passoc, apply pwhisker_right, @@ -314,12 +314,12 @@ namespace spectrum -- | (n, fin.mk k H) := πₛ[n] (sfiber f) -- definition shomotopy_groups_fun : Π(n : -3ℤ), shomotopy_groups (S n) →g shomotopy_groups n --- | (n, fin.mk 0 H) := proof π→g[1+1] (f (n + 2)) qed --π→*[2] f (n+2) +-- | (n, fin.mk 0 H) := proof π→g[1+1] (f (n + 2)) qed --π→[2] f (n+2) -- --pmap_of_homomorphism (πₛ→[n] f) -- | (n, fin.mk 1 H) := proof π→g[1+1] (ppoint (f (n + 2))) qed -- | (n, fin.mk 2 H) := -- proof _ ∘g π→g[1+1] equiv_glue Y (pred n + 2) qed --- --π→*[n] boundary_map ∘* pcast (ap (ptrunc 0) (loop_space_succ_eq_in Y n)) +-- --π→[n] boundary_map ∘* pcast (ap (ptrunc 0) (loop_space_succ_eq_in Y n)) -- | (n, fin.mk (k+3) H) := begin exfalso, apply lt_le_antisymm H, apply le_add_left end end @@ -348,7 +348,7 @@ namespace spectrum gen_spectrum N := gen_spectrum.mk (mapping_prespectrum X Y) - (is_spectrum.mk (λn, to_is_equiv (equiv_ppcompose_left (equiv_glue Y n) ⬝e + (is_spectrum.mk (λn, to_is_equiv (pequiv_ppcompose_left (equiv_glue Y n) ⬝e pfunext X (Y (S n))))) /- Spectrification -/ diff --git a/homotopy/spherical_fibrations.hlean b/homotopy/spherical_fibrations.hlean index c6e274a..288b9f5 100644 --- a/homotopy/spherical_fibrations.hlean +++ b/homotopy/spherical_fibrations.hlean @@ -48,10 +48,10 @@ namespace spherical_fibrations /- classifying type of pointed spherical fibrations -/ definition BF (n : ℕ) : Type₁ := - Σ(X : Type*), ∥ X ≃* S. n ∥ + Σ(X : Type*), ∥ X ≃* S* n ∥ definition pointed_BF [instance] [constructor] (n : ℕ) : pointed (BF n) := - pointed.mk ⟨ S. n , tr pequiv.rfl ⟩ + pointed.mk ⟨ S* n , tr pequiv.rfl ⟩ definition pBF [constructor] (n : ℕ) : Type* := pointed.mk' (BF n) diff --git a/move_to_lib.hlean b/move_to_lib.hlean index 13d0ab2..2c0cb92 100644 --- a/move_to_lib.hlean +++ b/move_to_lib.hlean @@ -20,13 +20,13 @@ open sigma namespace group open is_trunc - definition pSet_of_Group {i : signature} (G : Group i) : Set* := ptrunctype.mk G _ 1 + definition pSet_of_Group (G : Group) : Set* := ptrunctype.mk G _ 1 - definition pmap_of_isomorphism [constructor] {i j : signature} {G₁ : Group i} {G₂ : Group j} + definition pmap_of_isomorphism [constructor] {G₁ : Group} {G₂ : Group} (φ : G₁ ≃g G₂) : pType_of_Group G₁ →* pType_of_Group G₂ := pequiv_of_isomorphism φ - definition pequiv_of_isomorphism_of_eq {i : signature} {G₁ G₂ : Group i} (p : G₁ = G₂) : + definition pequiv_of_isomorphism_of_eq {G₁ G₂ : Group} (p : G₁ = G₂) : pequiv_of_isomorphism (isomorphism_of_eq p) = pequiv_of_eq (ap pType_of_Group p) := begin induction p, @@ -36,7 +36,7 @@ namespace group { apply is_prop.elim} end - definition homomorphism_change_fun [constructor] {i j : signature} {G₁ : Group i} {G₂ : Group j} + definition homomorphism_change_fun [constructor] {G₁ G₂ : Group} (φ : G₁ →g G₂) (f : G₁ → G₂) (p : φ ~ f) : G₁ →g G₂ := homomorphism.mk f (λg h, (p (g * h))⁻¹ ⬝ to_respect_mul φ g h ⬝ ap011 mul (p g) (p h)) @@ -128,30 +128,30 @@ namespace pointed ... -/ ≃ (A →* Ω B) : pmap.sigma_char) (by reflexivity) - definition ppcompose_left {A B C : Type*} (g : B →* C) : ppmap A B →* ppmap A C := - pmap.mk (pcompose g) (eq_of_phomotopy (phomotopy.mk (λa, resp_pt g) (idp_con _)⁻¹)) + -- definition ppcompose_left {A B C : Type*} (g : B →* C) : ppmap A B →* ppmap A C := + -- pmap.mk (pcompose g) (eq_of_phomotopy (phomotopy.mk (λa, resp_pt g) (idp_con _)⁻¹)) - definition is_equiv_ppcompose_left [instance] {A B C : Type*} (g : B →* C) [H : is_equiv g] : is_equiv (@ppcompose_left A B C g) := - begin - fapply is_equiv.adjointify, - { exact (ppcompose_left (pequiv_of_pmap g H)⁻¹ᵉ*) }, - all_goals (intros f; esimp; apply eq_of_phomotopy), - { exact calc g ∘* ((pequiv_of_pmap g H)⁻¹ᵉ* ∘* f) ~* (g ∘* (pequiv_of_pmap g H)⁻¹ᵉ*) ∘* f : passoc - ... ~* pid _ ∘* f : pwhisker_right f (pright_inv (pequiv_of_pmap g H)) - ... ~* f : pid_comp f }, - { exact calc (pequiv_of_pmap g H)⁻¹ᵉ* ∘* (g ∘* f) ~* ((pequiv_of_pmap g H)⁻¹ᵉ* ∘* g) ∘* f : passoc - ... ~* pid _ ∘* f : pwhisker_right f (pleft_inv (pequiv_of_pmap g H)) - ... ~* f : pid_comp f } - end + -- definition is_equiv_ppcompose_left [instance] {A B C : Type*} (g : B →* C) [H : is_equiv g] : is_equiv (@ppcompose_left A B C g) := + -- begin + -- fapply is_equiv.adjointify, + -- { exact (ppcompose_left (pequiv_of_pmap g H)⁻¹ᵉ*) }, + -- all_goals (intros f; esimp; apply eq_of_phomotopy), + -- { exact calc g ∘* ((pequiv_of_pmap g H)⁻¹ᵉ* ∘* f) ~* (g ∘* (pequiv_of_pmap g H)⁻¹ᵉ*) ∘* f : passoc + -- ... ~* pid _ ∘* f : pwhisker_right f (pright_inv (pequiv_of_pmap g H)) + -- ... ~* f : pid_pcompose f }, + -- { exact calc (pequiv_of_pmap g H)⁻¹ᵉ* ∘* (g ∘* f) ~* ((pequiv_of_pmap g H)⁻¹ᵉ* ∘* g) ∘* f : passoc + -- ... ~* pid _ ∘* f : pwhisker_right f (pleft_inv (pequiv_of_pmap g H)) + -- ... ~* f : pid_pcompose f } + -- end - definition equiv_ppcompose_left {A B C : Type*} (g : B ≃* C) : ppmap A B ≃* ppmap A C := - pequiv_of_pmap (ppcompose_left g) _ + -- definition pequiv_ppcompose_left {A B C : Type*} (g : B ≃* C) : ppmap A B ≃* ppmap A C := + -- pequiv_of_pmap (ppcompose_left g) _ - definition pcompose_pconst {A B C : Type*} (f : B →* C) : f ∘* pconst A B ~* pconst A C := - phomotopy.mk (λa, respect_pt f) (idp_con _)⁻¹ + -- definition pcompose_pconst {A B C : Type*} (f : B →* C) : f ∘* pconst A B ~* pconst A C := + -- phomotopy.mk (λa, respect_pt f) (idp_con _)⁻¹ - definition pconst_pcompose {A B C : Type*} (f : A →* B) : pconst B C ∘* f ~* pconst A C := - phomotopy.mk (λa, rfl) (ap_constant _ _)⁻¹ + -- definition pconst_pcompose {A B C : Type*} (f : A →* B) : pconst B C ∘* f ~* pconst A C := + -- phomotopy.mk (λa, rfl) (ap_constant _ _)⁻¹ definition ap1_pconst (A B : Type*) : Ω→(pconst A B) ~* pconst (Ω A) (Ω B) := phomotopy.mk (λp, idp_con _ ⬝ ap_constant p pt) rfl @@ -232,7 +232,7 @@ end fiber namespace eq --algebra.homotopy_group - definition phomotopy_group_functor_pid (n : ℕ) (A : Type*) : π→*[n] (pid A) ~* pid (π*[n] A) := + definition phomotopy_group_functor_pid (n : ℕ) (A : Type*) : π→[n] (pid A) ~* pid (π[n] A) := ptrunc_functor_phomotopy 0 !apn_pid ⬝* !ptrunc_functor_pid end eq