From 2b722b3e34240511534810c5ff1ff11d6d9c6da5 Mon Sep 17 00:00:00 2001 From: Floris van Doorn Date: Mon, 10 Sep 2018 14:29:06 +0200 Subject: [PATCH] use psquare for naturality squares consistently this commit renames some definitions and swaps some arguments around for consistency --- hott/algebra/homotopy_group.hlean | 11 ++- hott/homotopy/LES_of_homotopy_groups.hlean | 8 +- hott/homotopy/susp.hlean | 18 +++-- hott/types/pointed.hlean | 94 +++++++++++----------- 4 files changed, 68 insertions(+), 63 deletions(-) diff --git a/hott/algebra/homotopy_group.hlean b/hott/algebra/homotopy_group.hlean index 0eb2cee0a..ab8d25185 100644 --- a/hott/algebra/homotopy_group.hlean +++ b/hott/algebra/homotopy_group.hlean @@ -161,22 +161,21 @@ namespace eq @(is_equiv_trunc_functor 0 _) (is_equiv_apn n f H) definition homotopy_group_succ_in_natural (n : ℕ) {A B : Type*} (f : A →* B) : - homotopy_group_succ_in n B ∘* π→[n + 1] f ~* - π→[n] (Ω→ f) ∘* homotopy_group_succ_in n A := + psquare (homotopy_group_succ_in n A) (homotopy_group_succ_in n B) + (π→[n + 1] f) (π→[n] (Ω→ f)) := begin - refine !ptrunc_functor_pcompose⁻¹* ⬝* _ ⬝* !ptrunc_functor_pcompose, - exact ptrunc_functor_phomotopy 0 (apn_succ_phomotopy_in n f) + exact ptrunc_functor_psquare 0 (loopn_succ_in_natural n f), end definition homotopy_group_succ_in_natural_unpointed (n : ℕ) {A B : Type*} (f : A →* B) : hsquare (homotopy_group_succ_in n A) (homotopy_group_succ_in n B) (π→[n+1] f) (π→[n] (Ω→ f)) := - (homotopy_group_succ_in_natural n f)⁻¹* + homotopy_group_succ_in_natural n f definition is_equiv_homotopy_group_functor_ap1 (n : ℕ) {A B : Type*} (f : A →* B) [is_equiv (π→[n + 1] f)] : is_equiv (π→[n] (Ω→ f)) := have is_equiv (π→[n] (Ω→ f) ∘ homotopy_group_succ_in n A), from is_equiv_of_equiv_of_homotopy (equiv.mk (π→[n+1] f) _ ⬝e homotopy_group_succ_in n B) - (homotopy_group_succ_in_natural n f), + (homotopy_group_succ_in_natural n f)⁻¹*, is_equiv.cancel_right (homotopy_group_succ_in n A) _ definition tinverse [constructor] {X : Type*} : π[1] X →* π[1] X := diff --git a/hott/homotopy/LES_of_homotopy_groups.hlean b/hott/homotopy/LES_of_homotopy_groups.hlean index 9efa2a01c..8068627b9 100644 --- a/hott/homotopy/LES_of_homotopy_groups.hlean +++ b/hott/homotopy/LES_of_homotopy_groups.hlean @@ -272,7 +272,7 @@ namespace chain_complex definition pid_or_pinverse_add4_rev (n : ℕ) : pid_or_pinverse (n + 4) ~* !pinverse ∘* Ω→(pid_or_pinverse (n + 1)) := - !ap1_pcompose_pinverse + !pinverse_natural theorem fiber_sequence_phomotopy_loop_spaces : Π(n : ℕ), fiber_sequence_pequiv_loop_spaces n ∘* fiber_sequence_fun n ~* @@ -300,7 +300,7 @@ namespace chain_complex xrewrite [loop_spaces_fun_add3, pid_or_pinverse_add4, to_pmap_pequiv_trans], refine _ ⬝* !passoc⁻¹*, refine _ ⬝* pwhisker_left _ !passoc⁻¹*, - refine _ ⬝* pwhisker_left _ (pwhisker_left _ !ap1_pcompose_pinverse), + refine _ ⬝* pwhisker_left _ (pwhisker_left _ !pinverse_natural), refine !passoc⁻¹* ⬝* _ ⬝* !passoc ⬝* !passoc, apply pwhisker_right, refine !ap1_pcompose⁻¹* ⬝* _ ⬝* !ap1_pcompose ⬝* pwhisker_right _ !ap1_pcompose, @@ -345,7 +345,7 @@ namespace chain_complex apply pwhisker_left, refine !ap1_pcompose ⬝* _ ⬝* !passoc ⬝* !passoc, apply pwhisker_right, - refine _ ⬝* pwhisker_right _ !ap1_pcompose_pinverse, + refine _ ⬝* pwhisker_right _ !pinverse_natural, refine _ ⬝* !passoc⁻¹*, refine !pcompose_pid⁻¹* ⬝* pwhisker_left _ _, symmetry, apply pinverse_pinverse @@ -364,7 +364,7 @@ namespace chain_complex replace (k + 4) with (k + 1 + 3), rewrite [loop_spaces_fun_add3], refine !passoc⁻¹* ⬝* _ ⬝* !passoc⁻¹*, - refine _ ⬝* pwhisker_left _ !ap1_pcompose_pinverse, + refine _ ⬝* pwhisker_left _ !pinverse_natural, refine _ ⬝* !passoc, apply pwhisker_right, refine !ap1_pcompose⁻¹* ⬝* _ ⬝* !ap1_pcompose, diff --git a/hott/homotopy/susp.hlean b/hott/homotopy/susp.hlean index 24df3f986..7d8eba65e 100644 --- a/hott/homotopy/susp.hlean +++ b/hott/homotopy/susp.hlean @@ -213,6 +213,8 @@ namespace susp { reflexivity } end + notation `⅀→`:(max+5) := susp_functor + definition is_equiv_susp_functor [constructor] (f : X →* Y) [Hf : is_equiv f] : is_equiv (susp_functor f) := susp.is_equiv_functor f @@ -245,6 +247,8 @@ namespace susp { reflexivity }, end + notation `⅀⇒`:(max+5) := susp_functor_phomotopy + definition susp_functor_pid (A : Type*) : susp_functor (pid A) ~* pid (susp A) := begin fapply phomotopy.mk, @@ -266,8 +270,9 @@ namespace susp end definition loop_susp_unit_natural (f : X →* Y) - : loop_susp_unit Y ∘* f ~* Ω→ (susp_functor f) ∘* loop_susp_unit X := + : psquare (loop_susp_unit X) (loop_susp_unit Y) f (Ω→ (susp_functor f)) := begin + apply ptranspose, induction X with X x, induction Y with Y y, induction f with f pf, esimp at *, induction pf, fapply phomotopy.mk, { intro x', symmetry, @@ -294,7 +299,7 @@ namespace susp end definition loop_susp_counit_natural (f : X →* Y) - : f ∘* loop_susp_counit X ~* loop_susp_counit Y ∘* (susp_functor (ap1 f)) := + : psquare (loop_susp_counit X) (loop_susp_counit Y) (⅀→ (Ω→ f)) f := begin induction X with X x, induction Y with Y y, induction f with f pf, esimp at *, induction pf, fconstructor, @@ -360,7 +365,7 @@ namespace susp definition loop_susp_intro_natural {X Y Z : Type*} (g : susp Y →* Z) (f : X →* Y) : loop_susp_intro (g ∘* susp_functor f) ~* loop_susp_intro g ∘* f := - pwhisker_right _ !ap1_pcompose ⬝* !passoc ⬝* pwhisker_left _ !loop_susp_unit_natural⁻¹* ⬝* + pwhisker_right _ !ap1_pcompose ⬝* !passoc ⬝* pwhisker_left _ !loop_susp_unit_natural ⬝* !passoc⁻¹* definition susp_adjoint_loop_right_inv {X Y : Type*} (g : X →* Ω Y) : @@ -368,7 +373,7 @@ namespace susp begin refine !pwhisker_right !ap1_pcompose ⬝* _, refine !passoc ⬝* _, - refine !pwhisker_left !loop_susp_unit_natural⁻¹* ⬝* _, + refine !pwhisker_left !loop_susp_unit_natural ⬝* _, refine !passoc⁻¹* ⬝* _, refine !pwhisker_right !loop_susp_counit_unit ⬝* _, apply pid_pcompose @@ -403,7 +408,8 @@ namespace susp { apply eq_pathover, refine !elim_merid ⬝ph _ ⬝hp !ap_constant⁻¹, exact square_of_eq !con.right_inv⁻¹ } end - definition susp_functor_pconst [constructor] (X Y : Type*) : susp_functor (pconst X Y) ~* pconst (susp X) (susp Y) := + definition susp_functor_pconst [constructor] (X Y : Type*) : + susp_functor (pconst X Y) ~* pconst (susp X) (susp Y) := begin fapply phomotopy.mk, { exact susp_functor_pconst_homotopy }, @@ -422,7 +428,7 @@ namespace susp definition loop_susp_pintro_natural_left (f : X' →* X) : psquare (loop_susp_pintro X Y) (loop_susp_pintro X' Y) (ppcompose_right (susp_functor f)) (ppcompose_right f) := - !pap1_natural_left ⬝h* ppcompose_right_psquare (loop_susp_unit_natural f)⁻¹* + !pap1_natural_left ⬝h* ppcompose_right_psquare (loop_susp_unit_natural f) definition loop_susp_pintro_natural_right (f : Y →* Y') : psquare (loop_susp_pintro X Y) (loop_susp_pintro X Y') diff --git a/hott/types/pointed.hlean b/hott/types/pointed.hlean index f0b1bab35..74980714e 100644 --- a/hott/types/pointed.hlean +++ b/hott/types/pointed.hlean @@ -309,13 +309,6 @@ namespace pointed : pinverse X p⁻¹ = (pinverse X p)⁻¹ := idp - definition ap1_pcompose_pinverse [constructor] {X Y : Type*} (f : X →* Y) : - Ω→ f ∘* pinverse X ~* pinverse Y ∘* Ω→ f := - phomotopy.mk (ap1_gen_inv f (respect_pt f) (respect_pt f)) - abstract begin - induction Y with Y y₀, induction f with f f₀, esimp at * ⊢, induction f₀, reflexivity - end end - definition is_equiv_pcast [instance] {A B : Type*} (p : A = B) : is_equiv (pcast p) := !is_equiv_cast @@ -580,6 +573,8 @@ namespace pointed definition ap1_phomotopy {f g : A →* B} (p : f ~* g) : Ω→ f ~* Ω→ g := pap Ω→ p + notation `Ω⇒`:(max+5) := ap1_phomotopy + definition ap1_phomotopy_refl {X Y : Type*} (f : X →* Y) : ap1_phomotopy (phomotopy.refl f) = phomotopy.refl (Ω→ f) := !pap_refl @@ -676,11 +671,6 @@ namespace pointed (r : p = q) : ptransport B p ~* ptransport B q := phomotopy.mk (λb, ap (λp, transport B p b) r) begin induction r, apply idp_con end - definition pnatural_square {A B : Type} (X : B → Type*) {f g : A → B} - (h : Πa, X (f a) →* X (g a)) {a a' : A} (p : a = a') : - h a' ∘* ptransport X (ap f p) ~* ptransport X (ap g p) ∘* h a := - by induction p; exact !pcompose_pid ⬝* !pid_pcompose⁻¹* - definition apn_pid [constructor] {A : Type*} (n : ℕ) : apn n (pid A) ~* pid (Ω[n] A) := begin induction n with n IH, @@ -730,12 +720,6 @@ namespace pointed { reflexivity} end - definition pcast_commute [constructor] {A : Type} {B C : A → Type*} (f : Πa, B a →* C a) - {a₁ a₂ : A} (p : a₁ = a₂) : pcast (ap C p) ∘* f a₁ ~* f a₂ ∘* pcast (ap B p) := - phomotopy.mk - begin induction p, reflexivity end - begin induction p, esimp, refine !idp_con ⬝ !idp_con ⬝ !ap_id⁻¹ end - /- pointed equivalences -/ structure pequiv (A B : Type*) := @@ -868,11 +852,6 @@ namespace pointed definition peap {A B : Type*} (F : Type* → Type*) (p : A ≃* B) : F A ≃* F B := pequiv_of_pmap (pcast (ap F (eq_of_pequiv p))) begin cases eq_of_pequiv p, apply is_equiv_id end - -- rename pequiv_of_eq_natural - definition pequiv_of_eq_commute [constructor] {A : Type} {B C : A → Type*} (f : Πa, B a →* C a) - {a₁ a₂ : A} (p : a₁ = a₂) : pequiv_of_eq (ap C p) ∘* f a₁ ~* f a₂ ∘* pequiv_of_eq (ap B p) := - pcast_commute f p - -- definition pequiv.eta_expand [constructor] {A B : Type*} (f : A ≃* B) : A ≃* B := -- pequiv.mk' f (to_pinv f) (pequiv.to_pinv2 f) (pright_inv f) _ @@ -1178,27 +1157,6 @@ namespace pointed ... = Ω[2+n] A : eq_of_pequiv !loopn_add ... = Ω[n+2] A : by rewrite [algebra.add.comm] - definition apn_succ_phomotopy_in (n : ℕ) (f : A →* B) : - loopn_succ_in n B ∘* Ω→[n + 1] f ~* Ω→[n] (Ω→ f) ∘* loopn_succ_in n A := - begin - induction n with n IH, - { reflexivity}, - { exact !ap1_pcompose⁻¹* ⬝* ap1_phomotopy IH ⬝* !ap1_pcompose} - end - - definition loopn_succ_in_natural {A B : Type*} (n : ℕ) (f : A →* B) : - loopn_succ_in n B ∘* Ω→[n+1] f ~* Ω→[n] (Ω→ f) ∘* loopn_succ_in n A := - !apn_succ_phomotopy_in - - definition loopn_succ_in_inv_natural {A B : Type*} (n : ℕ) (f : A →* B) : - Ω→[n + 1] f ∘* (loopn_succ_in n A)⁻¹ᵉ* ~* (loopn_succ_in n B)⁻¹ᵉ* ∘* Ω→[n] (Ω→ f):= - begin - apply pinv_right_phomotopy_of_phomotopy, - refine _ ⬝* !passoc⁻¹*, - apply phomotopy_pinv_left_of_phomotopy, - apply apn_succ_phomotopy_in - end - section psquare /- Squares of pointed maps @@ -1206,7 +1164,7 @@ namespace pointed We treat expressions of the form psquare f g h k :≡ k ∘* f ~* g ∘* h as squares, where f is the top, g is the bottom, h is the left face and k is the right face. - Then the following are operations on squares + These squares are very useful for naturality squares -/ variables {A' A₀₀ A₂₀ A₄₀ A₀₂ A₂₂ A₄₂ A₀₄ A₂₄ A₄₄ : Type*} @@ -1226,6 +1184,9 @@ namespace pointed definition phomotopy_of_psquare (p : psquare f₁₀ f₁₂ f₀₁ f₂₁) : f₂₁ ∘* f₁₀ ~* f₁₂ ∘* f₀₁ := p + definition hsquare_of_psquare (p : psquare f₁₀ f₁₂ f₀₁ f₂₁) : hsquare f₁₀ f₁₂ f₀₁ f₂₁ := + to_homotopy p + definition phdeg_square {f f' : A →* A'} (p : f ~* f') : psquare !pid !pid f f' := !pcompose_pid ⬝* p⁻¹* ⬝* !pid_pcompose⁻¹* definition pvdeg_square {f f' : A →* A'} (p : f ~* f') : psquare f f' !pid !pid := @@ -1233,9 +1194,9 @@ namespace pointed variables (f₁₀ f₁₂ f₀₁ f₂₁) - definition hpconst_square : psquare !pconst !pconst f₀₁ f₂₁ := + definition phconst_square : psquare !pconst !pconst f₀₁ f₂₁ := !pcompose_pconst ⬝* !pconst_pcompose⁻¹* - definition vpconst_square : psquare f₁₀ f₁₂ !pconst !pconst := + definition pvconst_square : psquare f₁₀ f₁₂ !pconst !pconst := !pconst_pcompose ⬝* !pcompose_pconst⁻¹* definition phrefl : psquare !pid !pid f₀₁ f₀₁ := phdeg_square phomotopy.rfl definition pvrefl : psquare f₁₀ f₁₀ !pid !pid := pvdeg_square phomotopy.rfl @@ -1243,6 +1204,9 @@ namespace pointed definition phrfl : psquare !pid !pid f₀₁ f₀₁ := phrefl f₀₁ definition pvrfl : psquare f₁₀ f₁₀ !pid !pid := pvrefl f₁₀ + definition ptranspose (p : psquare f₁₀ f₁₂ f₀₁ f₂₁) : psquare f₀₁ f₂₁ f₁₀ f₁₂ := + p⁻¹* + definition phconcat (p : psquare f₁₀ f₁₂ f₀₁ f₂₁) (q : psquare f₃₀ f₃₂ f₂₁ f₄₁) : psquare (f₃₀ ∘* f₁₀) (f₃₂ ∘* f₁₂) f₀₁ f₄₁ := !passoc⁻¹* ⬝* pwhisker_right f₁₀ q ⬝* !passoc ⬝* pwhisker_left f₃₂ p ⬝* !passoc⁻¹* @@ -1300,4 +1264,40 @@ namespace pointed end psquare + definition pinverse_natural [constructor] {X Y : Type*} (f : X →* Y) : + psquare (pinverse X) (pinverse Y) (Ω→ f) (Ω→ f) := + phomotopy.mk (ap1_gen_inv f (respect_pt f) (respect_pt f)) + abstract begin + induction Y with Y y₀, induction f with f f₀, esimp at * ⊢, induction f₀, reflexivity + end end + + definition pcast_natural [constructor] {A : Type} {B C : A → Type*} (f : Πa, B a →* C a) + {a₁ a₂ : A} (p : a₁ = a₂) : psquare (pcast (ap B p)) (pcast (ap C p)) (f a₁) (f a₂) := + phomotopy.mk + begin induction p, reflexivity end + begin induction p, exact whisker_left idp !ap_id end + + definition pequiv_of_eq_natural [constructor] {A : Type} {B C : A → Type*} (f : Πa, B a →* C a) + {a₁ a₂ : A} (p : a₁ = a₂) : + psquare (pequiv_of_eq (ap B p)) (pequiv_of_eq (ap C p)) (f a₁) (f a₂) := + pcast_natural f p + + definition loopn_succ_in_natural {A B : Type*} (n : ℕ) (f : A →* B) : + psquare (loopn_succ_in n A) (loopn_succ_in n B) (Ω→[n+1] f) (Ω→[n] (Ω→ f)) := + begin + induction n with n IH, + { exact phomotopy.rfl }, + { exact ap1_psquare IH } + end + + definition loopn_succ_in_inv_natural {A B : Type*} (n : ℕ) (f : A →* B) : + psquare (loopn_succ_in n A)⁻¹ᵉ* (loopn_succ_in n B)⁻¹ᵉ* (Ω→[n] (Ω→ f)) (Ω→[n + 1] f) := + (loopn_succ_in_natural n f)⁻¹ʰ* + + definition pnatural_square {A B : Type} (X : B → Type*) {f g : A → B} + (h : Πa, X (f a) →* X (g a)) {a a' : A} (p : a = a') : + psquare (ptransport X (ap f p)) (ptransport X (ap g p)) (h a) (h a') := + by induction p; exact !pcompose_pid ⬝* !pid_pcompose⁻¹* + + end pointed