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

define pmap in terms of ppi. Also move many facts about ppi to the standard library

Browse source
This commit is contained in:
Floris van Doorn 2017-07-21 15:55:27 +01:00
parent a6d621c6f3
commit 9a693f1ee3
18 changed files with 323 additions and 574 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

251
algebra/arrow_group.hlean
View file

@ -4,24 +4,132 @@ Released under Apache 2.0 license as described in the file LICENSE.
Authors: Floris van Doorn, Ulrik Buchholtz
Various groups of maps. Most importantly we define a group structure
on trunc 0 (A →* Ω B), which is used in the definition of cohomology.
on trunc 0 (A →* Ω B) and the dependent version trunc 0 (ppi _ _),
which are used in the definition of cohomology.
-/
import algebra.group_theory ..pointed ..pointed_pi eq2
open pi pointed algebra group eq equiv is_trunc trunc susp
namespace group
/- Group of dependent functions into a loop space -/
definition ppi_mul [constructor] {A : Type*} {B : A → Type*} (f g : Π*a, Ω (B a)) : Π*a, Ω (B a) :=
proof ppi.mk (λa, f a ⬝ g a) (respect_pt f ◾ respect_pt g ⬝ !idp_con) qed
definition ppi_inv [constructor] {A : Type*} {B : A → Type*} (f : Π*a, Ω (B a)) : Π*a, Ω (B a) :=
proof ppi.mk (λa, (f a)⁻¹ᵖ) (respect_pt f)⁻² qed
definition inf_group_ppi [constructor] [instance] {A : Type*} (B : A → Type*) :
inf_group (Π*a, Ω (B a)) :=
begin
fapply inf_group.mk,
{ exact ppi_mul },
{ intro f g h, apply eq_of_phomotopy, fapply phomotopy.mk,
{ intro a, exact con.assoc (f a) (g a) (h a) },
{ symmetry, rexact eq_of_square (con2_assoc (respect_pt f) (respect_pt g) (respect_pt h)) }},
{ apply ppi_const },
{ intros f, apply eq_of_phomotopy, fapply phomotopy.mk,
{ intro a, exact one_mul (f a) },
{ symmetry, apply eq_of_square, refine _ ⬝vp !ap_id, apply natural_square_tr }},
{ intros f, apply eq_of_phomotopy, fapply phomotopy.mk,
{ intro a, exact mul_one (f a) },
{ reflexivity }},
{ exact ppi_inv },
{ intro f, apply eq_of_phomotopy, fapply phomotopy.mk,
{ intro a, exact con.left_inv (f a) },
{ exact !con_left_inv_idp }},
end
definition group_trunc_ppi [constructor] [instance] {A : Type*} (B : A → Type*) :
group (trunc 0 (Π*a, Ω (B a))) :=
!trunc_group
definition Group_trunc_ppi [reducible] [constructor] {A : Type*} (B : A → Type*) : Group :=
Group.mk (trunc 0 (Π*a, Ω (B a))) _
definition ab_inf_group_ppi [constructor] [instance] {A : Type*} (B : A → Type*) :
ab_inf_group (Π*a, Ω (Ω (B a))) :=
⦃ab_inf_group, inf_group_ppi (λa, Ω (B a)), mul_comm :=
begin
intro f g, apply eq_of_phomotopy, fapply phomotopy.mk,
{ intro a, exact eckmann_hilton (f a) (g a) },
{ symmetry, rexact eq_of_square (eckmann_hilton_con2 (respect_pt f) (respect_pt g)) }
end⦄
definition ab_group_trunc_ppi [constructor] [instance] {A : Type*} (B : A → Type*) :
ab_group (trunc 0 (Π*a, Ω (Ω (B a)))) :=
!trunc_ab_group
definition AbGroup_trunc_ppi [reducible] [constructor] {A : Type*} (B : A → Type*) : AbGroup :=
AbGroup.mk (trunc 0 (Π*a, Ω (Ω (B a)))) _
definition trunc_ppi_isomorphic_pmap (A B : Type*)
: Group.mk (trunc 0 (Π*(a : A), Ω B)) !trunc_group
≃g Group.mk (trunc 0 (A →* Ω B)) !trunc_group :=
begin
apply trunc_isomorphism_of_equiv (pppi_equiv_pmap A (Ω B)),
intro h k, induction h with h h_pt, induction k with k k_pt, reflexivity
end
section
universe variables u v
variables {A : pType.{u}} {B : A → Type.{v}} {x₀ : B pt} {k l m : ppi B x₀}
definition phomotopy_of_eq_homomorphism (p : k = l) (q : l = m)
: phomotopy_of_eq (p ⬝ q) = phomotopy_of_eq p ⬝* phomotopy_of_eq q :=
begin
induction q, induction p, induction k with k q, induction q, reflexivity
end
protected definition ppi_mul_loop.lemma1 {X : Type} {x : X} (p q : x = x) (p_pt : idp = p) (q_pt : idp = q)
: refl (p ⬝ q) ⬝ whisker_left p q_pt⁻¹ ⬝ p_pt⁻¹ = p_pt⁻¹ ◾ q_pt⁻¹ :=
by induction p_pt; induction q_pt; reflexivity
protected definition ppi_mul_loop.lemma2 {X : Type} {x : X} (p q : x = x) (p_pt : p = idp) (q_pt : q = idp)
: refl (p ⬝ q) ⬝ whisker_left p q_pt ⬝ p_pt = p_pt ◾ q_pt :=
by rewrite [-(inv_inv p_pt),-(inv_inv q_pt)]; exact ppi_mul_loop.lemma1 p q p_pt⁻¹ q_pt⁻¹
definition ppi_mul_loop {h : Πa, B a} (f g : ppi.mk h idp ~* ppi.mk h idp) : f ⬝* g = ppi_mul f g :=
begin
apply ap (ppi.mk (λa, f a ⬝ g a)),
apply ppi.rec_on f, intros f' f_pt, apply ppi.rec_on g, intros g' g_pt,
clear f g, esimp at *, exact ppi_mul_loop.lemma2 (f' pt) (g' pt) f_pt g_pt
end
variable (k)
definition trunc_ppi_loop_isomorphism_lemma
: isomorphism.{(max u v) (max u v)}
(Group.mk (trunc 0 (k = k)) (@trunc_group (k = k) !inf_group_loop))
(Group.mk (trunc 0 (Π*(a : A), Ω (pType.mk (B a) (k a)))) !trunc_group) :=
begin
apply @trunc_isomorphism_of_equiv _ _ !inf_group_loop !inf_group_ppi (ppi_loop_equiv k),
intro f g, induction k with k p, induction p,
apply trans (phomotopy_of_eq_homomorphism f g),
exact ppi_mul_loop (phomotopy_of_eq f) (phomotopy_of_eq g)
end
end
definition trunc_ppi_loop_isomorphism {A : Type*} (B : A → Type*)
: Group.mk (trunc 0 (Ω (Π*(a : A), B a))) !trunc_group
≃g Group.mk (trunc 0 (Π*(a : A), Ω (B a))) !trunc_group :=
trunc_ppi_loop_isomorphism_lemma (ppi_const B)
/- We first define the group structure on A →* Ω B (except for truncatedness).
Instead of Ω B, we could also choose any infinity group. However, we need various 2-coherences,
so it's easier to just do it for the loop space. -/
definition pmap_mul [constructor] {A B : Type*} (f g : A →* Ω B) : A →* Ω B :=
pmap.mk (λa, f a ⬝ g a) (respect_pt f ◾ respect_pt g ⬝ !idp_con)
ppi_mul f g
definition pmap_inv [constructor] {A B : Type*} (f : A →* Ω B) : A →* Ω B :=
pmap.mk (λa, (f a)⁻¹ᵖ) (respect_pt f)⁻²
ppi_inv f
/- we prove some coherences of the multiplication. We don't need them for the group structure, but they
are used to show that cohomology satisfies the Eilenberg-Steenrod axioms -/
/- we prove some coherences of the multiplication. We don't need them for the group structure,
but they are used to show that cohomology satisfies the Eilenberg-Steenrod axioms -/
definition ap1_pmap_mul {X Y : Type*} (f g : X →* Ω Y) :
Ω→ (pmap_mul f g) ~* pmap_mul (Ω→ f) (Ω→ g) :=
begin
@ -63,24 +171,7 @@ namespace group
pwhisker_right _ !ap1_pmap_mul ⬝* !pmap_mul_pcompose
definition inf_group_pmap [constructor] [instance] (A B : Type*) : inf_group (A →* Ω B) :=
begin
fapply inf_group.mk,
{ exact pmap_mul },
{ intro f g h, fapply pmap_eq,
{ intro a, exact con.assoc (f a) (g a) (h a) },
{ rexact eq_of_square (con2_assoc (respect_pt f) (respect_pt g) (respect_pt h)) }},
{ apply pconst },
{ intros f, fapply pmap_eq,
{ intro a, exact one_mul (f a) },
{ esimp, apply eq_of_square, refine _ ⬝vp !ap_id, apply natural_square_tr }},
{ intros f, fapply pmap_eq,
{ intro a, exact mul_one (f a) },
{ reflexivity }},
{ exact pmap_inv },
{ intro f, fapply pmap_eq,
{ intro a, exact con.left_inv (f a) },
{ exact !con_left_inv_idp⁻¹ }},
end
!inf_group_ppi
definition group_trunc_pmap [constructor] [instance] (A B : Type*) : group (trunc 0 (A →* Ω B)) :=
!trunc_group
@ -94,9 +185,9 @@ namespace group
fapply homomorphism.mk,
{ apply trunc_functor, intro g, exact g ∘* f},
{ intro g h, induction g with g, induction h with h, apply ap tr,
fapply pmap_eq,
apply eq_of_phomotopy, fapply phomotopy.mk,
{ intro a, reflexivity },
{ refine _ ⬝ !idp_con⁻¹,
{ symmetry, refine _ ⬝ !idp_con⁻¹,
refine whisker_right _ !ap_con_fn ⬝ _, apply con2_con_con2 }}
end
@ -152,9 +243,9 @@ namespace group
ab_inf_group (A →* Ω (Ω B)) :=
⦃ab_inf_group, inf_group_pmap A (Ω B), mul_comm :=
begin
intro f g, fapply pmap_eq,
intro f g, apply eq_of_phomotopy, fapply phomotopy.mk,
{ intro a, exact eckmann_hilton (f a) (g a) },
{ rexact eq_of_square (eckmann_hilton_con2 (respect_pt f) (respect_pt g)) }
{ symmetry, rexact eq_of_square (eckmann_hilton_con2 (respect_pt f) (respect_pt g)) }
end⦄
definition ab_group_trunc_pmap [constructor] [instance] (A B : Type*) :
@ -195,110 +286,4 @@ namespace group
{ intro g h, apply eq_of_homotopy, intro a, exact respect_mul (f a) g h }
end
/- Group of dependent functions into a loop space -/
definition ppi_mul [constructor] {A : Type*} {B : A → Type*} (f g : Π*a, Ω (B a)) : Π*a, Ω (B a) :=
proof ppi.mk (λa, f a ⬝ g a) (ppi.resp_pt f ◾ ppi.resp_pt g ⬝ !idp_con) qed
definition ppi_inv [constructor] {A : Type*} {B : A → Type*} (f : Π*a, Ω (B a)) : Π*a, Ω (B a) :=
proof ppi.mk (λa, (f a)⁻¹ᵖ) (ppi.resp_pt f)⁻² qed
definition inf_group_ppi [constructor] [instance] {A : Type*} (B : A → Type*) :
inf_group (Π*a, Ω (B a)) :=
begin
fapply inf_group.mk,
{ exact ppi_mul },
{ intro f g h, apply ppi_eq, fapply ppi_homotopy.mk,
{ intro a, exact con.assoc (f a) (g a) (h a) },
{ symmetry, rexact eq_of_square (con2_assoc (ppi.resp_pt f) (ppi.resp_pt g) (ppi.resp_pt h)) }},
{ apply ppi_const },
{ intros f, apply ppi_eq, fapply ppi_homotopy.mk,
{ intro a, exact one_mul (f a) },
{ symmetry, apply eq_of_square, refine _ ⬝vp !ap_id, apply natural_square_tr }},
{ intros f, apply ppi_eq, fapply ppi_homotopy.mk,
{ intro a, exact mul_one (f a) },
{ reflexivity }},
{ exact ppi_inv },
{ intro f, apply ppi_eq, fapply ppi_homotopy.mk,
{ intro a, exact con.left_inv (f a) },
{ exact !con_left_inv_idp }},
end
definition group_trunc_ppi [constructor] [instance] {A : Type*} (B : A → Type*) :
group (trunc 0 (Π*a, Ω (B a))) :=
!trunc_group
definition Group_trunc_ppi [reducible] [constructor] {A : Type*} (B : A → Type*) : Group :=
Group.mk (trunc 0 (Π*a, Ω (B a))) _
definition ab_inf_group_ppi [constructor] [instance] {A : Type*} (B : A → Type*) :
ab_inf_group (Π*a, Ω (Ω (B a))) :=
⦃ab_inf_group, inf_group_ppi (λa, Ω (B a)), mul_comm :=
begin
intro f g, apply ppi_eq, fapply ppi_homotopy.mk,
{ intro a, exact eckmann_hilton (f a) (g a) },
{ symmetry, rexact eq_of_square (eckmann_hilton_con2 (ppi.resp_pt f) (ppi.resp_pt g)) }
end⦄
definition ab_group_trunc_ppi [constructor] [instance] {A : Type*} (B : A → Type*) :
ab_group (trunc 0 (Π*a, Ω (Ω (B a)))) :=
!trunc_ab_group
definition AbGroup_trunc_ppi [reducible] [constructor] {A : Type*} (B : A → Type*) : AbGroup :=
AbGroup.mk (trunc 0 (Π*a, Ω (Ω (B a)))) _
definition trunc_ppi_isomorphic_pmap (A B : Type*)
: Group.mk (trunc 0 (Π*(a : A), Ω B)) !trunc_group
≃g Group.mk (trunc 0 (A →* Ω B)) !trunc_group :=
begin
apply trunc_isomorphism_of_equiv (pppi_equiv_pmap A (Ω B)),
intro h k, induction h with h h_pt, induction k with k k_pt, reflexivity
end
section
universe variables u v
variables {A : pType.{u}} {B : A → Type.{v}} {x₀ : B pt} {k l m : ppi B x₀}
definition ppi_homotopy_of_eq_homomorphism (p : k = l) (q : l = m)
: ppi_homotopy_of_eq (p ⬝ q) = ppi_homotopy_of_eq p ⬝*' ppi_homotopy_of_eq q :=
begin
induction q, induction p, induction k with k q, induction q, reflexivity
end
protected definition ppi_mul_loop.lemma1 {X : Type} {x : X} (p q : x = x) (p_pt : idp = p) (q_pt : idp = q)
: refl (p ⬝ q) ⬝ whisker_left p q_pt⁻¹ ⬝ p_pt⁻¹ = p_pt⁻¹ ◾ q_pt⁻¹ :=
by induction p_pt; induction q_pt; reflexivity
protected definition ppi_mul_loop.lemma2 {X : Type} {x : X} (p q : x = x) (p_pt : p = idp) (q_pt : q = idp)
: refl (p ⬝ q) ⬝ whisker_left p q_pt ⬝ p_pt = p_pt ◾ q_pt :=
by rewrite [-(inv_inv p_pt),-(inv_inv q_pt)]; exact ppi_mul_loop.lemma1 p q p_pt⁻¹ q_pt⁻¹
definition ppi_mul_loop {h : Πa, B a} (f g : ppi.mk h idp ~~* ppi.mk h idp) : f ⬝*' g = ppi_mul f g :=
begin
apply ap (ppi.mk (λa, f a ⬝ g a)),
apply ppi.rec_on f, intros f' f_pt, apply ppi.rec_on g, intros g' g_pt,
clear f g, esimp at *, exact ppi_mul_loop.lemma2 (f' pt) (g' pt) f_pt g_pt
end
variable (k)
definition trunc_ppi_loop_isomorphism_lemma
: isomorphism.{(max u v) (max u v)}
(Group.mk (trunc 0 (k = k)) (@trunc_group (k = k) !inf_group_loop))
(Group.mk (trunc 0 (Π*(a : A), Ω (pType.mk (B a) (k a)))) !trunc_group) :=
begin
apply @trunc_isomorphism_of_equiv _ _ !inf_group_loop !inf_group_ppi (ppi_loop_equiv k),
intro f g, induction k with k p, induction p,
apply trans (ppi_homotopy_of_eq_homomorphism f g),
exact ppi_mul_loop (ppi_homotopy_of_eq f) (ppi_homotopy_of_eq g)
end
end
definition trunc_ppi_loop_isomorphism {A : Type*} (B : A → Type*)
: Group.mk (trunc 0 (Ω (Π*(a : A), B a))) !trunc_group
≃g Group.mk (trunc 0 (Π*(a : A), Ω (B a))) !trunc_group :=
trunc_ppi_loop_isomorphism_lemma (ppi_const B)
end group

12
algebra/cogroup.hlean
View file

@ -16,17 +16,17 @@ section
apply equiv.MK (λ f, (ppr1 ∘* f, ppr2 ∘* f))
(λ w, prod.elim w prod.pair_pmap),
{ intro p, induction p with f g, apply pair_eq,
{ fapply pmap_eq,
{ apply eq_of_phomotopy, fapply phomotopy.mk,
{ intro x, reflexivity },
{ apply trans (prod_eq_pr1 (respect_pt f) (respect_pt g)),
{ symmetry, apply trans (prod_eq_pr1 (respect_pt f) (respect_pt g)),
apply inverse, apply idp_con } },
{ fapply pmap_eq,
{ apply eq_of_phomotopy, fapply phomotopy.mk,
{ intro x, reflexivity },
{ apply trans (prod_eq_pr2 (respect_pt f) (respect_pt g)),
{ symmetry, apply trans (prod_eq_pr2 (respect_pt f) (respect_pt g)),
apply inverse, apply idp_con } } },
{ intro f, fapply pmap_eq,
{ intro f, apply eq_of_phomotopy, fapply phomotopy.mk,
{ intro x, apply prod.eta },
{ exact prod.pair_eq_eta (respect_pt f) } }
{ symmetry, exact prod.pair_eq_eta (respect_pt f) } }
end
-- since ~* is the identity type of pointed maps,

6
cohomology/serre.hlean
View file

@ -111,11 +111,11 @@ definition postnikov_smap_postnikov_map (A : spectrum) (n k l : ℤ) (p : n + k
(ptrunc_maxm2_change_int p (A k)) (ptrunc_maxm2_pred (A k) (ap pred p⁻¹ ⬝ add.right_comm n k (- 1))) :=
begin
cases l with l,
{ cases l with l, apply phomotopy_of_is_contr_cod, apply is_contr_ptrunc_minus_one,
{ cases l with l, apply phomotopy_of_is_contr_cod_pmap, apply is_contr_ptrunc_minus_one,
refine psquare_postnikov_map_ptrunc_elim (A k) _ _ _ ⬝hp* _,
exact ap maxm2 (add.right_comm n (- 1) k ⬝ ap pred p ⬝ !pred_succ),
apply ptrunc_maxm2_pred_nat },
{ apply phomotopy_of_is_contr_cod, apply is_trunc_trunc }
{ apply phomotopy_of_is_contr_cod_pmap, apply is_trunc_trunc }
end
definition sfiber_postnikov_smap_pequiv (A : spectrum) (n : ℤ) (k : ℤ) :
@ -148,7 +148,7 @@ section atiyah_hirzebruch
(ppi_pequiv_right (λx, ptrunc_pequiv_ptrunc_of_is_trunc _ _ (H x n))) _,
{ intro x, apply maxm2_monotone, apply add_le_add_right, exact le.trans !le_add_one Hs },
{ intro x, apply maxm2_monotone, apply add_le_add_right, exact le_sub_one_of_lt Hs },
intro f, apply eq_of_ppi_homotopy,
intro f, apply eq_of_phomotopy,
apply pmap_compose_ppi_phomotopy_left, intro x,
fapply phomotopy.mk,
{ refine @trunc.rec _ _ _ _ _,

4
colim.hlean
View file

@ -246,7 +246,7 @@ namespace seq_colim
begin
fapply pequiv_of_equiv,
{ apply shift_equiv },
{ exact ap (ι _) !respect_pt }
{ exact ap (ι _) (respect_pt (f 0)) }
end
definition pshift_equiv_pinclusion {A : ℕ → Type*} (f : Πn, A n →* A (succ n)) (n : ℕ) :
@ -356,7 +356,7 @@ namespace seq_colim
xrewrite[-IH],
rewrite[-+ap_compose', -+con.assoc],
apply whisker_right, esimp,
rewrite[(eq_con_inv_of_con_eq (!to_homotopy_pt))],
rewrite[(eq_con_inv_of_con_eq (to_homotopy_pt (@p _)))],
rewrite[ap_con], esimp,
rewrite[-+con.assoc, ap_con, -ap_compose', +ap_inv],
rewrite[-+con.assoc],

14
homology/basic.hlean
View file

@ -56,7 +56,12 @@ namespace homology
calc Hh theory n f x
= Hh theory n (pmap.mk f (respect_pt f)) x : by exact ap (λ f, Hh theory n f x) (pmap.eta f)⁻¹
... = Hh theory n (pmap.mk f (h pt ⬝ respect_pt g)) x : by exact Hh_homotopy' n f (respect_pt f) (h pt ⬝ respect_pt g) x
... = Hh theory n g x : by exact ap (λ f, Hh theory n f x) (@pmap_eq _ _ (pmap.mk f (h pt ⬝ respect_pt g)) _ h (refl (h pt ⬝ respect_pt g)))
... = Hh theory n g x :
begin
apply ap (λ f, Hh theory n f x), apply eq_of_phomotopy, fapply phomotopy.mk,
{ exact h },
reflexivity
end
definition HH_isomorphism (n : ℤ) {A B : Type*} (e : A ≃* B)
: HH theory n A ≃g HH theory n B :=
@ -175,12 +180,9 @@ definition homology_functor [constructor] {X Y : Type*} {E F : prespectrum} (f :
(g : E →ₛ F) (n : ℤ) : homology X E n →g homology Y F n :=
pshomotopy_group_fun n (smash_prespectrum_fun f g)
print is_exact_g
print is_exact
definition homology_theory_spectrum_is_exact.{u} (E : spectrum.{u}) (n : ℤ) {X Y : Type*} (f : X →* Y) :
is_exact_g (homology_functor f (sid E) n) (homology_functor (pcod f) (sid E) n) :=
definition homology_theory_spectrum_is_exact.{u} (E : spectrum.{u}) (n : ℤ) {X Y : Type*}
(f : X →* Y) : is_exact_g (homology_functor f (sid E) n) (homology_functor (pcod f) (sid E) n) :=
begin
esimp [is_exact_g],
-- fconstructor,
-- { intro a, exact sorry },
-- { intro a, exact sorry }

8
homotopy/EM.hlean
View file

@ -585,12 +585,14 @@ namespace EM
/- fiber of EM_functor -/
open fiber
definition is_trunc_fiber_EM1_functor {G H : Group} (φ : G →g H) : is_trunc 1 (pfiber (EM1_functor φ)) :=
definition is_trunc_fiber_EM1_functor {G H : Group} (φ : G →g H) :
is_trunc 1 (pfiber (EM1_functor φ)) :=
!is_trunc_fiber
definition is_conn_fiber_EM1_functor {G H : Group} (φ : G →g H) : is_conn -1 (pfiber (EM1_functor φ)) :=
definition is_conn_fiber_EM1_functor {G H : Group} (φ : G →g H) :
is_conn -1 (pfiber (EM1_functor φ)) :=
begin
apply is_conn_fiber, apply is_conn_of_is_conn_succ
apply is_conn_fiber
end
definition is_trunc_fiber_EMadd1_functor {G H : AbGroup} (φ : G →g H) (n : ℕ) :

10
homotopy/degree.hlean
View file

@ -79,7 +79,7 @@ namespace sphere
-- (pair 1 2))
-- (tr surf))
definition πnSn_surf (n : ℕ) : πnSn n (tr surf) = 1 :> ℤ :=
definition πnSn_surf (n : ℕ) : πnSn (n+1) (tr surf) = 1 :> ℤ :=
begin
cases n with n IH,
{ refine ap (πnSn _ ∘ tr) surf_eq_loop ⬝ _, apply transport_code_loop },
@ -87,17 +87,17 @@ namespace sphere
end
definition deg {n : ℕ} [H : is_succ n] (f : S n →* S n) : ℤ :=
by induction H with n; exact πnSn n (π→g[n+1] f (tr surf))
by induction H with n; exact πnSn (n+1) (π→g[n+1] f (tr surf))
definition deg_id (n : ℕ) [H : is_succ n] : deg (pid (S n)) = (1 : ℤ) :=
by induction H with n;
exact ap (πnSn n) (homotopy_group_functor_pid (succ n) (S (succ n)) (tr surf)) ⬝ πnSn_surf n
exact ap (πnSn (n+1)) (homotopy_group_functor_pid (succ n) (S (succ n)) (tr surf)) ⬝ πnSn_surf n
definition deg_phomotopy {n : ℕ} [H : is_succ n] {f g : S n →* S n} (p : f ~* g) :
deg f = deg g :=
begin
induction H with n,
exact ap (πnSn n) (homotopy_group_functor_phomotopy (succ n) p (tr surf)),
exact ap (πnSn (n+1)) (homotopy_group_functor_phomotopy (succ n) p (tr surf)),
end
definition endomorphism_int (f : gℤ →g gℤ) (n : ℤ) : f n = f (1 : ℤ) *[ℤ] n :=
@ -119,7 +119,7 @@ namespace sphere
deg (g ∘* f) = deg g *[ℤ] deg f :=
begin
induction H with n,
refine ap (πnSn n) (homotopy_group_functor_compose (succ n) g f (tr surf)) ⬝ _,
refine ap (πnSn (n+1)) (homotopy_group_functor_compose (succ n) g f (tr surf)) ⬝ _,
apply endomorphism_equiv_Z !πnSn !πnSn_surf (π→g[n+1] g)
end

6
homotopy/fwedge.hlean
View file

@ -96,7 +96,7 @@ namespace fwedge
definition fwedge_pmap [constructor] {I : Type} {F : I → Type*} {X : Type*} (f : Πi, F i →* X) : ⋁F →* X :=
begin
fconstructor,
fapply pmap.mk,
{ intro x, induction x,
exact f i x,
exact pt,
@ -205,9 +205,9 @@ namespace fwedge
definition fwedge_pmap_nat_square {A B X Y : Type*} (f : X →* Y) :
hsquare (fwedge_pmap_equiv (bool.rec A B) X)⁻¹ᵉ (fwedge_pmap_equiv (bool.rec A B) Y)⁻¹ᵉ (left_comp_pi_bool_funct f) (pcompose f) :=
begin
intro h, esimp, fapply pmap_eq,
intro h, esimp, fapply eq_of_phomotopy, fapply phomotopy.mk,
exact fwedge_pmap_nat₂ (λ u, bool.rec A B u) f h,
esimp,
reflexivity
end
-- hsquare 3:

2
homotopy/realprojective.hlean
View file

@ -3,7 +3,7 @@
import homotopy.join
open eq nat susp pointed pmap sigma is_equiv equiv fiber is_trunc trunc
open eq nat susp pointed sigma is_equiv equiv fiber is_trunc trunc
trunc_index is_conn bool unit join pushout
definition of_is_contr (A : Type) : is_contr A → A := @center A

20
homotopy/smash.hlean
View file

@ -228,8 +228,8 @@ namespace smash
definition smash_functor_phomotopy {f f' : A →* C} {g g' : B →* D}
(h₁ : f ~* f') (h₂ : g ~* g') : f ∧→ g ~* f' ∧→ g' :=
begin
induction h₁ using phomotopy_rec_on_idp,
induction h₂ using phomotopy_rec_on_idp,
induction h₁ using phomotopy_rec_idp,
induction h₂ using phomotopy_rec_idp,
reflexivity
end
@ -265,13 +265,13 @@ namespace smash
definition smash_functor_phomotopy_refl (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
!phomotopy_rec_idp_refl ⬝ !phomotopy_rec_idp_refl
definition smash_functor_phomotopy_symm {f₁ f₂ : A →* C} {g₁ g₂ : B →* D}
(h : f₁ ~* f₂) (k : g₁ ~* g₂) :
smash_functor_phomotopy h⁻¹* k⁻¹* = (smash_functor_phomotopy h k)⁻¹* :=
begin
induction h using phomotopy_rec_on_idp, induction k using phomotopy_rec_on_idp,
induction h using phomotopy_rec_idp, induction k using phomotopy_rec_idp,
exact ap011 smash_functor_phomotopy !refl_symm !refl_symm ⬝ !smash_functor_phomotopy_refl ⬝
!refl_symm⁻¹ ⬝ !smash_functor_phomotopy_refl⁻¹⁻²**
end
@ -281,8 +281,8 @@ namespace smash
smash_functor_phomotopy (h₁ ⬝* h₂) (k₁ ⬝* k₂) =
smash_functor_phomotopy h₁ k₁ ⬝* smash_functor_phomotopy h₂ k₂ :=
begin
induction h₁ using phomotopy_rec_on_idp, induction h₂ using phomotopy_rec_on_idp,
induction k₁ using phomotopy_rec_on_idp, induction k₂ using phomotopy_rec_on_idp,
induction h₁ using phomotopy_rec_idp, induction h₂ using phomotopy_rec_idp,
induction k₁ using phomotopy_rec_idp, induction k₂ using phomotopy_rec_idp,
refine ap011 smash_functor_phomotopy !trans_refl !trans_refl ⬝ !trans_refl⁻¹ ⬝ idp ◾** _,
exact !smash_functor_phomotopy_refl⁻¹
end
@ -310,7 +310,7 @@ namespace smash
(p : g ~* g') : ap (smash_functor f) (eq_of_phomotopy p) =
eq_of_phomotopy (smash_functor_phomotopy phomotopy.rfl p) :=
begin
induction p using phomotopy_rec_on_idp,
induction p using phomotopy_rec_idp,
refine ap02 _ !eq_of_phomotopy_refl ⬝ _,
refine !eq_of_phomotopy_refl⁻¹ ⬝ _,
apply ap eq_of_phomotopy,
@ -397,8 +397,8 @@ namespace smash
(smash_functor_phomotopy (h₂ ◾* h₁) (k₂ ◾* k₁))
(smash_functor_phomotopy h₂ k₂ ◾* smash_functor_phomotopy h₁ k₁) :=
begin
induction h₁ using phomotopy_rec_on_idp, induction h₂ using phomotopy_rec_on_idp,
induction k₁ using phomotopy_rec_on_idp, induction k₂ using phomotopy_rec_on_idp,
induction h₁ using phomotopy_rec_idp, induction h₂ using phomotopy_rec_idp,
induction k₁ using phomotopy_rec_idp, induction k₂ using phomotopy_rec_idp,
refine (ap011 smash_functor_phomotopy !pcompose2_refl !pcompose2_refl ⬝
!smash_functor_phomotopy_refl) ⬝ph** phvrfl ⬝hp**
(ap011 pcompose2 !smash_functor_phomotopy_refl !smash_functor_phomotopy_refl ⬝
@ -457,7 +457,7 @@ namespace smash
smash_functor_phomotopy p (phomotopy.refl (pconst B D)) ⬝* smash_functor_pconst_right f' =
smash_functor_pconst_right f :=
begin
induction p using phomotopy_rec_on_idp,
induction p using phomotopy_rec_idp,
exact !smash_functor_phomotopy_refl ◾** idp ⬝ !refl_trans
end

4
homotopy/smash_adjoint.hlean
View file

@ -305,7 +305,7 @@ namespace smash
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,
induction p using phomotopy_rec_idp,
refine ap02 _ !eq_of_phomotopy_refl ⬝ _,
refine !eq_of_phomotopy_refl⁻¹ ⬝ _,
apply ap eq_of_phomotopy,
@ -316,7 +316,7 @@ namespace smash
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,
induction p using phomotopy_rec_idp,
refine ap02 _ !eq_of_phomotopy_refl ⬝ _,
refine !eq_of_phomotopy_refl⁻¹ ⬝ _,
apply ap eq_of_phomotopy,

6
homotopy/wedge.hlean
View file

@ -28,8 +28,10 @@ namespace wedge
exact ap_compose wedge_flip' _ _ ⬝ ap02 _ !elim_glue ⬝ !ap_inv ⬝ !elim_glue⁻² ⬝ !inv_inv }
end
definition wedge_flip_wedge_flip (A B : Type*) : wedge_flip B A ∘* wedge_flip A B ~* pid (A ∨ B) :=
phomotopy.mk wedge_flip'_wedge_flip' (whisker_right _ (!ap_inv ⬝ !wedge.elim_glue⁻²) ⬝ !con.left_inv)⁻¹
definition wedge_flip_wedge_flip (A B : Type*) :
wedge_flip B A ∘* wedge_flip A B ~* pid (A ∨ B) :=
phomotopy.mk wedge_flip'_wedge_flip'
proof (whisker_right _ (!ap_inv ⬝ !wedge.elim_glue⁻²) ⬝ !con.left_inv)⁻¹ qed
definition wedge_comm [constructor] (A B : Type*) : A ∨ B ≃* B ∨ A :=
begin

35
move_to_lib.hlean
View file

@ -2,7 +2,7 @@
import homotopy.sphere2 homotopy.cofiber homotopy.wedge hit.prop_trunc hit.set_quotient eq2 types.pointed2
open eq nat int susp pointed pmap sigma is_equiv equiv fiber algebra trunc pi group
open eq nat int susp pointed sigma is_equiv equiv fiber algebra trunc pi group
is_trunc function unit prod bool
attribute pType.sigma_char sigma_pi_equiv_pi_sigma sigma.coind_unc [constructor]
@ -149,31 +149,6 @@ namespace eq
{D : Π⦃a⦄ ⦃b : B a⦄, C a b → Type} {f : Πa b (c : C a b), D c} : f ~3 f :=
λa b c, idp
definition homotopy.rec_idp [recursor] {A : Type} {P : A → Type} {f : Πa, P a}
(Q : Π{g}, (f ~ g) → Type) (H : Q (homotopy.refl f)) {g : Π x, P x} (p : f ~ g) : Q p :=
homotopy.rec_on_idp p H
open funext
definition homotopy_rec_on_apd10 {A : Type} {P : A → Type} {f g : Πa, P a}
(Q : f ~ g → Type) (H : Π(q : f = g), Q (apd10 q)) (p : f = g) :
homotopy.rec_on (apd10 p) H = H p :=
begin
unfold [homotopy.rec_on],
refine ap (λp, p ▸ _) !adj ⬝ _,
refine !tr_compose⁻¹ ⬝ _,
apply apdt
end
definition homotopy_rec_idp_refl {A : Type} {P : A → Type} {f : Πa, P a}
(Q : Π{g}, f ~ g → Type) (H : Q homotopy.rfl) :
homotopy.rec_idp @Q H homotopy.rfl = H :=
!homotopy_rec_on_apd10
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 eq_tr_of_pathover_con_tr_eq_of_pathover {A : Type} {B : A → Type}
{a₁ a₂ : A} (p : a₁ = a₂) {b₁ : B a₁} {b₂ : B a₂} (q : b₁ =[p] b₂) :
eq_tr_of_pathover q ⬝ tr_eq_of_pathover q⁻¹ᵒ = idp :=
@ -963,16 +938,16 @@ notation `Ω⇒`:(max+5) := ap1_phomotopy
definition ap1_phomotopy_symm {A B : Type*} {f g : A →* B} (p : f ~* g) : (Ω⇒ p)⁻¹* = Ω⇒ (p⁻¹*) :=
begin
induction p using phomotopy_rec_on_idp,
induction p using phomotopy_rec_idp,
rewrite ap1_phomotopy_refl,
rewrite [+refl_symm],
xrewrite [+refl_symm],
rewrite ap1_phomotopy_refl
end
definition ap1_phomotopy_trans {A B : Type*} {f g h : A →* B} (q : g ~* h) (p : f ~* g) : Ω⇒ (p ⬝* q) = Ω⇒ p ⬝* Ω⇒ q :=
begin
induction p using phomotopy_rec_on_idp,
induction q using phomotopy_rec_on_idp,
induction p using phomotopy_rec_idp,
induction q using phomotopy_rec_idp,
rewrite trans_refl,
rewrite [+ap1_phomotopy_refl],
rewrite trans_refl

23
pointed.hlean
View file

@ -33,10 +33,6 @@ namespace pointed
-- 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
/- remove some duplicates: loop_ppmap_commute, loop_ppmap_pequiv, loop_ppmap_pequiv', pfunext -/
definition pfunext (X Y : Type*) : ppmap X (Ω Y) ≃* Ω (ppmap X Y) :=
(loop_ppmap_commute X Y)⁻¹ᵉ*
@ -130,11 +126,11 @@ namespace pointed
(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 :=
definition phomotopy' {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
definition phomotopy2' {A : Type*} {P : A → Type} {x : P pt} {f g : ppi' A P x}
(p q : phomotopy' f g) : Type :=
phomotopy' p q
-- infix ` ~*2 `:50 := phomotopy2
@ -145,7 +141,7 @@ namespace pointed
/- Homotopy between a function and its eta expansion -/
definition pmap_eta {X Y : Type*} (f : X →* Y) : f ~* pmap.mk f (pmap.resp_pt f) :=
definition pmap_eta {X Y : Type*} (f : X →* Y) : f ~* pmap.mk f (respect_pt f) :=
begin
fapply phomotopy.mk,
reflexivity,
@ -219,15 +215,6 @@ namespace pointed
definition loop_punit : Ω punit ≃* punit :=
loop_pequiv_punit_of_is_set punit
definition phomotopy_of_is_contr_cod [constructor] {X Y : Type*} (f g : X →* Y) [is_contr Y] :
f ~* g :=
phomotopy.mk (λa, !eq_of_is_contr) !eq_of_is_contr
definition phomotopy_of_is_contr_dom [constructor] {X Y : Type*} (f g : X →* Y) [is_contr X] :
f ~* g :=
phomotopy.mk (λa, ap f !is_prop.elim ⬝ respect_pt f ⬝ (respect_pt g)⁻¹ ⬝ ap g !is_prop.elim)
begin rewrite [▸*, is_prop_elim_self, +ap_idp, idp_con, con_idp, inv_con_cancel_right] end
definition add_point_over [unfold 3] {A : Type} (B : A → Type*) : A₊ → Type*
| (some a) := B a
| none := plift punit

20
pointed_cubes.hlean
View file

@ -16,22 +16,22 @@ open eq pointed
definition psquare_of_phtpy_top {A B C D : Type*} {ftop : A →* B} {fbot : C →* D} {fleft : A →* C} {fright : B →* D} {ftop' : A →* B} (phtpy : ftop ~* ftop') (psq : psquare ftop' fbot fleft fright) : psquare ftop fbot fleft fright :=
begin
induction phtpy using phomotopy_rec_on_idp, exact psq,
induction phtpy using phomotopy_rec_idp, exact psq,
end
definition psquare_of_phtpy_bot {A B C D : Type*} {ftop : A →* B} {fbot : C →* D} {fleft : A →* C} {fright : B →* D} {fbot' : C →* D} (phtpy : fbot ~* fbot') (psq : psquare ftop fbot' fleft fright) : psquare ftop fbot fleft fright :=
begin
induction phtpy using phomotopy_rec_on_idp, exact psq,
induction phtpy using phomotopy_rec_idp, exact psq,
end
definition psquare_of_phtpy_left {A B C D : Type*} {ftop : A →* B} {fbot : C →* D} {fleft : A →* C} {fright : B →* D} {fleft' : A →* C} (phtpy : fleft ~* fleft') (psq : psquare ftop fbot fleft fright) : psquare ftop fbot fleft' fright :=
begin
induction phtpy using phomotopy_rec_on_idp, exact psq,
induction phtpy using phomotopy_rec_idp, exact psq,
end
definition psquare_of_phtpy_right {A B C D : Type*} {ftop : A →* B} {fbot : C →* D} {fleft : A →* C} {fright : B →* D} {fright' : B →* D} (phtpy : fright ~* fright') (psq : psquare ftop fbot fleft fright) : psquare ftop fbot fleft fright' :=
begin
induction phtpy using phomotopy_rec_on_idp, exact psq,
induction phtpy using phomotopy_rec_idp, exact psq,
end
definition psquare_of_pid_top_bot {A B : Type*} {fleft : A →* B} {fright : A →* B} (phtpy : fright ~* fleft) : psquare (pid A) (pid B) fleft fright :=
@ -91,8 +91,8 @@ begin
exact (pconst_pcompose fleft)⁻¹*,
end
definition phsquare_of_ppi_homotopy {A B : Type*} {f g h i : A →* B} {phtpy_top : f ~* g} {phtpy_bot : h ~* i} {phtpy_left : f ~* h} {phtpy_right : g ~* i} (H : phtpy_top ⬝* phtpy_right ~~* phtpy_left ⬝* phtpy_bot) : phsquare phtpy_top phtpy_bot phtpy_left phtpy_right :=
eq_of_ppi_homotopy H
definition phsquare_of_phomotopy {A B : Type*} {f g h i : A →* B} {phtpy_top : f ~* g} {phtpy_bot : h ~* i} {phtpy_left : f ~* h} {phtpy_right : g ~* i} (H : phtpy_top ⬝* phtpy_right ~* phtpy_left ⬝* phtpy_bot) : phsquare phtpy_top phtpy_bot phtpy_left phtpy_right :=
eq_of_phomotopy H
definition ptube_v {A B C D : Type*} {ftop ftop' : A →* B} (phtpy_top : ftop ~* ftop') {fbot fbot' : C →* D} (phtpy_bot : fbot ~* fbot') {fleft : A →* C} {fright : B →* D} (psq_back : psquare ftop fbot fleft fright) (psq_front : psquare ftop' fbot' fleft fright) : Type :=
phsquare (pwhisker_left fright phtpy_top) (pwhisker_right fleft phtpy_bot) psq_back psq_front
@ -127,7 +127,7 @@ structure p2homotopy {A B : Type*} {f g : A →* B} (H K : f ~* g) : Type :=
definition ptube_v_phtpy_bot {A B C D : Type*}
{ftop ftop' : A →* B} {phtpy_top : ftop ~* ftop'}
{fbot fbot' : C →* D} {phtpy_bot phtpy_bot' : fbot ~* fbot'} (ppi_htpy_bot : phtpy_bot ~~* phtpy_bot')
{fbot fbot' : C →* D} {phtpy_bot phtpy_bot' : fbot ~* fbot'} (ppi_htpy_bot : phtpy_bot ~* phtpy_bot')
{fleft : A →* C} {fright : B →* D}
{psq_back : psquare ftop fbot fleft fright}
{psq_front : psquare ftop' fbot' fleft fright}
@ -135,7 +135,7 @@ definition ptube_v_phtpy_bot {A B C D : Type*}
: ptube_v phtpy_top phtpy_bot' psq_back psq_front
:=
begin
induction ppi_htpy_bot using ppi_homotopy_rec_on_idp,
induction ppi_htpy_bot using phomotopy_rec_idp,
exact ptb,
end
@ -156,6 +156,6 @@ definition ptube_v_left_inv {A B C D : Type*} {ftop : A ≃* B} {fbot : C ≃* D
begin
refine ptube_v_phtpy_bot _ _,
exact pleft_inv fbot,
exact ppi_homotopy.rfl,
fapply phsquare_of_ppi_homotopy, repeat exact sorry,
exact phomotopy.rfl,
fapply phsquare_of_phomotopy, repeat exact sorry,
end

437
pointed_pi.hlean
View file

@ -283,7 +283,7 @@ namespace pointed
(h₃ : squareover B₂ (square_of_eq (to_homotopy_pt h₁)⁻¹) p₁ p₂ (h₂ b₁) idpo) :
psigma_gen_functor f₁ g₁ p₁ ~* psigma_gen_functor f₂ g₂ p₂ :=
begin
induction h₁ using phomotopy_rec_on_idp,
induction h₁ using phomotopy_rec_idp,
fapply phomotopy.mk,
{ intro x, induction x with a b, exact ap (dpair (f₁ a)) (eq_of_pathover_idp (h₂ b)) },
{ induction f₁ with f f₀, induction A₂ with A₂ a₂₀, esimp at * ⊢,
@ -330,260 +330,49 @@ namespace pointed
ppi (λx, f x = g x) (respect_pt f ⬝ (respect_pt g)⁻¹) :=
h
abbreviation pppi_resp_pt [unfold 3] := @pppi.resp_pt
definition ppi_homotopy {A : Type*} {P : A → Type} {x : P pt} (f g : ppi P x) : Type :=
ppi (λa, f a = g a) (ppi.resp_pt f ⬝ (ppi.resp_pt g)⁻¹)
definition phomotopy {A : Type*} {P : A → Type} {x : P pt} (f g : ppi P x) : Type :=
ppi (λa, f a = g a) (respect_pt f ⬝ (respect_pt g)⁻¹)
variables {A : Type*} {P Q R : A → Type*} {f g h : Π*a, P a}
{B C D : A → Type} {b₀ : B pt} {c₀ : C pt} {d₀ : D pt}
{k k' l m : ppi B b₀}
infix ` ~~* `:50 := ppi_homotopy
definition ppi_homotopy.mk [constructor] [reducible] (h : k ~ l)
(p : h pt ⬝ ppi.resp_pt l = ppi.resp_pt k) : k ~~* l :=
ppi.mk h (eq_con_inv_of_con_eq p)
definition ppi_to_homotopy [coercion] [unfold 6] [reducible] (p : k ~~* l) : Πa, k a = l a := p
definition ppi_to_homotopy_pt [unfold 6] [reducible] (p : k ~~* l) :
p pt ⬝ ppi.resp_pt l = ppi.resp_pt k :=
con_eq_of_eq_con_inv (ppi.resp_pt p)
variable (k)
protected definition ppi_homotopy.refl [constructor] : k ~~* k :=
ppi_homotopy.mk homotopy.rfl !idp_con
variable {k}
protected definition ppi_homotopy.rfl [constructor] [refl] : k ~~* k :=
ppi_homotopy.refl k
protected definition ppi_homotopy.symm [constructor] [symm] (p : k ~~* l) : l ~~* k :=
ppi_homotopy.mk p⁻¹ʰᵗʸ (inv_con_eq_of_eq_con (ppi_to_homotopy_pt p)⁻¹)
protected definition ppi_homotopy.trans [constructor] [trans] (p : k ~~* l) (q : l ~~* m) :
k ~~* m :=
ppi_homotopy.mk (λa, p a ⬝ q a) (!con.assoc ⬝ whisker_left (p pt) (ppi_to_homotopy_pt q) ⬝ ppi_to_homotopy_pt p)
infix ` ⬝*' `:75 := ppi_homotopy.trans
postfix `⁻¹*'`:(max+1) := ppi_homotopy.symm
definition ppi_trans2 {p p' : k ~~* l} {q q' : l ~~* m}
(r : p = p') (s : q = q') : p ⬝*' q = p' ⬝*' q' :=
ap011 ppi_homotopy.trans r s
definition ppi_symm2 {p p' : k ~~* l} (r : p = p') : p⁻¹*' = p'⁻¹*' :=
ap ppi_homotopy.symm r
infixl ` ◾**' `:80 := ppi_trans2
postfix `⁻²**'`:(max+1) := ppi_symm2
definition pppi_equiv_pmap [constructor] (A B : Type*) : (Π*(a : A), B) ≃ (A →* B) :=
begin
fapply equiv.MK,
{ intro k, induction k with k p, exact pmap.mk k p },
{ intro k, induction k with k p, exact pppi.mk k p },
{ intro k, induction k with k p, reflexivity },
{ intro k, induction k with k p, reflexivity }
end
by reflexivity
definition pppi_pequiv_ppmap [constructor] (A B : Type*) : (Π*(a : A), B) ≃* ppmap A B :=
pequiv_of_equiv (pppi_equiv_pmap A B) idp
by reflexivity
protected definition ppi.sigma_char [constructor] {A : Type*} (B : A → Type) (b₀ : B pt) :
ppi B b₀ ≃ Σ(k : Πa, B a), k pt = b₀ :=
definition apd10_to_fun_eq_of_phomotopy (h : f ~* g)
: apd10 (ap (λ k, pppi.to_fun k) (eq_of_phomotopy h)) = h :=
begin
fapply equiv.MK: intro x,
{ constructor, exact ppi.resp_pt x },
{ induction x, constructor, assumption },
{ induction x, reflexivity },
{ induction x, reflexivity }
induction h using phomotopy_rec_idp,
xrewrite [eq_of_phomotopy_refl f]
end
-- definition pppi.sigma_char [constructor] {A : Type*} (B : A → Type*)
-- : (Π*(a : A), B a) ≃ Σ(k : (Π (a : A), B a)), k pt = pt :=
-- ppi.sigma_char
definition ppi_homotopy_of_eq (p : k = l) : k ~~* l :=
ppi_homotopy.mk (ap010 ppi.to_fun p) begin induction p, refine !idp_con end
variables (k l)
definition ppi_homotopy.rec' [recursor] (B : k ~~* l → Type)
(H : Π(h : k ~ l) (p : h pt ⬝ ppi.resp_pt l = ppi.resp_pt k), B (ppi_homotopy.mk h p))
(h : k ~~* l) : B h :=
begin
induction h with h p,
refine transport (λp, B (ppi.mk h p)) _ (H h (con_eq_of_eq_con_inv p)),
apply to_left_inv !eq_con_inv_equiv_con_eq p
end
definition ppi_homotopy.sigma_char [constructor]
: (k ~~* l) ≃ Σ(p : k ~ l), p pt ⬝ ppi.resp_pt l = ppi.resp_pt k :=
begin
fapply equiv.MK : intros h,
{ exact ⟨h , ppi_to_homotopy_pt h⟩ },
{ cases h with h p, exact ppi_homotopy.mk h p },
{ cases h with h p, exact ap (dpair h) (to_right_inv !eq_con_inv_equiv_con_eq p) },
{ induction h using ppi_homotopy.rec' with h p,
exact ap (ppi_homotopy.mk h) (to_right_inv !eq_con_inv_equiv_con_eq p) }
end
-- the same as pmap_eq_equiv
definition ppi_eq_equiv_internal : (k = l) ≃ (k ~~* l) :=
calc (k = l) ≃ ppi.sigma_char B b₀ k = ppi.sigma_char B b₀ l
: eq_equiv_fn_eq (ppi.sigma_char B b₀) k l
... ≃ Σ(p : k = l),
pathover (λh, h pt = b₀) (ppi.resp_pt k) p (ppi.resp_pt l)
: sigma_eq_equiv _ _
... ≃ Σ(p : k = l),
ppi.resp_pt k = ap (λh, h pt) p ⬝ ppi.resp_pt l
: sigma_equiv_sigma_right
(λp, eq_pathover_equiv_Fl p (ppi.resp_pt k) (ppi.resp_pt l))
... ≃ Σ(p : k = l),
ppi.resp_pt k = apd10 p pt ⬝ ppi.resp_pt l
: sigma_equiv_sigma_right
(λp, equiv_eq_closed_right _ (whisker_right _ (ap_eq_apd10 p _)))
... ≃ Σ(p : k ~ l), ppi.resp_pt k = p pt ⬝ ppi.resp_pt l
: sigma_equiv_sigma_left' eq_equiv_homotopy
... ≃ Σ(p : k ~ l), p pt ⬝ ppi.resp_pt l = ppi.resp_pt k
: sigma_equiv_sigma_right (λp, eq_equiv_eq_symm _ _)
... ≃ (k ~~* l) : ppi_homotopy.sigma_char k l
definition ppi_eq_equiv_internal_idp :
ppi_eq_equiv_internal k k idp = ppi_homotopy.refl k :=
begin
apply ap (ppi_homotopy.mk (homotopy.refl _)), induction k with k k₀,
esimp at * ⊢, induction k₀, reflexivity
end
definition ppi_eq_equiv [constructor] : (k = l) ≃ (k ~~* l) :=
begin
refine equiv_change_fun (ppi_eq_equiv_internal k l) _,
{ apply ppi_homotopy_of_eq },
{ intro p, induction p, exact ppi_eq_equiv_internal_idp k }
end
variables {k l}
-- the same as pmap_eq
definition ppi_eq (h : k ~~* l) : k = l :=
(ppi_eq_equiv k l)⁻¹ᵉ h
definition eq_of_ppi_homotopy (h : k ~~* l) : k = l := ppi_eq h
definition ppi_homotopy_of_eq_of_ppi_homotopy (h : k ~~* l) :
ppi_homotopy_of_eq (eq_of_ppi_homotopy h) = h :=
proof to_right_inv (ppi_eq_equiv k l) h qed
variable (k)
definition eq_ppi_homotopy_refl_ppi_homotopy_of_eq_refl :
ppi_homotopy.refl k = ppi_homotopy_of_eq (refl k) :=
begin
reflexivity
end
definition ppi_homotopy_of_eq_refl : ppi_homotopy.refl k = ppi_homotopy_of_eq (refl k) :=
begin
reflexivity,
end
definition ppi_eq_refl : ppi_eq (ppi_homotopy.refl k) = refl k :=
to_inv_eq_of_eq !ppi_eq_equiv idp
variable {k}
definition ppi_homotopy_rec_on_eq [recursor]
{Q : (k ~~* k') → Type} (p : k ~~* k') (H : Π(q : k = k'), Q (ppi_homotopy_of_eq q)) : Q p :=
ppi_homotopy_of_eq_of_ppi_homotopy p ▸ H (eq_of_ppi_homotopy p)
definition ppi_homotopy_rec_on_idp [recursor]
{Q : Π {k' : ppi B b₀}, (k ~~* k') → Type} {k' : ppi B b₀} (H : k ~~* k')
(q : Q (ppi_homotopy.refl k)) : Q H :=
begin
induction H using ppi_homotopy_rec_on_eq with t,
induction t, exact eq_ppi_homotopy_refl_ppi_homotopy_of_eq_refl k ▸ q,
end
attribute ppi_homotopy.rec' [recursor]
definition ppi_homotopy_rec_on_eq_ppi_homotopy_of_eq
{Q : (k ~~* k') → Type} (H : Π(q : k = k'), Q (ppi_homotopy_of_eq q))
(p : k = k') : ppi_homotopy_rec_on_eq (ppi_homotopy_of_eq p) H = H p :=
begin
refine ap (λp, p ▸ _) !adj ⬝ _,
refine !tr_compose⁻¹ ⬝ _,
apply apdt
end
definition ppi_homotopy_rec_on_idp_refl {Q : Π {k' : ppi B b₀}, (k ~~* k') → Type}
(q : Q (ppi_homotopy.refl k)) : ppi_homotopy_rec_on_idp ppi_homotopy.rfl q = q :=
ppi_homotopy_rec_on_eq_ppi_homotopy_of_eq _ idp
definition ppi_homotopy_rec_idp'
(Q : Π ⦃k' : ppi B b₀⦄, (k ~~* k') → (k = k') → Type)
(q : Q (ppi_homotopy.refl k) idp) ⦃k' : ppi B b₀⦄ (H : k ~~* k') : Q H (ppi_eq H) :=
begin
induction H using ppi_homotopy_rec_on_idp,
exact transport (Q ppi_homotopy.rfl) !ppi_eq_refl⁻¹ q
end
definition ppi_homotopy_rec_idp'_refl
(Q : Π ⦃k' : ppi B b₀⦄, (k ~~* k') → (k = k') → Type)
(q : Q (ppi_homotopy.refl k) idp) :
ppi_homotopy_rec_idp' Q q ppi_homotopy.rfl = transport (Q ppi_homotopy.rfl) !ppi_eq_refl⁻¹ q :=
!ppi_homotopy_rec_on_idp_refl
definition ppi_trans_refl (p : k ~~* l) : p ⬝*' ppi_homotopy.refl l = p :=
begin
unfold ppi_homotopy.trans,
induction A with A a₀,
induction k with k k₀, induction l with l l₀, induction p with p p₀, esimp at p, induction l₀, esimp at p₀, induction p₀, reflexivity,
end
definition ppi_refl_trans (p : k ~~* l) : ppi_homotopy.refl k ⬝*' p = p :=
begin
induction p using ppi_homotopy_rec_on_idp,
apply ppi_trans_refl
end
definition ppi_homotopy_of_eq_con {A : Type*} {B : A → Type*} {f g h : Π* (a : A), B a} (p : f = g) (q : g = h) :
ppi_homotopy_of_eq (p ⬝ q) = ppi_homotopy_of_eq p ⬝*' ppi_homotopy_of_eq q :=
begin induction q, induction p,
fapply eq_of_ppi_homotopy,
rewrite [!idp_con],
refine transport (λ x, x ~~* x ⬝*' x) !ppi_homotopy_of_eq_refl _,
fapply ppi_homotopy_of_eq,
refine (ppi_trans_refl (ppi_homotopy.refl f))⁻¹ᵖ
end
definition apd10_to_fun_ppi_eq (h : f ~~* g)
: apd10 (ap (λ k, pppi.to_fun k) (ppi_eq h)) = ppi_to_homotopy h :=
begin
induction h using ppi_homotopy_rec_on_idp, rewrite ppi_eq_refl
end
-- definition ppi_homotopy_of_eq_of_ppi_homotopy
-- definition phomotopy_of_eq_of_phomotopy
definition phomotopy_mk_ppi [constructor] {A : Type*} {B : Type*} {C : B → Type*}
{f g : A →* (Π*b, C b)} (p : Πa, f a ~~* g a)
(q : p pt ⬝*' ppi_homotopy_of_eq (respect_pt g) = ppi_homotopy_of_eq (respect_pt f)) : f ~* g :=
{f g : A →* (Π*b, C b)} (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_ppi_homotopy (p a)),
apply phomotopy.mk (λa, eq_of_phomotopy (p a)),
apply eq_of_fn_eq_fn !ppi_eq_equiv,
refine !ppi_homotopy_of_eq_con ⬝ _, esimp,
refine ap (λx, x ⬝*' _) !ppi_homotopy_of_eq_of_ppi_homotopy ⬝ q
refine !phomotopy_of_eq_con ⬝ _, esimp,
refine ap (λx, x ⬝* _) !phomotopy_of_eq_of_phomotopy ⬝ q
end
-- definition ppi_homotopy_mk_ppmap [constructor]
-- definition phomotopy_mk_ppmap [constructor]
-- {A : Type*} {X : A → Type*} {Y : Π (a : A), X a → Type*}
-- {f g : Π* (a : A), Π*(x : (X a)), (Y a x)}
-- (p : Πa, f a ~~* g a)
-- (q : p pt ⬝*' ppi_homotopy_of_eq (ppi_resp_pt g) = ppi_homotopy_of_eq (ppi_resp_pt f))
-- : f ~~* g :=
-- (p : Πa, f a ~* g a)
-- (q : p pt ⬝* phomotopy_of_eq (ppi_resp_pt g) = phomotopy_of_eq (ppi_resp_pt f))
-- : f ~* g :=
-- begin
-- apply ppi_homotopy.mk (λa, eq_of_ppi_homotopy (p a)),
-- apply phomotopy.mk (λa, eq_of_phomotopy (p a)),
-- apply eq_of_fn_eq_fn (ppi_eq_equiv _ _),
-- refine !ppi_homotopy_of_eq_con ⬝ _,
-- -- refine !ppi_homotopy_of_eq_of_ppi_homotopy ◾** idp ⬝ q,
-- refine !phomotopy_of_eq_con ⬝ _,
-- -- refine !phomotopy_of_eq_of_phomotopy ◾** idp ⬝ q,
-- end
variable {k}
@ -597,54 +386,54 @@ namespace pointed
end
variables {k l}
-- definition eq_of_ppi_homotopy (h : k ~~* l) : k = l :=
-- definition eq_of_phomotopy (h : k ~* l) : k = l :=
-- (ppi_eq_equiv k l)⁻¹ᵉ h
definition ppi_functor_right [constructor] {A : Type*} {B B' : A → Type}
{b : B pt} {b' : B' pt} (f : Πa, B a → B' a) (p : f pt b = b') (g : ppi B b)
: ppi B' b' :=
ppi.mk (λa, f a (g a)) (ap (f pt) (ppi.resp_pt g) ⬝ p)
ppi.mk (λa, f a (g a)) (ap (f pt) (respect_pt g) ⬝ p)
definition ppi_functor_right_compose [constructor] {A : Type*} {B₁ B₂ B₃ : A → Type}
{b₁ : B₁ pt} {b₂ : B₂ pt} {b₃ : B₃ pt} (f₂ : Πa, B₂ a → B₃ a) (p₂ : f₂ pt b₂ = b₃)
(f₁ : Πa, B₁ a → B₂ a) (p₁ : f₁ pt b₁ = b₂)
(g : ppi B₁ b₁) : ppi_functor_right (λa, f₂ a ∘ f₁ a) (ap (f₂ pt) p₁ ⬝ p₂) g ~~*
(g : ppi B₁ b₁) : ppi_functor_right (λa, f₂ a ∘ f₁ a) (ap (f₂ pt) p₁ ⬝ p₂) g ~*
ppi_functor_right f₂ p₂ (ppi_functor_right f₁ p₁ g) :=
begin
fapply ppi_homotopy.mk,
fapply phomotopy.mk,
{ reflexivity },
{ induction p₁, induction p₂, exact !idp_con ⬝ !ap_compose⁻¹ }
end
definition ppi_functor_right_id [constructor] {A : Type*} {B : A → Type}
{b : B pt} (g : ppi B b) : ppi_functor_right (λa, id) idp g ~~* g :=
{b : B pt} (g : ppi B b) : ppi_functor_right (λa, id) idp g ~* g :=
begin
fapply ppi_homotopy.mk,
fapply phomotopy.mk,
{ reflexivity },
{ reflexivity }
end
definition ppi_functor_right_ppi_homotopy [constructor] {g g' : Π(a : A), B a → C a}
definition ppi_functor_right_phomotopy [constructor] {g g' : Π(a : A), B a → C a}
{g₀ : g pt b₀ = c₀} {g₀' : g' pt b₀ = c₀} {f f' : ppi B b₀}
(p : g ~2 g') (q : f ~~* f') (r : p pt b₀ ⬝ g₀' = g₀) :
ppi_functor_right g g₀ f ~~* ppi_functor_right g' g₀' f' :=
ppi_homotopy.mk (λa, p a (f a) ⬝ ap (g' a) (q a))
(p : g ~2 g') (q : f ~* f') (r : p pt b₀ ⬝ g₀' = g₀) :
ppi_functor_right g g₀ f ~* ppi_functor_right g' g₀' f' :=
phomotopy.mk (λa, p a (f a) ⬝ ap (g' a) (q a))
abstract begin
induction q using ppi_homotopy_rec_on_idp,
induction q using phomotopy_rec_idp,
induction r, revert g p, refine rec_idp_of_equiv _ homotopy2.rfl _ _ _,
{ intro h h', exact !eq_equiv_eq_symm ⬝e !eq_equiv_homotopy2 },
{ reflexivity },
induction g₀', induction f with f f₀, induction f₀, reflexivity
end end
definition ppi_functor_right_ppi_homotopy_refl [constructor] (g : Π(a : A), B a → C a)
definition ppi_functor_right_phomotopy_refl [constructor] (g : Π(a : A), B a → C a)
(g₀ : g pt b₀ = c₀) (f : ppi B b₀) :
ppi_functor_right_ppi_homotopy (homotopy2.refl g) (ppi_homotopy.refl f) !idp_con =
ppi_homotopy.refl (ppi_functor_right g g₀ f) :=
ppi_functor_right_phomotopy (homotopy2.refl g) (phomotopy.refl f) !idp_con =
phomotopy.refl (ppi_functor_right g g₀ f) :=
begin
induction g₀,
apply ap (ppi_homotopy.mk homotopy.rfl),
refine !ppi_homotopy_rec_on_idp_refl ⬝ _,
apply ap (phomotopy.mk homotopy.rfl),
refine !phomotopy_rec_idp_refl ⬝ _,
esimp,
refine !rec_idp_of_equiv_idp ⬝ _,
induction f with f f₀, induction f₀, reflexivity
@ -655,16 +444,16 @@ namespace pointed
ppi B b ≃ ppi B' b' :=
equiv.MK (ppi_functor_right f p) (ppi_functor_right (λa, (f a)⁻¹ᵉ) (inv_eq_of_eq p⁻¹))
abstract begin
intro g, apply ppi_eq,
refine !ppi_functor_right_compose⁻¹*' ⬝*' _,
refine ppi_functor_right_ppi_homotopy (λa, to_right_inv (f a)) (ppi_homotopy.refl g) _ ⬝*'
intro g, apply eq_of_phomotopy,
refine !ppi_functor_right_compose⁻¹* ⬝* _,
refine ppi_functor_right_phomotopy (λa, to_right_inv (f a)) (phomotopy.refl g) _ ⬝*
!ppi_functor_right_id, induction p, exact adj (f pt) b ⬝ ap02 (f pt) !idp_con⁻¹
end end
abstract begin
intro g, apply ppi_eq,
refine !ppi_functor_right_compose⁻¹*' ⬝*' _,
refine ppi_functor_right_ppi_homotopy (λa, to_left_inv (f a)) (ppi_homotopy.refl g) _ ⬝*'
intro g, apply eq_of_phomotopy,
refine !ppi_functor_right_compose⁻¹* ⬝* _,
refine ppi_functor_right_phomotopy (λa, to_left_inv (f a)) (phomotopy.refl g) _ ⬝*
!ppi_functor_right_id, induction p, exact (!idp_con ⬝ !idp_con)⁻¹,
end end
@ -677,75 +466,76 @@ namespace pointed
ppi_functor_right g (respect_pt (g pt)) f
definition pmap_compose_ppi_ppi_const [constructor] (g : Π(a : A), ppmap (P a) (Q a)) :
pmap_compose_ppi g (ppi_const P) ~~* ppi_const Q :=
proof ppi_homotopy.mk (λa, respect_pt (g a)) !idp_con⁻¹ qed
pmap_compose_ppi g (ppi_const P) ~* ppi_const Q :=
proof phomotopy.mk (λa, respect_pt (g a)) !idp_con⁻¹ qed
definition pmap_compose_ppi_pconst [constructor] (f : Π*(a : A), P a) :
pmap_compose_ppi (λa, pconst (P a) (Q a)) f ~~* ppi_const Q :=
ppi_homotopy.mk homotopy.rfl !ap_constant⁻¹
pmap_compose_ppi (λa, pconst (P a) (Q a)) f ~* ppi_const Q :=
phomotopy.mk homotopy.rfl !ap_constant⁻¹
definition pmap_compose_ppi2 [constructor] {g g' : Π(a : A), ppmap (P a) (Q a)}
{f f' : Π*(a : A), P a} (p : Πa, g a ~* g' a) (q : f ~~* f') :
pmap_compose_ppi g f ~~* pmap_compose_ppi g' f' :=
ppi_functor_right_ppi_homotopy p q (to_homotopy_pt (p pt))
{f f' : Π*(a : A), P a} (p : Πa, g a ~* g' a) (q : f ~* f') :
pmap_compose_ppi g f ~* pmap_compose_ppi g' f' :=
ppi_functor_right_phomotopy p q (to_homotopy_pt (p pt))
definition pmap_compose_ppi2_refl [constructor] (g : Π(a : A), P a →* Q a) (f : Π*(a : A), P a) :
pmap_compose_ppi2 (λa, phomotopy.refl (g a)) (ppi_homotopy.refl f) = ppi_homotopy.rfl :=
pmap_compose_ppi2 (λa, phomotopy.refl (g a)) (phomotopy.refl f) = phomotopy.rfl :=
begin
refine _ ⬝ ppi_functor_right_ppi_homotopy_refl g (respect_pt (g pt)) f,
exact ap (ppi_functor_right_ppi_homotopy _ _) (to_right_inv !eq_con_inv_equiv_con_eq _)
refine _ ⬝ ppi_functor_right_phomotopy_refl g (respect_pt (g pt)) f,
exact ap (ppi_functor_right_phomotopy _ _) (to_right_inv !eq_con_inv_equiv_con_eq _)
end
definition pmap_compose_ppi_phomotopy_left [constructor] {g g' : Π(a : A), ppmap (P a) (Q a)}
(f : Π*(a : A), P a) (p : Πa, g a ~* g' a) : pmap_compose_ppi g f ~~* pmap_compose_ppi g' f :=
pmap_compose_ppi2 p ppi_homotopy.rfl
(f : Π*(a : A), P a) (p : Πa, g a ~* g' a) : pmap_compose_ppi g f ~* pmap_compose_ppi g' f :=
pmap_compose_ppi2 p phomotopy.rfl
definition pmap_compose_ppi_phomotopy_right [constructor] (g : Π(a : A), ppmap (P a) (Q a))
{f f' : Π*(a : A), P a} (p : f ~~* f') : pmap_compose_ppi g f ~~* pmap_compose_ppi g f' :=
{f f' : Π*(a : A), P a} (p : f ~* f') : pmap_compose_ppi g f ~* pmap_compose_ppi g f' :=
pmap_compose_ppi2 (λa, phomotopy.rfl) p
definition pmap_compose_ppi_pid_left [constructor]
(f : Π*(a : A), P a) : pmap_compose_ppi (λa, pid (P a)) f ~~* f :=
ppi_homotopy.mk homotopy.rfl idp
(f : Π*(a : A), P a) : pmap_compose_ppi (λa, pid (P a)) f ~* f :=
phomotopy.mk homotopy.rfl idp
definition pmap_compose_ppi_pcompose [constructor] (h : Π(a : A), ppmap (Q a) (R a))
(g : Π(a : A), ppmap (P a) (Q a)) :
pmap_compose_ppi (λa, h a ∘* g a) f ~~* pmap_compose_ppi h (pmap_compose_ppi g f) :=
ppi_homotopy.mk homotopy.rfl
pmap_compose_ppi (λa, h a ∘* g a) f ~* pmap_compose_ppi h (pmap_compose_ppi g f) :=
phomotopy.mk homotopy.rfl
abstract !idp_con ⬝ whisker_right _ (!ap_con ⬝ whisker_right _ !ap_compose'⁻¹) ⬝ !con.assoc end
definition ppi_assoc [constructor] (h : Π (a : A), Q a →* R a) (g : Π (a : A), P a →* Q a)
(f : Π*a, P a) :
pmap_compose_ppi (λa, h a ∘* g a) f ~~* pmap_compose_ppi h (pmap_compose_ppi g f) :=
pmap_compose_ppi (λa, h a ∘* g a) f ~* pmap_compose_ppi h (pmap_compose_ppi g f) :=
begin
fapply ppi_homotopy.mk,
fapply phomotopy.mk,
{ intro a, reflexivity },
exact !idp_con ⬝ whisker_right _ (!ap_con ⬝ whisker_right _ !ap_compose⁻¹) ⬝ !con.assoc
end
definition pmap_compose_ppi_eq (g : Πa, P a →* Q a) {f f' : Π*a, P a} (p : f ~~* f') :
ap (pmap_compose_ppi g) (ppi_eq p) = ppi_eq (pmap_compose_ppi_phomotopy_right g p) :=
definition pmap_compose_ppi_eq_of_phomotopy (g : Πa, P a →* Q a) {f f' : Π*a, P a} (p : f ~* f') :
ap (pmap_compose_ppi g) (eq_of_phomotopy p) =
eq_of_phomotopy (pmap_compose_ppi_phomotopy_right g p) :=
begin
induction p using ppi_homotopy_rec_on_idp,
refine ap02 _ !ppi_eq_refl ⬝ !ppi_eq_refl⁻¹ ⬝ ap ppi_eq _,
induction p using phomotopy_rec_idp,
refine ap02 _ !eq_of_phomotopy_refl ⬝ !eq_of_phomotopy_refl⁻¹ ⬝ ap eq_of_phomotopy _,
exact !pmap_compose_ppi2_refl⁻¹
end
definition ppi_assoc_ppi_const_right (g : Πa, Q a →* R a) (f : Πa, P a →* Q a) :
ppi_assoc g f (ppi_const P) ⬝*'
(pmap_compose_ppi_phomotopy_right _ (pmap_compose_ppi_ppi_const f) ⬝*'
ppi_assoc g f (ppi_const P) ⬝*
(pmap_compose_ppi_phomotopy_right _ (pmap_compose_ppi_ppi_const f) ⬝*
pmap_compose_ppi_ppi_const g) = pmap_compose_ppi_ppi_const (λa, g a ∘* f a) :=
begin
revert R g, refine fiberwise_pointed_map_rec _ _,
revert Q f, refine fiberwise_pointed_map_rec _ _,
intro Q f R g,
refine ap (λx, _ ⬝*' (x ⬝*' _)) !pmap_compose_ppi2_refl ⬝ _,
refine ap (λx, _ ⬝* (x ⬝* _)) !pmap_compose_ppi2_refl ⬝ _,
reflexivity
end
definition pppi_compose_left [constructor] (g : Π(a : A), ppmap (P a) (Q a)) :
(Π*(a : A), P a) →* Π*(a : A), Q a :=
pmap.mk (pmap_compose_ppi g) (ppi_eq (pmap_compose_ppi_ppi_const g))
pmap.mk (pmap_compose_ppi g) (eq_of_phomotopy (pmap_compose_ppi_ppi_const g))
-- pppi_compose_left is a functor in the following sense
definition pppi_compose_left_pcompose (g : Π (a : A), Q a →* R a) (f : Π (a : A), P a →* Q a)
@ -753,9 +543,9 @@ namespace pointed
begin
fapply phomotopy_mk_ppi,
{ exact ppi_assoc g f },
{ refine idp ◾**' (!ppi_homotopy_of_eq_con ⬝
(ap ppi_homotopy_of_eq !pmap_compose_ppi_eq ⬝ !ppi_homotopy_of_eq_of_ppi_homotopy) ◾**'
!ppi_homotopy_of_eq_of_ppi_homotopy) ⬝ _ ⬝ !ppi_homotopy_of_eq_of_ppi_homotopy⁻¹,
{ refine idp ◾** (!phomotopy_of_eq_con ⬝
(ap phomotopy_of_eq !pmap_compose_ppi_eq_of_phomotopy ⬝ !phomotopy_of_eq_of_phomotopy) ◾**
!phomotopy_of_eq_of_phomotopy) ⬝ _ ⬝ !phomotopy_of_eq_of_phomotopy⁻¹,
apply ppi_assoc_ppi_const_right },
end
@ -787,13 +577,13 @@ namespace pointed
begin
apply pequiv_of_pmap (pppi_compose_left g),
apply adjointify _ (pppi_compose_left (λa, (g a)⁻¹ᵉ*)),
{ intro f, apply ppi_eq,
refine !pmap_compose_ppi_pcompose⁻¹*' ⬝*' _,
refine pmap_compose_ppi_phomotopy_left _ (λa, !pright_inv) ⬝*' _,
{ intro f, apply eq_of_phomotopy,
refine !pmap_compose_ppi_pcompose⁻¹* ⬝* _,
refine pmap_compose_ppi_phomotopy_left _ (λa, !pright_inv) ⬝* _,
apply pmap_compose_ppi_pid_left },
{ intro f, apply ppi_eq,
refine !pmap_compose_ppi_pcompose⁻¹*' ⬝*' _,
refine pmap_compose_ppi_phomotopy_left _ (λa, !pleft_inv) ⬝*' _,
{ intro f, apply eq_of_phomotopy,
refine !pmap_compose_ppi_pcompose⁻¹* ⬝* _,
refine pmap_compose_ppi_phomotopy_left _ (λa, !pleft_inv) ⬝* _,
apply pmap_compose_ppi_pid_left }
end
@ -837,7 +627,7 @@ namespace pointed
fapply sigma_eq2,
{ refine !sigma_eq_pr1 ⬝ _ ⬝ !ap_sigma_pr1⁻¹,
apply eq_of_fn_eq_fn eq_equiv_homotopy,
refine !apd10_eq_of_homotopy ⬝ _ ⬝ !apd10_to_fun_ppi_eq⁻¹,
refine !apd10_eq_of_homotopy ⬝ _ ⬝ !apd10_to_fun_eq_of_phomotopy⁻¹,
apply eq_of_homotopy, intro a, reflexivity },
{ exact sorry } }
end
@ -869,7 +659,7 @@ namespace pointed
definition ppi_psigma.{u v w} {A : pType.{u}} {B : A → pType.{v}} (C : Πa, B a → Type.{w})
(c : Πa, C a pt) : (Π*(a : A), (psigma_gen (C a) (c a))) ≃*
psigma_gen (λ(f : Π*(a : A), B a), ppi (λa, C a (f a))
(transport (C pt) (pppi.resp_pt f)⁻¹ (c pt))) (ppi_const _) :=
(transport (C pt) (respect_pt f)⁻¹ (c pt))) (ppi_const _) :=
proof
calc (Π*(a : A), psigma_gen (C a) (c a))
≃* @psigma_gen (Πᵘ*a, psigma_gen (C a) (c a)) (λf, f pt = pt) idp : pppi.sigma_char
@ -881,7 +671,7 @@ namespace pointed
(λv, Σ(g : Πa, C a (v.1 a)), g pt =[v.2] c pt) ⟨c, idpo⟩ :
by apply psigma_gen_swap
... ≃* psigma_gen (λ(f : Π*(a : A), B a), ppi (λa, C a (f a))
(transport (C pt) (pppi.resp_pt f)⁻¹ (c pt)))
(transport (C pt) (respect_pt f)⁻¹ (c pt)))
(ppi_const _) :
by exact (psigma_gen_pequiv_psigma_gen (pppi.sigma_char B)
(λf, !ppi.sigma_char ⬝e sigma_equiv_sigma_right (λg, !pathover_equiv_eq_tr⁻¹ᵉ))
@ -901,20 +691,21 @@ namespace pointed
calc
pfiber (pppi_compose_left f) ≃*
psigma_gen (λ(g : Π*(a : A), B a), pmap_compose_ppi f g = ppi_const C)
proof (ppi_eq (pmap_compose_ppi_ppi_const f)) qed : by exact !pfiber.sigma_char'
... ≃* psigma_gen (λ(g : Π*(a : A), B a), pmap_compose_ppi f g ~~* ppi_const C)
proof (eq_of_phomotopy (pmap_compose_ppi_ppi_const f)) qed :
by exact !pfiber.sigma_char'
... ≃* psigma_gen (λ(g : Π*(a : A), B a), pmap_compose_ppi f g ~* ppi_const C)
proof (pmap_compose_ppi_ppi_const f) qed :
by exact psigma_gen_pequiv_psigma_gen_right (λa, !ppi_eq_equiv)
!ppi_homotopy_of_eq_of_ppi_homotopy
... ≃* psigma_gen (λ(g : Π*(a : A), B a), ppi (λa, f a (g a) = pt)
(transport (λb, f pt b = pt) (pppi.resp_pt g)⁻¹ (respect_pt (f pt))))
!phomotopy_of_eq_of_phomotopy
... ≃* @psigma_gen (Π*(a : A), B a) (λ(g : Π*(a : A), B a), ppi (λa, f a (g a) = pt)
(transport (λb, f pt b = pt) (respect_pt g)⁻¹ (respect_pt (f pt))))
(ppi_const _) :
begin
refine psigma_gen_pequiv_psigma_gen_right
(λg, ppi_equiv_ppi_basepoint (_ ⬝ !eq_transport_Fl⁻¹)) _,
intro g, refine !con_idp ⬝ _, apply whisker_right,
exact ap02 (f pt) !inv_inv⁻¹ ⬝ !ap_inv,
apply ppi_eq, fapply ppi_homotopy.mk,
apply eq_of_phomotopy, fapply phomotopy.mk,
intro x, reflexivity,
refine !idp_con ⬝ _, symmetry, refine !ap_id ◾ !idp_con ⬝ _, apply con.right_inv
end
@ -941,7 +732,7 @@ namespace pointed
(λg, ppi_equiv_ppi_basepoint (_ ⬝ !eq_transport_Fl⁻¹)) _,
intro g, refine !con_idp ⬝ _, apply whisker_right,
exact ap02 f !inv_inv⁻¹ ⬝ !ap_inv,
apply ppi_eq, fapply ppi_homotopy.mk,
apply eq_of_phomotopy, fapply phomotopy.mk,
intro x, reflexivity,
refine !idp_con ⬝ _, symmetry, refine !ap_id ◾ !idp_con ⬝ _, apply con.right_inv
end
@ -961,7 +752,7 @@ namespace pointed
intro a, cases a, exact pt, exact f a,
reflexivity },
{ intro f, reflexivity },
{ intro f, cases f with f p, apply ppi_eq, fapply ppi_homotopy.mk,
{ intro f, cases f with f p, apply eq_of_phomotopy, fapply phomotopy.mk,
{ intro a, cases a, exact p⁻¹, reflexivity },
{ exact con.left_inv p }},
end
@ -978,52 +769,52 @@ namespace pointed
Ω (Π*a, B a) ≃* Π*(a : A), Ω (B a) -/
definition ppi_eq_equiv_natural_gen_lem {B C : A → Type} {b₀ : B pt} {c₀ : C pt}
{f : Π(a : A), B a → C a} {f₀ : f pt b₀ = c₀} {k : ppi B b₀} {k' : ppi C c₀}
(p : ppi_functor_right f f₀ k ~~* k') :
ap1_gen (f pt) (p pt) f₀ (ppi.resp_pt k) = ppi.resp_pt k' :=
(p : ppi_functor_right f f₀ k ~* k') :
ap1_gen (f pt) (p pt) f₀ (respect_pt k) = respect_pt k' :=
begin
symmetry,
refine _ ⬝ !con.assoc⁻¹,
exact eq_inv_con_of_con_eq (ppi_to_homotopy_pt p),
exact eq_inv_con_of_con_eq (to_homotopy_pt p),
end
definition ppi_eq_equiv_natural_gen_lem2 {B C : A → Type} {b₀ : B pt} {c₀ : C pt}
{f : Π(a : A), B a → C a} {f₀ : f pt b₀ = c₀} {k l : ppi B b₀}
{k' l' : ppi C c₀} (p : ppi_functor_right f f₀ k ~~* k')
(q : ppi_functor_right f f₀ l ~~* l') :
ap1_gen (f pt) (p pt) (q pt) (ppi.resp_pt k ⬝ (ppi.resp_pt l)⁻¹) =
ppi.resp_pt k' ⬝ (ppi.resp_pt l')⁻¹ :=
{k' l' : ppi C c₀} (p : ppi_functor_right f f₀ k ~* k')
(q : ppi_functor_right f f₀ l ~* l') :
ap1_gen (f pt) (p pt) (q pt) (respect_pt k ⬝ (respect_pt l)⁻¹) =
respect_pt k' ⬝ (respect_pt l')⁻¹ :=
(ap1_gen_con (f pt) _ f₀ _ _ _ ⬝ (ppi_eq_equiv_natural_gen_lem p) ◾
(!ap1_gen_inv ⬝ (ppi_eq_equiv_natural_gen_lem q)⁻²))
definition ppi_eq_equiv_natural_gen {B C : A → Type} {b₀ : B pt} {c₀ : C pt}
{f : Π(a : A), B a → C a} {f₀ : f pt b₀ = c₀} {k l : ppi B b₀}
{k' l' : ppi C c₀} (p : ppi_functor_right f f₀ k ~~* k')
(q : ppi_functor_right f f₀ l ~~* l') :
hsquare (ap1_gen (ppi_functor_right f f₀) (ppi_eq p) (ppi_eq q))
{k' l' : ppi C c₀} (p : ppi_functor_right f f₀ k ~* k')
(q : ppi_functor_right f f₀ l ~* l') :
hsquare (ap1_gen (ppi_functor_right f f₀) (eq_of_phomotopy p) (eq_of_phomotopy q))
(ppi_functor_right (λa, ap1_gen (f a) (p a) (q a))
(ppi_eq_equiv_natural_gen_lem2 p q))
ppi_homotopy_of_eq
ppi_homotopy_of_eq :=
phomotopy_of_eq
phomotopy_of_eq :=
begin
intro r, induction r,
induction f₀,
induction k with k k₀,
induction k₀,
refine idp ⬝ _,
revert l' q, refine ppi_homotopy_rec_idp' _ _,
revert k' p, refine ppi_homotopy_rec_idp' _ _,
revert l' q, refine phomotopy_rec_idp' _ _,
revert k' p, refine phomotopy_rec_idp' _ _,
reflexivity
end
definition ppi_eq_equiv_natural_gen_refl {B C : A → Type}
{f : Π(a : A), B a → C a} {k : Πa, B a} :
ppi_eq_equiv_natural_gen (ppi_homotopy.refl (ppi_functor_right f idp (ppi.mk k idp)))
(ppi_homotopy.refl (ppi_functor_right f idp (ppi.mk k idp))) idp =
ap ppi_homotopy_of_eq !ap1_gen_idp :=
ppi_eq_equiv_natural_gen (phomotopy.refl (ppi_functor_right f idp (ppi.mk k idp)))
(phomotopy.refl (ppi_functor_right f idp (ppi.mk k idp))) idp =
ap phomotopy_of_eq !ap1_gen_idp :=
begin
refine !idp_con ⬝ _,
refine ppi_homotopy_rec_idp'_refl _ _ ⬝ _,
refine ap (transport _ _) !ppi_homotopy_rec_idp'_refl ⬝ _,
refine !phomotopy_rec_idp'_refl ⬝ _,
refine ap (transport _ _) !phomotopy_rec_idp'_refl ⬝ _,
refine !tr_diag_eq_tr_tr⁻¹ ⬝ _,
refine !eq_transport_Fl ⬝ _,
refine !ap_inv⁻² ⬝ !inv_inv ⬝ !ap_compose ⬝ ap02 _ _,
@ -1045,7 +836,7 @@ namespace pointed
fapply phomotopy.mk,
{ exact ppi_eq_equiv_natural_gen (pmap_compose_ppi_ppi_const (λa, pmap_of_map (f a) pt))
(pmap_compose_ppi_ppi_const (λa, pmap_of_map (f a) pt)) },
{ exact !ppi_eq_equiv_natural_gen_refl ◾ (!idp_con ⬝ !ppi_eq_refl) }
{ exact !ppi_eq_equiv_natural_gen_refl ◾ (!idp_con ⬝ !eq_of_phomotopy_refl) }
end
@ -1095,7 +886,7 @@ namespace is_conn
begin
apply is_contr.mk pt,
intro f, induction f with f p,
apply ppi_eq, fapply ppi_homotopy.mk,
apply eq_of_phomotopy, fapply phomotopy.mk,
{ apply is_conn.elim n, exact p⁻¹ },
{ krewrite (is_conn.elim_β n), apply con.left_inv }
end

32
spectrum/basic.hlean
View file

@ -363,13 +363,13 @@ namespace spectrum
(eq.eq_equiv_homotopy) ⬝e pi_equiv_pi_right (λ n, pmap_eq_equiv (f n) (g n))
/-
definition ppi_homotopy_rec_on_eq [recursor]
definition phomotopy_rec_on_eq [recursor]
{k' : ppi B x₀}
{Q : (k ~~* k') → Type}
(p : k ~~* k')
(H : Π(q : k = k'), Q (ppi_homotopy_of_eq q))
{Q : (k ~* k') → Type}
(p : k ~* k')
(H : Π(q : k = k'), Q (phomotopy_of_eq q))
: Q p :=
ppi_homotopy_of_eq_of_ppi_homotopy p ▸ H (eq_of_ppi_homotopy p)
phomotopy_of_eq_of_phomotopy p ▸ H (eq_of_phomotopy p)
-/
definition fam_phomotopy_rec_on_eq {N : Type} {X Y : N → Type*} (f g : Π n, X n →* Y n)
{Q : (Π n, f n ~* g n) → Type}
@ -383,18 +383,18 @@ namespace spectrum
end
/-
definition ppi_homotopy_rec_on_idp [recursor]
{Q : Π {k' : ppi B x₀}, (k ~~* k') → Type}
(q : Q (ppi_homotopy.refl k)) {k' : ppi B x₀} (H : k ~~* k') : Q H :=
definition phomotopy_rec_idp [recursor]
{Q : Π {k' : ppi B x₀}, (k ~* k') → Type}
(q : Q (phomotopy.refl k)) {k' : ppi B x₀} (H : k ~* k') : Q H :=
begin
induction H using ppi_homotopy_rec_on_eq with t,
induction t, exact eq_ppi_homotopy_refl_ppi_homotopy_of_eq_refl k ▸ q,
induction H using phomotopy_rec_on_eq with t,
induction t, exact eq_phomotopy_refl_phomotopy_of_eq_refl k ▸ q,
end
-/
--set_option pp.coercions true
definition fam_phomotopy_rec_on_idp {N : Type} {X Y : N → Type*} (f : Π n, X n →* Y n)
definition fam_phomotopy_rec_idp {N : Type} {X Y : N → Type*} (f : Π n, X n →* Y n)
(Q : Π (g : Π n, X n →* Y n) (H : Π n, f n ~* g n), Type)
(q : Q f (λ n, phomotopy.rfl))
(g : Π n, X n →* Y n) (H : Π n, f n ~* g n) : Q g H :=
@ -418,14 +418,14 @@ namespace spectrum
intro n,
esimp at *,
revert g H gsq Hsq n,
refine fam_phomotopy_rec_on_idp f _ _,
refine fam_phomotopy_rec_idp f _ _,
intro gsq Hsq n,
refine change_path _ _,
-- have p : eq_of_homotopy (λ n, eq_of_phomotopy phomotopy.rfl) = refl f,
reflexivity,
refine (eq_of_homotopy_eta rfl)⁻¹ ⬝ _,
fapply ap (eq_of_homotopy), fapply eq_of_homotopy, intro n, refine (eq_of_phomotopy_refl _)⁻¹,
-- fapply eq_of_ppi_homotopy,
-- fapply eq_of_phomotopy,
fapply pathover_idp_of_eq,
note Hsq' := ptube_v_eq_bot phomotopy.rfl (ap1_phomotopy_refl _) (fsq n) (gsq n) (Hsq n),
unfold ptube_v at *,
@ -600,7 +600,11 @@ namespace spectrum
homotopy_group_pequiv 2 (equiv_glue_neg X n)
definition πg_glue (X : spectrum) (n : ℤ) : πg[2] (X (2 - succ n)) ≃g πg[3] (X (2 - n)) :=
by rexact homotopy_group_isomorphism_of_pequiv _ (equiv_glue_neg X n)
begin
change πg[2] (X (2 - succ n)) ≃g πg[2] (Ω (X (2 - n))),
apply homotopy_group_isomorphism_of_pequiv,
exact equiv_glue_neg X n
end
definition πg_glue_homotopy_π_glue (X : spectrum) (n : ℤ) : πg_glue X n ~ π_glue X n :=
by reflexivity

5
spectrum/trunc.hlean
View file

@ -52,7 +52,7 @@ begin
induction p, induction k with k k,
{ refine pwhisker_right _ (ap1_phomotopy _) ⬝* @(ap1_ptrunc_elim k f) H,
apply ptrunc_elim_phomotopy2, reflexivity },
{ apply phomotopy_of_is_contr_cod, exact is_trunc_maxm2_loop H }
{ apply phomotopy_of_is_contr_cod_pmap, exact is_trunc_maxm2_loop H }
end
definition loop_ptrunc_maxm2_pequiv_ptrunc_elim {k : ℤ} {l : ℕ₋₂} (p : maxm2 (k+1) = l)
@ -70,7 +70,8 @@ definition loop_ptrunc_maxm2_pequiv_ptr {k : ℤ} {l : ℕ₋₂} (p : maxm2 (k+
begin
induction p, induction k with k k,
{ exact ap1_ptr k A },
{ apply phomotopy_pinv_left_of_phomotopy, apply phomotopy_of_is_contr_cod, apply is_trunc_trunc }
{ apply phomotopy_pinv_left_of_phomotopy, apply phomotopy_of_is_contr_cod_pmap,
apply is_trunc_trunc }
end
definition is_trunc_of_is_trunc_maxm2 (k : ℤ) (X : Type)