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

feat(homotopy): prove adjunction between smash product and pointed maps

Browse source 
also develop library for equality reasoning on pointed homotopies.
Also do the renamings like homomorphism -> is_mul_hom
This commit is contained in:
Floris van Doorn 2017-01-18 23:19:00 +01:00
parent b2bfc978bf
commit 00e01fd2a6
9 changed files with 983 additions and 61 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

16
algebra/quotient_group.hlean
View file

@ -249,12 +249,12 @@ namespace group
-- FIRST ISOMORPHISM THEOREM
definition kernel_quotient_extension {A B : AbGroup} (f : A →g B) : quotient_ab_group (kernel_subgroup f) →g B :=
definition kernel_quotient_extension {A B : AbGroup} (f : A →g B) : quotient_ab_group (kernel_subgroup f) →g B :=
begin
fapply quotient_group_elim f, intro a, intro p, exact p
end
definition kernel_quotient_extension_triangle {A B : AbGroup} (f : A →g B) :
definition kernel_quotient_extension_triangle {A B : AbGroup} (f : A →g B) :
kernel_quotient_extension f ∘g ab_qg_map (kernel_subgroup f) ~ f :=
begin
intro a,
@ -264,7 +264,7 @@ definition kernel_quotient_extension_triangle {A B : AbGroup} (f : A →g B) :
definition is_embedding_kernel_quotient_extension {A B : AbGroup} (f : A →g B) :
is_embedding (kernel_quotient_extension f) :=
begin
fapply is_embedding_homomorphism,
fapply is_embedding_of_is_mul_hom,
intro x,
note H := is_surjective_ab_qg_map (kernel_subgroup f) x,
induction H, induction p,
@ -273,7 +273,7 @@ definition is_embedding_kernel_quotient_extension {A B : AbGroup} (f : A →g B)
refine _ ⬝ q,
symmetry,
rexact kernel_quotient_extension_triangle f a
end
end
definition ab_group_quotient_homomorphism (A B : AbGroup)(K : subgroup_rel A)(L : subgroup_rel B) (f : A →g B)
(p : Π(a:A), K(a) → L(f a)) : quotient_ab_group K →g quotient_ab_group L :=
@ -302,15 +302,15 @@ definition ab_group_triv_kernel_factor {A B C: AbGroup} (f : A →g B)(g : A
intro p,
intro a,
intro q,
fapply p,
exact ab_group_kernel_factor f g H a q
fapply p,
exact ab_group_kernel_factor f g H a q
end
definition triv_kern_is_embedding {A B : AbGroup} (f : A →g B):
is_trivial_subgroup _ (kernel_subgroup(f)) → is_embedding(f) :=
begin
intro p,
fapply is_embedding_homomorphism,
fapply is_embedding_of_is_mul_hom,
intro a q,
apply p,
exact q
@ -366,7 +366,7 @@ exact is_surjective_image_lift f
definition is_embedding_kernel_quotient_to_image {A B : AbGroup} (f : A →g B)
: is_embedding (ab_group_kernel_quotient_to_image f) :=
begin
fapply @is_embedding_factor _ (image f) B _ _ _ (ab_group_kernel_quotient_to_image f) (image_incl f) (kernel_quotient_extension f),
fapply @is_embedding_factor _ (image f) B _ _ _ (ab_group_kernel_quotient_to_image f) (image_incl f) (kernel_quotient_extension f),
exact ab_group_kernel_quotient_to_image_triangle f,
exact is_embedding_kernel_quotient_extension f
end

4
homotopy/EM.hlean
View file

@ -262,7 +262,7 @@ namespace EM
(ptrunc_elim_ptrunc_functor ((succ n).+1) _ _)⁻¹*,
apply ptrunc_elim_phomotopy,
refine _ ⬝* !psusp_elim_psusp_functor⁻¹*,
refine _ ⬝* psusp_elim_phomotopy (IH _ _ _ _ _ (is_homomorphism_EM_up eX rX) _ (@is_conn_loop _ _ H1)
refine _ ⬝* psusp_elim_phomotopy (IH _ _ _ _ _ (is_mul_hom_EM_up eX rX) _ (@is_conn_loop _ _ H1)
(@is_trunc_loop _ _ H2) _ _ (EM_up_natural φ f eX eY p)),
apply psusp_elim_natural }
end
@ -347,7 +347,7 @@ namespace EM
-- { exact EM1_pmap e⁻¹ᵉ* (equiv.inv_preserve_binary e concat mul r) },
-- rewrite [EMadd1_succ],
-- exact ptrunc.elim ((succ n).+1)
-- (psusp.elim (f _ (EM_up e) (is_homomorphism_EM_up e r) _ _)),
-- (psusp.elim (f _ (EM_up e) (is_mul_hom_EM_up e r) _ _)),
-- end
-- definition is_set_pmap_ptruncconntype {n : ℕ₋₂} (X Y : (n.+1)-Type*[n]) : is_set (X →* Y) :=

2
homotopy/degree.hlean
View file

@ -5,7 +5,7 @@ open fin eq equiv group algebra sphere.ops pointed nat int trunc is_equiv functi
definition eq_one_or_eq_neg_one_of_mul_eq_one {n : ℤ} (m : ℤ) (p : n * m = 1) : n = 1 ⊎ n = -1 :=
sorry
definition endomorphism_int_unbundled (f : ℤ → ℤ) [is_add_homomorphism f] (n : ℤ) :
definition endomorphism_int_unbundled (f : ℤ → ℤ) [is_add_hom f] (n : ℤ) :
f n = f 1 * n :=
begin
induction n using rec_nat_on with n IH n IH,

12
homotopy/pushout.hlean
View file

@ -10,9 +10,17 @@ namespace pushout
{TL' BL' TR' : Type*} {f' : TL' →* BL'} {g' : TL' →* TR'}
(tl : TL ≃ TL') (bl : BL ≃* BL') (tr : TR ≃ TR')
(fh : bl ∘ f ~ f' ∘ tl) (gh : tr ∘ g ~ g' ∘ tl)
include fh gh
definition ppushout_pequiv : ppushout f g ≃* ppushout f' g' :=
definition ppushout_functor [constructor] (tl : TL → TL') (bl : BL →* BL') (tr : TR → TR')
(fh : bl ∘ f ~ f' ∘ tl) (gh : tr ∘ g ~ g' ∘ tl) : ppushout f g →* ppushout f' g' :=
begin
fconstructor,
{ exact pushout.functor tl bl tr fh gh },
{ exact ap inl (respect_pt bl) },
end
definition ppushout_pequiv (tl : TL ≃ TL') (bl : BL ≃* BL') (tr : TR ≃ TR')
(fh : bl ∘ f ~ f' ∘ tl) (gh : tr ∘ g ~ g' ∘ tl) : ppushout f g ≃* ppushout f' g' :=
pequiv_of_equiv (pushout.equiv _ _ _ _ tl bl tr fh gh) (ap inl (respect_pt bl))
end

223
homotopy/smash.hlean
View file

@ -11,22 +11,184 @@ open bool pointed eq equiv is_equiv sum bool prod unit circle cofiber prod.ops w
/- To prove: associative, A ∧ S¹ ≃ ΣA -/
variables {A B C D : Type*}
variables {A B C D E F : Type*}
namespace smash
section
open pushout
definition smash_functor' [unfold 7] (f : A →* C) (g : B →* D) : A ∧ B → C ∧ D :=
begin
fapply pushout.functor,
{ exact sum_functor f g },
{ exact prod_functor f g },
{ exact id },
{ intro v, induction v with a b,
exact prod_eq idp (respect_pt g),
exact prod_eq (respect_pt f) idp },
{ intro v, induction v with a b: reflexivity }
end
definition smash_functor [constructor] (f : A →* C) (g : B →* D) : A ∧ B →* C ∧ D :=
begin
fapply pmap.mk,
{ exact smash_functor' f g },
{ exact ap inl (prod_eq (respect_pt f) (respect_pt g)) },
end
definition functor_gluel (f : A →* C) (g : B →* D) (a : A) :
ap (smash_functor f g) (gluel a) = ap (smash.mk (f a)) (respect_pt g) ⬝ gluel (f a) :=
begin
refine !pushout.elim_glue ⬝ _, esimp, apply whisker_right,
induction D with D d₀, induction g with g g₀, esimp at *, induction g₀, reflexivity
end
definition functor_gluer (f : A →* C) (g : B →* D) (b : B) :
ap (smash_functor f g) (gluer b) = ap (λc, smash.mk c (g b)) (respect_pt f) ⬝ gluer (g b) :=
begin
refine !pushout.elim_glue ⬝ _, esimp, apply whisker_right,
induction C with C c₀, induction f with f f₀, esimp at *, induction f₀, reflexivity
end
definition functor_gluel' (f : A →* C) (g : B →* D) (a a' : A) :
ap (smash_functor f g) (gluel' a a') = ap (smash.mk (f a)) (respect_pt g) ⬝
gluel' (f a) (f a') ⬝ (ap (smash.mk (f a')) (respect_pt g))⁻¹ :=
begin
refine !ap_con ⬝ !functor_gluel ◾ (!ap_inv ⬝ !functor_gluel⁻²) ⬝ _,
refine whisker_left _ !con_inv ⬝ _,
refine !con.assoc⁻¹ ⬝ _, apply whisker_right,
apply con.assoc
end
definition functor_gluer' (f : A →* C) (g : B →* D) (b b' : B) :
ap (smash_functor f g) (gluer' b b') = ap (λc, smash.mk c (g b)) (respect_pt f) ⬝
gluer' (g b) (g b') ⬝ (ap (λc, smash.mk c (g b')) (respect_pt f))⁻¹ :=
begin
refine !ap_con ⬝ whisker_left _ !ap_inv ⬝ _,
refine !functor_gluer ◾ !functor_gluer⁻² ⬝ _,
refine whisker_left _ !con_inv ⬝ _,
refine !con.assoc⁻¹ ⬝ _, apply whisker_right,
apply con.assoc
end
/- the statements of the above rules becomes easier if one of the functions respects the basepoint
by reflexivity -/
definition functor_gluel'2 {D : Type} (f : A →* C) (g : B → D) (a a' : A) :
ap (smash_functor f (pmap_of_map g pt)) (gluel' a a') = gluel' (f a) (f a') :=
begin
refine !ap_con ⬝ whisker_left _ !ap_inv ⬝ _,
refine (!functor_gluel ⬝ !idp_con) ◾ (!functor_gluel ⬝ !idp_con)⁻²
end
definition functor_gluer'2 {C : Type} (f : A → C) (g : B →* D) (b b' : B) :
ap (smash_functor (pmap_of_map f pt) g) (gluer' b b') = gluer' (g b) (g b') :=
begin
refine !ap_con ⬝ whisker_left _ !ap_inv ⬝ _,
refine (!functor_gluer ⬝ !idp_con) ◾ (!functor_gluer ⬝ !idp_con)⁻²
end
lemma functor_gluel'2_same {D : Type} (f : A →* C) (g : B → D) (a : A) :
functor_gluel'2 f (pmap_of_map g pt) a a =
ap02 (smash_functor f (pmap_of_map g pt)) (con.right_inv (gluel a)) ⬝
(con.right_inv (gluel (f a)))⁻¹ :=
begin
refine _ ⬝ whisker_right _ (eq_top_of_square (!ap_con_right_inv_sq))⁻¹,
refine _ ⬝ whisker_right _ !con_idp⁻¹,
refine _ ⬝ !con.assoc⁻¹,
apply whisker_left,
apply eq_con_inv_of_con_eq, symmetry,
apply con_right_inv_natural
end
lemma functor_gluer'2_same {C : Type} (f : A → C) (g : B →* D) (b : B) :
functor_gluer'2 (pmap_of_map f pt) g b b =
ap02 (smash_functor (pmap_of_map f pt) g) (con.right_inv (gluer b)) ⬝
(con.right_inv (gluer (g b)))⁻¹ :=
begin
refine _ ⬝ whisker_right _ (eq_top_of_square (!ap_con_right_inv_sq))⁻¹,
refine _ ⬝ whisker_right _ !con_idp⁻¹,
refine _ ⬝ !con.assoc⁻¹,
apply whisker_left,
apply eq_con_inv_of_con_eq, symmetry,
apply con_right_inv_natural
end
definition smash_functor_pcompose_homotopy (f' : C →* E) (f : A →* C) (g' : D →* F) (g : B →* D) :
smash_functor (f' ∘* f) (g' ∘* g) ~ smash_functor f' g' ∘* smash_functor f g :=
begin
intro x, induction x with a b a b,
{ reflexivity },
{ reflexivity },
{ reflexivity },
{ apply eq_pathover, apply hdeg_square,
refine !functor_gluel ⬝ _ ⬝ (ap_compose (smash_functor f' g') _ _)⁻¹,
refine whisker_right _ !ap_con ⬝ !con.assoc ⬝ _ ⬝ ap02 _ !functor_gluel⁻¹,
refine (!ap_compose'⁻¹ ⬝ !ap_compose') ◾ proof !functor_gluel⁻¹ qed ⬝ !ap_con⁻¹, },
{ apply eq_pathover, apply hdeg_square,
refine !functor_gluer ⬝ _ ⬝ (ap_compose (smash_functor f' g') _ _)⁻¹,
refine whisker_right _ !ap_con ⬝ !con.assoc ⬝ _ ⬝ ap02 _ !functor_gluer⁻¹,
refine (!ap_compose'⁻¹ ⬝ !ap_compose') ◾ proof !functor_gluer⁻¹ qed ⬝ !ap_con⁻¹, }
end
definition smash_functor_pcompose [constructor] (f' : C →* E) (f : A →* C) (g' : D →* F) (g : B →* D) :
smash_functor (f' ∘* f) (g' ∘* g) ~* smash_functor f' g' ∘* smash_functor f g :=
begin
fapply phomotopy.mk,
{ exact smash_functor_pcompose_homotopy f' f g' g },
{ exact abstract begin induction C, induction D, induction E, induction F,
induction f with f f₀, induction f' with f' f'₀, induction g with g g₀, induction g' with g' g'₀,
esimp at *, induction f₀, induction f'₀, induction g₀, induction g'₀, reflexivity end end }
end
definition smash_functor_phomotopy [constructor] {f f' : A →* C} {g g' : B →* D}
(h₁ : f ~* f') (h₂ : g ~* g') : smash_functor f g ~* smash_functor f' g' :=
begin
induction h₁ using phomotopy_rec_on_idp,
induction h₂ using phomotopy_rec_on_idp,
reflexivity
-- fapply phomotopy.mk,
-- { intro x, induction x with a b a b,
-- { exact ap011 smash.mk (h₁ a) (h₂ b) },
-- { reflexivity },
-- { reflexivity },
-- { apply eq_pathover,
-- refine !functor_gluel ⬝ph _ ⬝hp !functor_gluel⁻¹, exact sorry },
-- { apply eq_pathover,
-- refine !functor_gluer ⬝ph _ ⬝hp !functor_gluer⁻¹, exact sorry }},
-- { esimp, }
end
definition smash_functor_phomotopy_refl [constructor] (f : A →* C) (g : B →* D) :
smash_functor_phomotopy (phomotopy.refl f) (phomotopy.refl g) = phomotopy.rfl :=
!phomotopy_rec_on_idp_refl ⬝ !phomotopy_rec_on_idp_refl
definition smash_functor_pid [constructor] (A B : Type*) : smash_functor (pid A) (pid B) ~* pid (A ∧ B) :=
begin
fapply phomotopy.mk,
{ intro x, induction x with a b a b,
{ reflexivity },
{ reflexivity },
{ reflexivity },
{ apply eq_pathover_id_right, apply hdeg_square, exact !functor_gluel ⬝ !idp_con },
{ apply eq_pathover_id_right, apply hdeg_square, exact !functor_gluer ⬝ !idp_con }},
{ reflexivity }
end
definition smash_functor_pid_pcompose [constructor] (A : Type*) (g' : C →* D) (g : B →* C)
: smash_functor (pid A) (g' ∘* g) ~* smash_functor (pid A) g' ∘* smash_functor (pid A) g :=
smash_functor_phomotopy !pid_pcompose⁻¹* phomotopy.rfl ⬝* !smash_functor_pcompose
definition smash_functor_pcompose_pid [constructor] (B : Type*) (f' : C →* D) (f : A →* C)
: smash_functor (f' ∘* f) (pid B) ~* smash_functor f' (pid B) ∘* smash_functor f (pid B) :=
smash_functor_phomotopy phomotopy.rfl !pid_pcompose⁻¹* ⬝* !smash_functor_pcompose
definition smash_pequiv_smash [constructor] (f : A ≃* C) (g : B ≃* D) : A ∧ B ≃* C ∧ D :=
begin
fapply pequiv_of_equiv,
{ fapply pushout.equiv,
{ exact sum_equiv_sum f g },
{ exact prod_equiv_prod f g },
{ reflexivity },
{ intro v, induction v with a b, exact prod_eq idp (respect_pt g), exact prod_eq (respect_pt f) idp },
{ intro v, induction v with a b: reflexivity }},
{ exact ap inl (prod_eq (respect_pt f) (respect_pt g)) },
fapply pequiv_of_pmap (smash_functor f g),
apply pushout.is_equiv_functor,
exact to_is_equiv (sum_equiv_sum f g)
end
end
@ -37,27 +199,51 @@ namespace smash
definition smash_pequiv_smash_right [constructor] (A : Type*) (g : B ≃* D) : A ∧ B ≃* A ∧ D :=
smash_pequiv_smash pequiv.rfl g
/- smash A B ≃ pcofiber (pprod_of_pwedge A B) -/
theorem elim_gluel' {P : Type} {Pmk : Πa b, P} {Pl Pr : P}
definition elim_gluel' {P : Type} {Pmk : Πa b, P} {Pl Pr : P}
(Pgl : Πa : A, Pmk a pt = Pl) (Pgr : Πb : B, Pmk pt b = Pr) (a a' : A) :
ap (smash.elim Pmk Pl Pr Pgl Pgr) (gluel' a a') = Pgl a ⬝ (Pgl a')⁻¹ :=
!ap_con ⬝ !elim_gluel ◾ (!ap_inv ⬝ !elim_gluel⁻²)
!ap_con ⬝ whisker_left _ !ap_inv ⬝ !elim_gluel ◾ !elim_gluel⁻²
theorem elim_gluer' {P : Type} {Pmk : Πa b, P} {Pl Pr : P}
definition elim_gluer' {P : Type} {Pmk : Πa b, P} {Pl Pr : P}
(Pgl : Πa : A, Pmk a pt = Pl) (Pgr : Πb : B, Pmk pt b = Pr) (b b' : B) :
ap (smash.elim Pmk Pl Pr Pgl Pgr) (gluer' b b') = Pgr b ⬝ (Pgr b')⁻¹ :=
!ap_con ⬝ !elim_gluer ◾ (!ap_inv ⬝ !elim_gluer⁻²)
!ap_con ⬝ whisker_left _ !ap_inv ⬝ !elim_gluer ◾ !elim_gluer⁻²
theorem elim'_gluel'_pt {P : Type} {Pmk : Πa b, P}
definition elim_gluel'_same {P : Type} {Pmk : Πa b, P} {Pl Pr : P}
(Pgl : Πa : A, Pmk a pt = Pl) (Pgr : Πb : B, Pmk pt b = Pr) (a : A) :
elim_gluel' Pgl Pgr a a =
ap02 (smash.elim Pmk Pl Pr Pgl Pgr) (con.right_inv (gluel a)) ⬝ (con.right_inv (Pgl a))⁻¹ :=
begin
refine _ ⬝ whisker_right _ (eq_top_of_square (!ap_con_right_inv_sq))⁻¹,
refine _ ⬝ whisker_right _ !con_idp⁻¹,
refine _ ⬝ !con.assoc⁻¹,
apply whisker_left,
apply eq_con_inv_of_con_eq, symmetry,
apply con_right_inv_natural
end
definition elim_gluer'_same {P : Type} {Pmk : Πa b, P} {Pl Pr : P}
(Pgl : Πa : A, Pmk a pt = Pl) (Pgr : Πb : B, Pmk pt b = Pr) (b : B) :
elim_gluer' Pgl Pgr b b =
ap02 (smash.elim Pmk Pl Pr Pgl Pgr) (con.right_inv (gluer b)) ⬝ (con.right_inv (Pgr b))⁻¹ :=
begin
refine _ ⬝ whisker_right _ (eq_top_of_square (!ap_con_right_inv_sq))⁻¹,
refine _ ⬝ whisker_right _ !con_idp⁻¹,
refine _ ⬝ !con.assoc⁻¹,
apply whisker_left,
apply eq_con_inv_of_con_eq, symmetry,
apply con_right_inv_natural
end
definition elim'_gluel'_pt {P : Type} {Pmk : Πa b, P}
(Pgl : Πa : A, Pmk a pt = Pmk pt pt) (Pgr : Πb : B, Pmk pt b = Pmk pt pt)
(a : A) (ql : Pgl pt = idp) (qr : Pgr pt = idp) :
ap (smash.elim' Pmk Pgl Pgr ql qr) (gluel' a pt) = Pgl a :=
!elim_gluel' ⬝ whisker_left _ ql⁻²
theorem elim'_gluer'_pt {P : Type} {Pmk : Πa b, P}
definition elim'_gluer'_pt {P : Type} {Pmk : Πa b, P}
(Pgl : Πa : A, Pmk a pt = Pmk pt pt) (Pgr : Πb : B, Pmk pt b = Pmk pt pt)
(b : B) (ql : Pgl pt = idp) (qr : Pgr pt = idp) :
ap (smash.elim' Pmk Pgl Pgr ql qr) (gluer' b pt) = Pgr b :=
@ -131,7 +317,8 @@ namespace pushout
refine pushout_hcompose_equiv (sum_of_bool A B) (wedge_equiv_pushout_sum A B)
_ _ ⬝e _,
exact erfl,
intro x, induction x: esimp,
intro x, induction x,
reflexivity, reflexivity,
exact bool_of_sum_of_bool,
apply pushout_of_equiv_right
end

508
homotopy/smash_adjoint.hlean Normal file
View file

@ -0,0 +1,508 @@
-- Authors: Floris van Doorn
-- in collaboration with Egbert, Stefano, Robin
import .smash
open bool pointed eq equiv is_equiv sum bool prod unit circle cofiber prod.ops wedge is_trunc
function red_susp unit sigma
namespace smash
variables {A B C : Type*}
definition pinl [constructor] (A : Type*) {B : Type*} (b : B) : A →* A ∧ B :=
begin
fapply pmap.mk,
{ intro a, exact smash.mk a b },
{ exact gluer' b pt }
end
definition pinl_phomotopy {A B : Type*} {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
fconstructor,
{ intro a, exact gluel' a pt },
{ rexact con.right_inv (gluel pt) ⬝ (con.right_inv (gluer pt))⁻¹ }
end
definition smash_pmap_unit [constructor] (A B : Type*) : B →* ppmap A (A ∧ B) :=
begin
fapply pmap.mk,
{ exact pinl A },
{ apply eq_of_phomotopy, exact smash_pmap_unit_pt A B }
end
definition smash_functor_pid_gluer' (A : Type*) {B C : Type*} (b : B) (f : B →* C) :
ap (smash_functor (pid A) f) (gluer' b pt) = gluer' (f b) (f pt) :=
begin
rexact functor_gluer'2 (@id A) f b pt
end
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
fapply phomotopy.mk,
{ intro a, reflexivity },
{ refine !idp_con ⬝ _,
induction C with C c₀, induction f with f f₀, esimp at *,
induction f₀, rexact smash_functor_pid_gluer' A b (pmap_of_map f pt) }
end
definition smash_pmap_unit_pt_natural [constructor] (f : B →* C) :
smash_functor_pid_pinl' pt f ⬝*
pwhisker_left (smash_functor (pid A) f) (smash_pmap_unit_pt A B) ⬝*
pcompose_pconst (smash_functor (pid A) f) =
pinl_phomotopy (respect_pt f) ⬝* smash_pmap_unit_pt A C :=
begin
induction f with f f₀, induction C with C c₀, esimp at *,
induction f₀, refine _ ⬝ !refl_trans⁻¹,
refine !trans_refl ⬝ _,
fapply phomotopy_eq',
{ intro a, refine !idp_con ⬝ _,
rexact functor_gluel'2 (pid A) f a pt },
{ refine whisker_right_idp _ ⬝ph _,
refine ap (λx, _ ⬝ x) _ ⬝ph _,
rotate 1, rexact (functor_gluel'2_same (pid A) f pt),
-- refine whisker_left _ (!con.assoc ⬝ whisker_left _ !con.left_inv ⬝ !con_idp) ⬝ph _,
refine whisker_right _ !idp_con ⬝pv _,
refine !con.assoc⁻¹ ⬝ph _, apply whisker_bl,
refine !con.assoc⁻¹ ⬝ whisker_right _ _ ⬝pv _,
rotate 1, esimp, apply whisker_left_idp_con,
refine !con.assoc ⬝pv _, apply whisker_tl,
refine whisker_right _ !idp_con ⬝pv _,
refine whisker_right _ !whisker_right_idp ⬝pv _,
refine whisker_right _ (!idp_con ⬝ !ap02_con) ⬝ !con.assoc ⬝pv _,
apply whisker_tl,
apply vdeg_square,
refine whisker_right _ !ap_inv ⬝ _, apply inv_con_eq_of_eq_con,
unfold [smash_functor_pid_gluer'],
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) :
smash_pmap_unit A C ∘* f ~*
ppcompose_left (smash_functor (pid A) f) ∘* smash_pmap_unit A B :=
begin
induction A with A a₀, induction B with B b₀, induction C with C c₀,
induction f with f f₀, esimp at *, induction f₀, fapply phomotopy_mk_ppmap,
{ esimp [pcompose], intro b, exact smash_functor_pid_pinl' b (pmap_of_map f b₀) },
{ refine ap (λx, _ ⬝* phomotopy_of_eq x) !respect_pt_pcompose ⬝ _
⬝ 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, _ ⬝* x) (!phomotopy_of_eq_con ⬝
ap011 phomotopy.trans !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 :=
begin
induction af with a f a f,
{ exact f a },
{ exact pt },
{ exact pt },
{ reflexivity },
{ exact respect_pt f }
end
definition smash_pmap_counit [constructor] (A B : Type*) : A ∧ (ppmap A B) →* B :=
begin
fapply pmap.mk,
{ exact smash_pmap_counit_map },
{ 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) :=
begin
symmetry,
fapply phomotopy.mk,
{ intro af, induction af with a f a f,
{ reflexivity },
{ exact (respect_pt g)⁻¹ },
{ exact (respect_pt g)⁻¹ },
{ apply eq_pathover,
refine ap_compose (smash_pmap_counit A C) _ _ ⬝ph _ ⬝hp (ap_compose g _ _)⁻¹,
refine ap02 _ !functor_gluel ⬝ph _ ⬝hp ap02 _ !elim_gluel⁻¹,
refine !ap_con ⬝ !ap_compose'⁻¹ ◾ !elim_gluel ⬝ph _⁻¹ʰ,
apply square_of_eq_bot, refine !idp_con ⬝ _,
induction C with C c₀, induction g with g g₀, esimp at *,
induction g₀, refine ap02 _ !eq_of_phomotopy_refl },
{ apply eq_pathover,
refine ap_compose (smash_pmap_counit A C) _ _ ⬝ph _ ⬝hp (ap_compose g _ _)⁻¹,
refine ap02 _ !functor_gluer ⬝ph _ ⬝hp ap02 _ !elim_gluer⁻¹,
refine !ap_con ⬝ !ap_compose'⁻¹ ◾ !elim_gluer ⬝ph _,
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_unit_counit (A B : Type*) :
smash_pmap_counit A (A ∧ B) ∘* smash_functor (pid A) (smash_pmap_unit A B) ~* pid (A ∧ B) :=
begin
fconstructor,
{ intro x,
induction x with a b a b,
{ reflexivity },
{ exact gluel pt },
{ exact gluer pt },
{ apply eq_pathover_id_right,
refine ap_compose smash_pmap_counit_map _ _ ⬝ ap02 _ !functor_gluel ⬝ph _,
refine !ap_con ⬝ !ap_compose'⁻¹ ◾ !elim_gluel ⬝ph _,
refine !ap_eq_of_phomotopy ⬝ph _,
apply square_of_eq, refine !idp_con ⬝ !inv_con_cancel_right⁻¹ },
{ apply eq_pathover_id_right,
refine ap_compose smash_pmap_counit_map _ _ ⬝ ap02 _ !functor_gluer ⬝ph _,
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 _)⁻¹,
rexact (con.right_inv (gluer pt))⁻¹ }
end
definition smash_pmap_counit_unit_pt [constructor] {A B : Type*} (f : A →* B) :
smash_pmap_counit A B ∘* pinl A f ~* f :=
begin
fconstructor,
{ intro a, reflexivity },
{ refine !idp_con ⬝ !elim_gluer'⁻¹ }
end
definition smash_pmap_counit_unit (A B : Type*) :
ppcompose_left (smash_pmap_counit A B) ∘* smash_pmap_unit A (ppmap A B) ~* pid (ppmap A B) :=
begin
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 _ ⬝ !phomotopy_of_eq_con⁻¹,
refine _ ⬝ ap011 phomotopy.trans !phomotopy_of_eq_of_phomotopy⁻¹
!phomotopy_of_eq_of_phomotopy⁻¹,
refine _ ⬝ !trans_refl⁻¹,
fapply phomotopy_eq,
{ intro a, refine !elim_gluel'⁻¹ },
{ esimp, refine whisker_right _ !whisker_right_idp ⬝ _ ⬝ !idp_con⁻¹,
refine whisker_right _ !elim_gluel'_same⁻² ⬝ _ ⬝ !elim_gluer'_same⁻¹⁻²,
apply inv_con_eq_of_eq_con, refine !idp_con ⬝ _, esimp,
refine _ ⬝ !ap02_con ⬝ whisker_left _ !ap_inv,
refine !whisker_right_idp ⬝ _,
exact !idp_con }}
end
definition smash_elim [constructor] {A B C : Type*} (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 :=
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 :=
begin
refine !pwhisker_right !ppcompose_left_pcompose ⬝* _,
refine !passoc ⬝* _,
refine !pwhisker_left !smash_pmap_unit_natural⁻¹* ⬝* _,
refine !passoc⁻¹* ⬝* _,
refine !pwhisker_right !smash_pmap_counit_unit ⬝* _,
apply pid_pcompose
end
definition smash_elim_right_inv {A B C : Type*} (g : A ∧ B →* C) : smash_elim (smash_elim_inv g) ~* g :=
begin
refine !pwhisker_left !smash_functor_pid_pcompose ⬝* _,
refine !passoc⁻¹* ⬝* _,
refine !pwhisker_right !smash_pmap_counit_natural⁻¹* ⬝* _,
refine !passoc ⬝* _,
refine !pwhisker_left !smash_pmap_unit_counit ⬝* _,
apply pcompose_pid
end
definition smash_elim_pconst (A B C : Type*) :
smash_elim (pconst B (ppmap A C)) ~* pconst (A ∧ B) C :=
begin
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*) :
smash_elim_inv (pconst (A ∧ B) C) ~* pconst B (ppmap A C) :=
begin
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 ⬝
!phomotopy_of_eq_of_phomotopy) ◾** !phomotopy_of_eq_of_phomotopy)⁻¹,
apply pconst_pcompose_phomotopy_pconst }
end
definition smash_elim_natural {A B C C' : Type*} (f : C →* C')
(g : B →* ppmap A C) : f ∘* smash_elim g ~* smash_elim (ppcompose_left f ∘* g) :=
begin
refine _ ⬝* pwhisker_left _ !smash_functor_pid_pcompose⁻¹*,
refine !passoc⁻¹* ⬝* pwhisker_right _ _ ⬝* !passoc,
apply smash_pmap_counit_natural
end
definition smash_elim_inv_natural {A B C C' : Type*} (f : C →* C')
(g : A ∧ B →* C) : ppcompose_left f ∘* smash_elim_inv g ~* smash_elim_inv (f ∘* g) :=
begin
refine !passoc⁻¹* ⬝* pwhisker_right _ _,
exact !ppcompose_left_pcompose⁻¹*
end
definition smash_elim_phomotopy {A B C : Type*} {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}
(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}
(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,
refine ap02 _ !eq_of_phomotopy_refl ⬝ _,
refine !eq_of_phomotopy_refl⁻¹ ⬝ _,
apply ap eq_of_phomotopy,
refine _ ⬝ ap (pwhisker_left _) !smash_functor_phomotopy_refl⁻¹,
refine !pwhisker_left_refl⁻¹
end
definition smash_elim_inv_eq_of_phomotopy {A B C : Type*} {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,
refine ap02 _ !eq_of_phomotopy_refl ⬝ _,
refine !eq_of_phomotopy_refl⁻¹ ⬝ _,
apply ap eq_of_phomotopy,
refine _ ⬝ ap (pwhisker_right _) !ppcompose_left_phomotopy_refl⁻¹,
refine !pwhisker_right_refl⁻¹
end
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)
definition smash_pelim_inv [constructor] (A B C : Type*) : ppmap (B ∧ A) C →* ppmap A (ppmap B C) :=
pmap.mk smash_elim_inv (eq_of_phomotopy !smash_elim_inv_pconst)
definition smash_pelim_natural {A B C C' : Type*} (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 ⬝
!phomotopy_of_eq_of_phomotopy) ◾** !phomotopy_of_eq_of_phomotopy) ⬝ _ ,
refine _ ⬝ (!phomotopy_of_eq_con ⬝ (ap phomotopy_of_eq !pcompose_eq_of_phomotopy ⬝
!phomotopy_of_eq_of_phomotopy) ◾** !phomotopy_of_eq_of_phomotopy)⁻¹,
exact sorry }
end
definition smash_pelim_inv_natural {A B C C' : Type*} (f : C →* C') :
ppcompose_left (ppcompose_left f) ∘* smash_pelim_inv A B C ~*
smash_pelim_inv A B C' ∘* ppcompose_left f :=
begin
fapply phomotopy_mk_ppmap,
{ exact smash_elim_inv_natural f },
{ esimp,
refine idp ◾** (!phomotopy_of_eq_con ⬝ (ap phomotopy_of_eq !smash_elim_inv_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 ⬝
!phomotopy_of_eq_of_phomotopy) ◾** !phomotopy_of_eq_of_phomotopy)⁻¹,
exact sorry
}
end
-- definition smash_adjoint_pmap_2 [constructor] (A B C : Type*) : (A ∧ B →* C) ≃ B →* ppmap A C :=
-- begin
-- fapply equiv.MK,
-- { exact smash_elim_inv },
-- { exact smash_elim },
-- { intro f, apply eq_of_phomotopy, exact smash_elim_left_inv f },
-- { intro g, apply eq_of_phomotopy, exact smash_elim_right_inv g }
-- end
-- definition smash_adjoint_pmap_1 [constructor] (A B C : Type*) : (A ∧ B →* C) ≃ A →* ppmap B C :=
-- pequiv_ppcompose_right (smash_comm B A) ⬝e smash_adjoint_pmap_2 B A C
-- definition smash_elim_inv_pconst {A B C : Type*} :
-- smash_elim_inv (pconst (A ∧ B) C) ~* pconst B (ppmap A C) :=
-- begin
-- fapply phomotopy_mk_ppmap,
-- { intro b, exact pconst_pcompose (pinl A b) },
-- { refine !trans_refl ⬝ _ ⬝ !phomotopy_of_eq_con⁻¹,
-- refine _ ⬝ ap011 phomotopy.trans (!phomotopy_of_eq_of_phomotopy⁻¹ ⬝
-- ap phomotopy_of_eq !pcompose_eq_of_phomotopy⁻¹) !phomotopy_of_eq_of_phomotopy⁻¹,
-- fapply phomotopy_eq,
-- { intro a, exact !ap_constant⁻¹ },
-- { refine whisker_right _ !whisker_right_idp ⬝ _, esimp, }
-- }
-- end
-- definition smash_adjoint_pmap' [constructor] (A B C : Type*) : ppmap (A ∧ B) C ≃* ppmap B (ppmap A C) :=
-- pequiv_of_equiv (smash_adjoint_pmap_2 A B C) (eq_of_phomotopy begin esimp end)
definition smash_adjoint_pmap' [constructor] (A B C : Type*) : B →* ppmap A C ≃ A ∧ B →* C :=
begin
fapply equiv.MK,
{ exact smash_elim },
{ exact smash_elim_inv },
{ intro g, apply eq_of_phomotopy, exact smash_elim_right_inv g },
{ intro f, apply eq_of_phomotopy, exact smash_elim_left_inv f }
end
definition smash_adjoint_pmap [constructor] (A B C : Type*) :
ppmap (A ∧ B) C ≃* ppmap B (ppmap A C) :=
(pequiv_of_equiv (smash_adjoint_pmap' A B C) (eq_of_phomotopy (smash_elim_pconst A B C)))⁻¹ᵉ*
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
refine !passoc⁻¹* ⬝* pwhisker_right _ _,
exact !ppcompose_left_pcompose⁻¹*
end
definition smash_adjoint_pmap_natural [constructor] {A B C C' : Type*} (f : C →* C') :
ppcompose_left (ppcompose_left f) ∘* smash_adjoint_pmap A B C ~*
smash_adjoint_pmap A B C' ∘* ppcompose_left f :=
begin
fapply phomotopy_mk_ppmap,
{ exact smash_adjoint_pmap_natural_pt f },
{ exact sorry }
end
definition smash_adjoint_pmap_inv_natural_pt {A B C C' : Type*} (f : C →* C')
(g : B →* ppmap A C) : f ∘* (smash_adjoint_pmap A B C)⁻¹ᵉ* g ~*
(smash_adjoint_pmap A B C')⁻¹ᵉ* (ppcompose_left f ∘* g) :=
begin
refine _ ⬝* pwhisker_left _ !smash_functor_pid_pcompose⁻¹*,
refine !passoc⁻¹* ⬝* pwhisker_right _ _ ⬝* !passoc,
apply smash_pmap_counit_natural
end
definition smash_adjoint_pmap_inv_natural [constructor] {A B C C' : Type*} (f : C →* C') :
ppcompose_left f ∘* (smash_adjoint_pmap A B C)⁻¹ᵉ* ~*
(smash_adjoint_pmap A B C')⁻¹ᵉ* ∘* ppcompose_left (ppcompose_left f) :=
begin
exact sorry
end
-- begin
-- refine _ ⬝* pwhisker_left _ !smash_functor_pid_pcompose⁻¹*,
-- refine !passoc⁻¹* ⬝* pwhisker_right _ _ ⬝* !passoc,
-- apply smash_pmap_counit_natural
-- end
/- associativity of smash -/
definition smash_assoc_elim_equiv (A B C X : Type*) :
ppmap (A ∧ (B ∧ C)) X ≃* ppmap ((A ∧ B) ∧ C) X :=
calc
ppmap (A ∧ (B ∧ C)) X ≃* ppmap (B ∧ C) (ppmap A X) : smash_adjoint_pmap A (B ∧ C) X
... ≃* ppmap C (ppmap B (ppmap A X)) : smash_adjoint_pmap B C (ppmap A X)
... ≃* ppmap C (ppmap (A ∧ B) X) : pequiv_ppcompose_left (smash_adjoint_pmap A B X)⁻¹ᵉ*
... ≃* ppmap ((A ∧ B) ∧ C) X : (smash_adjoint_pmap (A ∧ B) C X)⁻¹ᵉ*
definition smash_assoc_elim_equiv_fn (A B C X : Type*) (f : A ∧ (B ∧ C) →* X) :
(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_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
refine !smash_adjoint_pmap_inv_natural_pt ⬝* _,
apply smash_elim_phomotopy,
refine !passoc⁻¹* ⬝* _,
refine pwhisker_right _ !smash_adjoint_pmap_inv_natural ⬝* _,
refine !passoc ⬝* _,
apply pwhisker_left,
refine !smash_adjoint_pmap_natural_pt ⬝* _,
apply smash_elim_inv_phomotopy,
refine !smash_adjoint_pmap_natural_pt
end
definition smash_assoc_elim_natural {A B C X X' : Type*} (f : X →* X') :
ppcompose_left f ∘* smash_assoc_elim_equiv A B C X ~*
smash_assoc_elim_equiv A B C X' ∘* ppcompose_left f :=
begin
exact sorry
-- refine !smash_adjoint_pmap_inv_natural_pt ⬝* _,
-- apply smash_elim_phomotopy,
-- refine !passoc⁻¹* ⬝* _,
-- refine pwhisker_right _ !smash_adjoint_pmap_inv_natural ⬝* _,
-- refine !passoc ⬝* _,
-- apply pwhisker_left,
-- refine !smash_adjoint_pmap_natural_pt ⬝* _,
-- apply smash_elim_inv_phomotopy,
-- refine !smash_adjoint_pmap_natural_pt
end
-- definition smash_assoc (A B C : Type*) : A ∧ (B ∧ C) ≃* (A ∧ B) ∧ C :=
-- begin
-- fapply pequiv.MK,
-- { exact !smash_assoc_elim_equiv⁻¹ᵉ* !pid },
-- { exact !smash_assoc_elim_equiv !pid },
-- { },
-- { }
-- end
end smash

1
homotopy/smash_assoc.hlean
View file

@ -1,4 +1,5 @@
-- Authors: Floris van Doorn
-- In collaboration with Stefano, Robin
import .smash

4
homotopy/spectrum.hlean
View file

@ -320,8 +320,8 @@ namespace spectrum
| (n, fin.mk (k+3) H) := begin exfalso, apply lt_le_antisymm H, apply le_add_left end
local attribute ab_group_LES_of_shomotopy_groups [instance]
definition is_homomorphism_LES_of_shomotopy_groups :
Π(v : +3ℤ), is_homomorphism (cc_to_fn LES_of_shomotopy_groups v)
definition is_mul_hom_LES_of_shomotopy_groups :
Π(v : +3ℤ), is_mul_hom (cc_to_fn LES_of_shomotopy_groups v)
| (n, fin.mk 0 H) := proof homomorphism.struct (πₛ→[n] f) qed
| (n, fin.mk 1 H) := proof homomorphism.struct (πₛ→[n] (spoint f)) qed
| (n, fin.mk 2 H) := proof homomorphism.struct

274
move_to_lib.hlean
View file

@ -10,9 +10,15 @@ attribute pwedge pushout.symm pushout.equiv pushout.is_equiv_functor [constructo
attribute is_succ_add_right is_succ_add_left is_succ_bit0 [constructor]
attribute pushout.functor [unfold 16]
attribute pushout.transpose [unfold 6]
attribute ap_eq_apd10 [unfold 5]
attribute eq_equiv_eq_symm [constructor]
namespace eq
protected definition homotopy.rfl [reducible] [unfold_full] {A B : Type} {f : A → B} : f ~ f :=
homotopy.refl f
definition compose_id {A B : Type} (f : A → B) : f ∘ id ~ f :=
by reflexivity
@ -32,7 +38,15 @@ namespace eq
(r : q = idp) : ap_is_constant p q = ap02 f r ⬝ (con.right_inv (p a))⁻¹ :=
by cases r; exact !idp_con⁻¹
end eq
definition con_right_inv_natural {A : Type} {a a' : A} {p p' : a = a'} (q : p = p') :
con.right_inv p = q ◾ q⁻² ⬝ con.right_inv p' :=
by induction q; induction p; reflexivity
definition whisker_right_ap {A B : Type} {a a' : A}{b₁ b₂ b₃ : B} (q : b₂ = b₃) (f : A → b₁ = b₂)
(p : a = a') : whisker_right q (ap f p) = ap (λa, f a ⬝ q) p :=
by induction p; reflexivity
end eq open eq
namespace cofiber
@ -53,9 +67,13 @@ end wedge
namespace pointed
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
-- 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
@ -147,6 +165,207 @@ namespace pointed
(p : k ∘ f ~ g ∘ h) : h ∘ f⁻¹ᵉ ~ g⁻¹ᵉ ∘ k :=
λb, eq_inv_of_eq ((p (f⁻¹ᵉ b))⁻¹ ⬝ ap k (to_right_inv f b))
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 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 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 A with A a₀, induction B with B b₀,
induction f with f f₀, esimp at *, induction f₀,
reflexivity
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 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 ap (λx, x ⬝* _) !phomotopy_of_eq_of_phomotopy ⬝ 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 ap (λx, _ ⬝* x) (!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_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
end pointed open pointed
namespace trunc
@ -200,6 +419,9 @@ end is_equiv
namespace prod
definition pprod_functor [constructor] {A B C D : Type*} (f : A →* C) (g : B →* D) : A ×* B →* C ×* D :=
pmap.mk (prod_functor f g) (prod_eq (respect_pt f) (respect_pt g))
open prod.ops
definition prod_pathover_equiv {A : Type} {B C : A → Type} {a a' : A} (p : a = a')
(x : B a × C a) (x' : B a' × C a') : x =[p] x' ≃ x.1 =[p] x'.1 × x.2 =[p] x'.2 :=
@ -317,44 +539,40 @@ namespace group
-- some extra instances for type class inference
-- definition is_homomorphism_comm_homomorphism [instance] {G G' : AbGroup} (φ : G →g G')
-- : @is_homomorphism G G' (@ab_group.to_group _ (AbGroup.struct G))
-- definition is_mul_hom_comm_homomorphism [instance] {G G' : AbGroup} (φ : G →g G')
-- : @is_mul_hom G G' (@ab_group.to_group _ (AbGroup.struct G))
-- (@ab_group.to_group _ (AbGroup.struct G')) φ :=
-- homomorphism.struct φ
-- definition is_homomorphism_comm_homomorphism1 [instance] {G G' : AbGroup} (φ : G →g G')
-- : @is_homomorphism G G' _
-- definition is_mul_hom_comm_homomorphism1 [instance] {G G' : AbGroup} (φ : G →g G')
-- : @is_mul_hom G G' _
-- (@ab_group.to_group _ (AbGroup.struct G')) φ :=
-- homomorphism.struct φ
-- definition is_homomorphism_comm_homomorphism2 [instance] {G G' : AbGroup} (φ : G →g G')
-- : @is_homomorphism G G' (@ab_group.to_group _ (AbGroup.struct G)) _ φ :=
-- definition is_mul_hom_comm_homomorphism2 [instance] {G G' : AbGroup} (φ : G →g G')
-- : @is_mul_hom G G' (@ab_group.to_group _ (AbGroup.struct G)) _ φ :=
-- homomorphism.struct φ
end group open group
namespace pi -- move to types.arrow
namespace pointed -- move to types.pointed
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_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 :=
begin
cases f with f p, esimp [pmap_eq],
refine apd011 (apd011 pmap.mk) !eq_of_homotopy_idp _,
induction Y with Y y0, esimp at *, induction p, esimp, exact sorry
end
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
@ -373,7 +591,7 @@ namespace pi -- move to types.arrow
{ apply pmap_eq_idp}
end
end pi open pi
end pointed open pointed
namespace eq
@ -686,7 +904,7 @@ namespace category
theorem Group_eq_equiv_lemma {G H : Group}
(p : (Group.sigma_char2 G).1 = (Group.sigma_char2 H).1) :
((Group.sigma_char2 G).2 =[p] (Group.sigma_char2 H).2) ≃
(is_homomorphism (equiv_of_eq (proof p qed : Group.carrier G = Group.carrier H))) :=
(is_mul_hom (equiv_of_eq (proof p qed : Group.carrier G = Group.carrier H))) :=
begin
refine !sigma_pathover_equiv_of_is_prop ⬝e _,
induction G with G g, induction H with H h,
@ -697,7 +915,7 @@ namespace category
(Group.sigma_char2 (Group.mk G (group.mk μ σ μa ε εμ με ι μι))).2.2
end
definition isomorphism.sigma_char (G H : Group) : (G ≃g H) ≃ Σ(e : G ≃ H), is_homomorphism e :=
definition isomorphism.sigma_char (G H : Group) : (G ≃g H) ≃ Σ(e : G ≃ H), is_mul_hom e :=
begin
fapply equiv.MK,
{ intro φ, exact ⟨equiv_of_isomorphism φ, to_respect_mul φ⟩ },
@ -712,7 +930,7 @@ namespace category
refine !sigma_eq_equiv ⬝e _,
refine sigma_equiv_sigma_right Group_eq_equiv_lemma ⬝e _,
transitivity (Σ(e : (Group.sigma_char2 G).1 ≃ (Group.sigma_char2 H).1),
@is_homomorphism _ _ _ _ (to_fun e)), apply sigma_ua,
@is_mul_hom _ _ _ _ (to_fun e)), apply sigma_ua,
exact !isomorphism.sigma_char⁻¹ᵉ
end