michael/Spectral
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

Prove the naturality of the smash-pmap adjunction, and hence of the associativity of the smash product

Browse source
This commit is contained in:
Floris van Doorn 2017-03-06 01:01:36 -05:00
parent f013c631d0
commit 47532e4315
11 changed files with 1876 additions and 1325 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
algebra/arrow_group.hlean
View file

@ -1,4 +1,4 @@
import algebra.group_theory ..move_to_lib eq2
import algebra.group_theory ..pointed eq2
open pi pointed algebra group eq equiv is_trunc trunc
namespace group

8
homotopy/EM.hlean
View file

@ -1,6 +1,6 @@
-- Authors: Floris van Doorn
import homotopy.EM ..move_to_lib algebra.category.functor.equivalence ..pointed_pi
import homotopy.EM algebra.category.functor.equivalence ..pointed ..pointed_pi
open eq equiv is_equiv algebra group nat pointed EM.ops is_trunc trunc susp function is_conn
@ -233,7 +233,7 @@ namespace EM
begin
assert p' : ptrunc_functor 0 (Ω→ f) ∘* pequiv_of_isomorphism eX ~*
pequiv_of_isomorphism eY ∘* pmap_of_homomorphism φ, exact phomotopy_of_homotopy p,
exact phcompose p' (ptrunc_pequiv_natural 0 (Ω→ f)),
exact p' ⬝h* (ptrunc_pequiv_natural 0 (Ω→ f)),
end
definition EM1_pequiv_type_natural {X Y : Type*} (f : X →* Y) [H1 : is_conn 0 X] [H2 : is_trunc 1 X]
@ -286,7 +286,7 @@ namespace EM
EMadd1_pequiv'_natural f n
((ptrunc_pequiv 0 (Ω[succ n] X))⁻¹ᵉ* ⬝e* pequiv_of_isomorphism eX)
((ptrunc_pequiv 0 (Ω[succ n] Y))⁻¹ᵉ* ⬝e* pequiv_of_isomorphism eY)
_ _ φ (hhcompose (to_homotopy (phinverse (ptrunc_pequiv_natural 0 (Ω→[succ n] f)))) p)
_ _ φ (hhconcat (to_homotopy (phinverse (ptrunc_pequiv_natural 0 (Ω→[succ n] f)))) p)
definition EMadd1_pequiv_succ_natural {G H : AbGroup} {X Y : Type*} (f : X →* Y) (n : ℕ)
(eX : πag[n+2] X ≃g G) (eY : πag[n+2] Y ≃g H) [is_conn (n.+1) X] [is_trunc (n.+2) X]
@ -383,7 +383,7 @@ namespace EM
begin
cases n with n, { exact _ },
cases Y with Y H1 H2, cases Y with Y y₀,
exact is_trunc_pmap X n -1 (ptrunctype.mk Y _ y₀),
exact is_trunc_pmap_of_is_conn X n -1 (ptrunctype.mk Y _ y₀),
end
open category

30
homotopy/cohomology.hlean
View file

@ -12,30 +12,30 @@ open eq spectrum int trunc pointed EM group algebra circle sphere nat EM.ops equ
function fwedge cofiber bool lift sigma is_equiv choice pushout algebra unit pi
-- TODO: move
structure is_short_exact {A B : Type} {C : Type*} (f : A → B) (g : B → C) :=
structure is_exact {A B : Type} {C : Type*} (f : A → B) (g : B → C) :=
( im_in_ker : Π(a:A), g (f a) = pt)
( ker_in_im : Π(b:B), (g b = pt) → image f b)
definition is_short_exact_g {A B C : Group} (f : A →g B) (g : B →g C) :=
is_short_exact f g
definition is_exact_g {A B C : Group} (f : A →g B) (g : B →g C) :=
is_exact f g
definition is_short_exact_g.mk {A B C : Group} {f : A →g B} {g : B →g C}
(H₁ : Πa, g (f a) = 1) (H₂ : Πb, g b = 1 → image f b) : is_short_exact_g f g :=
is_short_exact.mk H₁ H₂
definition is_exact_g.mk {A B C : Group} {f : A →g B} {g : B →g C}
(H₁ : Πa, g (f a) = 1) (H₂ : Πb, g b = 1 → image f b) : is_exact_g f g :=
is_exact.mk H₁ H₂
definition is_short_exact_trunc_functor {A B : Type} {C : Type*} {f : A → B} {g : B → C}
(H : is_short_exact_t f g) : @is_short_exact _ _ (ptrunc 0 C) (trunc_functor 0 f) (trunc_functor 0 g) :=
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_short_exact_t.im_in_ker H 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_short_exact_t.ker_in_im H b q with a r,
induction is_exact_t.ker_in_im H b q with a r,
exact image.mk (tr a) (ap tr r) }
end
definition is_short_exact_homotopy {A B C : Type*} {f f' : A → B} {g g' : B → C}
(p : f ~ f') (q : g ~ g') (H : is_short_exact f g) : is_short_exact f' g' :=
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,
@ -199,8 +199,8 @@ end
/- exactness -/
definition cohomology_exact {X X' : Type*} (f : X →* X') (Y : spectrum) (n : ℤ) :
is_short_exact_g (cohomology_functor (pcod f) Y n) (cohomology_functor f Y n) :=
is_short_exact_trunc_functor (cofiber_exact f)
is_exact_g (cohomology_functor (pcod f) Y n) (cohomology_functor f Y n) :=
is_exact_trunc_functor (cofiber_exact f)
/- additivity -/
@ -253,7 +253,7 @@ structure cohomology_theory.{u} : Type.{u+1} :=
(Hsusp : Π(n : ℤ) (X : Type*), HH (succ n) (psusp X) ≃g HH n X)
(Hsusp_natural : Π(n : ℤ) {X Y : Type*} (f : X →* Y),
Hsusp n X ∘ Hh (succ n) (psusp_functor f) ~ Hh n f ∘ Hsusp n Y)
(Hexact : Π(n : ℤ) {X Y : Type*} (f : X →* Y), is_short_exact_g (Hh n (pcod f)) (Hh n f))
(Hexact : Π(n : ℤ) {X Y : Type*} (f : X →* Y), is_exact_g (Hh n (pcod f)) (Hh n f))
(Hadditive : Π(n : ℤ) {I : Type.{u}} (X : I → Type*), has_choice 0 I →
is_equiv (Group_pi_intro (λi, Hh n (pinl i)) : HH n (⋁ X) → Πᵍ i, HH n (X i)))

4
homotopy/pushout.hlean
View file

@ -464,7 +464,7 @@ namespace pushout
/- universal property of cofiber -/
structure is_short_exact_t {A B : Type} {C : Type*} (f : A → B) (g : B → C) :=
structure is_exact_t {A B : Type} {C : Type*} (f : A → B) (g : B → C) :=
( im_in_ker : Π(a:A), g (f a) = pt)
( ker_in_im : Π(b:B), (g b = pt) → fiber f b)
@ -491,7 +491,7 @@ namespace pushout
end
definition cofiber_exact {X Y Z : Type*} (f : X →* Y) :
is_short_exact_t (@ppcompose_right _ _ Z (pcod f)) (ppcompose_right f) :=
is_exact_t (@ppcompose_right _ _ Z (pcod f)) (ppcompose_right f) :=
begin
constructor,
{ intro g, apply eq_of_phomotopy, apply cofiber_exact_1 },

1371
homotopy/smash.hlean
View file

File diff suppressed because it is too large Load diff

226
homotopy/smash_adjoint.hlean
View file

@ -1,7 +1,7 @@
-- Authors: Floris van Doorn
-- in collaboration with Egbert, Stefano, Robin, Ulrik
/- the adjunction between the smash product and pointed maps -/
import .smash
open bool pointed eq equiv is_equiv sum bool prod unit circle cofiber prod.ops wedge is_trunc
@ -10,8 +10,9 @@ open bool pointed eq equiv is_equiv sum bool prod unit circle cofiber prod.ops w
namespace smash
variables {A B C : Type*}
variables {A A' B B' C C' X X' : Type*}
/- we start by defining the unit of the adjunction -/
definition pinl [constructor] (A : Type*) {B : Type*} (b : B) : A →* A ∧ B :=
begin
fapply pmap.mk,
@ -19,20 +20,13 @@ namespace smash
{ exact gluer' b pt }
end
definition pinl_phomotopy {A B : Type*} {b b' : B} (p : b = b') : pinl A b ~* pinl A b' :=
definition pinl_phomotopy {b b' : B} (p : b = b') : pinl A b ~* pinl A b' :=
begin
fapply phomotopy.mk,
{ exact ap010 (pmap.to_fun ∘ pinl A) p },
{ induction p, apply idp_con }
end
definition pinr [constructor] {A : Type*} (B : Type*) (a : A) : B →* A ∧ B :=
begin
fapply pmap.mk,
{ intro b, exact smash.mk a b },
{ exact gluel' a pt }
end
definition smash_pmap_unit_pt [constructor] (A B : Type*)
: pinl A pt ~* pconst A (A ∧ B) :=
begin
@ -41,6 +35,7 @@ namespace smash
{ rexact con.right_inv (gluel pt) ⬝ (con.right_inv (gluer pt))⁻¹ }
end
/- We chose an unfortunate order of arguments, but it might be bothersome to change it-/
definition smash_pmap_unit [constructor] (A B : Type*) : B →* ppmap A (A ∧ B) :=
begin
fapply pmap.mk,
@ -48,6 +43,7 @@ namespace smash
{ apply eq_of_phomotopy, exact smash_pmap_unit_pt A B }
end
/- The unit is natural in the second argument -/
definition smash_functor_pid_pinl' [constructor] {A B C : Type*} (b : B) (f : B →* C) :
pinl A (f b) ~* smash_functor (pid A) f ∘* pinl A b :=
begin
@ -87,7 +83,7 @@ namespace smash
rexact functor_gluer'2_same (pmap_of_map id (Point A)) (pmap_of_map f pt) pt }
end
definition smash_pmap_unit_natural {A B C : Type*} (f : B →* C) :
definition smash_pmap_unit_natural (f : B →* C) :
smash_pmap_unit A C ∘* f ~*
ppcompose_left (smash_functor (pid A) f) ∘* smash_pmap_unit A B :=
begin
@ -98,16 +94,16 @@ namespace smash
⬝ ap phomotopy_of_eq !respect_pt_pcompose⁻¹,
esimp, refine _ ⬝ ap phomotopy_of_eq !idp_con⁻¹,
refine _ ⬝ !phomotopy_of_eq_of_phomotopy⁻¹,
refine ap (λx, _ ⬝* phomotopy_of_eq (x ⬝ _)) !pcompose_eq_of_phomotopy ⬝ _,
refine ap (λx, _ ⬝* phomotopy_of_eq (x ⬝ _)) !pcompose_left_eq_of_phomotopy ⬝ _,
refine ap (λx, _ ⬝* x) (!phomotopy_of_eq_con ⬝
ap011 phomotopy.trans !phomotopy_of_eq_of_phomotopy
!phomotopy_of_eq_of_phomotopy ⬝ !trans_refl) ⬝ _,
!phomotopy_of_eq_of_phomotopy ◾** !phomotopy_of_eq_of_phomotopy ⬝ !trans_refl) ⬝ _,
refine _ ⬝ smash_pmap_unit_pt_natural (pmap_of_map f b₀) ⬝ _,
{ exact !trans_refl⁻¹ },
{ exact !refl_trans }}
end
definition smash_pmap_counit_map [unfold 3] {A B : Type*} (af : A ∧ (ppmap A B)) : B :=
/- The counit -/
definition smash_pmap_counit_map [unfold 3] (af : A ∧ (ppmap A B)) : B :=
begin
induction af with a f a f,
{ exact f a },
@ -124,8 +120,9 @@ namespace smash
{ reflexivity }
end
definition smash_pmap_counit_natural {A B C : Type*} (g : B →* C) :
g ∘* smash_pmap_counit A B ~* smash_pmap_counit A C ∘* smash_functor (pid A) (ppcompose_left g) :=
/- The counit is natural in both arguments -/
definition smash_pmap_counit_natural (g : B →* C) : g ∘* smash_pmap_counit A B ~*
smash_pmap_counit A C ∘* smash_functor (pid A) (ppcompose_left g) :=
begin
symmetry,
fapply phomotopy.mk,
@ -147,10 +144,34 @@ namespace smash
refine !idp_con ⬝ph _, apply square_of_eq,
refine !idp_con ⬝ !con_inv_cancel_right⁻¹ }},
{ refine !idp_con ⬝ !idp_con ⬝ _, refine _ ⬝ !ap_compose',
refine _ ⬝ !ap_prod_elim⁻¹, esimp,
refine _ ⬝ (ap_is_constant respect_pt _)⁻¹, refine !idp_con⁻¹ }
end
definition smash_pmap_counit_natural_left (g : A →* A') :
smash_pmap_counit A' B ∘* g ∧→ (pid (ppmap A' B)) ~*
smash_pmap_counit A B ∘* (pid A) ∧→ (ppcompose_right g) :=
begin
fapply phomotopy.mk,
{ intro af, induction af with a f a f,
{ reflexivity },
{ reflexivity },
{ reflexivity },
{ apply eq_pathover, apply hdeg_square,
refine ap_compose !smash_pmap_counit _ _ ⬝ ap02 _ (!elim_gluel ⬝ !idp_con) ⬝
!elim_gluel ⬝ _,
refine (ap_compose !smash_pmap_counit _ _ ⬝ ap02 _ !elim_gluel ⬝ !ap_con ⬝
!ap_compose'⁻¹ ◾ !elim_gluel ⬝ !con_idp ⬝ _)⁻¹,
refine !to_fun_eq_of_phomotopy ⬝ _, reflexivity },
{ apply eq_pathover, apply hdeg_square,
refine ap_compose !smash_pmap_counit _ _ ⬝ ap02 _ !elim_gluer ⬝ !ap_con ⬝
!ap_compose'⁻¹ ◾ !elim_gluer ⬝ _,
refine (ap_compose !smash_pmap_counit _ _ ⬝ ap02 _ !elim_gluer ⬝ !ap_con ⬝
!ap_compose'⁻¹ ◾ !elim_gluer ⬝ !idp_con)⁻¹ }},
{ refine !idp_con ⬝ _, refine !ap_compose'⁻¹ ⬝ _ ⬝ !ap_ap011⁻¹, esimp,
refine !to_fun_eq_of_phomotopy ⬝ _, exact !ap_constant⁻¹, }
end
/- The unit-counit laws -/
definition smash_pmap_unit_counit (A B : Type*) :
smash_pmap_counit A (A ∧ B) ∘* smash_functor (pid A) (smash_pmap_unit A B) ~* pid (A ∧ B) :=
begin
@ -170,12 +191,11 @@ namespace smash
refine !ap_con ⬝ !ap_compose'⁻¹ ◾ !elim_gluer ⬝ph _,
refine !idp_con ⬝ph _,
apply square_of_eq, refine !idp_con ⬝ !inv_con_cancel_right⁻¹ }},
{ refine _ ⬝ !ap_compose',
refine _ ⬝ !ap_prod_elim⁻¹, refine _ ⬝ (ap_is_constant respect_pt _)⁻¹,
{ refine _ ⬝ !ap_compose', refine _ ⬝ (ap_is_constant respect_pt _)⁻¹,
rexact (con.right_inv (gluer pt))⁻¹ }
end
definition smash_pmap_counit_unit_pt [constructor] {A B : Type*} (f : A →* B) :
definition smash_pmap_counit_unit_pt [constructor] (f : A →* B) :
smash_pmap_counit A B ∘* pinl A f ~* f :=
begin
fconstructor,
@ -189,10 +209,9 @@ namespace smash
fapply phomotopy_mk_ppmap,
{ intro f, exact smash_pmap_counit_unit_pt f },
{ refine !trans_refl ⬝ _,
refine _ ⬝ ap (λx, phomotopy_of_eq (x ⬝ _)) !pcompose_eq_of_phomotopy⁻¹,
refine _ ⬝ ap (λx, phomotopy_of_eq (x ⬝ _)) !pcompose_left_eq_of_phomotopy⁻¹,
refine _ ⬝ !phomotopy_of_eq_con⁻¹,
refine _ ⬝ ap011 phomotopy.trans !phomotopy_of_eq_of_phomotopy⁻¹
!phomotopy_of_eq_of_phomotopy⁻¹,
refine _ ⬝ !phomotopy_of_eq_of_phomotopy⁻¹ ◾** !phomotopy_of_eq_of_phomotopy⁻¹,
refine _ ⬝ !trans_refl⁻¹,
fapply phomotopy_eq,
{ intro a, refine !elim_gluel'⁻¹ },
@ -204,13 +223,15 @@ namespace smash
exact !idp_con }}
end
definition smash_elim [constructor] {A B C : Type*} (f : A →* ppmap B C) : B ∧ A →* C :=
/- The underlying (unpointed) functions of the equivalence A →* (B →* C) ≃* A ∧ B →* C) -/
definition smash_elim [constructor] (f : A →* ppmap B C) : B ∧ A →* C :=
smash_pmap_counit B C ∘* smash_functor (pid B) f
definition smash_elim_inv [constructor] {A B C : Type*} (g : A ∧ B →* C) : B →* ppmap A C :=
definition smash_elim_inv [constructor] (g : A ∧ B →* C) : B →* ppmap A C :=
ppcompose_left g ∘* smash_pmap_unit A B
definition smash_elim_left_inv {A B C : Type*} (f : A →* ppmap B C) : smash_elim_inv (smash_elim f) ~* f :=
/- They are inverses, constant on the constant function and natural -/
definition smash_elim_left_inv (f : A →* ppmap B C) : smash_elim_inv (smash_elim f) ~* f :=
begin
refine !pwhisker_right !ppcompose_left_pcompose ⬝* _,
refine !passoc ⬝* _,
@ -220,7 +241,7 @@ namespace smash
apply pid_pcompose
end
definition smash_elim_right_inv {A B C : Type*} (g : A ∧ B →* C) : smash_elim (smash_elim_inv g) ~* g :=
definition smash_elim_right_inv (g : A ∧ B →* C) : smash_elim (smash_elim_inv g) ~* g :=
begin
refine !pwhisker_left !smash_functor_pid_pcompose ⬝* _,
refine !passoc⁻¹* ⬝* _,
@ -234,38 +255,6 @@ namespace smash
smash_elim (pconst B (ppmap A C)) ~* pconst (A ∧ B) C :=
begin
refine pwhisker_left _ (smash_functor_pconst_right (pid A)) ⬝* !pcompose_pconst
-- fconstructor,
-- { intro x, induction x with a b a b,
-- { reflexivity },
-- { reflexivity },
-- { reflexivity },
-- { apply eq_pathover_constant_right, apply hdeg_square,
-- refine ap_compose smash_pmap_counit_map _ _ ⬝ ap02 _ !functor_gluel ⬝ !ap_con ⬝
-- !ap_compose'⁻¹ ◾ !elim_gluel},
-- { apply eq_pathover_constant_right, apply hdeg_square,
-- refine ap_compose smash_pmap_counit_map _ _ ⬝ ap02 _ !functor_gluer ⬝ !ap_con ⬝
-- !ap_compose'⁻¹ ◾ !elim_gluer }},
-- { reflexivity }
end
definition pconst_pcompose_pconst (A B C : Type*) :
pconst_pcompose (pconst A B) = pcompose_pconst (pconst B C) :=
idp
definition symm_symm {A B : Type*} {f g : A →* B} (p : f ~* g) : p⁻¹*⁻¹* = p :=
phomotopy_eq (λa, !inv_inv)
begin
induction p using phomotopy_rec_on_idp, induction f with f f₀, induction B with B b₀, esimp at *,
induction f₀, esimp,
end
definition pconst_pcompose_phomotopy_pconst {A B C : Type*} {f : A →* B} (p : f ~* pconst A B) :
pconst_pcompose f = pwhisker_left (pconst B C) p ⬝* pcompose_pconst (pconst B C) :=
begin
assert H : Π(p : pconst A B ~* f),
pconst_pcompose f = pwhisker_left (pconst B C) p⁻¹* ⬝* pcompose_pconst (pconst B C),
{ intro p, induction p using phomotopy_rec_on_idp, reflexivity },
refine H p⁻¹* ⬝ ap (pwhisker_left _) !symm_symm ◾** idp,
end
definition smash_elim_inv_pconst (A B C : Type*) :
@ -274,7 +263,7 @@ namespace smash
fapply phomotopy_mk_ppmap,
{ intro f, apply pconst_pcompose },
{ esimp, refine !trans_refl ⬝ _,
refine _ ⬝ (!phomotopy_of_eq_con ⬝ (ap phomotopy_of_eq !pcompose_eq_of_phomotopy ⬝
refine _ ⬝ (!phomotopy_of_eq_con ⬝ (ap phomotopy_of_eq !pcompose_left_eq_of_phomotopy ⬝
!phomotopy_of_eq_of_phomotopy) ◾** !phomotopy_of_eq_of_phomotopy)⁻¹,
apply pconst_pcompose_phomotopy_pconst }
end
@ -294,18 +283,26 @@ namespace smash
exact !ppcompose_left_pcompose⁻¹*
end
definition smash_elim_phomotopy {A B C : Type*} {f f' : A →* ppmap B C}
definition smash_elim_natural_left (f : A →* A') (g : B →* B')
(h : B' →* ppmap A' C) : smash_elim h ∘* (f ∧→ g) ~* smash_elim (ppcompose_right f ∘* h ∘* g) :=
begin
refine !smash_functor_pid_pcompose ⬝ph* _,
refine _ ⬝v* !smash_pmap_counit_natural_left,
refine smash_functor_psquare (pvrefl f) !pid_pcompose⁻¹*
end
definition smash_elim_phomotopy {f f' : A →* ppmap B C}
(p : f ~* f') : smash_elim f ~* smash_elim f' :=
begin
apply pwhisker_left,
exact smash_functor_phomotopy phomotopy.rfl p
end
definition smash_elim_inv_phomotopy {A B C : Type*} {f f' : A ∧ B →* C}
definition smash_elim_inv_phomotopy {f f' : A ∧ B →* C}
(p : f ~* f') : smash_elim_inv f ~* smash_elim_inv f' :=
pwhisker_right _ (ppcompose_left_phomotopy p)
definition smash_elim_eq_of_phomotopy {A B C : Type*} {f f' : A →* ppmap B C}
definition smash_elim_eq_of_phomotopy {f f' : A →* ppmap B C}
(p : f ~* f') : ap smash_elim (eq_of_phomotopy p) = eq_of_phomotopy (smash_elim_phomotopy p) :=
begin
induction p using phomotopy_rec_on_idp,
@ -316,7 +313,7 @@ namespace smash
refine !pwhisker_left_refl⁻¹
end
definition smash_elim_inv_eq_of_phomotopy {A B C : Type*} {f f' : A ∧ B →* C} (p : f ~* f') :
definition smash_elim_inv_eq_of_phomotopy {f f' : A ∧ B →* C} (p : f ~* f') :
ap smash_elim_inv (eq_of_phomotopy p) = eq_of_phomotopy (smash_elim_inv_phomotopy p) :=
begin
induction p using phomotopy_rec_on_idp,
@ -327,6 +324,7 @@ namespace smash
refine !pwhisker_right_refl⁻¹
end
/- The pointed maps of the equivalence A →* (B →* C) ≃* A ∧ B →* C -/
definition smash_pelim [constructor] (A B C : Type*) : ppmap A (ppmap B C) →* ppmap (B ∧ A) C :=
pmap.mk smash_elim (eq_of_phomotopy !smash_elim_pconst)
@ -334,7 +332,8 @@ namespace smash
ppmap (B ∧ A) C →* ppmap A (ppmap B C) :=
pmap.mk smash_elim_inv (eq_of_phomotopy !smash_elim_inv_pconst)
theorem smash_elim_natural_pconst {A B C C' : Type*} (f : C →* C') :
/- The forward function is natural in all three arguments -/
theorem smash_elim_natural_pconst (f : C →* C') :
smash_elim_natural f (pconst A (ppmap B C)) ⬝*
(smash_elim_phomotopy (pcompose_pconst (ppcompose_left f)) ⬝*
smash_elim_pconst B A C') =
@ -344,31 +343,65 @@ namespace smash
refine idp ◾** (!trans_assoc⁻¹ ⬝ (!pwhisker_left_trans⁻¹ ◾** idp)) ⬝ _,
refine !trans_assoc⁻¹ ⬝ _,
refine (!trans_assoc ⬝ (idp ◾** (!pwhisker_left_trans⁻¹ ⬝
ap (pwhisker_left _) (smash_functor_pconst_right_pid_pcompose' (ppcompose_left f))⁻¹ ⬝
ap (pwhisker_left _) (smash_functor_pid_pcompose_pconst' (ppcompose_left f))⁻¹ ⬝
!pwhisker_left_trans))) ◾** idp ⬝ _,
refine (!trans_assoc⁻¹ ⬝ (!passoc_phomotopy_right⁻¹ʰ** ⬝h**
!pwhisker_right_pwhisker_left ⬝h** !passoc_phomotopy_right) ◾** idp) ◾** idp ⬝ _,
refine !trans_assoc ⬝ !trans_assoc ⬝ idp ◾**_ ⬝ !trans_assoc⁻¹ ⬝ !pwhisker_left_trans⁻¹ ◾** idp,
refine !trans_assoc ⬝ !trans_assoc ⬝ (eq_symm_trans_of_trans_eq _)⁻¹,
refine !pcompose_pconst_pcompose⁻¹ ⬝ _,
refine _ ⬝ idp ◾** (!pcompose_pconst_pcompose),
refine !passoc_pconst_right ⬝ _,
refine _ ⬝ idp ◾** !passoc_pconst_right⁻¹,
refine !pcompose_pconst_phomotopy⁻¹
end
definition smash_pelim_natural {A B C C' : Type*} (f : C →* C') :
definition smash_pelim_natural (f : C →* C') :
ppcompose_left f ∘* smash_pelim A B C ~*
smash_pelim A B C' ∘* ppcompose_left (ppcompose_left f) :=
begin
fapply phomotopy_mk_ppmap,
{ exact smash_elim_natural f },
{ esimp,
refine idp ◾** (!phomotopy_of_eq_con ⬝ (ap phomotopy_of_eq !smash_elim_eq_of_phomotopy ⬝
{ refine idp ◾** (!phomotopy_of_eq_con ⬝ (ap phomotopy_of_eq !smash_elim_eq_of_phomotopy ⬝
!phomotopy_of_eq_of_phomotopy) ◾** !phomotopy_of_eq_of_phomotopy) ⬝ _ ,
refine _ ⬝ (!phomotopy_of_eq_con ⬝ (ap phomotopy_of_eq !pcompose_eq_of_phomotopy ⬝
refine _ ⬝ (!phomotopy_of_eq_con ⬝ (ap phomotopy_of_eq !pcompose_left_eq_of_phomotopy ⬝
!phomotopy_of_eq_of_phomotopy) ◾** !phomotopy_of_eq_of_phomotopy)⁻¹,
exact smash_elim_natural_pconst f }
end
definition smash_pelim_natural_left (C : Type*) (f : A →* A') (g : B →* B') :
psquare (smash_pelim A' B' C) (smash_pelim A B C)
(ppcompose_left (ppcompose_right g) ∘* ppcompose_right f) (ppcompose_right (g ∧→ f)) :=
begin
fapply phomotopy_mk_ppmap,
{ intro h, apply smash_elim_natural_left },
{ esimp,
refine idp ◾** (!phomotopy_of_eq_con ⬝ (ap phomotopy_of_eq
(ap02 _ (whisker_right _ !pcompose_left_eq_of_phomotopy ⬝ !eq_of_phomotopy_trans⁻¹) ⬝
!smash_elim_eq_of_phomotopy) ⬝ !phomotopy_of_eq_of_phomotopy) ◾**
!phomotopy_of_eq_of_phomotopy) ⬝ _,
refine _ ⬝ (ap phomotopy_of_eq (!pcompose_right_eq_of_phomotopy ◾ idp ⬝
!eq_of_phomotopy_trans⁻¹) ⬝ !phomotopy_of_eq_of_phomotopy)⁻¹,
refine ((idp ⬝h** ((ap (pwhisker_left _) (!trans_assoc⁻¹ ⬝ !pwhisker_left_trans⁻¹ ◾** idp) ⬝
!pwhisker_left_trans)⁻¹ ⬝ph** (pwhisker_left_phsquare _
(!smash_functor_phomotopy_trans_right ⬝ph**
(!smash_functor_pid_pcompose_phomotopy_right ⬝v**
!smash_functor_pid_pcompose_pconst))⁻¹ʰ** ⬝vp** !pwhisker_left_symm))) ⬝v**
(phwhisker_rt _ idp)) ⬝ _,
refine (idp ⬝h** (!passoc_phomotopy_right ⬝v** idp)) ◾** idp ⬝ _,
refine !trans_assoc ⬝ idp ◾** (!trans_assoc ⬝ !trans_assoc ⬝ idp ◾**
!passoc_pconst_right) ⬝ _,
refine idp ⬝h** (phwhisker_br _ !pwhisker_right_pwhisker_left ⬝vp**
!pcompose_pconst_phomotopy) ⬝ _,
refine (idp ⬝h** (phwhisker_br _ !passoc_phomotopy_right⁻¹ʰ** ⬝vp**
(eq_symm_trans_of_trans_eq !passoc_pconst_right)⁻¹)) ⬝ _,
refine (idp ⬝h** ((idp ◾** !pwhisker_left_trans⁻¹ ⬝
pwhisker_left_phsquare _ !smash_psquare_lemma) ⬝v** idp ⬝hp** !trans_assoc)) ⬝ _,
refine (!passoc_phomotopy_middle ⬝v** idp ⬝v** idp) ⬝ _,
refine !trans_assoc ⬝ !trans_assoc ⬝ idp ◾** !passoc_pconst_middle ⬝ _,
refine !trans_assoc⁻¹ ⬝ _ ◾** idp,
exact !pwhisker_right_trans⁻¹ }
end
/- The equivalence (note: the forward function of smash_adjoint_pmap is smash_pelim_inv) -/
definition smash_adjoint_pmap' [constructor] (A B C : Type*) : B →* ppmap A C ≃ A ∧ B →* C :=
begin
fapply equiv.MK,
@ -386,6 +419,7 @@ namespace smash
ppmap (A ∧ B) C ≃* ppmap B (ppmap A C) :=
(smash_adjoint_pmap_inv A B C)⁻¹ᵉ*
/- The naturality of the equivalence is a direct consequence of the earlier naturalities -/
definition smash_adjoint_pmap_natural_pt {A B C C' : Type*} (f : C →* C') (g : A ∧ B →* C) :
ppcompose_left f ∘* smash_adjoint_pmap A B C g ~* smash_adjoint_pmap A B C' (f ∘* g) :=
begin
@ -412,7 +446,12 @@ namespace smash
smash_adjoint_pmap A B C' ∘* ppcompose_left f :=
(smash_adjoint_pmap_inv_natural f)⁻¹ʰ*
/- associativity of smash -/
definition smash_adjoint_pmap_natural_left (C : Type*) (f : A →* A') (g : B →* B') :
psquare (smash_adjoint_pmap A' B' C) (smash_adjoint_pmap A B C)
(ppcompose_right (f ∧→ g)) (ppcompose_left (ppcompose_right f) ∘* ppcompose_right g) :=
(smash_pelim_natural_left C g f)⁻¹ʰ*
/- Corollary: associativity of smash -/
definition smash_assoc_elim_equiv (A B C X : Type*) :
ppmap (A ∧ (B ∧ C)) X ≃* ppmap ((A ∧ B) ∧ C) X :=
@ -426,6 +465,18 @@ namespace smash
(A ∧ B) ∧ C →* X :=
smash_elim (ppcompose_left (smash_adjoint_pmap A B X)⁻¹ᵉ* (smash_elim_inv (smash_elim_inv f)))
definition smash_assoc_elim_natural (A B C : Type*) (f : X →* X') :
psquare (smash_assoc_elim_equiv A B C X) (smash_assoc_elim_equiv A B C X')
(ppcompose_left f) (ppcompose_left f) :=
!smash_adjoint_pmap_natural ⬝h*
!smash_adjoint_pmap_natural ⬝h*
ppcompose_left_psquare !smash_adjoint_pmap_inv_natural ⬝h*
!smash_adjoint_pmap_inv_natural
/-
We could prove the following two pointed homotopies by applying smash_assoc_elim_natural to g,
but we give a more explicit proof
-/
definition smash_assoc_elim_natural_pt {A B C X X' : Type*} (f : X →* X') (g : A ∧ (B ∧ C) →* X) :
f ∘* smash_assoc_elim_equiv A B C X g ~* smash_assoc_elim_equiv A B C X' (f ∘* g) :=
begin
@ -459,7 +510,6 @@ namespace smash
apply smash_elim_inv_natural
end
-- TODO: maybe do it without pap / phomotopy_of_eq
definition smash_assoc (A B C : Type*) : A ∧ (B ∧ C) ≃* (A ∧ B) ∧ C :=
begin
fapply pequiv.MK2,
@ -473,6 +523,30 @@ namespace smash
apply phomotopy_of_eq, apply to_right_inv !smash_assoc_elim_equiv }
end
print axioms smash_assoc
/- the associativity of smash is natural in all arguments -/
definition smash_assoc_elim_equiv_natural_left (X : Type*)
(f : A →* A') (g : B →* B') (h : C →* C') :
psquare (smash_assoc_elim_equiv A' B' C' X) (smash_assoc_elim_equiv A B C X)
(ppcompose_right (f ∧→ g ∧→ h)) (ppcompose_right ((f ∧→ g) ∧→ h)) :=
begin
refine !smash_adjoint_pmap_natural_left ⬝h* _ ⬝h*
(!ppcompose_left_ppcompose_right ⬝v* ppcompose_left_psquare !smash_pelim_natural_left) ⬝h*
!smash_pelim_natural_left,
refine !ppcompose_left_ppcompose_right⁻¹* ⬝ph* _,
refine _ ⬝hp* pwhisker_right _ (ppcompose_left_phomotopy !ppcompose_left_ppcompose_right⁻¹* ⬝*
!ppcompose_left_pcompose) ⬝* !passoc ⬝* pwhisker_left _ !ppcompose_left_ppcompose_right⁻¹* ⬝*
!passoc⁻¹*,
refine _ ⬝v* !smash_adjoint_pmap_natural_left,
refine !smash_adjoint_pmap_natural
end
definition smash_assoc_natural (f : A →* A') (g : B →* B') (h : C →* C') :
psquare (smash_assoc A B C) (smash_assoc A' B' C') (f ∧→ (g ∧→ h)) ((f ∧→ g) ∧→ h) :=
begin
refine !smash_assoc_elim_inv_natural_pt ⬝* _,
refine pap !smash_assoc_elim_equiv⁻¹ᵉ* (!pcompose_pid ⬝* !pid_pcompose⁻¹*) ⬝* _,
rexact phomotopy_of_eq ((smash_assoc_elim_equiv_natural_left _ f g h)⁻¹ʰ* !pid)⁻¹
end
end smash

2
homotopy/spectrum.hlean
View file

@ -5,7 +5,7 @@ Authors: Michael Shulman, Floris van Doorn
-/
import homotopy.LES_of_homotopy_groups .splice homotopy.susp ..move_to_lib ..colim ..pointed_pi
import homotopy.LES_of_homotopy_groups .splice homotopy.susp ..colim ..pointed
open eq nat int susp pointed pmap sigma is_equiv equiv fiber algebra trunc trunc_index pi group
seq_colim succ_str

123
homotopy/temp2.hlean Normal file
View file

@ -0,0 +1,123 @@
import .smash_adjoint
open bool pointed eq equiv is_equiv sum bool prod unit circle cofiber prod.ops wedge is_trunc
function red_susp unit smash
variables {A A' B B' C C' D E F X X' : Type*}
-- definition concat2o {A B : Type} {f g h : A → B} {a₁ a₂ : A} {p₁ : f a₁ = g a₁} {p₂ : f a₂ = g a₂}
-- {q₁ : g a₁ = h a₁} {q₂ : g a₂ = h a₂} {r : a₁ = a₂} (s₁ : p₁ =[r] p₂) (s₂ : q₁ =[r] q₂) :
-- p₁ ⬝ q₁ =[r] p₂ ⬝ q₂ :=
-- apo011 (λx, concat) s₁ s₂
-- infixl ` ◾o' `:75 := concat2o
-- definition apd_con_fn {A B : Type} {f g h : A → B} {a₁ a₂ : A} (p : f ~ g) (q : g ~ h) (r : a₁ = a₂)
-- : apd (λa, p a ⬝ q a) r = apd p r ◾o' apd q r :=
-- begin
-- induction r, reflexivity
-- end
-- definition ap02o {A : Type} {B C : A → Type} {g h : Πa, B a} (f : Πa, B a → C a) {a₁ a₂ : A} {p₁ : g a₁ = h a₁}
-- {p₂ : g a₂ = h a₂} {q : a₁ = a₂} (r : p₁ =[q] p₂) : ap (f a₁) p₁ =[q] ap (f a₂) p₂ :=
-- apo (λx, ap (f x)) r
-- definition apo_eq_pathover {A A' B B' : Type} {a a' : A} {f g : A → B} {i : A → A'} {f' g' : A' → B'}
-- {p : a = a'} {q : f a = g a} (h : Πa, f a = g a → f' (i a) = g' (i a))
-- {r : f a' = g a'} (s : square q r (ap f p) (ap g p)) :
-- apo h (eq_pathover s) = eq_pathover _ :=
-- sorry
-- definition ap02o_eq_pathover {A A' B B' : Type} {a a' : A} {f g : A → B} {i : A → A'} {f' g' : A' → B'}
-- {p : a = a'} {q : f a = g a} (h : Πa, f a = g a → f' (i a) = g' (i a))
-- {r : f a' = g a'} (s : square q r (ap f p) (ap g p)) :
-- apo h (eq_pathover s) = eq_pathover _ :=
-- sorry
-- definition apd_ap_fn {A : Type} {B C : A → Type} {g h : Πa, B a} (f : Πa, B a → C a) (p : g ~ h)
-- {a₁ a₂ : A} (r : a₁ = a₂) : apd (λa, ap (f a) (p a)) r = ap02o f (apd p r) :=
-- begin
-- induction r; reflexivity
-- end
-- definition apd_ap_fn {A : Type} {B C : A → Type} {g h : Πa, B a} (f : Πa, B a → C a) (p : g ~ h)
-- {a₁ a₂ : A} (r : a₁ = a₂) : apd (λa, ap (f a) (p a)) r = ap02o f (apd p r) :=

603
move_to_lib.hlean
View file

@ -53,13 +53,23 @@ section -- squares
aps f (hrefl p) = hrefl (ap f p) :=
by induction p; reflexivity
definition natural_square_ap_fn {A B C : Type} {a a' : A} {g h : A → B} (f : B → C) (p : g ~ h) (q : a = a') :
natural_square (λa, ap f (p a)) q =
-- should the following two equalities be cubes?
definition natural_square_ap_fn {A B C : Type} {a a' : A} {g h : A → B} (f : B → C) (p : g ~ h)
(q : a = a') : natural_square (λa, ap f (p a)) q =
ap_compose f g q ⬝ph (aps f (natural_square p q) ⬝hp (ap_compose f h q)⁻¹) :=
begin
induction q, exact !aps_vrfl⁻¹
end
definition natural_square_compose {A B C : Type} {a a' : A} {g g' : B → C}
(p : g ~ g') (f : A → B) (q : a = a') : natural_square (λa, p (f a)) q =
ap_compose g f q ⬝ph (natural_square p (ap f q) ⬝hp (ap_compose g' f q)⁻¹) :=
by induction q; reflexivity
definition natural_square_eq2 {A B : Type} {a a' : A} {f f' : A → B} (p : f ~ f') {q q' : a = a'}
(r : q = q') : natural_square p q = ap02 f r ⬝ph (natural_square p q' ⬝hp (ap02 f' r)⁻¹) :=
by induction r; reflexivity
definition natural_square_refl {A B : Type} {a a' : A} (f : A → B) (q : a = a')
: natural_square (homotopy.refl f) q = hrfl :=
by induction q; reflexivity
@ -143,6 +153,21 @@ section -- cubes
end
definition ap_eq_ap010 {A B C : Type} (f : A → B → C) {a a' : A} (p : a = a') (b : B) :
ap (λa, f a b) p = ap010 f p b :=
by reflexivity
definition ap011_idp {A B C : Type} (f : A → B → C) {a a' : A} (p : a = a') (b : B) :
ap011 f p idp = ap010 f p b :=
by reflexivity
definition ap011_flip {A B C : Type} (f : A → B → C) {a a' : A} {b b' : B} (p : a = a') (q : b = b') :
ap011 f p q = ap011 (λb a, f a b) q p :=
by induction q; induction p; reflexivity
theorem apd_constant' {A A' : Type} {B : A' → Type} {a₁ a₂ : A} {a' : A'} (b : B a')
(p : a₁ = a₂) : apd (λx, b) p = pathover_of_eq p idp :=
by induction p; reflexivity
definition apo011 {A : Type} {B C D : A → Type} {a a' : A} {p : a = a'} {b : B a} {b' : B a'}
{c : C a} {c' : C a'} (f : Π⦃a⦄, B a → C a → D a) (q : b =[p] b') (r : c =[p] c') :
@ -261,13 +286,13 @@ end
definition homotopy_of_hsquare (p : hsquare f₁₀ f₁₂ f₀₁ f₂₁) : f₂₁ ∘ f₁₀ ~ f₁₂ ∘ f₀₁ :=
p
definition hhcompose (p : hsquare f₁₀ f₁₂ f₀₁ f₂₁) (q : hsquare f₃₀ f₃₂ f₂₁ f₄₁) :
definition hhconcat (p : hsquare f₁₀ f₁₂ f₀₁ f₂₁) (q : hsquare f₃₀ f₃₂ f₂₁ f₄₁) :
hsquare (f₃₀ ∘ f₁₀) (f₃₂ ∘ f₁₂) f₀₁ f₄₁ :=
hwhisker_right f₁₀ q ⬝hty hwhisker_left f₃₂ p
definition hvcompose (p : hsquare f₁₀ f₁₂ f₀₁ f₂₁) (q : hsquare f₁₂ f₁₄ f₀₃ f₂₃) :
definition hvconcat (p : hsquare f₁₀ f₁₂ f₀₁ f₂₁) (q : hsquare f₁₂ f₁₄ f₀₃ f₂₃) :
hsquare f₁₀ f₁₄ (f₀₃ ∘ f₀₁) (f₂₃ ∘ f₂₁) :=
(hhcompose p⁻¹ʰᵗʸ q⁻¹ʰᵗʸ)⁻¹ʰᵗʸ
(hhconcat p⁻¹ʰᵗʸ q⁻¹ʰᵗʸ)⁻¹ʰᵗʸ
definition hhinverse {f₁₀ : A₀₀ ≃ A₂₀} {f₁₂ : A₀₂ ≃ A₂₂} (p : hsquare f₁₀ f₁₂ f₀₁ f₂₁) :
hsquare f₁₀⁻¹ᵉ f₁₂⁻¹ᵉ f₂₁ f₀₁ :=
@ -277,8 +302,8 @@ end
hsquare f₁₂ f₁₀ f₀₁⁻¹ᵉ f₂₁⁻¹ᵉ :=
(hhinverse p⁻¹ʰᵗʸ)⁻¹ʰᵗʸ
infix ` ⬝htyh `:73 := hhcompose
infix ` ⬝htyv `:73 := hvcompose
infix ` ⬝htyh `:73 := hhconcat
infix ` ⬝htyv `:73 := hvconcat
postfix `⁻¹ʰᵗʸʰ`:(max+1) := hhinverse
postfix `⁻¹ʰᵗʸᵛ`:(max+1) := hvinverse
@ -291,11 +316,19 @@ end
induction p using homotopy.rec_on, induction q, exact H
end
--eq2
--eq2 (duplicate of ap_compose_ap02_constant)
definition ap02_ap_constant {A B C : Type} {a a' : A} (f : B → C) (b : B) (p : a = a') :
square (ap_constant p (f b)) (ap02 f (ap_constant p b)) (ap_compose f (λx, b) p) idp :=
by induction p; exact ids
definition ap_constant_compose {A B C : Type} {a a' : A} (c : C) (f : A → B) (p : a = a') :
square (ap_constant p c) (ap_constant (ap f p) c) (ap_compose (λx, c) f p) idp :=
by induction p; exact ids
definition ap02_constant {A B : Type} {a a' : A} (b : B) {p p' : a = a'}
(q : p = p') : square (ap_constant p b) (ap_constant p' b) (ap02 (λx, b) q) idp :=
by induction q; exact vrfl
end eq open eq
namespace wedge
@ -313,540 +346,6 @@ namespace pi
end
end pi
namespace pointed
-- FALSE
-- definition phomotopy_pconst {A B : Type*} {f : A →* B} (p q : f ~* pconst A B) : p = q :=
-- begin
-- induction f with f f₀,
-- induction p with p p₀, induction q with q q₀,
-- esimp at *, induction q₀,
-- end
definition punit_pmap_phomotopy [constructor] {A : Type*} (f : punit →* A) : f ~* pconst punit A :=
begin
fapply phomotopy.mk,
{ intro u, induction u, exact respect_pt f },
{ reflexivity }
end
definition is_contr_punit_pmap (A : Type*) : is_contr (punit →* A) :=
is_contr.mk (pconst punit A) (λf, eq_of_phomotopy (punit_pmap_phomotopy f)⁻¹*)
definition phomotopy_of_eq_idp {A B : Type*} (f : A →* B) : phomotopy_of_eq idp = phomotopy.refl f :=
idp
definition to_fun_pequiv_trans {X Y Z : Type*} (f : X ≃* Y) (g :Y ≃* Z) : f ⬝e* g ~ g ∘ f :=
λx, idp
definition pr1_phomotopy_eq {A B : Type*} {f g : A →* B} {p q : f ~* g} (r : p = q) (a : A) :
p a = q a :=
ap010 to_homotopy r a
-- replace pcompose2 with this
definition pcompose2' {A B C : Type*} {g g' : B →* C} {f f' : A →* B} (q : g ~* g') (p : f ~* f') :
g ∘* f ~* g' ∘* f' :=
pwhisker_right f q ⬝* pwhisker_left g' p
infixr ` ◾*' `:80 := pcompose2'
definition phomotopy_of_homotopy {X Y : Type*} {f g : X →* Y} (h : f ~ g) [is_set Y] : f ~* g :=
begin
fapply phomotopy.mk,
{ exact h },
{ apply is_set.elim }
end
definition ap1_gen_con_left {A B : Type} {a a' : A} {b₀ b₁ b₂ : B}
{f : A → b₀ = b₁} {f' : A → b₁ = b₂} (p : a = a') {q₀ q₁ : b₀ = b₁} {q₀' q₁' : b₁ = b₂}
(r₀ : f a = q₀) (r₁ : f a' = q₁) (r₀' : f' a = q₀') (r₁' : f' a' = q₁') :
ap1_gen (λa, f a ⬝ f' a) p (r₀ ◾ r₀') (r₁ ◾ r₁') =
whisker_right q₀' (ap1_gen f p r₀ r₁) ⬝ whisker_left q₁ (ap1_gen f' p r₀' r₁') :=
begin induction r₀, induction r₁, induction r₀', induction r₁', induction p, reflexivity end
definition ap1_gen_con_left_idp {A B : Type} {a : A} {b₀ b₁ b₂ : B}
{f : A → b₀ = b₁} {f' : A → b₁ = b₂} {q₀ : b₀ = b₁} {q₁ : b₁ = b₂}
(r₀ : f a = q₀) (r₁ : f' a = q₁) :
ap1_gen_con_left idp r₀ r₀ r₁ r₁ =
!con.left_inv ⬝ (ap (whisker_right q₁) !con.left_inv ◾ ap (whisker_left _) !con.left_inv)⁻¹ :=
begin induction r₀, induction r₁, reflexivity end
-- /- the pointed type of (unpointed) dependent maps -/
-- definition pupi [constructor] {A : Type} (P : A → Type*) : Type* :=
-- pointed.mk' (Πa, P a)
-- definition loop_pupi_commute {A : Type} (B : A → Type*) : Ω(pupi B) ≃* pupi (λa, Ω (B a)) :=
-- pequiv_of_equiv eq_equiv_homotopy rfl
-- definition equiv_pupi_right {A : Type} {P Q : A → Type*} (g : Πa, P a ≃* Q a)
-- : pupi P ≃* pupi Q :=
-- pequiv_of_equiv (pi_equiv_pi_right g)
-- begin esimp, apply eq_of_homotopy, intros a, esimp, exact (respect_pt (g a)) end
section psquare
/-
Squares of pointed maps
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
-/
variables {A₀₀ A₂₀ A₄₀ A₀₂ A₂₂ A₄₂ A₀₄ A₂₄ A₄₄ : Type*}
{f₁₀ : A₀₀ →* A₂₀} {f₃₀ : A₂₀ →* A₄₀}
{f₀₁ : A₀₀ →* A₀₂} {f₂₁ : A₂₀ →* A₂₂} {f₄₁ : A₄₀ →* A₄₂}
{f₁₂ : A₀₂ →* A₂₂} {f₃₂ : A₂₂ →* A₄₂}
{f₀₃ : A₀₂ →* A₀₄} {f₂₃ : A₂₂ →* A₂₄} {f₄₃ : A₄₂ →* A₄₄}
{f₁₄ : A₀₄ →* A₂₄} {f₃₄ : A₂₄ →* A₄₄}
definition psquare [reducible] (f₁₀ : A₀₀ →* A₂₀) (f₁₂ : A₀₂ →* A₂₂)
(f₀₁ : A₀₀ →* A₀₂) (f₂₁ : A₂₀ →* A₂₂) : Type :=
f₂₁ ∘* f₁₀ ~* f₁₂ ∘* f₀₁
definition psquare_of_phomotopy (p : f₂₁ ∘* f₁₀ ~* f₁₂ ∘* f₀₁) : psquare f₁₀ f₁₂ f₀₁ f₂₁ :=
p
definition phomotopy_of_psquare (p : psquare f₁₀ f₁₂ f₀₁ f₂₁) : f₂₁ ∘* f₁₀ ~* f₁₂ ∘* f₀₁ :=
p
definition phcompose (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⁻¹*
definition pvcompose (p : psquare f₁₀ f₁₂ f₀₁ f₂₁) (q : psquare f₁₂ f₁₄ f₀₃ f₂₃) :
psquare f₁₀ f₁₄ (f₀₃ ∘* f₀₁) (f₂₃ ∘* f₂₁) :=
(phcompose p⁻¹* q⁻¹*)⁻¹*
definition phinverse {f₁₀ : A₀₀ ≃* A₂₀} {f₁₂ : A₀₂ ≃* A₂₂} (p : psquare f₁₀ f₁₂ f₀₁ f₂₁) :
psquare f₁₀⁻¹ᵉ* f₁₂⁻¹ᵉ* f₂₁ f₀₁ :=
!pid_pcompose⁻¹* ⬝* pwhisker_right _ (pleft_inv f₁₂)⁻¹* ⬝* !passoc ⬝*
pwhisker_left _
(!passoc⁻¹* ⬝* pwhisker_right _ p⁻¹* ⬝* !passoc ⬝* pwhisker_left _ !pright_inv ⬝* !pcompose_pid)
definition pvinverse {f₀₁ : A₀₀ ≃* A₀₂} {f₂₁ : A₂₀ ≃* A₂₂} (p : psquare f₁₀ f₁₂ f₀₁ f₂₁) :
psquare f₁₂ f₁₀ f₀₁⁻¹ᵉ* f₂₁⁻¹ᵉ* :=
(phinverse p⁻¹*)⁻¹*
infix ` ⬝h* `:73 := phcompose
infix ` ⬝v* `:73 := pvcompose
postfix `⁻¹ʰ*`:(max+1) := phinverse
postfix `⁻¹ᵛ*`:(max+1) := pvinverse
definition ap1_psquare (p : psquare f₁₀ f₁₂ f₀₁ f₂₁) :
psquare (Ω→ f₁₀) (Ω→ f₁₂) (Ω→ f₀₁) (Ω→ f₂₁) :=
!ap1_pcompose⁻¹* ⬝* ap1_phomotopy p ⬝* !ap1_pcompose
definition apn_psquare (n : ℕ) (p : psquare f₁₀ f₁₂ f₀₁ f₂₁) :
psquare (Ω→[n] f₁₀) (Ω→[n] f₁₂) (Ω→[n] f₀₁) (Ω→[n] f₂₁) :=
!apn_pcompose⁻¹* ⬝* apn_phomotopy n p ⬝* !apn_pcompose
definition ptrunc_functor_psquare (n : ℕ₋₂) (p : psquare f₁₀ f₁₂ f₀₁ f₂₁) :
psquare (ptrunc_functor n f₁₀) (ptrunc_functor n f₁₂)
(ptrunc_functor n f₀₁) (ptrunc_functor n f₂₁) :=
!ptrunc_functor_pcompose⁻¹* ⬝* ptrunc_functor_phomotopy n p ⬝* !ptrunc_functor_pcompose
definition homotopy_group_functor_psquare (n : ℕ) (p : psquare f₁₀ f₁₂ f₀₁ f₂₁) :
psquare (π→[n] f₁₀) (π→[n] f₁₂) (π→[n] f₀₁) (π→[n] f₂₁) :=
!homotopy_group_functor_compose⁻¹* ⬝* homotopy_group_functor_phomotopy n p ⬝*
!homotopy_group_functor_compose
definition homotopy_group_homomorphism_psquare (n : ℕ) [H : is_succ n]
(p : psquare f₁₀ f₁₂ f₀₁ f₂₁) : hsquare (π→g[n] f₁₀) (π→g[n] f₁₂) (π→g[n] f₀₁) (π→g[n] f₂₁) :=
begin
induction H with n, exact to_homotopy (ptrunc_functor_psquare 0 (apn_psquare (succ n) p))
end
end psquare
definition phomotopy_of_eq_of_phomotopy {A B : Type*} {f g : A →* B} (p : f ~* g) :
phomotopy_of_eq (eq_of_phomotopy p) = p :=
to_right_inv (pmap_eq_equiv f g) p
definition ap_eq_of_phomotopy {A B : Type*} {f g : A →* B} (p : f ~* g) (a : A) :
ap (λf : A →* B, f a) (eq_of_phomotopy p) = p a :=
ap010 to_homotopy (phomotopy_of_eq_of_phomotopy p) a
definition phomotopy_rec_on_eq [recursor] {A B : Type*} {f g : A →* B}
{Q : (f ~* g) → Type} (p : f ~* g) (H : Π(q : f = g), Q (phomotopy_of_eq q)) : Q p :=
phomotopy_of_eq_of_phomotopy p ▸ H (eq_of_phomotopy p)
definition phomotopy_rec_on_idp [recursor] {A B : Type*} {f : A →* B}
{Q : Π{g}, (f ~* g) → Type} {g : A →* B} (p : f ~* g) (H : Q (phomotopy.refl f)) : Q p :=
begin
induction p using phomotopy_rec_on_eq,
induction q, exact H
end
definition phomotopy_rec_on_eq_phomotopy_of_eq {A B : Type*} {f g: A →* B}
{Q : (f ~* g) → Type} (p : f = g) (H : Π(q : f = g), Q (phomotopy_of_eq q)) :
phomotopy_rec_on_eq (phomotopy_of_eq p) H = H p :=
begin
unfold phomotopy_rec_on_eq,
refine ap (λp, p ▸ _) !adj ⬝ _,
refine !tr_compose⁻¹ ⬝ _,
apply apdt
end
definition phomotopy_rec_on_idp_refl {A B : Type*} (f : A →* B)
{Q : Π{g}, (f ~* g) → Type} (H : Q (phomotopy.refl f)) :
phomotopy_rec_on_idp phomotopy.rfl H = H :=
!phomotopy_rec_on_eq_phomotopy_of_eq
definition phomotopy_eq_equiv {A B : Type*} {f g : A →* B} (h k : f ~* g) :
(h = k) ≃ Σ(p : to_homotopy h ~ to_homotopy k),
whisker_right (respect_pt g) (p pt) ⬝ to_homotopy_pt k = to_homotopy_pt h :=
calc
h = k ≃ phomotopy.sigma_char _ _ h = phomotopy.sigma_char _ _ k
: eq_equiv_fn_eq (phomotopy.sigma_char f g) h k
... ≃ Σ(p : to_homotopy h = to_homotopy k),
pathover (λp, p pt ⬝ respect_pt g = respect_pt f) (to_homotopy_pt h) p (to_homotopy_pt k)
: sigma_eq_equiv _ _
... ≃ Σ(p : to_homotopy h = to_homotopy k),
to_homotopy_pt h = ap (λq, q pt ⬝ respect_pt g) p ⬝ to_homotopy_pt k
: sigma_equiv_sigma_right (λp, eq_pathover_equiv_Fl p (to_homotopy_pt h) (to_homotopy_pt k))
... ≃ Σ(p : to_homotopy h = to_homotopy k),
ap (λq, q pt ⬝ respect_pt g) p ⬝ to_homotopy_pt k = to_homotopy_pt h
: sigma_equiv_sigma_right (λp, eq_equiv_eq_symm _ _)
... ≃ Σ(p : to_homotopy h = to_homotopy k),
whisker_right (respect_pt g) (apd10 p pt) ⬝ to_homotopy_pt k = to_homotopy_pt h
: sigma_equiv_sigma_right (λp, equiv_eq_closed_left _ (whisker_right _ !whisker_right_ap⁻¹))
... ≃ Σ(p : to_homotopy h ~ to_homotopy k),
whisker_right (respect_pt g) (p pt) ⬝ to_homotopy_pt k = to_homotopy_pt h
: sigma_equiv_sigma_left' eq_equiv_homotopy
definition phomotopy_eq {A B : Type*} {f g : A →* B} {h k : f ~* g} (p : to_homotopy h ~ to_homotopy k)
(q : whisker_right (respect_pt g) (p pt) ⬝ to_homotopy_pt k = to_homotopy_pt h) : h = k :=
to_inv (phomotopy_eq_equiv h k) ⟨p, q⟩
definition phomotopy_eq' {A B : Type*} {f g : A →* B} {h k : f ~* g} (p : to_homotopy h ~ to_homotopy k)
(q : square (to_homotopy_pt h) (to_homotopy_pt k) (whisker_right (respect_pt g) (p pt)) idp) : h = k :=
phomotopy_eq p (eq_of_square q)⁻¹
definition eq_of_phomotopy_refl {X Y : Type*} (f : X →* Y) :
eq_of_phomotopy (phomotopy.refl f) = idpath f :=
begin
apply to_inv_eq_of_eq, reflexivity
end
definition trans_refl {A B : Type*} {f g : A →* B} (p : f ~* g) : p ⬝* phomotopy.refl g = p :=
begin
induction A with A a₀, induction B with B b₀,
induction f with f f₀, induction g with g g₀, induction p with p p₀,
esimp at *, induction g₀, induction p₀,
reflexivity
end
definition refl_trans {A B : Type*} {f g : A →* B} (p : f ~* g) : phomotopy.refl f ⬝* p = p :=
begin
induction p using phomotopy_rec_on_idp,
induction A with A a₀, induction B with B b₀,
induction f with f f₀, esimp at *, induction f₀,
reflexivity
end
definition trans_assoc {A B : Type*} {f g h i : A →* B} (p : f ~* g) (q : g ~* h)
(r : h ~* i) : p ⬝* q ⬝* r = p ⬝* (q ⬝* r) :=
begin
induction r using phomotopy_rec_on_idp,
induction q using phomotopy_rec_on_idp,
induction p using phomotopy_rec_on_idp,
induction B with B b₀,
induction f with f f₀, esimp at *, induction f₀,
reflexivity
end
definition refl_symm {A B : Type*} (f : A →* B) : phomotopy.rfl⁻¹* = phomotopy.refl f :=
begin
induction B with B b₀,
induction f with f f₀, esimp at *, induction f₀,
reflexivity
end
definition trans_symm {A B : Type*} {f g : A →* B} (p : f ~* g) : p ⬝* p⁻¹* = phomotopy.rfl :=
begin
induction p using phomotopy_rec_on_idp, exact !refl_trans ⬝ !refl_symm
end
definition symm_trans {A B : Type*} {f g : A →* B} (p : f ~* g) : p⁻¹* ⬝* p = phomotopy.rfl :=
begin
induction p using phomotopy_rec_on_idp, exact !trans_refl ⬝ !refl_symm
end
definition trans2 {A B : Type*} {f g h : A →* B} {p p' : f ~* g} {q q' : g ~* h}
(r : p = p') (s : q = q') : p ⬝* q = p' ⬝* q' :=
ap011 phomotopy.trans r s
infixl ` ◾** `:80 := pointed.trans2
definition phwhisker_left {A B : Type*} {f g h : A →* B} (p : f ~* g) {q q' : g ~* h}
(s : q = q') : p ⬝* q = p ⬝* q' :=
idp ◾** s
definition phwhisker_right {A B : Type*} {f g h : A →* B} {p p' : f ~* g} (q : g ~* h)
(r : p = p') : p ⬝* q = p' ⬝* q :=
r ◾** idp
definition pwhisker_left_refl {A B C : Type*} (g : B →* C) (f : A →* B) :
pwhisker_left g (phomotopy.refl f) = phomotopy.refl (g ∘* f) :=
begin
induction A with A a₀, induction B with B b₀, induction C with C c₀,
induction f with f f₀, induction g with g g₀,
esimp at *, induction g₀, induction f₀, reflexivity
end
definition pwhisker_right_refl {A B C : Type*} (f : A →* B) (g : B →* C) :
pwhisker_right f (phomotopy.refl g) = phomotopy.refl (g ∘* f) :=
begin
induction A with A a₀, induction B with B b₀, induction C with C c₀,
induction f with f f₀, induction g with g g₀,
esimp at *, induction g₀, induction f₀, reflexivity
end
definition pwhisker_left_trans {A B C : Type*} (g : B →* C) {f₁ f₂ f₃ : A →* B}
(p : f₁ ~* f₂) (q : f₂ ~* f₃) :
pwhisker_left g (p ⬝* q) = pwhisker_left g p ⬝* pwhisker_left g q :=
begin
induction p using phomotopy_rec_on_idp,
induction q using phomotopy_rec_on_idp,
refine _ ⬝ !pwhisker_left_refl⁻¹ ◾** !pwhisker_left_refl⁻¹,
refine ap (pwhisker_left g) !trans_refl ⬝ !pwhisker_left_refl ⬝ !trans_refl⁻¹
end
definition pwhisker_right_trans {A B C : Type*} (f : A →* B) {g₁ g₂ g₃ : B →* C}
(p : g₁ ~* g₂) (q : g₂ ~* g₃) :
pwhisker_right f (p ⬝* q) = pwhisker_right f p ⬝* pwhisker_right f q :=
begin
induction p using phomotopy_rec_on_idp,
induction q using phomotopy_rec_on_idp,
refine _ ⬝ !pwhisker_right_refl⁻¹ ◾** !pwhisker_right_refl⁻¹,
refine ap (pwhisker_right f) !trans_refl ⬝ !pwhisker_right_refl ⬝ !trans_refl⁻¹
end
definition trans_eq_of_eq_symm_trans {A B : Type*} {f g h : A →* B} {p : f ~* g} {q : g ~* h}
{r : f ~* h} (s : q = p⁻¹* ⬝* r) : p ⬝* q = r :=
idp ◾** s ⬝ !trans_assoc⁻¹ ⬝ trans_symm p ◾** idp ⬝ !refl_trans
definition eq_symm_trans_of_trans_eq {A B : Type*} {f g h : A →* B} {p : f ~* g} {q : g ~* h}
{r : f ~* h} (s : p ⬝* q = r) : q = p⁻¹* ⬝* r :=
!refl_trans⁻¹ ⬝ !symm_trans⁻¹ ◾** idp ⬝ !trans_assoc ⬝ idp ◾** s
definition trans_eq_of_eq_trans_symm {A B : Type*} {f g h : A →* B} {p : f ~* g} {q : g ~* h}
{r : f ~* h} (s : p = r ⬝* q⁻¹*) : p ⬝* q = r :=
s ◾** idp ⬝ !trans_assoc ⬝ idp ◾** symm_trans q ⬝ !trans_refl
definition eq_trans_symm_of_trans_eq {A B : Type*} {f g h : A →* B} {p : f ~* g} {q : g ~* h}
{r : f ~* h} (s : p ⬝* q = r) : p = r ⬝* q⁻¹* :=
!trans_refl⁻¹ ⬝ idp ◾** !trans_symm⁻¹ ⬝ !trans_assoc⁻¹ ⬝ s ◾** idp
section phsquare
/-
Squares of pointed homotopies
-/
variables {A B : Type*} {f₀₀ f₂₀ f₄₀ f₀₂ f₂₂ f₄₂ f₀₄ f₂₄ f₄₄ : A →* B}
{p₁₀ : f₀₀ ~* f₂₀} {p₃₀ : f₂₀ ~* f₄₀}
{p₀₁ : f₀₀ ~* f₀₂} {p₂₁ : f₂₀ ~* f₂₂} {p₄₁ : f₄₀ ~* f₄₂}
{p₁₂ : f₀₂ ~* f₂₂} {p₃₂ : f₂₂ ~* f₄₂}
{p₀₃ : f₀₂ ~* f₀₄} {p₂₃ : f₂₂ ~* f₂₄} {p₄₃ : f₄₂ ~* f₄₄}
{p₁₄ : f₀₄ ~* f₂₄} {p₃₄ : f₂₄ ~* f₄₄}
definition phsquare [reducible] (p₁₀ : f₀₀ ~* f₂₀) (p₁₂ : f₀₂ ~* f₂₂)
(p₀₁ : f₀₀ ~* f₀₂) (p₂₁ : f₂₀ ~* f₂₂) : Type :=
p₁₀ ⬝* p₂₁ = p₀₁ ⬝* p₁₂
definition phsquare_of_eq (p : p₁₀ ⬝* p₂₁ = p₀₁ ⬝* p₁₂) : phsquare p₁₀ p₁₂ p₀₁ p₂₁ := p
definition eq_of_phsquare (p : phsquare p₁₀ p₁₂ p₀₁ p₂₁) : p₁₀ ⬝* p₂₁ = p₀₁ ⬝* p₁₂ := p
definition phhcompose (p : phsquare p₁₀ p₁₂ p₀₁ p₂₁) (q : phsquare p₃₀ p₃₂ p₂₁ p₄₁) :
phsquare (p₁₀ ⬝* p₃₀) (p₁₂ ⬝* p₃₂) p₀₁ p₄₁ :=
!trans_assoc ⬝ idp ◾** q ⬝ !trans_assoc⁻¹ ⬝ p ◾** idp ⬝ !trans_assoc
definition phvcompose (p : phsquare p₁₀ p₁₂ p₀₁ p₂₁) (q : phsquare p₁₂ p₁₄ p₀₃ p₂₃) :
phsquare p₁₀ p₁₄ (p₀₁ ⬝* p₀₃) (p₂₁ ⬝* p₂₃) :=
(phhcompose p⁻¹ q⁻¹)⁻¹
/-
The names are very baroque. The following stands for
"pointed homotopy path-horizontal composition" (i.e. composition on the left with a path)
The names are obtained by using the ones for squares, and putting "ph" in front of it.
In practice, use the notation ⬝ph** defined below, which might be easier to remember
-/
definition phphcompose {p₀₁'} (p : p₀₁' = p₀₁) (q : phsquare p₁₀ p₁₂ p₀₁ p₂₁) :
phsquare p₁₀ p₁₂ p₀₁' p₂₁ :=
by induction p; exact q
definition phhpcompose {p₂₁'} (q : phsquare p₁₀ p₁₂ p₀₁ p₂₁) (p : p₂₁ = p₂₁') :
phsquare p₁₀ p₁₂ p₀₁ p₂₁' :=
by induction p; exact q
definition phpvcompose {p₁₀'} (p : p₁₀' = p₁₀) (q : phsquare p₁₀ p₁₂ p₀₁ p₂₁) :
phsquare p₁₀' p₁₂ p₀₁ p₂₁ :=
by induction p; exact q
definition phvpcompose {p₁₂'} (q : phsquare p₁₀ p₁₂ p₀₁ p₂₁) (p : p₁₂ = p₁₂') :
phsquare p₁₀ p₁₂' p₀₁ p₂₁ :=
by induction p; exact q
definition phhinverse (p : phsquare p₁₀ p₁₂ p₀₁ p₂₁) : phsquare p₁₀⁻¹* p₁₂⁻¹* p₂₁ p₀₁ :=
begin
refine (eq_symm_trans_of_trans_eq _)⁻¹,
refine !trans_assoc⁻¹ ⬝ _,
refine (eq_trans_symm_of_trans_eq _)⁻¹,
exact (eq_of_phsquare p)⁻¹
end
definition phvinverse (p : phsquare p₁₀ p₁₂ p₀₁ p₂₁) : phsquare p₁₂ p₁₀ p₀₁⁻¹* p₂₁⁻¹* :=
(phhinverse p⁻¹)⁻¹
infix ` ⬝h** `:71 := phhcompose
infix ` ⬝v** `:72 := phvcompose
infix ` ⬝ph** `:73 := phphcompose
infix ` ⬝hp** `:73 := phhpcompose
infix ` ⬝pv** `:73 := phpvcompose
infix ` ⬝vp** `:73 := phvpcompose
postfix `⁻¹ʰ**`:(max+1) := phhinverse
postfix `⁻¹ᵛ**`:(max+1) := phvinverse
definition passoc_phomotopy_right {A B C D : Type*} (h : C →* D) (g : B →* C) {f f' : A →* B}
(p : f ~* f') : phsquare (passoc h g f) (passoc h g f')
(pwhisker_left (h ∘* g) p) (pwhisker_left h (pwhisker_left g p)) :=
begin
induction p using phomotopy_rec_on_idp,
refine idp ◾** (ap (pwhisker_left h) !pwhisker_left_refl ⬝ !pwhisker_left_refl) ⬝ _ ⬝
!pwhisker_left_refl⁻¹ ◾** idp,
exact !trans_refl ⬝ !refl_trans⁻¹
end
definition pwhisker_right_pwhisker_left {A B C : Type*} {g g' : B →* C} {f f' : A →* B}
(p : g ~* g') (q : f ~* f') :
phsquare (pwhisker_right f p) (pwhisker_right f' p) (pwhisker_left g q) (pwhisker_left g' q) :=
begin
induction p using phomotopy_rec_on_idp,
induction q using phomotopy_rec_on_idp,
exact !pwhisker_right_refl ◾** !pwhisker_left_refl ⬝
!pwhisker_left_refl⁻¹ ◾** !pwhisker_right_refl⁻¹
end
end phsquare
definition phomotopy_of_eq_con {A B : Type*} {f g h : A →* B} (p : f = g) (q : g = h) :
phomotopy_of_eq (p ⬝ q) = phomotopy_of_eq p ⬝* phomotopy_of_eq q :=
begin induction q, induction p, exact !trans_refl⁻¹ end
definition pcompose_eq_of_phomotopy {A B C : Type*} (g : B →* C) {f f' : A →* B} (H : f ~* f') :
ap (λf, g ∘* f) (eq_of_phomotopy H) = eq_of_phomotopy (pwhisker_left g H) :=
begin
induction H using phomotopy_rec_on_idp,
refine ap02 _ !eq_of_phomotopy_refl ⬝ !eq_of_phomotopy_refl⁻¹ ⬝ ap eq_of_phomotopy _,
exact !pwhisker_left_refl⁻¹
end
definition respect_pt_pcompose {A B C : Type*} (g : B →* C) (f : A →* B)
: respect_pt (g ∘* f) = ap g (respect_pt f) ⬝ respect_pt g :=
idp
definition phomotopy_mk_ppmap [constructor] {A B C : Type*} {f g : A →* ppmap B C} (p : Πa, f a ~* g a)
(q : p pt ⬝* phomotopy_of_eq (respect_pt g) = phomotopy_of_eq (respect_pt f))
: f ~* g :=
begin
apply phomotopy.mk (λa, eq_of_phomotopy (p a)),
apply eq_of_fn_eq_fn (pmap_eq_equiv _ _), esimp [pmap_eq_equiv],
refine !phomotopy_of_eq_con ⬝ _,
refine !phomotopy_of_eq_of_phomotopy ◾** idp ⬝ q,
end
definition pcompose_pconst_pcompose {A B C D : Type*} (h : C →* D) (g : B →* C) :
pcompose_pconst (h ∘* g) =
passoc h g (pconst A B) ⬝* (pwhisker_left h (pcompose_pconst g) ⬝* pcompose_pconst h) :=
begin
fapply phomotopy_eq,
{ intro a, exact !idp_con⁻¹ },
{ induction h with h h₀, induction g with g g₀, induction D with D d₀, induction C with C c₀,
esimp at *, induction g₀, induction h₀, reflexivity }
end
definition ppcompose_left_pcompose [constructor] {A B C D : Type*} (h : C →* D) (g : B →* C) :
@ppcompose_left A _ _ (h ∘* g) ~* ppcompose_left h ∘* ppcompose_left g :=
begin
fapply phomotopy_mk_ppmap,
{ exact passoc h g },
{ esimp,
refine idp ◾** (!phomotopy_of_eq_con ⬝ ap011 phomotopy.trans
(ap phomotopy_of_eq !pcompose_eq_of_phomotopy ⬝ !phomotopy_of_eq_of_phomotopy)
!phomotopy_of_eq_of_phomotopy) ⬝ _ ⬝ !phomotopy_of_eq_of_phomotopy⁻¹,
exact (pcompose_pconst_pcompose h g)⁻¹ }
end
definition pcompose_pconst_phomotopy {A B C : Type*} {f f' : B →* C} (p : f ~* f') :
pwhisker_right (pconst A B) p ⬝* pcompose_pconst f' = pcompose_pconst f :=
begin
fapply phomotopy_eq,
{ intro a, exact to_homotopy_pt p },
{ induction p using phomotopy_rec_on_idp, induction C with C c₀, induction f with f f₀,
esimp at *, induction f₀, reflexivity }
end
definition ppcompose_left_pconst [constructor] (A B C : Type*) :
@ppcompose_left A _ _ (pconst B C) ~* pconst (ppmap A B) (ppmap A C) :=
begin
fapply phomotopy_mk_ppmap,
{ exact pconst_pcompose },
{ refine idp ◾** !phomotopy_of_eq_idp ⬝ !phomotopy_of_eq_of_phomotopy⁻¹ }
end
definition ppcompose_left_phomotopy [constructor] {A B C : Type*} {g g' : B →* C} (p : g ~* g') :
@ppcompose_left A _ _ g ~* ppcompose_left g' :=
begin
induction p using phomotopy_rec_on_idp,
reflexivity
end
/- a more explicit proof of ppcompose_left_phomotopy, which might be useful if we need to prove properties about it
-/
-- fapply phomotopy_mk_ppmap,
-- { intro f, exact pwhisker_right f p },
-- { refine ap (λx, _ ⬝* x) !phomotopy_of_eq_of_phomotopy ⬝ _ ⬝ !phomotopy_of_eq_of_phomotopy⁻¹,
-- exact pcompose_pconst_phomotopy p }
definition ppcompose_left_phomotopy_refl {A B C : Type*} (g : B →* C) :
ppcompose_left_phomotopy (phomotopy.refl g) = phomotopy.refl (@ppcompose_left A _ _ g) :=
!phomotopy_rec_on_idp_refl
-- definition pmap_eq_equiv {X Y : Type*} (f g : X →* Y) : (f = g) ≃ (f ~* g) :=
-- begin
-- refine eq_equiv_fn_eq_of_equiv (@pmap.sigma_char X Y) f g ⬝e _,
-- refine !sigma_eq_equiv ⬝e _,
-- refine _ ⬝e (phomotopy.sigma_char f g)⁻¹ᵉ,
-- fapply sigma_equiv_sigma,
-- { esimp, apply eq_equiv_homotopy },
-- { induction g with g gp, induction Y with Y y0, esimp, intro p, induction p, esimp at *,
-- refine !pathover_idp ⬝e _, refine _ ⬝e !eq_equiv_eq_symm,
-- apply equiv_eq_closed_right, exact !idp_con⁻¹ }
-- end
definition pmap_eq_idp {X Y : Type*} (f : X →* Y) :
pmap_eq (λx, idpath (f x)) !idp_con⁻¹ = idpath f :=
ap (λx, eq_of_phomotopy (phomotopy.mk _ x)) !inv_inv ⬝ eq_of_phomotopy_refl f
definition pfunext [constructor] (X Y : Type*) : ppmap X (Ω Y) ≃* Ω (ppmap X Y) :=
begin
fapply pequiv_of_equiv,
{ fapply equiv.MK: esimp,
{ intro f, fapply pmap_eq,
{ intro x, exact f x },
{ exact (respect_pt f)⁻¹ }},
{ intro p, fapply pmap.mk,
{ intro x, exact ap010 pmap.to_fun p x },
{ note z := apd respect_pt p,
note z2 := square_of_pathover z,
refine eq_of_hdeg_square z2 ⬝ !ap_constant }},
{ intro p, exact sorry },
{ intro p, exact sorry }},
{ apply pmap_eq_idp}
end
end pointed open pointed
namespace trunc
-- TODO: redefine loopn_ptrunc_pequiv
@ -964,6 +463,17 @@ namespace sigma
end sigma open sigma
namespace pointed
definition phomotopy_of_homotopy {X Y : Type*} {f g : X →* Y} (h : f ~ g) [is_set Y] : f ~* g :=
begin
fapply phomotopy.mk,
{ exact h },
{ apply is_set.elim }
end
end pointed open pointed
namespace group
open is_trunc
@ -1137,6 +647,15 @@ namespace circle
exact to_right_inv !eq_pathover_equiv_square q
end
definition circle_elim_constant [unfold 5] {A : Type} {a : A} {p : a = a} (r : p = idp) (x : S¹) :
circle.elim a p x = a :=
begin
induction x,
{ reflexivity },
{ apply eq_pathover_constant_right, apply hdeg_square, exact !elim_loop ⬝ r }
end
end circle

828
pointed.hlean Normal file
View file

@ -0,0 +1,828 @@
/- equalities between pointed homotopies -/
-- Author: Floris van Doorn
--import .pointed_pi
import .move_to_lib
open pointed eq equiv function is_equiv unit is_trunc trunc nat algebra group sigma
namespace pointed
definition punit_pmap_phomotopy [constructor] {A : Type*} (f : punit →* A) : f ~* pconst punit A :=
begin
fapply phomotopy.mk,
{ intro u, induction u, exact respect_pt f },
{ reflexivity }
end
definition is_contr_punit_pmap (A : Type*) : is_contr (punit →* A) :=
is_contr.mk (pconst punit A) (λf, eq_of_phomotopy (punit_pmap_phomotopy f)⁻¹*)
definition phomotopy_of_eq_idp {A B : Type*} (f : A →* B) : phomotopy_of_eq idp = phomotopy.refl f :=
idp
definition to_fun_pequiv_trans {X Y Z : Type*} (f : X ≃* Y) (g :Y ≃* Z) : f ⬝e* g ~ g ∘ f :=
λx, idp
definition pr1_phomotopy_eq {A B : Type*} {f g : A →* B} {p q : f ~* g} (r : p = q) (a : A) :
p a = q a :=
ap010 to_homotopy r a
definition ap1_gen_con_left {A B : Type} {a a' : A} {b₀ b₁ b₂ : B}
{f : A → b₀ = b₁} {f' : A → b₁ = b₂} (p : a = a') {q₀ q₁ : b₀ = b₁} {q₀' q₁' : b₁ = b₂}
(r₀ : f a = q₀) (r₁ : f a' = q₁) (r₀' : f' a = q₀') (r₁' : f' a' = q₁') :
ap1_gen (λa, f a ⬝ f' a) p (r₀ ◾ r₀') (r₁ ◾ r₁') =
whisker_right q₀' (ap1_gen f p r₀ r₁) ⬝ whisker_left q₁ (ap1_gen f' p r₀' r₁') :=
begin induction r₀, induction r₁, induction r₀', induction r₁', induction p, reflexivity end
definition ap1_gen_con_left_idp {A B : Type} {a : A} {b₀ b₁ b₂ : B}
{f : A → b₀ = b₁} {f' : A → b₁ = b₂} {q₀ : b₀ = b₁} {q₁ : b₁ = b₂}
(r₀ : f a = q₀) (r₁ : f' a = q₁) :
ap1_gen_con_left idp r₀ r₀ r₁ r₁ =
!con.left_inv ⬝ (ap (whisker_right q₁) !con.left_inv ◾ ap (whisker_left _) !con.left_inv)⁻¹ :=
begin induction r₀, induction r₁, reflexivity end
-- /- the pointed type of (unpointed) dependent maps -/
-- definition pupi [constructor] {A : Type} (P : A → Type*) : Type* :=
-- pointed.mk' (Πa, P a)
-- definition loop_pupi_commute {A : Type} (B : A → Type*) : Ω(pupi B) ≃* pupi (λa, Ω (B a)) :=
-- pequiv_of_equiv eq_equiv_homotopy rfl
-- definition equiv_pupi_right {A : Type} {P Q : A → Type*} (g : Πa, P a ≃* Q a)
-- : pupi P ≃* pupi Q :=
-- pequiv_of_equiv (pi_equiv_pi_right g)
-- begin esimp, apply eq_of_homotopy, intros a, esimp, exact (respect_pt (g a)) end
section psquare
/-
Squares of pointed maps
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
-/
variables {A A' A₀₀ A₂₀ A₄₀ A₀₂ A₂₂ A₄₂ A₀₄ A₂₄ A₄₄ : Type*}
{f₁₀ f₁₀' : A₀₀ →* A₂₀} {f₃₀ : A₂₀ →* A₄₀}
{f₀₁ f₀₁' : A₀₀ →* A₀₂} {f₂₁ f₂₁' : A₂₀ →* A₂₂} {f₄₁ : A₄₀ →* A₄₂}
{f₁₂ f₁₂' : A₀₂ →* A₂₂} {f₃₂ : A₂₂ →* A₄₂}
{f₀₃ : A₀₂ →* A₀₄} {f₂₃ : A₂₂ →* A₂₄} {f₄₃ : A₄₂ →* A₄₄}
{f₁₄ : A₀₄ →* A₂₄} {f₃₄ : A₂₄ →* A₄₄}
definition psquare [reducible] (f₁₀ : A₀₀ →* A₂₀) (f₁₂ : A₀₂ →* A₂₂)
(f₀₁ : A₀₀ →* A₀₂) (f₂₁ : A₂₀ →* A₂₂) : Type :=
f₂₁ ∘* f₁₀ ~* f₁₂ ∘* f₀₁
definition psquare_of_phomotopy (p : f₂₁ ∘* f₁₀ ~* f₁₂ ∘* f₀₁) : psquare f₁₀ f₁₂ f₀₁ f₂₁ :=
p
definition phomotopy_of_psquare (p : psquare f₁₀ f₁₂ f₀₁ f₂₁) : f₂₁ ∘* f₁₀ ~* f₁₂ ∘* f₀₁ :=
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 :=
!pid_pcompose ⬝* p ⬝* !pcompose_pid⁻¹*
variables (f₀₁ f₁₀)
definition phrefl : psquare !pid !pid f₀₁ f₀₁ := phdeg_square phomotopy.rfl
definition pvrefl : psquare f₁₀ f₁₀ !pid !pid := pvdeg_square phomotopy.rfl
variables {f₀₁ f₁₀}
definition phrfl : psquare !pid !pid f₀₁ f₀₁ := phrefl f₀₁
definition pvrfl : psquare f₁₀ f₁₀ !pid !pid := pvrefl f₁₀
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⁻¹*
definition pvconcat (p : psquare f₁₀ f₁₂ f₀₁ f₂₁) (q : psquare f₁₂ f₁₄ f₀₃ f₂₃) :
psquare f₁₀ f₁₄ (f₀₃ ∘* f₀₁) (f₂₃ ∘* f₂₁) :=
!passoc ⬝* pwhisker_left _ p ⬝* !passoc⁻¹* ⬝* pwhisker_right _ q ⬝* !passoc
definition phinverse {f₁₀ : A₀₀ ≃* A₂₀} {f₁₂ : A₀₂ ≃* A₂₂} (p : psquare f₁₀ f₁₂ f₀₁ f₂₁) :
psquare f₁₀⁻¹ᵉ* f₁₂⁻¹ᵉ* f₂₁ f₀₁ :=
!pid_pcompose⁻¹* ⬝* pwhisker_right _ (pleft_inv f₁₂)⁻¹* ⬝* !passoc ⬝*
pwhisker_left _
(!passoc⁻¹* ⬝* pwhisker_right _ p⁻¹* ⬝* !passoc ⬝* pwhisker_left _ !pright_inv ⬝* !pcompose_pid)
definition pvinverse {f₀₁ : A₀₀ ≃* A₀₂} {f₂₁ : A₂₀ ≃* A₂₂} (p : psquare f₁₀ f₁₂ f₀₁ f₂₁) :
psquare f₁₂ f₁₀ f₀₁⁻¹ᵉ* f₂₁⁻¹ᵉ* :=
(phinverse p⁻¹*)⁻¹*
definition phomotopy_hconcat (q : f₀₁' ~* f₀₁) (p : psquare f₁₀ f₁₂ f₀₁ f₂₁) :
psquare f₁₀ f₁₂ f₀₁' f₂₁ :=
p ⬝* pwhisker_left f₁₂ q⁻¹*
definition hconcat_phomotopy (p : psquare f₁₀ f₁₂ f₀₁ f₂₁) (q : f₂₁' ~* f₂₁) :
psquare f₁₀ f₁₂ f₀₁ f₂₁' :=
pwhisker_right f₁₀ q ⬝* p
definition phomotopy_vconcat (q : f₁₀' ~* f₁₀) (p : psquare f₁₀ f₁₂ f₀₁ f₂₁) :
psquare f₁₀' f₁₂ f₀₁ f₂₁ :=
pwhisker_left f₂₁ q ⬝* p
definition vconcat_phomotopy (p : psquare f₁₀ f₁₂ f₀₁ f₂₁) (q : f₁₂' ~* f₁₂) :
psquare f₁₀ f₁₂' f₀₁ f₂₁ :=
p ⬝* pwhisker_right f₀₁ q⁻¹*
infix ` ⬝h* `:73 := phconcat
infix ` ⬝v* `:73 := pvconcat
infixl ` ⬝hp* `:72 := hconcat_phomotopy
infixr ` ⬝ph* `:72 := phomotopy_hconcat
infixl ` ⬝vp* `:72 := vconcat_phomotopy
infixr ` ⬝pv* `:72 := phomotopy_vconcat
postfix `⁻¹ʰ*`:(max+1) := phinverse
postfix `⁻¹ᵛ*`:(max+1) := pvinverse
definition ap1_psquare (p : psquare f₁₀ f₁₂ f₀₁ f₂₁) :
psquare (Ω→ f₁₀) (Ω→ f₁₂) (Ω→ f₀₁) (Ω→ f₂₁) :=
!ap1_pcompose⁻¹* ⬝* ap1_phomotopy p ⬝* !ap1_pcompose
definition apn_psquare (n : ℕ) (p : psquare f₁₀ f₁₂ f₀₁ f₂₁) :
psquare (Ω→[n] f₁₀) (Ω→[n] f₁₂) (Ω→[n] f₀₁) (Ω→[n] f₂₁) :=
!apn_pcompose⁻¹* ⬝* apn_phomotopy n p ⬝* !apn_pcompose
definition ptrunc_functor_psquare (n : ℕ₋₂) (p : psquare f₁₀ f₁₂ f₀₁ f₂₁) :
psquare (ptrunc_functor n f₁₀) (ptrunc_functor n f₁₂)
(ptrunc_functor n f₀₁) (ptrunc_functor n f₂₁) :=
!ptrunc_functor_pcompose⁻¹* ⬝* ptrunc_functor_phomotopy n p ⬝* !ptrunc_functor_pcompose
definition homotopy_group_functor_psquare (n : ℕ) (p : psquare f₁₀ f₁₂ f₀₁ f₂₁) :
psquare (π→[n] f₁₀) (π→[n] f₁₂) (π→[n] f₀₁) (π→[n] f₂₁) :=
!homotopy_group_functor_compose⁻¹* ⬝* homotopy_group_functor_phomotopy n p ⬝*
!homotopy_group_functor_compose
definition homotopy_group_homomorphism_psquare (n : ℕ) [H : is_succ n]
(p : psquare f₁₀ f₁₂ f₀₁ f₂₁) : hsquare (π→g[n] f₁₀) (π→g[n] f₁₂) (π→g[n] f₀₁) (π→g[n] f₂₁) :=
begin
induction H with n, exact to_homotopy (ptrunc_functor_psquare 0 (apn_psquare (succ n) p))
end
end psquare
definition phomotopy_of_eq_of_phomotopy {A B : Type*} {f g : A →* B} (p : f ~* g) :
phomotopy_of_eq (eq_of_phomotopy p) = p :=
to_right_inv (pmap_eq_equiv f g) p
definition ap_eq_of_phomotopy {A B : Type*} {f g : A →* B} (p : f ~* g) (a : A) :
ap (λf : A →* B, f a) (eq_of_phomotopy p) = p a :=
ap010 to_homotopy (phomotopy_of_eq_of_phomotopy p) a
definition phomotopy_rec_on_eq [recursor] {A B : Type*} {f g : A →* B}
{Q : (f ~* g) → Type} (p : f ~* g) (H : Π(q : f = g), Q (phomotopy_of_eq q)) : Q p :=
phomotopy_of_eq_of_phomotopy p ▸ H (eq_of_phomotopy p)
definition phomotopy_rec_on_idp [recursor] {A B : Type*} {f : A →* B}
{Q : Π{g}, (f ~* g) → Type} {g : A →* B} (p : f ~* g) (H : Q (phomotopy.refl f)) : Q p :=
begin
induction p using phomotopy_rec_on_eq,
induction q, exact H
end
definition phomotopy_rec_on_eq_phomotopy_of_eq {A B : Type*} {f g: A →* B}
{Q : (f ~* g) → Type} (p : f = g) (H : Π(q : f = g), Q (phomotopy_of_eq q)) :
phomotopy_rec_on_eq (phomotopy_of_eq p) H = H p :=
begin
unfold phomotopy_rec_on_eq,
refine ap (λp, p ▸ _) !adj ⬝ _,
refine !tr_compose⁻¹ ⬝ _,
apply apdt
end
definition phomotopy_rec_on_idp_refl {A B : Type*} (f : A →* B)
{Q : Π{g}, (f ~* g) → Type} (H : Q (phomotopy.refl f)) :
phomotopy_rec_on_idp phomotopy.rfl H = H :=
!phomotopy_rec_on_eq_phomotopy_of_eq
definition phomotopy_eq_equiv {A B : Type*} {f g : A →* B} (h k : f ~* g) :
(h = k) ≃ Σ(p : to_homotopy h ~ to_homotopy k),
whisker_right (respect_pt g) (p pt) ⬝ to_homotopy_pt k = to_homotopy_pt h :=
calc
h = k ≃ phomotopy.sigma_char _ _ h = phomotopy.sigma_char _ _ k
: eq_equiv_fn_eq (phomotopy.sigma_char f g) h k
... ≃ Σ(p : to_homotopy h = to_homotopy k),
pathover (λp, p pt ⬝ respect_pt g = respect_pt f) (to_homotopy_pt h) p (to_homotopy_pt k)
: sigma_eq_equiv _ _
... ≃ Σ(p : to_homotopy h = to_homotopy k),
to_homotopy_pt h = ap (λq, q pt ⬝ respect_pt g) p ⬝ to_homotopy_pt k
: sigma_equiv_sigma_right (λp, eq_pathover_equiv_Fl p (to_homotopy_pt h) (to_homotopy_pt k))
... ≃ Σ(p : to_homotopy h = to_homotopy k),
ap (λq, q pt ⬝ respect_pt g) p ⬝ to_homotopy_pt k = to_homotopy_pt h
: sigma_equiv_sigma_right (λp, eq_equiv_eq_symm _ _)
... ≃ Σ(p : to_homotopy h = to_homotopy k),
whisker_right (respect_pt g) (apd10 p pt) ⬝ to_homotopy_pt k = to_homotopy_pt h
: sigma_equiv_sigma_right (λp, equiv_eq_closed_left _ (whisker_right _ !whisker_right_ap⁻¹))
... ≃ Σ(p : to_homotopy h ~ to_homotopy k),
whisker_right (respect_pt g) (p pt) ⬝ to_homotopy_pt k = to_homotopy_pt h
: sigma_equiv_sigma_left' eq_equiv_homotopy
definition phomotopy_eq {A B : Type*} {f g : A →* B} {h k : f ~* g} (p : to_homotopy h ~ to_homotopy k)
(q : whisker_right (respect_pt g) (p pt) ⬝ to_homotopy_pt k = to_homotopy_pt h) : h = k :=
to_inv (phomotopy_eq_equiv h k) ⟨p, q⟩
definition phomotopy_eq' {A B : Type*} {f g : A →* B} {h k : f ~* g} (p : to_homotopy h ~ to_homotopy k)
(q : square (to_homotopy_pt h) (to_homotopy_pt k) (whisker_right (respect_pt g) (p pt)) idp) : h = k :=
phomotopy_eq p (eq_of_square q)⁻¹
definition eq_of_phomotopy_refl {X Y : Type*} (f : X →* Y) :
eq_of_phomotopy (phomotopy.refl f) = idpath f :=
begin
apply to_inv_eq_of_eq, reflexivity
end
definition trans_refl {A B : Type*} {f g : A →* B} (p : f ~* g) : p ⬝* phomotopy.refl g = p :=
begin
induction A with A a₀, induction B with B b₀,
induction f with f f₀, induction g with g g₀, induction p with p p₀,
esimp at *, induction g₀, induction p₀,
reflexivity
end
definition eq_of_phomotopy_trans {X Y : Type*} {f g h : X →* Y} (p : f ~* g) (q : g ~* h) :
eq_of_phomotopy (p ⬝* q) = eq_of_phomotopy p ⬝ eq_of_phomotopy q :=
begin
induction p using phomotopy_rec_on_idp, induction q using phomotopy_rec_on_idp,
exact ap eq_of_phomotopy !trans_refl ⬝ whisker_left _ !eq_of_phomotopy_refl⁻¹
end
definition refl_trans {A B : Type*} {f g : A →* B} (p : f ~* g) : phomotopy.refl f ⬝* p = p :=
begin
induction p using phomotopy_rec_on_idp,
induction A with A a₀, induction B with B b₀,
induction f with f f₀, esimp at *, induction f₀,
reflexivity
end
definition trans_assoc {A B : Type*} {f g h i : A →* B} (p : f ~* g) (q : g ~* h)
(r : h ~* i) : p ⬝* q ⬝* r = p ⬝* (q ⬝* r) :=
begin
induction r using phomotopy_rec_on_idp,
induction q using phomotopy_rec_on_idp,
induction p using phomotopy_rec_on_idp,
induction B with B b₀,
induction f with f f₀, esimp at *, induction f₀,
reflexivity
end
definition refl_symm {A B : Type*} (f : A →* B) : phomotopy.rfl⁻¹* = phomotopy.refl f :=
begin
induction B with B b₀,
induction f with f f₀, esimp at *, induction f₀,
reflexivity
end
definition symm_symm {A B : Type*} {f g : A →* B} (p : f ~* g) : p⁻¹*⁻¹* = p :=
phomotopy_eq (λa, !inv_inv)
begin
induction p using phomotopy_rec_on_idp, induction f with f f₀, induction B with B b₀,
esimp at *, induction f₀, reflexivity
end
definition trans_right_inv {A B : Type*} {f g : A →* B} (p : f ~* g) : p ⬝* p⁻¹* = phomotopy.rfl :=
begin
induction p using phomotopy_rec_on_idp, exact !refl_trans ⬝ !refl_symm
end
definition trans_left_inv {A B : Type*} {f g : A →* B} (p : f ~* g) : p⁻¹* ⬝* p = phomotopy.rfl :=
begin
induction p using phomotopy_rec_on_idp, exact !trans_refl ⬝ !refl_symm
end
definition trans2 {A B : Type*} {f g h : A →* B} {p p' : f ~* g} {q q' : g ~* h}
(r : p = p') (s : q = q') : p ⬝* q = p' ⬝* q' :=
ap011 phomotopy.trans r s
definition pcompose3 {A B C : Type*} {g g' : B →* C} {f f' : A →* B}
{p p' : g ~* g'} {q q' : f ~* f'} (r : p = p') (s : q = q') : p ◾* q = p' ◾* q' :=
ap011 pcompose2 r s
definition symm2 {A B : Type*} {f g : A →* B} {p p' : f ~* g} (r : p = p') : p⁻¹* = p'⁻¹* :=
ap phomotopy.symm r
infixl ` ◾** `:80 := pointed.trans2
infixl ` ◽* `:81 := pointed.pcompose3
postfix `⁻²**`:(max+1) := pointed.symm2
definition trans_symm {A B : Type*} {f g h : A →* B} (p : f ~* g) (q : g ~* h) :
(p ⬝* q)⁻¹* = q⁻¹* ⬝* p⁻¹* :=
begin
induction p using phomotopy_rec_on_idp, induction q using phomotopy_rec_on_idp,
exact !trans_refl⁻²** ⬝ !trans_refl⁻¹ ⬝ idp ◾** !refl_symm⁻¹
end
definition phwhisker_left {A B : Type*} {f g h : A →* B} (p : f ~* g) {q q' : g ~* h}
(s : q = q') : p ⬝* q = p ⬝* q' :=
idp ◾** s
definition phwhisker_right {A B : Type*} {f g h : A →* B} {p p' : f ~* g} (q : g ~* h)
(r : p = p') : p ⬝* q = p' ⬝* q :=
r ◾** idp
definition pwhisker_left_refl {A B C : Type*} (g : B →* C) (f : A →* B) :
pwhisker_left g (phomotopy.refl f) = phomotopy.refl (g ∘* f) :=
begin
induction A with A a₀, induction B with B b₀, induction C with C c₀,
induction f with f f₀, induction g with g g₀,
esimp at *, induction g₀, induction f₀, reflexivity
end
definition pwhisker_right_refl {A B C : Type*} (f : A →* B) (g : B →* C) :
pwhisker_right f (phomotopy.refl g) = phomotopy.refl (g ∘* f) :=
begin
induction A with A a₀, induction B with B b₀, induction C with C c₀,
induction f with f f₀, induction g with g g₀,
esimp at *, induction g₀, induction f₀, reflexivity
end
definition pcompose2_refl {A B C : Type*} (g : B →* C) (f : A →* B) :
phomotopy.refl g ◾* phomotopy.refl f = phomotopy.rfl :=
!pwhisker_right_refl ◾** !pwhisker_left_refl ⬝ !refl_trans
definition pcompose2_refl_left {A B C : Type*} (g : B →* C) {f f' : A →* B} (p : f ~* f') :
phomotopy.rfl ◾* p = pwhisker_left g p :=
!pwhisker_right_refl ◾** idp ⬝ !refl_trans
definition pcompose2_refl_right {A B C : Type*} {g g' : B →* C} (f : A →* B) (p : g ~* g') :
p ◾* phomotopy.rfl = pwhisker_right f p :=
idp ◾** !pwhisker_left_refl ⬝ !trans_refl
definition pwhisker_left_trans {A B C : Type*} (g : B →* C) {f₁ f₂ f₃ : A →* B}
(p : f₁ ~* f₂) (q : f₂ ~* f₃) :
pwhisker_left g (p ⬝* q) = pwhisker_left g p ⬝* pwhisker_left g q :=
begin
induction p using phomotopy_rec_on_idp,
induction q using phomotopy_rec_on_idp,
refine _ ⬝ !pwhisker_left_refl⁻¹ ◾** !pwhisker_left_refl⁻¹,
refine ap (pwhisker_left g) !trans_refl ⬝ !pwhisker_left_refl ⬝ !trans_refl⁻¹
end
definition pwhisker_right_trans {A B C : Type*} (f : A →* B) {g₁ g₂ g₃ : B →* C}
(p : g₁ ~* g₂) (q : g₂ ~* g₃) :
pwhisker_right f (p ⬝* q) = pwhisker_right f p ⬝* pwhisker_right f q :=
begin
induction p using phomotopy_rec_on_idp,
induction q using phomotopy_rec_on_idp,
refine _ ⬝ !pwhisker_right_refl⁻¹ ◾** !pwhisker_right_refl⁻¹,
refine ap (pwhisker_right f) !trans_refl ⬝ !pwhisker_right_refl ⬝ !trans_refl⁻¹
end
definition pwhisker_left_symm {A B C : Type*} (g : B →* C) {f₁ f₂ : A →* B} (p : f₁ ~* f₂) :
pwhisker_left g p⁻¹* = (pwhisker_left g p)⁻¹* :=
begin
induction p using phomotopy_rec_on_idp,
refine _ ⬝ ap phomotopy.symm !pwhisker_left_refl⁻¹,
refine ap (pwhisker_left g) !refl_symm ⬝ !pwhisker_left_refl ⬝ !refl_symm⁻¹
end
definition pwhisker_right_symm {A B C : Type*} (f : A →* B) {g₁ g₂ : B →* C} (p : g₁ ~* g₂) :
pwhisker_right f p⁻¹* = (pwhisker_right f p)⁻¹* :=
begin
induction p using phomotopy_rec_on_idp,
refine _ ⬝ ap phomotopy.symm !pwhisker_right_refl⁻¹,
refine ap (pwhisker_right f) !refl_symm ⬝ !pwhisker_right_refl ⬝ !refl_symm⁻¹
end
definition trans_eq_of_eq_symm_trans {A B : Type*} {f g h : A →* B} {p : f ~* g} {q : g ~* h}
{r : f ~* h} (s : q = p⁻¹* ⬝* r) : p ⬝* q = r :=
idp ◾** s ⬝ !trans_assoc⁻¹ ⬝ trans_right_inv p ◾** idp ⬝ !refl_trans
definition eq_symm_trans_of_trans_eq {A B : Type*} {f g h : A →* B} {p : f ~* g} {q : g ~* h}
{r : f ~* h} (s : p ⬝* q = r) : q = p⁻¹* ⬝* r :=
!refl_trans⁻¹ ⬝ !trans_left_inv⁻¹ ◾** idp ⬝ !trans_assoc ⬝ idp ◾** s
definition trans_eq_of_eq_trans_symm {A B : Type*} {f g h : A →* B} {p : f ~* g} {q : g ~* h}
{r : f ~* h} (s : p = r ⬝* q⁻¹*) : p ⬝* q = r :=
s ◾** idp ⬝ !trans_assoc ⬝ idp ◾** trans_left_inv q ⬝ !trans_refl
definition eq_trans_symm_of_trans_eq {A B : Type*} {f g h : A →* B} {p : f ~* g} {q : g ~* h}
{r : f ~* h} (s : p ⬝* q = r) : p = r ⬝* q⁻¹* :=
!trans_refl⁻¹ ⬝ idp ◾** !trans_right_inv⁻¹ ⬝ !trans_assoc⁻¹ ⬝ s ◾** idp
section phsquare
/-
Squares of pointed homotopies
-/
variables {A B C : Type*} {f f' f₀₀ f₂₀ f₄₀ f₀₂ f₂₂ f₄₂ f₀₄ f₂₄ f₄₄ : A →* B}
{p₁₀ : f₀₀ ~* f₂₀} {p₃₀ : f₂₀ ~* f₄₀}
{p₀₁ : f₀₀ ~* f₀₂} {p₂₁ : f₂₀ ~* f₂₂} {p₄₁ : f₄₀ ~* f₄₂}
{p₁₂ : f₀₂ ~* f₂₂} {p₃₂ : f₂₂ ~* f₄₂}
{p₀₃ : f₀₂ ~* f₀₄} {p₂₃ : f₂₂ ~* f₂₄} {p₄₃ : f₄₂ ~* f₄₄}
{p₁₄ : f₀₄ ~* f₂₄} {p₃₄ : f₂₄ ~* f₄₄}
definition phsquare [reducible] (p₁₀ : f₀₀ ~* f₂₀) (p₁₂ : f₀₂ ~* f₂₂)
(p₀₁ : f₀₀ ~* f₀₂) (p₂₁ : f₂₀ ~* f₂₂) : Type :=
p₁₀ ⬝* p₂₁ = p₀₁ ⬝* p₁₂
definition phsquare_of_eq (p : p₁₀ ⬝* p₂₁ = p₀₁ ⬝* p₁₂) : phsquare p₁₀ p₁₂ p₀₁ p₂₁ := p
definition eq_of_phsquare (p : phsquare p₁₀ p₁₂ p₀₁ p₂₁) : p₁₀ ⬝* p₂₁ = p₀₁ ⬝* p₁₂ := p
definition phhconcat (p : phsquare p₁₀ p₁₂ p₀₁ p₂₁) (q : phsquare p₃₀ p₃₂ p₂₁ p₄₁) :
phsquare (p₁₀ ⬝* p₃₀) (p₁₂ ⬝* p₃₂) p₀₁ p₄₁ :=
!trans_assoc ⬝ idp ◾** q ⬝ !trans_assoc⁻¹ ⬝ p ◾** idp ⬝ !trans_assoc
definition phvconcat (p : phsquare p₁₀ p₁₂ p₀₁ p₂₁) (q : phsquare p₁₂ p₁₄ p₀₃ p₂₃) :
phsquare p₁₀ p₁₄ (p₀₁ ⬝* p₀₃) (p₂₁ ⬝* p₂₃) :=
(phhconcat p⁻¹ q⁻¹)⁻¹
definition phhdeg_square {p₁ p₂ : f ~* f'} (q : p₁ = p₂) : phsquare phomotopy.rfl phomotopy.rfl p₁ p₂ :=
!refl_trans ⬝ q⁻¹ ⬝ !trans_refl⁻¹
definition phvdeg_square {p₁ p₂ : f ~* f'} (q : p₁ = p₂) : phsquare p₁ p₂ phomotopy.rfl phomotopy.rfl :=
!trans_refl ⬝ q ⬝ !refl_trans⁻¹
variables (p₀₁ p₁₀)
definition phhrefl : phsquare phomotopy.rfl phomotopy.rfl p₀₁ p₀₁ := phhdeg_square idp
definition phvrefl : phsquare p₁₀ p₁₀ phomotopy.rfl phomotopy.rfl := phvdeg_square idp
variables {p₀₁ p₁₀}
definition phhrfl : phsquare phomotopy.rfl phomotopy.rfl p₀₁ p₀₁ := phhrefl p₀₁
definition phvrfl : phsquare p₁₀ p₁₀ phomotopy.rfl phomotopy.rfl := phvrefl p₁₀
/-
The names are very baroque. The following stands for
"pointed homotopy path-horizontal composition" (i.e. composition on the left with a path)
The names are obtained by using the ones for squares, and putting "ph" in front of it.
In practice, use the notation ⬝ph** defined below, which might be easier to remember
-/
definition phphconcat {p₀₁'} (p : p₀₁' = p₀₁) (q : phsquare p₁₀ p₁₂ p₀₁ p₂₁) :
phsquare p₁₀ p₁₂ p₀₁' p₂₁ :=
by induction p; exact q
definition phhpconcat {p₂₁'} (q : phsquare p₁₀ p₁₂ p₀₁ p₂₁) (p : p₂₁ = p₂₁') :
phsquare p₁₀ p₁₂ p₀₁ p₂₁' :=
by induction p; exact q
definition phpvconcat {p₁₀'} (p : p₁₀' = p₁₀) (q : phsquare p₁₀ p₁₂ p₀₁ p₂₁) :
phsquare p₁₀' p₁₂ p₀₁ p₂₁ :=
by induction p; exact q
definition phvpconcat {p₁₂'} (q : phsquare p₁₀ p₁₂ p₀₁ p₂₁) (p : p₁₂ = p₁₂') :
phsquare p₁₀ p₁₂' p₀₁ p₂₁ :=
by induction p; exact q
definition phhinverse (p : phsquare p₁₀ p₁₂ p₀₁ p₂₁) : phsquare p₁₀⁻¹* p₁₂⁻¹* p₂₁ p₀₁ :=
begin
refine (eq_symm_trans_of_trans_eq _)⁻¹,
refine !trans_assoc⁻¹ ⬝ _,
refine (eq_trans_symm_of_trans_eq _)⁻¹,
exact (eq_of_phsquare p)⁻¹
end
definition phvinverse (p : phsquare p₁₀ p₁₂ p₀₁ p₂₁) : phsquare p₁₂ p₁₀ p₀₁⁻¹* p₂₁⁻¹* :=
(phhinverse p⁻¹)⁻¹
infix ` ⬝h** `:78 := phhconcat
infix ` ⬝v** `:78 := phvconcat
infixr ` ⬝ph** `:77 := phphconcat
infixl ` ⬝hp** `:77 := phhpconcat
infixr ` ⬝pv** `:77 := phpvconcat
infixl ` ⬝vp** `:77 := phvpconcat
postfix `⁻¹ʰ**`:(max+1) := phhinverse
postfix `⁻¹ᵛ**`:(max+1) := phvinverse
definition phwhisker_rt (p : f ~* f₂₀) (q : phsquare p₁₀ p₁₂ p₀₁ p₂₁) :
phsquare (p₁₀ ⬝* p⁻¹*) p₁₂ p₀₁ (p ⬝* p₂₁) :=
!trans_assoc ⬝ idp ◾** (!trans_assoc⁻¹ ⬝ !trans_left_inv ◾** idp ⬝ !refl_trans) ⬝ q
definition phwhisker_br (p : f₂₂ ~* f) (q : phsquare p₁₀ p₁₂ p₀₁ p₂₁) :
phsquare p₁₀ (p₁₂ ⬝* p) p₀₁ (p₂₁ ⬝* p) :=
!trans_assoc⁻¹ ⬝ q ◾** idp ⬝ !trans_assoc
definition phmove_top_of_left' {p₀₁ : f ~* f₀₂} (p : f₀₀ ~* f)
(q : phsquare p₁₀ p₁₂ (p ⬝* p₀₁) p₂₁) : phsquare (p⁻¹* ⬝* p₁₀) p₁₂ p₀₁ p₂₁ :=
!trans_assoc ⬝ (eq_symm_trans_of_trans_eq (q ⬝ !trans_assoc)⁻¹)⁻¹
definition passoc_phomotopy_right {A B C D : Type*} (h : C →* D) (g : B →* C) {f f' : A →* B}
(p : f ~* f') : phsquare (passoc h g f) (passoc h g f')
(pwhisker_left (h ∘* g) p) (pwhisker_left h (pwhisker_left g p)) :=
begin
induction p using phomotopy_rec_on_idp,
refine idp ◾** (ap (pwhisker_left h) !pwhisker_left_refl ⬝ !pwhisker_left_refl) ⬝ _ ⬝
!pwhisker_left_refl⁻¹ ◾** idp,
exact !trans_refl ⬝ !refl_trans⁻¹
end
theorem passoc_phomotopy_middle {A B C D : Type*} (h : C →* D) {g g' : B →* C} (f : A →* B)
(p : g ~* g') : phsquare (passoc h g f) (passoc h g' f)
(pwhisker_right f (pwhisker_left h p)) (pwhisker_left h (pwhisker_right f p)) :=
begin
induction p using phomotopy_rec_on_idp,
rewrite [pwhisker_right_refl, pwhisker_left_refl],
rewrite [pwhisker_right_refl, pwhisker_left_refl],
exact phvrfl
end
definition pwhisker_right_pwhisker_left {A B C : Type*} {g g' : B →* C} {f f' : A →* B}
(p : g ~* g') (q : f ~* f') :
phsquare (pwhisker_right f p) (pwhisker_right f' p) (pwhisker_left g q) (pwhisker_left g' q) :=
begin
induction p using phomotopy_rec_on_idp,
induction q using phomotopy_rec_on_idp,
exact !pwhisker_right_refl ◾** !pwhisker_left_refl ⬝
!pwhisker_left_refl⁻¹ ◾** !pwhisker_right_refl⁻¹
end
definition pwhisker_left_phsquare (f : B →* C) (p : phsquare p₁₀ p₁₂ p₀₁ p₂₁) :
phsquare (pwhisker_left f p₁₀) (pwhisker_left f p₁₂)
(pwhisker_left f p₀₁) (pwhisker_left f p₂₁) :=
!pwhisker_left_trans⁻¹ ⬝ ap (pwhisker_left f) p ⬝ !pwhisker_left_trans
definition pwhisker_right_phsquare (f : C →* A) (p : phsquare p₁₀ p₁₂ p₀₁ p₂₁) :
phsquare (pwhisker_right f p₁₀) (pwhisker_right f p₁₂)
(pwhisker_right f p₀₁) (pwhisker_right f p₂₁) :=
!pwhisker_right_trans⁻¹ ⬝ ap (pwhisker_right f) p ⬝ !pwhisker_right_trans
end phsquare
definition phomotopy_of_eq_con {A B : Type*} {f g h : A →* B} (p : f = g) (q : g = h) :
phomotopy_of_eq (p ⬝ q) = phomotopy_of_eq p ⬝* phomotopy_of_eq q :=
begin induction q, induction p, exact !trans_refl⁻¹ end
definition pcompose_left_eq_of_phomotopy {A B C : Type*} (g : B →* C) {f f' : A →* B}
(H : f ~* f') : ap (λf, g ∘* f) (eq_of_phomotopy H) = eq_of_phomotopy (pwhisker_left g H) :=
begin
induction H using phomotopy_rec_on_idp,
refine ap02 _ !eq_of_phomotopy_refl ⬝ !eq_of_phomotopy_refl⁻¹ ⬝ ap eq_of_phomotopy _,
exact !pwhisker_left_refl⁻¹
end
definition pcompose_right_eq_of_phomotopy {A B C : Type*} {g g' : B →* C} (f : A →* B)
(H : g ~* g') : ap (λg, g ∘* f) (eq_of_phomotopy H) = eq_of_phomotopy (pwhisker_right f H) :=
begin
induction H using phomotopy_rec_on_idp,
refine ap02 _ !eq_of_phomotopy_refl ⬝ !eq_of_phomotopy_refl⁻¹ ⬝ ap eq_of_phomotopy _,
exact !pwhisker_right_refl⁻¹
end
definition to_fun_eq_of_phomotopy {A B : Type*} {f g : A →* B} (p : f ~* g) (a : A) :
ap010 pmap.to_fun (eq_of_phomotopy p) a = p a :=
begin
induction p using phomotopy_rec_on_idp,
exact ap (λx, ap010 pmap.to_fun x a) !eq_of_phomotopy_refl
end
definition respect_pt_pcompose {A B C : Type*} (g : B →* C) (f : A →* B)
: respect_pt (g ∘* f) = ap g (respect_pt f) ⬝ respect_pt g :=
idp
definition phomotopy_mk_ppmap [constructor] {A B C : Type*} {f g : A →* ppmap B C} (p : Πa, f a ~* g a)
(q : p pt ⬝* phomotopy_of_eq (respect_pt g) = phomotopy_of_eq (respect_pt f))
: f ~* g :=
begin
apply phomotopy.mk (λa, eq_of_phomotopy (p a)),
apply eq_of_fn_eq_fn (pmap_eq_equiv _ _), esimp [pmap_eq_equiv],
refine !phomotopy_of_eq_con ⬝ _,
refine !phomotopy_of_eq_of_phomotopy ◾** idp ⬝ q,
end
definition pconst_pcompose_pconst (A B C : Type*) :
pconst_pcompose (pconst A B) = pcompose_pconst (pconst B C) :=
idp
definition pconst_pcompose_phomotopy_pconst {A B C : Type*} {f : A →* B} (p : f ~* pconst A B) :
pconst_pcompose f = pwhisker_left (pconst B C) p ⬝* pcompose_pconst (pconst B C) :=
begin
assert H : Π(p : pconst A B ~* f),
pconst_pcompose f = pwhisker_left (pconst B C) p⁻¹* ⬝* pcompose_pconst (pconst B C),
{ intro p, induction p using phomotopy_rec_on_idp, reflexivity },
refine H p⁻¹* ⬝ ap (pwhisker_left _) !symm_symm ◾** idp,
end
definition passoc_pconst_right {A B C D : Type*} (h : C →* D) (g : B →* C) :
passoc h g (pconst A B) ⬝* (pwhisker_left h (pcompose_pconst g) ⬝* pcompose_pconst h) =
pcompose_pconst (h ∘* g) :=
begin
fapply phomotopy_eq,
{ intro a, exact !idp_con },
{ induction h with h h₀, induction g with g g₀, induction D with D d₀, induction C with C c₀,
esimp at *, induction g₀, induction h₀, reflexivity }
end
definition passoc_pconst_middle {A A' B B' : Type*} (g : B →* B') (f : A' →* A) :
passoc g (pconst A B) f ⬝* (pwhisker_left g (pconst_pcompose f) ⬝* pcompose_pconst g) =
pwhisker_right f (pcompose_pconst g) ⬝* pconst_pcompose f :=
begin
fapply phomotopy_eq,
{ intro a, esimp, exact !idp_con ⬝ !idp_con },
{ induction g with g g₀, induction f with f f₀, induction B' with D d₀, induction A with C c₀,
esimp at *, induction g₀, induction f₀, reflexivity }
end
definition ppcompose_left_pcompose [constructor] {A B C D : Type*} (h : C →* D) (g : B →* C) :
@ppcompose_left A _ _ (h ∘* g) ~* ppcompose_left h ∘* ppcompose_left g :=
begin
fapply phomotopy_mk_ppmap,
{ exact passoc h g },
{ esimp,
refine idp ◾** (!phomotopy_of_eq_con ⬝
(ap phomotopy_of_eq !pcompose_left_eq_of_phomotopy ⬝ !phomotopy_of_eq_of_phomotopy) ◾**
!phomotopy_of_eq_of_phomotopy) ⬝ _ ⬝ !phomotopy_of_eq_of_phomotopy⁻¹,
exact passoc_pconst_right h g }
end
definition ppcompose_left_ppcompose_right {A A' B B' : Type*} (g : B →* B') (f : A' →* A) :
psquare (ppcompose_left g) (ppcompose_left g) (ppcompose_right f) (ppcompose_right f) :=
begin
fapply phomotopy_mk_ppmap,
{ intro h, exact passoc g h f },
{ refine idp ◾** (!phomotopy_of_eq_con ⬝
(ap phomotopy_of_eq !pcompose_left_eq_of_phomotopy ⬝ !phomotopy_of_eq_of_phomotopy) ◾**
!phomotopy_of_eq_of_phomotopy) ⬝ _ ⬝ (!phomotopy_of_eq_con ⬝
(ap phomotopy_of_eq !pcompose_right_eq_of_phomotopy ⬝ !phomotopy_of_eq_of_phomotopy) ◾**
!phomotopy_of_eq_of_phomotopy)⁻¹,
apply passoc_pconst_middle }
end
definition pcompose_pconst_phomotopy {A B C : Type*} {f f' : B →* C} (p : f ~* f') :
pwhisker_right (pconst A B) p ⬝* pcompose_pconst f' = pcompose_pconst f :=
begin
fapply phomotopy_eq,
{ intro a, exact to_homotopy_pt p },
{ induction p using phomotopy_rec_on_idp, induction C with C c₀, induction f with f f₀,
esimp at *, induction f₀, reflexivity }
end
definition pid_pconst (A B : Type*) : pcompose_pconst (pid B) = pid_pcompose (pconst A B) :=
by reflexivity
definition pid_pconst_pcompose {A B C : Type*} (f : A →* B) :
phsquare (pid_pcompose (pconst B C ∘* f))
(pcompose_pconst (pid C))
(pwhisker_left (pid C) (pconst_pcompose f))
(pconst_pcompose f) :=
begin
fapply phomotopy_eq,
{ reflexivity },
{ induction f with f f₀, induction B with B b₀, esimp at *, induction f₀, reflexivity }
end
definition ppcompose_left_pconst [constructor] (A B C : Type*) :
@ppcompose_left A _ _ (pconst B C) ~* pconst (ppmap A B) (ppmap A C) :=
begin
fapply phomotopy_mk_ppmap,
{ exact pconst_pcompose },
{ refine idp ◾** !phomotopy_of_eq_idp ⬝ !phomotopy_of_eq_of_phomotopy⁻¹ }
end
definition ppcompose_left_phomotopy [constructor] {A B C : Type*} {g g' : B →* C} (p : g ~* g') :
@ppcompose_left A _ _ g ~* ppcompose_left g' :=
begin
induction p using phomotopy_rec_on_idp,
reflexivity
end
section psquare
variables {A A' A₀₀ A₂₀ A₄₀ A₀₂ A₂₂ A₄₂ A₀₄ A₂₄ A₄₄ : Type*}
{f₁₀ f₁₀' : A₀₀ →* A₂₀} {f₃₀ : A₂₀ →* A₄₀}
{f₀₁ f₀₁' : A₀₀ →* A₀₂} {f₂₁ f₂₁' : A₂₀ →* A₂₂} {f₄₁ : A₄₀ →* A₄₂}
{f₁₂ f₁₂' : A₀₂ →* A₂₂} {f₃₂ : A₂₂ →* A₄₂}
{f₀₃ : A₀₂ →* A₀₄} {f₂₃ : A₂₂ →* A₂₄} {f₄₃ : A₄₂ →* A₄₄}
{f₁₄ : A₀₄ →* A₂₄} {f₃₄ : A₂₄ →* A₄₄}
definition ppcompose_left_psquare {A : Type*} (p : psquare f₁₀ f₁₂ f₀₁ f₂₁) :
psquare (@ppcompose_left A _ _ f₁₀) (ppcompose_left f₁₂)
(ppcompose_left f₀₁) (ppcompose_left f₂₁) :=
!ppcompose_left_pcompose⁻¹* ⬝* ppcompose_left_phomotopy p ⬝* !ppcompose_left_pcompose
definition trans_phomotopy_hconcat {f₀₁' f₀₁''}
(q₂ : f₀₁'' ~* f₀₁') (q₁ : f₀₁' ~* f₀₁) (p : psquare f₁₀ f₁₂ f₀₁ f₂₁) :
(q₂ ⬝* q₁) ⬝ph* p = q₂ ⬝ph* q₁ ⬝ph* p :=
idp ◾** (ap (pwhisker_left f₁₂) !trans_symm ⬝ !pwhisker_left_trans) ⬝ !trans_assoc⁻¹
definition symm_phomotopy_hconcat {f₀₁'} (q : f₀₁ ~* f₀₁')
(p : psquare f₁₀ f₁₂ f₀₁ f₂₁) : q⁻¹* ⬝ph* p = p ⬝* pwhisker_left f₁₂ q :=
idp ◾** ap (pwhisker_left f₁₂) !symm_symm
definition refl_phomotopy_hconcat (p : psquare f₁₀ f₁₂ f₀₁ f₂₁) : phomotopy.rfl ⬝ph* p = p :=
idp ◾** (ap (pwhisker_left _) !refl_symm ⬝ !pwhisker_left_refl) ⬝ !trans_refl
local attribute phomotopy.rfl [reducible]
theorem pwhisker_left_phomotopy_hconcat {f₀₁'} (r : f₀₁' ~* f₀₁)
(p : psquare f₁₀ f₁₂ f₀₁ f₂₁) (q : psquare f₁₂ f₁₄ f₀₃ f₂₃) :
pwhisker_left f₀₃ r ⬝ph* (p ⬝v* q) = (r ⬝ph* p) ⬝v* q :=
by induction r using phomotopy_rec_on_idp; rewrite [pwhisker_left_refl, +refl_phomotopy_hconcat]
theorem pvcompose_pwhisker_left {f₀₁'} (r : f₀₁ ~* f₀₁')
(p : psquare f₁₀ f₁₂ f₀₁ f₂₁) (q : psquare f₁₂ f₁₄ f₀₃ f₂₃) :
(p ⬝v* q) ⬝* (pwhisker_left f₁₄ (pwhisker_left f₀₃ r)) = (p ⬝* pwhisker_left f₁₂ r) ⬝v* q :=
by induction r using phomotopy_rec_on_idp; rewrite [+pwhisker_left_refl, + trans_refl]
definition phconcat2 {p p' : psquare f₁₀ f₁₂ f₀₁ f₂₁} {q q' : psquare f₃₀ f₃₂ f₂₁ f₄₁}
(r : p = p') (s : q = q') : p ⬝h* q = p' ⬝h* q' :=
ap011 phconcat r s
definition pvconcat2 {p p' : psquare f₁₀ f₁₂ f₀₁ f₂₁} {q q' : psquare f₁₂ f₁₄ f₀₃ f₂₃}
(r : p = p') (s : q = q') : p ⬝v* q = p' ⬝v* q' :=
ap011 pvconcat r s
definition phinverse2 {f₁₀ : A₀₀ ≃* A₂₀} {f₁₂ : A₀₂ ≃* A₂₂} {p p' : psquare f₁₀ f₁₂ f₀₁ f₂₁}
(r : p = p') : p⁻¹ʰ* = p'⁻¹ʰ* :=
ap phinverse r
definition pvinverse2 {f₀₁ : A₀₀ ≃* A₀₂} {f₂₁ : A₂₀ ≃* A₂₂} {p p' : psquare f₁₀ f₁₂ f₀₁ f₂₁}
(r : p = p') : p⁻¹ᵛ* = p'⁻¹ᵛ* :=
ap pvinverse r
definition phomotopy_hconcat2 {q q' : f₀₁' ~* f₀₁} {p p' : psquare f₁₀ f₁₂ f₀₁ f₂₁}
(r : q = q') (s : p = p') : q ⬝ph* p = q' ⬝ph* p' :=
ap011 phomotopy_hconcat r s
definition hconcat_phomotopy2 {p p' : psquare f₁₀ f₁₂ f₀₁ f₂₁} {q q' : f₂₁' ~* f₂₁}
(r : p = p') (s : q = q') : p ⬝hp* q = p' ⬝hp* q' :=
ap011 hconcat_phomotopy r s
definition phomotopy_vconcat2 {q q' : f₁₀' ~* f₁₀} {p p' : psquare f₁₀ f₁₂ f₀₁ f₂₁}
(r : q = q') (s : p = p') : q ⬝pv* p = q' ⬝pv* p' :=
ap011 phomotopy_vconcat r s
definition vconcat_phomotopy2 {p p' : psquare f₁₀ f₁₂ f₀₁ f₂₁} {q q' : f₁₂' ~* f₁₂}
(r : p = p') (s : q = q') : p ⬝vp* q = p' ⬝vp* q' :=
ap011 vconcat_phomotopy r s
-- for consistency, should there be a second star here?
infix ` ◾h* `:79 := phconcat2
infix ` ◾v* `:79 := pvconcat2
infixl ` ◾hp* `:79 := hconcat_phomotopy2
infixr ` ◾ph* `:79 := phomotopy_hconcat2
infixl ` ◾vp* `:79 := vconcat_phomotopy2
infixr ` ◾pv* `:79 := phomotopy_vconcat2
postfix `⁻²ʰ*`:(max+1) := phinverse2
postfix `⁻²ᵛ*`:(max+1) := pvinverse2
end psquare
/- a more explicit proof of ppcompose_left_phomotopy, which might be useful if we need to prove properties about it
-/
-- fapply phomotopy_mk_ppmap,
-- { intro f, exact pwhisker_right f p },
-- { refine ap (λx, _ ⬝* x) !phomotopy_of_eq_of_phomotopy ⬝ _ ⬝ !phomotopy_of_eq_of_phomotopy⁻¹,
-- exact pcompose_pconst_phomotopy p }
definition ppcompose_left_phomotopy_refl {A B C : Type*} (g : B →* C) :
ppcompose_left_phomotopy (phomotopy.refl g) = phomotopy.refl (@ppcompose_left A _ _ g) :=
!phomotopy_rec_on_idp_refl
-- definition pmap_eq_equiv {X Y : Type*} (f g : X →* Y) : (f = g) ≃ (f ~* g) :=
-- begin
-- refine eq_equiv_fn_eq_of_equiv (@pmap.sigma_char X Y) f g ⬝e _,
-- refine !sigma_eq_equiv ⬝e _,
-- refine _ ⬝e (phomotopy.sigma_char f g)⁻¹ᵉ,
-- fapply sigma_equiv_sigma,
-- { esimp, apply eq_equiv_homotopy },
-- { induction g with g gp, induction Y with Y y0, esimp, intro p, induction p, esimp at *,
-- refine !pathover_idp ⬝e _, refine _ ⬝e !eq_equiv_eq_symm,
-- apply equiv_eq_closed_right, exact !idp_con⁻¹ }
-- end
definition pmap_eq_idp {X Y : Type*} (f : X →* Y) :
pmap_eq (λx, idpath (f x)) !idp_con⁻¹ = idpath f :=
ap (λx, eq_of_phomotopy (phomotopy.mk _ x)) !inv_inv ⬝ eq_of_phomotopy_refl f
definition pfunext [constructor] (X Y : Type*) : ppmap X (Ω Y) ≃* Ω (ppmap X Y) :=
begin
fapply pequiv_of_equiv,
{ fapply equiv.MK: esimp,
{ intro f, fapply pmap_eq,
{ intro x, exact f x },
{ exact (respect_pt f)⁻¹ }},
{ intro p, fapply pmap.mk,
{ intro x, exact ap010 pmap.to_fun p x },
{ note z := apd respect_pt p,
note z2 := square_of_pathover z,
refine eq_of_hdeg_square z2 ⬝ !ap_constant }},
{ intro p, exact sorry },
{ intro p, exact sorry }},
{ apply pmap_eq_idp}
end
/-
Do we want to use a structure of homotopies between pointed homotopies? Or are equalities fine?
If we set up things more generally, we could define this as
"pointed homotopies between the dependent pointed maps p and q"
-/
structure phomotopy2 {A B : Type*} {f g : A →* B} (p q : f ~* g) : Type :=
(homotopy_eq : p ~ q)
(homotopy_pt_eq : whisker_right (respect_pt g) (homotopy_eq pt) ⬝ to_homotopy_pt q = to_homotopy_pt p)
/- this sets it up more generally, for illustrative purposes -/
structure ppi' (A : Type*) (P : A → Type) (p : P pt) :=
(to_fun : Π a : A, P a)
(resp_pt : to_fun (Point A) = p)
attribute ppi'.to_fun [coercion]
definition ppi_homotopy' {A : Type*} {P : A → Type} {x : P pt} (f g : ppi' A P x) : Type :=
ppi' A (λa, f a = g a) (ppi'.resp_pt f ⬝ (ppi'.resp_pt g)⁻¹)
definition ppi_homotopy2' {A : Type*} {P : A → Type} {x : P pt} {f g : ppi' A P x} (p q : ppi_homotopy' f g) : Type :=
ppi_homotopy' p q
infix ` ~*2 `:50 := phomotopy2
variables {A B : Type*} {f g : A →* B} (p q : f ~* g)
-- definition phomotopy_eq_equiv_phomotopy2 : p = q ≃ p ~*2 q :=
-- sorry
end pointed

4
pointed_pi.hlean
View file

@ -12,7 +12,7 @@ open eq pointed equiv sigma
The goal of this file is to give the truncation level
of the type of pointed maps, giving the connectivity of
the domain and the truncation level of the codomain.
This is is_trunc_pmap at the end.
This is is_trunc_pmap_of_is_conn at the end.
First we define the type of dependent pointed maps
as a tool, because these appear in the more general
@ -164,7 +164,7 @@ section
{ exact pt } }
end
definition is_trunc_pmap (k : ℕ₋₂) (B : (n.+1+2+k)-Type*)
definition is_trunc_pmap_of_is_conn (k : ℕ₋₂) (B : (n.+1+2+k)-Type*)
: is_trunc k.+1 (A →* B) :=
@is_trunc_equiv_closed _ _ k.+1 (ppi_equiv_pmap A B)
(is_trunc_ppi A n k (λ a, B))