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

move basic lemmas from the spectral repository to the main repository

Browse source
This commit is contained in:
Floris van Doorn 2017-06-02 12:15:31 -04:00
parent c7fb842124
commit ed7de51d02
19 changed files with 190 additions and 2355 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
TODO.txt
View file

@ -2,3 +2,9 @@
- define pmap in terms of ppi
- move move_to_lib and pointed to library
talk with Favonia about:
- dependent pointed maps
- higher cube filling strategies
- HIT equivalences
- algebra

4
algebra/direct_sum.hlean
View file

@ -71,8 +71,8 @@ namespace group
(r : ∥dirsum_rel g∥) : free_ab_group_elim (λv, f v.1 v.2) g = 1 :=
begin
induction r with r, induction r,
rewrite [to_respect_add, to_respect_neg], apply add_neg_eq_of_eq_add,
rewrite [zero_add, to_respect_add, ▸*, ↑foldl, +one_mul, to_respect_add']
rewrite [to_respect_add, to_respect_neg, to_respect_add, ▸*, ↑foldl, +one_mul,
to_respect_add'], apply mul.right_inv
end
definition dirsum_elim [constructor] (f : Πi, Y i →a A') : dirsum →a A' :=

22
algebra/exact_couple.hlean
View file

@ -38,9 +38,9 @@ definition homology_ugly {B : AbGroup} (d : B →g B) (H : is_differential d) :
definition homology_iso_ugly {B : AbGroup} (d : B →g B) (H : is_differential d) : (homology d H) ≃g (homology_ugly d H) :=
begin
fapply @iso_of_ab_qg_group (ab_kernel d),
fapply @iso_of_ab_qg_group (ab_kernel d),
intro a,
intro p, induction p with f, induction f with b p,
intro p, induction p with f, induction f with b p,
fapply tr, fapply fiber.mk, fapply sigma.mk, exact d b, fapply tr, fapply fiber.mk, exact b, reflexivity,
induction a with c q, fapply subtype_eq, refine p ⬝ _, reflexivity,
intro b p, induction p with f, induction f with c p, induction p,
@ -50,7 +50,7 @@ definition homology_iso_ugly {B : AbGroup} (d : B →g B) (H : is_differential d
definition SES_iso_C {A B C C' : AbGroup} (ses : SES A B C) (k : C ≃g C') : SES A B C' :=
begin
begin
fapply SES.mk,
exact SES.f ses,
exact k ∘g SES.g ses,
@ -139,14 +139,14 @@ definition SES_of_exact_couple_at_i : SES (ab_kernel i) A (ab_image i) :=
fapply ab_group_first_iso_thm i,
end
definition kj_zero (a : A) : k (j a) = 1 :=
definition kj_zero (a : A) : k (j a) = 1 :=
is_exact.im_in_ker (exact_couple.exact_jk EC) a
definition j_factor : A →g (ab_kernel d) :=
definition j_factor : A →g (ab_kernel d) :=
begin
fapply ab_hom_lift j,
intro a,
unfold kernel_subgroup,
intro a,
unfold kernel_subgroup,
exact calc
d (j a) = j (k (j a)) : rfl
... = j 1 : by exact ap j (kj_zero a)
@ -164,7 +164,7 @@ definition subgroup_iso_exact_at_A : ab_kernel i ≃g ab_image k :=
induction EC,
induction exact_ki,
exact im_in_ker b,
end
end
definition subgroup_iso_exact_at_A_triangle : ab_kernel_incl i ~ ab_image_incl k ∘g subgroup_iso_exact_at_A :=
begin
@ -183,10 +183,10 @@ definition left_square_derived_ses : j_factor ∘g (ab_kernel_incl i) ~ (SES.f (
refine sorry --(ap (j_factor) subgroup_iso_exact_at_A_triangle) ⬝ _,
end
definition derived_couple_j : derived_couple_A EC →g derived_couple_B EC :=
/-definition derived_couple_j : derived_couple_A EC →g derived_couple_B EC :=
begin
exact sorry,
-- refine (comm_gq_map (comm_kernel (boundary CC)) (image_subgroup_of_bd (boundary CC) (boundary_is_boundary CC))) ∘g _,
end
end-/
end derived_couple

124
algebra/exactness.hlean Normal file
View file

@ -0,0 +1,124 @@
/-
Copyright (c) 2017 Jeremy Avigad. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Jeremy Avigad
Short exact sequences
-/
import homotopy.chain_complex eq2
open pointed is_trunc equiv is_equiv eq algebra group trunc function
structure is_exact_t {A B : Type} {C : Type*} (f : A → B) (g : B → C) :=
( im_in_ker : Π(a:A), g (f a) = pt)
( ker_in_im : Π(b:B), (g b = pt) → fiber f b)
structure is_exact {A B : Type} {C : Type*} (f : A → B) (g : B → C) :=
( im_in_ker : Π(a:A), g (f a) = pt)
( ker_in_im : Π(b:B), (g b = pt) → image f b)
namespace algebra
definition is_exact_g {A B C : Group} (f : A →g B) (g : B →g C) :=
is_exact f g
definition is_exact_ag {A B C : AbGroup} (f : A →g B) (g : B →g C) :=
is_exact f g
definition is_exact_g.mk {A B C : Group} {f : A →g B} {g : B →g C}
(H₁ : Πa, g (f a) = 1) (H₂ : Πb, g b = 1 → image f b) : is_exact_g f g :=
is_exact.mk H₁ H₂
definition is_exact.im_in_ker2 {A B : Type} {C : Set*} {f : A → B} {g : B → C} (H : is_exact f g)
{b : B} (h : image f b) : g b = pt :=
begin
induction h with a p, exact ap g p⁻¹ ⬝ is_exact.im_in_ker H a
end
-- TO DO: give less univalency proof
definition is_exact_homotopy {A B : Type} {C : Type*} {f f' : A → B} {g g' : B → C}
(p : f ~ f') (q : g ~ g') (H : is_exact f g) : is_exact f' g' :=
begin
induction p using homotopy.rec_on_idp,
induction q using homotopy.rec_on_idp,
exact H
end
definition is_exact_trunc_functor {A B : Type} {C : Type*} {f : A → B} {g : B → C}
(H : is_exact_t f g) : @is_exact _ _ (ptrunc 0 C) (trunc_functor 0 f) (trunc_functor 0 g) :=
begin
constructor,
{ intro a, esimp, induction a with a,
exact ap tr (is_exact_t.im_in_ker H a) },
{ intro b p, induction b with b, note q := !tr_eq_tr_equiv p, induction q with q,
induction is_exact_t.ker_in_im H b q with a r,
exact image.mk (tr a) (ap tr r) }
end
definition is_contr_middle_of_is_exact {A B : Type} {C : Type*} {f : A → B} {g : B → C} (H : is_exact f g)
[is_contr A] [is_set B] [is_contr C] : is_contr B :=
begin
apply is_contr.mk (f pt),
intro b,
induction is_exact.ker_in_im H b !is_prop.elim,
exact ap f !is_prop.elim ⬝ p
end
definition is_surjective_of_is_exact_of_is_contr {A B : Type} {C : Type*} {f : A → B} {g : B → C}
(H : is_exact f g) [is_contr C] : is_surjective f :=
λb, is_exact.ker_in_im H b !is_prop.elim
section chain_complex
open succ_str chain_complex
definition is_exact_of_is_exact_at {N : succ_str} {A : chain_complex N} {n : N}
(H : is_exact_at A n) : is_exact (cc_to_fn A (S n)) (cc_to_fn A n) :=
is_exact.mk (cc_is_chain_complex A n) H
end chain_complex
structure is_short_exact {A B : Type} {C : Type*} (f : A → B) (g : B → C) :=
(is_emb : is_embedding f)
(im_in_ker : Π(a:A), g (f a) = pt)
(ker_in_im : Π(b:B), (g b = pt) → image f b)
(is_surj : is_surjective g)
structure is_short_exact_t {A B : Type} {C : Type*} (f : A → B) (g : B → C) :=
(is_emb : is_embedding f)
(im_in_ker : Π(a:A), g (f a) = pt)
(ker_in_im : Π(b:B), (g b = pt) → fiber f b)
(is_surj : is_split_surjective g)
lemma is_short_exact_of_is_exact {X A B C Y : Group}
(k : X →g A) (f : A →g B) (g : B →g C) (l : C →g Y)
(hX : is_contr X) (hY : is_contr Y)
(kf : is_exact k f) (fg : is_exact f g) (gl : is_exact g l) : is_short_exact f g :=
begin
constructor,
{ apply to_is_embedding_homomorphism, intro a p,
induction is_exact.ker_in_im kf a p with x q,
exact q⁻¹ ⬝ ap k !is_prop.elim ⬝ to_respect_one k },
{ exact is_exact.im_in_ker fg },
{ exact is_exact.ker_in_im fg },
{ intro c, exact is_exact.ker_in_im gl c !is_prop.elim },
end
lemma is_short_exact_equiv {A B A' B' : Type} {C C' : Type*}
{f' : A' → B'} {g' : B' → C'} (f : A → B) (g : B → C)
(eA : A ≃ A') (eB : B ≃ B') (eC : C ≃* C')
(h₁ : hsquare f f' eA eB) (h₂ : hsquare g g' eB eC)
(H : is_short_exact f' g') : is_short_exact f g :=
begin
constructor,
{ apply is_embedding_homotopy_closed_rev (homotopy_top_of_hsquare h₁),
apply is_embedding_compose, apply is_embedding_of_is_equiv,
apply is_embedding_compose, apply is_short_exact.is_emb H, apply is_embedding_of_is_equiv },
{ intro a, refine homotopy_top_of_hsquare' (hhconcat h₁ h₂) a ⬝ _,
refine ap eC⁻¹ _ ⬝ respect_pt eC⁻¹ᵉ*, exact is_short_exact.im_in_ker H (eA a) },
{ intro b p, note q := eq_of_inv_eq ((homotopy_top_of_hsquare' h₂ b)⁻¹ ⬝ p) ⬝ respect_pt eC,
induction is_short_exact.ker_in_im H (eB b) q with a' r,
apply image.mk (eA⁻¹ a'),
exact eq_of_fn_eq_fn eB ((homotopy_top_of_hsquare h₁⁻¹ʰᵗʸᵛ a')⁻¹ ⬝ r) },
{ apply is_surjective_homotopy_closed_rev (homotopy_top_of_hsquare' h₂),
apply is_surjective_compose, apply is_surjective_of_is_equiv,
apply is_surjective_compose, apply is_short_exact.is_surj H, apply is_surjective_of_is_equiv }
end
end algebra

57
algebra/is_short_exact.hlean
View file

@ -1,57 +0,0 @@
/-
Copyright (c) 2017 Jeremy Avigad. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Jeremy Avigad
Short exact sequences
-/
import .quotient_group
open eq nat int susp pointed pmap sigma is_equiv equiv fiber algebra trunc trunc_index pi group
is_trunc function sphere unit sum prod
structure is_short_exact {A B : Type} {C : Type*} (f : A → B) (g : B → C) :=
(is_emb : is_embedding f)
(im_in_ker : Π(a:A), g (f a) = pt)
(ker_in_im : Π(b:B), (g b = pt) → image f b)
(is_surj : is_surjective g)
structure is_short_exact_t {A B : Type} {C : Type*} (f : A → B) (g : B → C) :=
(is_emb : is_embedding f)
(im_in_ker : Π(a:A), g (f a) = pt)
(ker_in_im : Π(b:B), (g b = pt) → fiber f b)
(is_surj : is_split_surjective g)
lemma is_short_exact_of_is_exact {X A B C Y : Group}
(k : X →g A) (f : A →g B) (g : B →g C) (l : C →g Y)
(hX : is_contr X) (hY : is_contr Y)
(kf : is_exact k f) (fg : is_exact f g) (gl : is_exact g l) : is_short_exact f g :=
begin
constructor,
{ apply to_is_embedding_homomorphism, intro a p,
induction is_exact.ker_in_im kf a p with x q,
exact q⁻¹ ⬝ ap k !is_prop.elim ⬝ to_respect_one k },
{ exact is_exact.im_in_ker fg },
{ exact is_exact.ker_in_im fg },
{ intro c, exact is_exact.ker_in_im gl c !is_prop.elim },
end
lemma is_short_exact_equiv {A B A' B' : Type} {C C' : Type*}
{f' : A' → B'} {g' : B' → C'} (f : A → B) (g : B → C)
(eA : A ≃ A') (eB : B ≃ B') (eC : C ≃* C')
(h₁ : hsquare f f' eA eB) (h₂ : hsquare g g' eB eC)
(H : is_short_exact f' g') : is_short_exact f g :=
begin
constructor,
{ apply is_embedding_homotopy_closed_rev (homotopy_top_of_hsquare h₁),
apply is_embedding_compose, apply is_embedding_of_is_equiv,
apply is_embedding_compose, apply is_short_exact.is_emb H, apply is_embedding_of_is_equiv },
{ intro a, refine homotopy_top_of_hsquare' (hhconcat h₁ h₂) a ⬝ _,
refine ap eC⁻¹ _ ⬝ respect_pt eC⁻¹ᵉ*, exact is_short_exact.im_in_ker H (eA a) },
{ intro b p, note q := eq_of_inv_eq ((homotopy_top_of_hsquare' h₂ b)⁻¹ ⬝ p) ⬝ respect_pt eC,
induction is_short_exact.ker_in_im H (eB b) q with a' r,
apply image.mk (eA⁻¹ a'),
exact eq_of_fn_eq_fn eB ((homotopy_top_of_hsquare h₁⁻¹ʰᵗʸᵛ a')⁻¹ ⬝ r) },
{ apply is_surjective_homotopy_closed_rev (homotopy_top_of_hsquare' h₂),
apply is_surjective_compose, apply is_surjective_of_is_equiv,
apply is_surjective_compose, apply is_short_exact.is_surj H, apply is_surjective_of_is_equiv }
end

4
algebra/left_module.hlean
View file

@ -7,7 +7,7 @@ Modules prod vector spaces over a ring.
(We use "left_module," which is more precise, because "module" is a keyword.)
-/
import algebra.field ..move_to_lib .is_short_exact algebra.group_power
import algebra.field ..move_to_lib .exactness algebra.group_power
open is_trunc pointed function sigma eq algebra prod is_equiv equiv group
structure has_scalar [class] (F V : Type) :=
@ -273,7 +273,7 @@ section
definition homomorphism_eq (φ₁ φ₂ : M₁ →lm M₂) (p : φ₁ ~ φ₂) : φ₁ = φ₂ :=
begin
induction φ₁ with φ₁ q₁, induction φ₂ with φ₂ q₂, esimp at p, induction p,
exact ap (homomorphism.mk φ₂) !is_prop.elim
exact ap (homomorphism.mk φ₁) !is_prop.elim
end
end

4
algebra/module_chain_complex.hlean
View file

@ -1,7 +1,7 @@
/-
Author: Jeremy Avigad
-/
import homotopy.chain_complex .left_module .is_short_exact ..move_to_lib
import homotopy.chain_complex .left_module .exactness ..move_to_lib
open eq pointed sigma fiber equiv is_equiv sigma.ops is_trunc nat trunc
open algebra function
open chain_complex
@ -53,5 +53,5 @@ namespace left_module
variables {A₀ B₀ C₀ : LeftModule R}
variables (f₀ : A₀ →lm B₀) (g₀ : B₀ →lm C₀)
definition is_short_exact := @_root_.is_short_exact _ _ C₀ f₀ g₀
definition is_short_exact := @algebra.is_short_exact _ _ C₀ f₀ g₀
end left_module

13
algebra/module_exact_couple.hlean
View file

@ -136,6 +136,7 @@ namespace left_module
definition deg_k' : deg k' ~ deg k := by reflexivity
open group
set_option pp.coercions true
lemma i'j' : is_exact_gmod i' j' :=
begin
intro x, refine equiv_rect (deg i) _ _,
@ -165,7 +166,7 @@ namespace left_module
{ exact is_exact.ker_in_im (exact_couple.ij X _ _) _ s },
refine image.mk ⟨m - k x n, t⟩ _,
apply subtype_eq, refine !i'_eq ⬝ !to_respect_sub ⬝ _,
refine ap (sub _) _ ⬝ !sub_zero,
refine ap (@sub (D (deg i (deg k x))) _ _) _ ⬝ @sub_zero _ _ _,
apply is_exact.im_in_ker (exact_couple.ki X _ _) }
end
@ -314,7 +315,7 @@ namespace left_module
definition deg_j_inv (r : ℕ) :
(deg (j (page r)))⁻¹ ~ iterate (deg (i X)) r ∘ (deg (j X))⁻¹ :=
have H : deg (j (page r)) ~ iterate_equiv (deg (i X))⁻¹ᵉ r ⬝e deg (j X), from deg_j r,
λx, to_inv_homotopy_to_inv H x ⬝ iterate_inv (deg (i X))⁻¹ᵉ r ((deg (j X))⁻¹ x)
λx, to_inv_homotopy_inv H x ⬝ iterate_inv (deg (i X))⁻¹ᵉ r ((deg (j X))⁻¹ x)
definition deg_d (r : ℕ) :
deg (d (page r)) ~ deg (j X) ∘ iterate (deg (i X))⁻¹ r ∘ deg (k X) :=
@ -322,7 +323,7 @@ namespace left_module
definition deg_d_inv (r : ℕ) :
(deg (d (page r)))⁻¹ ~ (deg (k X))⁻¹ ∘ iterate (deg (i X)) r ∘ (deg (j X))⁻¹ :=
compose2 (to_inv_homotopy_to_inv (deg_k r)) (deg_j_inv r)
compose2 (to_inv_homotopy_inv (deg_k r)) (deg_j_inv r)
definition B3 (x : I) : ℕ :=
max (B (deg (j X) (deg (k X) x))) (B2 ((deg (k X))⁻¹ ((deg (j X))⁻¹ x)))
@ -468,15 +469,15 @@ namespace pointed
definition homotopy_group_conn_nat_functor (n : ℕ) {A B : Type*[1]} (f : A →* B) :
homotopy_group_conn_nat n A →g homotopy_group_conn_nat n B :=
begin
cases n with n, { apply homomorphism_of_is_contr_right },
cases n with n, { apply homomorphism_of_is_contr_right },
cases n with n, { apply trivial_homomorphism },
cases n with n, { apply trivial_homomorphism },
exact π→g[n+2] f
end
definition homotopy_group_conn_functor :
Π(n : ℤ) {A B : Type*[1]} (f : A →* B), πc[n] A →g πc[n] B
| (of_nat n) A B f := homotopy_group_conn_nat_functor n f
| (-[1+ n]) A B f := homomorphism_of_is_contr_right _ _
| (-[1+ n]) A B f := trivial_homomorphism _ _
notation `π→c[`:95 n:0 `]`:0 := homotopy_group_conn_functor n

4
algebra/quotient_group.hlean
View file

@ -551,7 +551,7 @@ definition ab_group_kernel_quotient_to_image_codomain_triangle {A B : AbGroup} (
definition is_surjective_kernel_quotient_to_image {A B : AbGroup} (f : A →g B)
: is_surjective (ab_group_kernel_quotient_to_image f) :=
begin
fapply @is_surjective_factor A _ (image f) _ _ _ (group_fun (ab_qg_map (kernel_subgroup f))),
fapply is_surjective_factor (group_fun (ab_qg_map (kernel_subgroup f))),
exact image_lift f,
apply quotient_group_compute,
exact is_surjective_image_lift f
@ -560,7 +560,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 (ab_group_kernel_quotient_to_image f) (image_incl f) (kernel_quotient_extension f),
exact ab_group_kernel_quotient_to_image_codomain_triangle f,
exact is_embedding_kernel_quotient_extension f
end

12
algebra/ses.hlean
View file

@ -8,7 +8,7 @@ Basic facts about short exact sequences.
At the moment, it only covers short exact sequences of abelian groups, but this should be extended to short exact sequences in any abelian category.
-/
import algebra.group_theory hit.set_quotient types.sigma types.list types.sum .quotient_group .subgroup
import algebra.group_theory hit.set_quotient types.sigma types.list types.sum .quotient_group .subgroup .exactness
open eq algebra is_trunc set_quotient relation sigma sigma.ops prod prod.ops sum list trunc function group trunc
equiv is_equiv
@ -111,7 +111,7 @@ parameters {A B C : AbGroup} (ses : SES A B C)
definition SES_iso_stable {A' B' C' : AbGroup} (f' : A' →g B') (g' : B' →g C') (α : A' ≃g A) (β : B' ≃g B) (γ : C' ≃g C) (Hαβ : f ∘g α ~ β ∘g f') (Hβγ : g ∘g β ~ γ ∘g g') : SES A' B' C' :=
begin
fapply SES.mk,
fapply SES.mk,
exact f',
exact g',
fapply is_embedding_of_is_injective,
@ -120,10 +120,10 @@ definition SES_iso_stable {A' B' C' : AbGroup} (f' : A' →g B') (g' : B' →g C
f (α x) = β (f' x) : Hαβ x
... = β (f' y) : ap β p
... = f (α y) : (Hαβ y)⁻¹,
have path' : α x = α y, by exact @is_injective_of_is_embedding _ _ f (SES.Hf ses) _ _ path,
have path' : α x = α y, by exact @is_injective_of_is_embedding _ _ f (SES.Hf ses) _ _ path,
exact @is_injective_of_is_embedding _ _ α (is_embedding_of_is_equiv α) _ _ path',
exact sorry,
exact sorry,
exact sorry,
end
definition SES_of_triangle_left {A' : AbGroup} (α : A' ≃g A) (f' : A' →g B) (H : Π a' : A', f (α a') = f' a') : SES A' B C :=
@ -132,7 +132,7 @@ begin
exact f',
exact g,
fapply is_embedding_of_is_injective,
intro x y p,
intro x y p,
fapply eq_of_fn_eq_fn (equiv_of_isomorphism α),
fapply @is_injective_of_is_embedding _ _ f (SES.Hf ses) (α x) (α y),
rewrite [H x], rewrite [H y], exact p,
@ -143,7 +143,7 @@ begin
fapply is_exact.im_in_ker (SES.ex ses),
intro b p,
have t : trunctype.carrier (subgroup_to_rel (image_subgroup f) b), from is_exact.ker_in_im (SES.ex ses) b p,
induction t, fapply tr, induction a with a q, fapply fiber.mk, exact α⁻¹ᵍ a, rewrite [(H (α⁻¹ᵍ a))⁻¹],
induction t, fapply tr, induction a with a q, fapply fiber.mk, exact α⁻¹ᵍ a, rewrite [(H (α⁻¹ᵍ a))⁻¹],
krewrite [right_inv (equiv_of_isomorphism α) a], assumption
end

4
algebra/short_five.hlean
View file

@ -20,7 +20,7 @@ section short_five
include short_exact₀ short_exact₁ hsquare₁ hsquare₂
open is_short_exact
open algebra.is_short_exact
lemma short_five_mono [embh : is_embedding h] [embl : is_embedding l] :
is_embedding k :=
@ -56,7 +56,7 @@ section short_five
assume ha₀ : h a₀ = a₁,
have k (f₀ a₀) = k b₀ - b₁, by rewrite [hsquare₁, ▸*, ha₀, f₁a₁],
have k (b₀ - f₀ a₀) = b₁, by rewrite [respect_sub, this, sub_sub_self],
image.intro this))))
image.mk _ this))))
end short_five
section short_exact

2
homotopy/cohomology.hlean
View file

@ -87,7 +87,7 @@ definition cohomology_psusp_2 (Y : spectrum) (n : ℤ) :
Ω (Ω[2] (Y ((n+1)+2))) ≃* Ω[2] (Y (n+2)) :=
begin
apply loopn_pequiv_loopn 2,
exact loop_pequiv_loop (pequiv_of_eq (ap Y (add_comm_right n 1 2))) ⬝e* !equiv_glue⁻¹ᵉ*
exact loop_pequiv_loop (pequiv_of_eq (ap Y (add.right_comm n 1 2))) ⬝e* !equiv_glue⁻¹ᵉ*
end
definition cohomology_psusp_1 (X : Type*) (Y : spectrum) (n : ℤ) :

3
homotopy/pushout.hlean
View file

@ -1,5 +1,5 @@
import ..move_to_lib
import algebra.exactness homotopy.cofiber homotopy.wedge
open eq function is_trunc sigma prod lift is_equiv equiv pointed sum unit bool cofiber
@ -25,7 +25,6 @@ namespace pushout
end
/-
WIP: proving that satisfying the universal property of the pushout is equivalent to
being equivalent to the pushout

2
homotopy/smash.hlean
View file

@ -1,6 +1,6 @@
-- Authors: Floris van Doorn
import homotopy.smash ..pointed .pushout homotopy.red_susp
import homotopy.smash types.pointed2 .pushout homotopy.red_susp
open bool pointed eq equiv is_equiv sum bool prod unit circle cofiber prod.ops wedge is_trunc
function red_susp unit

4
homotopy/smash_adjoint.hlean
View file

@ -2,7 +2,7 @@
-- in collaboration with Egbert, Stefano, Robin, Ulrik
/- the adjunction between the smash product and pointed maps -/
import .smash .susp
import .smash .susp ..pointed
open bool pointed eq equiv is_equiv sum bool prod unit circle cofiber prod.ops wedge is_trunc
function unit sigma susp sphere
@ -510,7 +510,7 @@ namespace smash
calc
ppmap (A ∧ psusp B) X ≃* ppmap (psusp B) (ppmap A X) : smash_adjoint_pmap A (psusp B) X
... ≃* ppmap B (Ω (ppmap A X)) : psusp_adjoint_loop' B (ppmap A X)
... ≃* ppmap B (ppmap A (Ω X)) : pequiv_ppcompose_left (loop_pmap_commute A X)
... ≃* ppmap B (ppmap A (Ω X)) : pequiv_ppcompose_left (loop_ppmap_commute A X)
... ≃* ppmap (A ∧ B) (Ω X) : smash_adjoint_pmap A B (Ω X)
... ≃* ppmap (psusp (A ∧ B)) X : psusp_adjoint_loop' (A ∧ B) X

8
homotopy/spectrum.hlean
View file

@ -5,7 +5,7 @@ Authors: Michael Shulman, Floris van Doorn
-/
import homotopy.LES_of_homotopy_groups .splice homotopy.susp ..colim ..pointed .EM ..pointed_pi
import homotopy.LES_of_homotopy_groups .splice ..colim types.pointed2 .EM ..pointed_pi
open eq nat int susp pointed pmap sigma is_equiv equiv fiber algebra trunc trunc_index pi group
seq_colim succ_str EM EM.ops
@ -234,7 +234,7 @@ namespace spectrum
definition sp_cotensor [constructor] {N : succ_str} (A : Type*) (B : gen_spectrum N) : gen_spectrum N :=
spectrum.MK (λn, ppmap A (B n))
(λn, (loop_pmap_commute A (B (S n)))⁻¹ᵉ* ∘*ᵉ (pequiv_ppcompose_left (equiv_glue B n)))
(λn, (loop_ppmap_commute A (B (S n)))⁻¹ᵉ* ∘*ᵉ (pequiv_ppcompose_left (equiv_glue B n)))
----------------------------------------
-- Sections of parametrized spectra
@ -250,7 +250,7 @@ namespace spectrum
definition sfiber {N : succ_str} {X Y : gen_spectrum N} (f : X →ₛ Y) : gen_spectrum N :=
spectrum.MK (λn, pfiber (f n))
(λn, (loop_pfiber (f (S n)))⁻¹ᵉ* ∘*ᵉ pfiber_equiv_of_square _ _ (sglue_square f n))
(λn, (loop_pfiber (f (S n)))⁻¹ᵉ* ∘*ᵉ pfiber_pequiv_of_square _ _ (sglue_square f n))
/- the map from the fiber to the domain -/
definition spoint {N : succ_str} {X Y : gen_spectrum N} (f : X →ₛ Y) : sfiber f →ₛ X :=
@ -259,7 +259,7 @@ namespace spectrum
intro n,
refine _ ⬝* !passoc,
refine _ ⬝* pwhisker_right _ !ppoint_loop_pfiber_inv⁻¹*,
rexact (pfiber_equiv_of_square_ppoint (equiv_glue X n) (equiv_glue Y n) (sglue_square f n))⁻¹*
rexact (pfiber_pequiv_of_square_ppoint (equiv_glue X n) (equiv_glue Y n) (sglue_square f n))⁻¹*
end
definition scompose_spoint {N : succ_str} {X Y : gen_spectrum N} (f : X →ₛ Y)

2
homotopy/susp.hlean
View file

@ -1,4 +1,4 @@
import ..pointed
import homotopy.susp types.pointed2
open susp eq pointed function is_equiv

1327
move_to_lib.hlean
View file

File diff suppressed because it is too large Load diff

943
pointed.hlean
View file

@ -2,50 +2,12 @@
-- Author: Floris van Doorn
import .move_to_lib
import types.pointed2
open pointed eq equiv function is_equiv unit is_trunc trunc nat algebra group sigma
open pointed eq equiv function is_equiv unit is_trunc trunc nat algebra sigma group
namespace pointed
definition loop_pequiv_eq_closed [constructor] {A : Type} {a a' : A} (p : a = a')
: pointed.MK (a = a) idp ≃* pointed.MK (a' = a') idp :=
pequiv_of_equiv (loop_equiv_eq_closed p) (con.left_inv p)
definition punit_pmap_phomotopy [constructor] {A : Type*} (f : punit →* A) : f ~* pconst punit A :=
begin
fapply phomotopy.mk,
{ intro u, induction u, exact respect_pt f },
{ reflexivity }
end
definition is_contr_punit_pmap (A : Type*) : is_contr (punit →* A) :=
is_contr.mk (pconst punit A) (λf, eq_of_phomotopy (punit_pmap_phomotopy f)⁻¹*)
definition phomotopy_of_eq_idp {A B : Type*} (f : A →* B) : phomotopy_of_eq idp = phomotopy.refl f :=
idp
definition to_fun_pequiv_trans {X Y Z : Type*} (f : X ≃* Y) (g :Y ≃* Z) : f ⬝e* g ~ g ∘ f :=
λx, idp
definition pr1_phomotopy_eq {A B : Type*} {f g : A →* B} {p q : f ~* g} (r : p = q) (a : A) :
p a = q a :=
ap010 to_homotopy r a
definition ap1_gen_con_left {A B : Type} {a a' : A} {b₀ b₁ b₂ : B}
{f : A → b₀ = b₁} {f' : A → b₁ = b₂} {q₀ q₁ : b₀ = b₁} {q₀' q₁' : b₁ = b₂}
(r₀ : f a = q₀) (r₁ : f a' = q₁) (r₀' : f' a = q₀') (r₁' : f' a' = q₁') (p : a = a') :
ap1_gen (λa, f a ⬝ f' a) (r₀ ◾ r₀') (r₁ ◾ r₁') p =
whisker_right q₀' (ap1_gen f r₀ r₁ p) ⬝ whisker_left q₁ (ap1_gen f' r₀' r₁' p) :=
begin induction r₀, induction r₁, induction r₀', induction r₁', induction p, reflexivity end
definition ap1_gen_con_left_idp {A B : Type} {a : A} {b₀ b₁ b₂ : B}
{f : A → b₀ = b₁} {f' : A → b₁ = b₂} {q₀ : b₀ = b₁} {q₁ : b₁ = b₂}
(r₀ : f a = q₀) (r₁ : f' a = q₁) :
ap1_gen_con_left r₀ r₀ r₁ r₁ idp =
!con.left_inv ⬝ (ap (whisker_right q₁) !con.left_inv ◾ ap (whisker_left _) !con.left_inv)⁻¹ :=
begin induction r₀, induction r₁, reflexivity end
-- /- the pointed type of (unpointed) dependent maps -/
-- definition pupi [constructor] {A : Type} (P : A → Type*) : Type* :=
-- pointed.mk' (Πa, P a)
@ -58,816 +20,6 @@ namespace pointed
-- pequiv_of_equiv (pi_equiv_pi_right g)
-- begin esimp, apply eq_of_homotopy, intros a, esimp, exact (respect_pt (g a)) end
section psquare
/-
Squares of pointed maps
We treat expressions of the form
psquare f g h k :≡ k ∘* f ~* g ∘* h
as squares, where f is the top, g is the bottom, h is the left face and k is the right face.
Then the following are operations on squares
-/
variables {A A' A₀₀ A₂₀ A₄₀ A₀₂ A₂₂ A₄₂ A₀₄ A₂₄ A₄₄ : Type*}
{f₁₀ f₁₀' : A₀₀ →* A₂₀} {f₃₀ : A₂₀ →* A₄₀}
{f₀₁ f₀₁' : A₀₀ →* A₀₂} {f₂₁ f₂₁' : A₂₀ →* A₂₂} {f₄₁ : A₄₀ →* A₄₂}
{f₁₂ f₁₂' : A₀₂ →* A₂₂} {f₃₂ : A₂₂ →* A₄₂}
{f₀₃ : A₀₂ →* A₀₄} {f₂₃ : A₂₂ →* A₂₄} {f₄₃ : A₄₂ →* A₄₄}
{f₁₄ : A₀₄ →* A₂₄} {f₃₄ : A₂₄ →* A₄₄}
definition psquare [reducible] (f₁₀ : A₀₀ →* A₂₀) (f₁₂ : A₀₂ →* A₂₂)
(f₀₁ : A₀₀ →* A₀₂) (f₂₁ : A₂₀ →* A₂₂) : Type :=
f₂₁ ∘* f₁₀ ~* f₁₂ ∘* f₀₁
definition psquare_of_phomotopy (p : f₂₁ ∘* f₁₀ ~* f₁₂ ∘* f₀₁) : psquare f₁₀ f₁₂ f₀₁ f₂₁ :=
p
definition phomotopy_of_psquare (p : psquare f₁₀ f₁₂ f₀₁ f₂₁) : f₂₁ ∘* f₁₀ ~* f₁₂ ∘* f₀₁ :=
p
definition phdeg_square {f f' : A →* A'} (p : f ~* f') : psquare !pid !pid f f' :=
!pcompose_pid ⬝* p⁻¹* ⬝* !pid_pcompose⁻¹*
definition pvdeg_square {f f' : A →* A'} (p : f ~* f') : psquare f f' !pid !pid :=
!pid_pcompose ⬝* p ⬝* !pcompose_pid⁻¹*
variables (f₀₁ f₁₀)
definition phrefl : psquare !pid !pid f₀₁ f₀₁ := phdeg_square phomotopy.rfl
definition pvrefl : psquare f₁₀ f₁₀ !pid !pid := pvdeg_square phomotopy.rfl
variables {f₀₁ f₁₀}
definition phrfl : psquare !pid !pid f₀₁ f₀₁ := phrefl f₀₁
definition pvrfl : psquare f₁₀ f₁₀ !pid !pid := pvrefl f₁₀
definition phconcat (p : psquare f₁₀ f₁₂ f₀₁ f₂₁) (q : psquare f₃₀ f₃₂ f₂₁ f₄₁) :
psquare (f₃₀ ∘* f₁₀) (f₃₂ ∘* f₁₂) f₀₁ f₄₁ :=
!passoc⁻¹* ⬝* pwhisker_right f₁₀ q ⬝* !passoc ⬝* pwhisker_left f₃₂ p ⬝* !passoc⁻¹*
definition pvconcat (p : psquare f₁₀ f₁₂ f₀₁ f₂₁) (q : psquare f₁₂ f₁₄ f₀₃ f₂₃) :
psquare f₁₀ f₁₄ (f₀₃ ∘* f₀₁) (f₂₃ ∘* f₂₁) :=
!passoc ⬝* pwhisker_left _ p ⬝* !passoc⁻¹* ⬝* pwhisker_right _ q ⬝* !passoc
definition phinverse {f₁₀ : A₀₀ ≃* A₂₀} {f₁₂ : A₀₂ ≃* A₂₂} (p : psquare f₁₀ f₁₂ f₀₁ f₂₁) :
psquare f₁₀⁻¹ᵉ* f₁₂⁻¹ᵉ* f₂₁ f₀₁ :=
!pid_pcompose⁻¹* ⬝* pwhisker_right _ (pleft_inv f₁₂)⁻¹* ⬝* !passoc ⬝*
pwhisker_left _
(!passoc⁻¹* ⬝* pwhisker_right _ p⁻¹* ⬝* !passoc ⬝* pwhisker_left _ !pright_inv ⬝* !pcompose_pid)
definition pvinverse {f₀₁ : A₀₀ ≃* A₀₂} {f₂₁ : A₂₀ ≃* A₂₂} (p : psquare f₁₀ f₁₂ f₀₁ f₂₁) :
psquare f₁₂ f₁₀ f₀₁⁻¹ᵉ* f₂₁⁻¹ᵉ* :=
(phinverse p⁻¹*)⁻¹*
definition phomotopy_hconcat (q : f₀₁' ~* f₀₁) (p : psquare f₁₀ f₁₂ f₀₁ f₂₁) :
psquare f₁₀ f₁₂ f₀₁' f₂₁ :=
p ⬝* pwhisker_left f₁₂ q⁻¹*
definition hconcat_phomotopy (p : psquare f₁₀ f₁₂ f₀₁ f₂₁) (q : f₂₁' ~* f₂₁) :
psquare f₁₀ f₁₂ f₀₁ f₂₁' :=
pwhisker_right f₁₀ q ⬝* p
definition phomotopy_vconcat (q : f₁₀' ~* f₁₀) (p : psquare f₁₀ f₁₂ f₀₁ f₂₁) :
psquare f₁₀' f₁₂ f₀₁ f₂₁ :=
pwhisker_left f₂₁ q ⬝* p
definition vconcat_phomotopy (p : psquare f₁₀ f₁₂ f₀₁ f₂₁) (q : f₁₂' ~* f₁₂) :
psquare f₁₀ f₁₂' f₀₁ f₂₁ :=
p ⬝* pwhisker_right f₀₁ q⁻¹*
infix ` ⬝h* `:73 := phconcat
infix ` ⬝v* `:73 := pvconcat
infixl ` ⬝hp* `:72 := hconcat_phomotopy
infixr ` ⬝ph* `:72 := phomotopy_hconcat
infixl ` ⬝vp* `:72 := vconcat_phomotopy
infixr ` ⬝pv* `:72 := phomotopy_vconcat
postfix `⁻¹ʰ*`:(max+1) := phinverse
postfix `⁻¹ᵛ*`:(max+1) := pvinverse
definition pwhisker_tl (f : A →* A₀₀) (q : psquare f₁₀ f₁₂ f₀₁ f₂₁) :
psquare (f₁₀ ∘* f) f₁₂ (f₀₁ ∘* f) f₂₁ :=
!passoc⁻¹* ⬝* pwhisker_right f q ⬝* !passoc
definition ap1_psquare (p : psquare f₁₀ f₁₂ f₀₁ f₂₁) :
psquare (Ω→ f₁₀) (Ω→ f₁₂) (Ω→ f₀₁) (Ω→ f₂₁) :=
!ap1_pcompose⁻¹* ⬝* ap1_phomotopy p ⬝* !ap1_pcompose
definition apn_psquare (n : ℕ) (p : psquare f₁₀ f₁₂ f₀₁ f₂₁) :
psquare (Ω→[n] f₁₀) (Ω→[n] f₁₂) (Ω→[n] f₀₁) (Ω→[n] f₂₁) :=
!apn_pcompose⁻¹* ⬝* apn_phomotopy n p ⬝* !apn_pcompose
definition ptrunc_functor_psquare (n : ℕ₋₂) (p : psquare f₁₀ f₁₂ f₀₁ f₂₁) :
psquare (ptrunc_functor n f₁₀) (ptrunc_functor n f₁₂)
(ptrunc_functor n f₀₁) (ptrunc_functor n f₂₁) :=
!ptrunc_functor_pcompose⁻¹* ⬝* ptrunc_functor_phomotopy n p ⬝* !ptrunc_functor_pcompose
definition homotopy_group_functor_psquare (n : ℕ) (p : psquare f₁₀ f₁₂ f₀₁ f₂₁) :
psquare (π→[n] f₁₀) (π→[n] f₁₂) (π→[n] f₀₁) (π→[n] f₂₁) :=
!homotopy_group_functor_compose⁻¹* ⬝* homotopy_group_functor_phomotopy n p ⬝*
!homotopy_group_functor_compose
definition homotopy_group_homomorphism_psquare (n : ℕ) [H : is_succ n]
(p : psquare f₁₀ f₁₂ f₀₁ f₂₁) : hsquare (π→g[n] f₁₀) (π→g[n] f₁₂) (π→g[n] f₀₁) (π→g[n] f₂₁) :=
begin
induction H with n, exact to_homotopy (ptrunc_functor_psquare 0 (apn_psquare (succ n) p))
end
end psquare
definition phomotopy_of_eq_of_phomotopy {A B : Type*} {f g : A →* B} (p : f ~* g) :
phomotopy_of_eq (eq_of_phomotopy p) = p :=
to_right_inv (pmap_eq_equiv f g) p
definition ap_eq_of_phomotopy {A B : Type*} {f g : A →* B} (p : f ~* g) (a : A) :
ap (λf : A →* B, f a) (eq_of_phomotopy p) = p a :=
ap010 to_homotopy (phomotopy_of_eq_of_phomotopy p) a
definition phomotopy_rec_on_eq [recursor] {A B : Type*} {f g : A →* B}
{Q : (f ~* g) → Type} (p : f ~* g) (H : Π(q : f = g), Q (phomotopy_of_eq q)) : Q p :=
phomotopy_of_eq_of_phomotopy p ▸ H (eq_of_phomotopy p)
definition phomotopy_rec_on_idp [recursor] {A B : Type*} {f : A →* B}
{Q : Π{g}, (f ~* g) → Type} {g : A →* B} (p : f ~* g) (H : Q (phomotopy.refl f)) : Q p :=
begin
induction p using phomotopy_rec_on_eq,
induction q, exact H
end
definition phomotopy_rec_on_eq_phomotopy_of_eq {A B : Type*} {f g: A →* B}
{Q : (f ~* g) → Type} (p : f = g) (H : Π(q : f = g), Q (phomotopy_of_eq q)) :
phomotopy_rec_on_eq (phomotopy_of_eq p) H = H p :=
begin
unfold phomotopy_rec_on_eq,
refine ap (λp, p ▸ _) !adj ⬝ _,
refine !tr_compose⁻¹ ⬝ _,
apply apdt
end
definition phomotopy_rec_on_idp_refl {A B : Type*} (f : A →* B)
{Q : Π{g}, (f ~* g) → Type} (H : Q (phomotopy.refl f)) :
phomotopy_rec_on_idp phomotopy.rfl H = H :=
!phomotopy_rec_on_eq_phomotopy_of_eq
definition phomotopy_eq_equiv {A B : Type*} {f g : A →* B} (h k : f ~* g) :
(h = k) ≃ Σ(p : to_homotopy h ~ to_homotopy k),
whisker_right (respect_pt g) (p pt) ⬝ to_homotopy_pt k = to_homotopy_pt h :=
calc
h = k ≃ phomotopy.sigma_char _ _ h = phomotopy.sigma_char _ _ k
: eq_equiv_fn_eq (phomotopy.sigma_char f g) h k
... ≃ Σ(p : to_homotopy h = to_homotopy k),
pathover (λp, p pt ⬝ respect_pt g = respect_pt f) (to_homotopy_pt h) p (to_homotopy_pt k)
: sigma_eq_equiv _ _
... ≃ Σ(p : to_homotopy h = to_homotopy k),
to_homotopy_pt h = ap (λq, q pt ⬝ respect_pt g) p ⬝ to_homotopy_pt k
: sigma_equiv_sigma_right (λp, eq_pathover_equiv_Fl p (to_homotopy_pt h) (to_homotopy_pt k))
... ≃ Σ(p : to_homotopy h = to_homotopy k),
ap (λq, q pt ⬝ respect_pt g) p ⬝ to_homotopy_pt k = to_homotopy_pt h
: sigma_equiv_sigma_right (λp, eq_equiv_eq_symm _ _)
... ≃ Σ(p : to_homotopy h = to_homotopy k),
whisker_right (respect_pt g) (apd10 p pt) ⬝ to_homotopy_pt k = to_homotopy_pt h
: sigma_equiv_sigma_right (λp, equiv_eq_closed_left _ (whisker_right _ !whisker_right_ap⁻¹))
... ≃ Σ(p : to_homotopy h ~ to_homotopy k),
whisker_right (respect_pt g) (p pt) ⬝ to_homotopy_pt k = to_homotopy_pt h
: sigma_equiv_sigma_left' eq_equiv_homotopy
definition phomotopy_eq {A B : Type*} {f g : A →* B} {h k : f ~* g} (p : to_homotopy h ~ to_homotopy k)
(q : whisker_right (respect_pt g) (p pt) ⬝ to_homotopy_pt k = to_homotopy_pt h) : h = k :=
to_inv (phomotopy_eq_equiv h k) ⟨p, q⟩
definition phomotopy_eq' {A B : Type*} {f g : A →* B} {h k : f ~* g} (p : to_homotopy h ~ to_homotopy k)
(q : square (to_homotopy_pt h) (to_homotopy_pt k) (whisker_right (respect_pt g) (p pt)) idp) : h = k :=
phomotopy_eq p (eq_of_square q)⁻¹
definition eq_of_phomotopy_refl {X Y : Type*} (f : X →* Y) :
eq_of_phomotopy (phomotopy.refl f) = idpath f :=
begin
apply to_inv_eq_of_eq, reflexivity
end
definition trans_refl {A B : Type*} {f g : A →* B} (p : f ~* g) : p ⬝* phomotopy.refl g = p :=
begin
induction A with A a₀, induction B with B b₀,
induction f with f f₀, induction g with g g₀, induction p with p p₀,
esimp at *, induction g₀, induction p₀,
reflexivity
end
definition eq_of_phomotopy_trans {X Y : Type*} {f g h : X →* Y} (p : f ~* g) (q : g ~* h) :
eq_of_phomotopy (p ⬝* q) = eq_of_phomotopy p ⬝ eq_of_phomotopy q :=
begin
induction p using phomotopy_rec_on_idp, induction q using phomotopy_rec_on_idp,
exact ap eq_of_phomotopy !trans_refl ⬝ whisker_left _ !eq_of_phomotopy_refl⁻¹
end
definition refl_trans {A B : Type*} {f g : A →* B} (p : f ~* g) : phomotopy.refl f ⬝* p = p :=
begin
induction p using phomotopy_rec_on_idp,
induction A with A a₀, induction B with B b₀,
induction f with f f₀, esimp at *, induction f₀,
reflexivity
end
definition trans_assoc {A B : Type*} {f g h i : A →* B} (p : f ~* g) (q : g ~* h)
(r : h ~* i) : p ⬝* q ⬝* r = p ⬝* (q ⬝* r) :=
begin
induction r using phomotopy_rec_on_idp,
induction q using phomotopy_rec_on_idp,
induction p using phomotopy_rec_on_idp,
induction B with B b₀,
induction f with f f₀, esimp at *, induction f₀,
reflexivity
end
definition refl_symm {A B : Type*} (f : A →* B) : phomotopy.rfl⁻¹* = phomotopy.refl f :=
begin
induction B with B b₀,
induction f with f f₀, esimp at *, induction f₀,
reflexivity
end
definition symm_symm {A B : Type*} {f g : A →* B} (p : f ~* g) : p⁻¹*⁻¹* = p :=
phomotopy_eq (λa, !inv_inv)
begin
induction p using phomotopy_rec_on_idp, induction f with f f₀, induction B with B b₀,
esimp at *, induction f₀, reflexivity
end
definition trans_right_inv {A B : Type*} {f g : A →* B} (p : f ~* g) : p ⬝* p⁻¹* = phomotopy.rfl :=
begin
induction p using phomotopy_rec_on_idp, exact !refl_trans ⬝ !refl_symm
end
definition trans_left_inv {A B : Type*} {f g : A →* B} (p : f ~* g) : p⁻¹* ⬝* p = phomotopy.rfl :=
begin
induction p using phomotopy_rec_on_idp, exact !trans_refl ⬝ !refl_symm
end
definition trans2 {A B : Type*} {f g h : A →* B} {p p' : f ~* g} {q q' : g ~* h}
(r : p = p') (s : q = q') : p ⬝* q = p' ⬝* q' :=
ap011 phomotopy.trans r s
definition pcompose3 {A B C : Type*} {g g' : B →* C} {f f' : A →* B}
{p p' : g ~* g'} {q q' : f ~* f'} (r : p = p') (s : q = q') : p ◾* q = p' ◾* q' :=
ap011 pcompose2 r s
definition symm2 {A B : Type*} {f g : A →* B} {p p' : f ~* g} (r : p = p') : p⁻¹* = p'⁻¹* :=
ap phomotopy.symm r
infixl ` ◾** `:80 := pointed.trans2
infixl ` ◽* `:81 := pointed.pcompose3
postfix `⁻²**`:(max+1) := pointed.symm2
definition trans_symm {A B : Type*} {f g h : A →* B} (p : f ~* g) (q : g ~* h) :
(p ⬝* q)⁻¹* = q⁻¹* ⬝* p⁻¹* :=
begin
induction p using phomotopy_rec_on_idp, induction q using phomotopy_rec_on_idp,
exact !trans_refl⁻²** ⬝ !trans_refl⁻¹ ⬝ idp ◾** !refl_symm⁻¹
end
definition phwhisker_left {A B : Type*} {f g h : A →* B} (p : f ~* g) {q q' : g ~* h}
(s : q = q') : p ⬝* q = p ⬝* q' :=
idp ◾** s
definition phwhisker_right {A B : Type*} {f g h : A →* B} {p p' : f ~* g} (q : g ~* h)
(r : p = p') : p ⬝* q = p' ⬝* q :=
r ◾** idp
definition pwhisker_left_refl {A B C : Type*} (g : B →* C) (f : A →* B) :
pwhisker_left g (phomotopy.refl f) = phomotopy.refl (g ∘* f) :=
begin
induction A with A a₀, induction B with B b₀, induction C with C c₀,
induction f with f f₀, induction g with g g₀,
esimp at *, induction g₀, induction f₀, reflexivity
end
definition pwhisker_right_refl {A B C : Type*} (f : A →* B) (g : B →* C) :
pwhisker_right f (phomotopy.refl g) = phomotopy.refl (g ∘* f) :=
begin
induction A with A a₀, induction B with B b₀, induction C with C c₀,
induction f with f f₀, induction g with g g₀,
esimp at *, induction g₀, induction f₀, reflexivity
end
definition pcompose2_refl {A B C : Type*} (g : B →* C) (f : A →* B) :
phomotopy.refl g ◾* phomotopy.refl f = phomotopy.rfl :=
!pwhisker_right_refl ◾** !pwhisker_left_refl ⬝ !refl_trans
definition pcompose2_refl_left {A B C : Type*} (g : B →* C) {f f' : A →* B} (p : f ~* f') :
phomotopy.rfl ◾* p = pwhisker_left g p :=
!pwhisker_right_refl ◾** idp ⬝ !refl_trans
definition pcompose2_refl_right {A B C : Type*} {g g' : B →* C} (f : A →* B) (p : g ~* g') :
p ◾* phomotopy.rfl = pwhisker_right f p :=
idp ◾** !pwhisker_left_refl ⬝ !trans_refl
definition pwhisker_left_trans {A B C : Type*} (g : B →* C) {f₁ f₂ f₃ : A →* B}
(p : f₁ ~* f₂) (q : f₂ ~* f₃) :
pwhisker_left g (p ⬝* q) = pwhisker_left g p ⬝* pwhisker_left g q :=
begin
induction p using phomotopy_rec_on_idp,
induction q using phomotopy_rec_on_idp,
refine _ ⬝ !pwhisker_left_refl⁻¹ ◾** !pwhisker_left_refl⁻¹,
refine ap (pwhisker_left g) !trans_refl ⬝ !pwhisker_left_refl ⬝ !trans_refl⁻¹
end
definition pwhisker_right_trans {A B C : Type*} (f : A →* B) {g₁ g₂ g₃ : B →* C}
(p : g₁ ~* g₂) (q : g₂ ~* g₃) :
pwhisker_right f (p ⬝* q) = pwhisker_right f p ⬝* pwhisker_right f q :=
begin
induction p using phomotopy_rec_on_idp,
induction q using phomotopy_rec_on_idp,
refine _ ⬝ !pwhisker_right_refl⁻¹ ◾** !pwhisker_right_refl⁻¹,
refine ap (pwhisker_right f) !trans_refl ⬝ !pwhisker_right_refl ⬝ !trans_refl⁻¹
end
definition pwhisker_left_symm {A B C : Type*} (g : B →* C) {f₁ f₂ : A →* B} (p : f₁ ~* f₂) :
pwhisker_left g p⁻¹* = (pwhisker_left g p)⁻¹* :=
begin
induction p using phomotopy_rec_on_idp,
refine _ ⬝ ap phomotopy.symm !pwhisker_left_refl⁻¹,
refine ap (pwhisker_left g) !refl_symm ⬝ !pwhisker_left_refl ⬝ !refl_symm⁻¹
end
definition pwhisker_right_symm {A B C : Type*} (f : A →* B) {g₁ g₂ : B →* C} (p : g₁ ~* g₂) :
pwhisker_right f p⁻¹* = (pwhisker_right f p)⁻¹* :=
begin
induction p using phomotopy_rec_on_idp,
refine _ ⬝ ap phomotopy.symm !pwhisker_right_refl⁻¹,
refine ap (pwhisker_right f) !refl_symm ⬝ !pwhisker_right_refl ⬝ !refl_symm⁻¹
end
definition trans_eq_of_eq_symm_trans {A B : Type*} {f g h : A →* B} {p : f ~* g} {q : g ~* h}
{r : f ~* h} (s : q = p⁻¹* ⬝* r) : p ⬝* q = r :=
idp ◾** s ⬝ !trans_assoc⁻¹ ⬝ trans_right_inv p ◾** idp ⬝ !refl_trans
definition eq_symm_trans_of_trans_eq {A B : Type*} {f g h : A →* B} {p : f ~* g} {q : g ~* h}
{r : f ~* h} (s : p ⬝* q = r) : q = p⁻¹* ⬝* r :=
!refl_trans⁻¹ ⬝ !trans_left_inv⁻¹ ◾** idp ⬝ !trans_assoc ⬝ idp ◾** s
definition trans_eq_of_eq_trans_symm {A B : Type*} {f g h : A →* B} {p : f ~* g} {q : g ~* h}
{r : f ~* h} (s : p = r ⬝* q⁻¹*) : p ⬝* q = r :=
s ◾** idp ⬝ !trans_assoc ⬝ idp ◾** trans_left_inv q ⬝ !trans_refl
definition eq_trans_symm_of_trans_eq {A B : Type*} {f g h : A →* B} {p : f ~* g} {q : g ~* h}
{r : f ~* h} (s : p ⬝* q = r) : p = r ⬝* q⁻¹* :=
!trans_refl⁻¹ ⬝ idp ◾** !trans_right_inv⁻¹ ⬝ !trans_assoc⁻¹ ⬝ s ◾** idp
definition eq_trans_of_symm_trans_eq {A B : Type*} {f g h : A →* B} {p : f ~* g} {q : g ~* h}
{r : f ~* h} (s : p⁻¹* ⬝* r = q) : r = p ⬝* q :=
!refl_trans⁻¹ ⬝ !trans_right_inv⁻¹ ◾** idp ⬝ !trans_assoc ⬝ idp ◾** s
definition symm_trans_eq_of_eq_trans {A B : Type*} {f g h : A →* B} {p : f ~* g} {q : g ~* h}
{r : f ~* h} (s : r = p ⬝* q) : p⁻¹* ⬝* r = q :=
idp ◾** s ⬝ !trans_assoc⁻¹ ⬝ trans_left_inv p ◾** idp ⬝ !refl_trans
definition eq_trans_of_trans_symm_eq {A B : Type*} {f g h : A →* B} {p : f ~* g} {q : g ~* h}
{r : f ~* h} (s : r ⬝* q⁻¹* = p) : r = p ⬝* q :=
!trans_refl⁻¹ ⬝ idp ◾** !trans_left_inv⁻¹ ⬝ !trans_assoc⁻¹ ⬝ s ◾** idp
definition trans_symm_eq_of_eq_trans {A B : Type*} {f g h : A →* B} {p : f ~* g} {q : g ~* h}
{r : f ~* h} (s : r = p ⬝* q) : r ⬝* q⁻¹* = p :=
s ◾** idp ⬝ !trans_assoc ⬝ idp ◾** trans_right_inv q ⬝ !trans_refl
section phsquare
/-
Squares of pointed homotopies
-/
variables {A B C : Type*} {f f' f₀₀ f₂₀ f₄₀ f₀₂ f₂₂ f₄₂ f₀₄ f₂₄ f₄₄ : A →* B}
{p₁₀ : f₀₀ ~* f₂₀} {p₃₀ : f₂₀ ~* f₄₀}
{p₀₁ : f₀₀ ~* f₀₂} {p₂₁ : f₂₀ ~* f₂₂} {p₄₁ : f₄₀ ~* f₄₂}
{p₁₂ : f₀₂ ~* f₂₂} {p₃₂ : f₂₂ ~* f₄₂}
{p₀₃ : f₀₂ ~* f₀₄} {p₂₃ : f₂₂ ~* f₂₄} {p₄₃ : f₄₂ ~* f₄₄}
{p₁₄ : f₀₄ ~* f₂₄} {p₃₄ : f₂₄ ~* f₄₄}
definition phsquare [reducible] (p₁₀ : f₀₀ ~* f₂₀) (p₁₂ : f₀₂ ~* f₂₂)
(p₀₁ : f₀₀ ~* f₀₂) (p₂₁ : f₂₀ ~* f₂₂) : Type :=
p₁₀ ⬝* p₂₁ = p₀₁ ⬝* p₁₂
definition phsquare_of_eq (p : p₁₀ ⬝* p₂₁ = p₀₁ ⬝* p₁₂) : phsquare p₁₀ p₁₂ p₀₁ p₂₁ := p
definition eq_of_phsquare (p : phsquare p₁₀ p₁₂ p₀₁ p₂₁) : p₁₀ ⬝* p₂₁ = p₀₁ ⬝* p₁₂ := p
-- definition phsquare.mk (p : Πx, square (p₁₀ x) (p₁₂ x) (p₀₁ x) (p₂₁ x))
-- (q : cube (square_of_eq (to_homotopy_pt p₁₀)) (square_of_eq (to_homotopy_pt p₁₂))
-- (square_of_eq (to_homotopy_pt p₀₁)) (square_of_eq (to_homotopy_pt p₂₁))
-- (p pt) ids) : phsquare p₁₀ p₁₂ p₀₁ p₂₁ :=
-- begin
-- fapply phomotopy_eq,
-- { intro x, apply eq_of_square (p x) },
-- { generalize p pt, intro r, exact sorry }
-- end
definition phhconcat (p : phsquare p₁₀ p₁₂ p₀₁ p₂₁) (q : phsquare p₃₀ p₃₂ p₂₁ p₄₁) :
phsquare (p₁₀ ⬝* p₃₀) (p₁₂ ⬝* p₃₂) p₀₁ p₄₁ :=
!trans_assoc ⬝ idp ◾** q ⬝ !trans_assoc⁻¹ ⬝ p ◾** idp ⬝ !trans_assoc
definition phvconcat (p : phsquare p₁₀ p₁₂ p₀₁ p₂₁) (q : phsquare p₁₂ p₁₄ p₀₃ p₂₃) :
phsquare p₁₀ p₁₄ (p₀₁ ⬝* p₀₃) (p₂₁ ⬝* p₂₃) :=
(phhconcat p⁻¹ q⁻¹)⁻¹
definition phhdeg_square {p₁ p₂ : f ~* f'} (q : p₁ = p₂) : phsquare phomotopy.rfl phomotopy.rfl p₁ p₂ :=
!refl_trans ⬝ q⁻¹ ⬝ !trans_refl⁻¹
definition phvdeg_square {p₁ p₂ : f ~* f'} (q : p₁ = p₂) : phsquare p₁ p₂ phomotopy.rfl phomotopy.rfl :=
!trans_refl ⬝ q ⬝ !refl_trans⁻¹
variables (p₀₁ p₁₀)
definition phhrefl : phsquare phomotopy.rfl phomotopy.rfl p₀₁ p₀₁ := phhdeg_square idp
definition phvrefl : phsquare p₁₀ p₁₀ phomotopy.rfl phomotopy.rfl := phvdeg_square idp
variables {p₀₁ p₁₀}
definition phhrfl : phsquare phomotopy.rfl phomotopy.rfl p₀₁ p₀₁ := phhrefl p₀₁
definition phvrfl : phsquare p₁₀ p₁₀ phomotopy.rfl phomotopy.rfl := phvrefl p₁₀
/-
The names are very baroque. The following stands for
"pointed homotopy path-horizontal composition" (i.e. composition on the left with a path)
The names are obtained by using the ones for squares, and putting "ph" in front of it.
In practice, use the notation ⬝ph** defined below, which might be easier to remember
-/
definition phphconcat {p₀₁'} (p : p₀₁' = p₀₁) (q : phsquare p₁₀ p₁₂ p₀₁ p₂₁) :
phsquare p₁₀ p₁₂ p₀₁' p₂₁ :=
by induction p; exact q
definition phhpconcat {p₂₁'} (q : phsquare p₁₀ p₁₂ p₀₁ p₂₁) (p : p₂₁ = p₂₁') :
phsquare p₁₀ p₁₂ p₀₁ p₂₁' :=
by induction p; exact q
definition phpvconcat {p₁₀'} (p : p₁₀' = p₁₀) (q : phsquare p₁₀ p₁₂ p₀₁ p₂₁) :
phsquare p₁₀' p₁₂ p₀₁ p₂₁ :=
by induction p; exact q
definition phvpconcat {p₁₂'} (q : phsquare p₁₀ p₁₂ p₀₁ p₂₁) (p : p₁₂ = p₁₂') :
phsquare p₁₀ p₁₂' p₀₁ p₂₁ :=
by induction p; exact q
definition phhinverse (p : phsquare p₁₀ p₁₂ p₀₁ p₂₁) : phsquare p₁₀⁻¹* p₁₂⁻¹* p₂₁ p₀₁ :=
begin
refine (eq_symm_trans_of_trans_eq _)⁻¹,
refine !trans_assoc⁻¹ ⬝ _,
refine (eq_trans_symm_of_trans_eq _)⁻¹,
exact (eq_of_phsquare p)⁻¹
end
definition phvinverse (p : phsquare p₁₀ p₁₂ p₀₁ p₂₁) : phsquare p₁₂ p₁₀ p₀₁⁻¹* p₂₁⁻¹* :=
(phhinverse p⁻¹)⁻¹
infix ` ⬝h** `:78 := phhconcat
infix ` ⬝v** `:78 := phvconcat
infixr ` ⬝ph** `:77 := phphconcat
infixl ` ⬝hp** `:77 := phhpconcat
infixr ` ⬝pv** `:77 := phpvconcat
infixl ` ⬝vp** `:77 := phvpconcat
postfix `⁻¹ʰ**`:(max+1) := phhinverse
postfix `⁻¹ᵛ**`:(max+1) := phvinverse
definition phwhisker_rt (p : f ~* f₂₀) (q : phsquare p₁₀ p₁₂ p₀₁ p₂₁) :
phsquare (p₁₀ ⬝* p⁻¹*) p₁₂ p₀₁ (p ⬝* p₂₁) :=
!trans_assoc ⬝ idp ◾** (!trans_assoc⁻¹ ⬝ !trans_left_inv ◾** idp ⬝ !refl_trans) ⬝ q
definition phwhisker_br (p : f₂₂ ~* f) (q : phsquare p₁₀ p₁₂ p₀₁ p₂₁) :
phsquare p₁₀ (p₁₂ ⬝* p) p₀₁ (p₂₁ ⬝* p) :=
!trans_assoc⁻¹ ⬝ q ◾** idp ⬝ !trans_assoc
definition phmove_top_of_left' {p₀₁ : f ~* f₀₂} (p : f₀₀ ~* f)
(q : phsquare p₁₀ p₁₂ (p ⬝* p₀₁) p₂₁) : phsquare (p⁻¹* ⬝* p₁₀) p₁₂ p₀₁ p₂₁ :=
!trans_assoc ⬝ (eq_symm_trans_of_trans_eq (q ⬝ !trans_assoc)⁻¹)⁻¹
definition phmove_bot_of_left {p₀₁ : f₀₀ ~* f} (p : f ~* f₀₂)
(q : phsquare p₁₀ p₁₂ (p₀₁ ⬝* p) p₂₁) : phsquare p₁₀ (p ⬝* p₁₂) p₀₁ p₂₁ :=
q ⬝ !trans_assoc
definition passoc_phomotopy_right {A B C D : Type*} (h : C →* D) (g : B →* C) {f f' : A →* B}
(p : f ~* f') : phsquare (passoc h g f) (passoc h g f')
(pwhisker_left (h ∘* g) p) (pwhisker_left h (pwhisker_left g p)) :=
begin
induction p using phomotopy_rec_on_idp,
refine idp ◾** (ap (pwhisker_left h) !pwhisker_left_refl ⬝ !pwhisker_left_refl) ⬝ _ ⬝
!pwhisker_left_refl⁻¹ ◾** idp,
exact !trans_refl ⬝ !refl_trans⁻¹
end
theorem passoc_phomotopy_middle {A B C D : Type*} (h : C →* D) {g g' : B →* C} (f : A →* B)
(p : g ~* g') : phsquare (passoc h g f) (passoc h g' f)
(pwhisker_right f (pwhisker_left h p)) (pwhisker_left h (pwhisker_right f p)) :=
begin
induction p using phomotopy_rec_on_idp,
rewrite [pwhisker_right_refl, pwhisker_left_refl],
rewrite [pwhisker_right_refl, pwhisker_left_refl],
exact phvrfl
end
definition pwhisker_right_pwhisker_left {A B C : Type*} {g g' : B →* C} {f f' : A →* B}
(p : g ~* g') (q : f ~* f') :
phsquare (pwhisker_right f p) (pwhisker_right f' p) (pwhisker_left g q) (pwhisker_left g' q) :=
begin
induction p using phomotopy_rec_on_idp,
induction q using phomotopy_rec_on_idp,
exact !pwhisker_right_refl ◾** !pwhisker_left_refl ⬝
!pwhisker_left_refl⁻¹ ◾** !pwhisker_right_refl⁻¹
end
definition pwhisker_left_phsquare (f : B →* C) (p : phsquare p₁₀ p₁₂ p₀₁ p₂₁) :
phsquare (pwhisker_left f p₁₀) (pwhisker_left f p₁₂)
(pwhisker_left f p₀₁) (pwhisker_left f p₂₁) :=
!pwhisker_left_trans⁻¹ ⬝ ap (pwhisker_left f) p ⬝ !pwhisker_left_trans
definition pwhisker_right_phsquare (f : C →* A) (p : phsquare p₁₀ p₁₂ p₀₁ p₂₁) :
phsquare (pwhisker_right f p₁₀) (pwhisker_right f p₁₂)
(pwhisker_right f p₀₁) (pwhisker_right f p₂₁) :=
!pwhisker_right_trans⁻¹ ⬝ ap (pwhisker_right f) p ⬝ !pwhisker_right_trans
end phsquare
definition phomotopy_of_eq_con {A B : Type*} {f g h : A →* B} (p : f = g) (q : g = h) :
phomotopy_of_eq (p ⬝ q) = phomotopy_of_eq p ⬝* phomotopy_of_eq q :=
begin induction q, induction p, exact !trans_refl⁻¹ end
definition pcompose_left_eq_of_phomotopy {A B C : Type*} (g : B →* C) {f f' : A →* B}
(H : f ~* f') : ap (λf, g ∘* f) (eq_of_phomotopy H) = eq_of_phomotopy (pwhisker_left g H) :=
begin
induction H using phomotopy_rec_on_idp,
refine ap02 _ !eq_of_phomotopy_refl ⬝ !eq_of_phomotopy_refl⁻¹ ⬝ ap eq_of_phomotopy _,
exact !pwhisker_left_refl⁻¹
end
definition pcompose_right_eq_of_phomotopy {A B C : Type*} {g g' : B →* C} (f : A →* B)
(H : g ~* g') : ap (λg, g ∘* f) (eq_of_phomotopy H) = eq_of_phomotopy (pwhisker_right f H) :=
begin
induction H using phomotopy_rec_on_idp,
refine ap02 _ !eq_of_phomotopy_refl ⬝ !eq_of_phomotopy_refl⁻¹ ⬝ ap eq_of_phomotopy _,
exact !pwhisker_right_refl⁻¹
end
definition phomotopy_of_eq_pcompose_left {A B C : Type*} (g : B →* C) {f f' : A →* B}
(p : f = f') : phomotopy_of_eq (ap (λf, g ∘* f) p) = pwhisker_left g (phomotopy_of_eq p) :=
begin
induction p, exact !pwhisker_left_refl⁻¹
end
definition phomotopy_of_eq_pcompose_right {A B C : Type*} {g g' : B →* C} (f : A →* B)
(p : g = g') : phomotopy_of_eq (ap (λg, g ∘* f) p) = pwhisker_right f (phomotopy_of_eq p) :=
begin
induction p, exact !pwhisker_right_refl⁻¹
end
definition ap1_phomotopy_refl {X Y : Type*} (f : X →* Y) :
ap1_phomotopy (phomotopy.refl f) = phomotopy.refl (Ω→ f) :=
begin
-- induction X with X x₀, induction Y with Y y₀, induction f with f f₀, esimp at *, induction f₀,
-- fapply phomotopy_eq,
-- { intro x, unfold [ap1_phomotopy], },
-- { }
exact sorry
end
definition ap1_eq_of_phomotopy {A B : Type*} {f g : A →* B} (p : f ~* g) :
ap Ω→ (eq_of_phomotopy p) = eq_of_phomotopy (ap1_phomotopy p) :=
begin
induction p using phomotopy_rec_on_idp,
refine ap02 _ !eq_of_phomotopy_refl ⬝ !eq_of_phomotopy_refl⁻¹ ⬝ ap eq_of_phomotopy _,
exact !ap1_phomotopy_refl⁻¹
end
-- duplicate of ap_eq_of_phomotopy
definition to_fun_eq_of_phomotopy {A B : Type*} {f g : A →* B} (p : f ~* g) (a : A) :
ap010 pmap.to_fun (eq_of_phomotopy p) a = p a :=
begin
induction p using phomotopy_rec_on_idp,
exact ap (λx, ap010 pmap.to_fun x a) !eq_of_phomotopy_refl
end
definition respect_pt_pcompose {A B C : Type*} (g : B →* C) (f : A →* B)
: respect_pt (g ∘* f) = ap g (respect_pt f) ⬝ respect_pt g :=
idp
definition phomotopy_mk_ppmap [constructor] {A B C : Type*} {f g : A →* ppmap B C} (p : Πa, f a ~* g a)
(q : p pt ⬝* phomotopy_of_eq (respect_pt g) = phomotopy_of_eq (respect_pt f))
: f ~* g :=
begin
apply phomotopy.mk (λa, eq_of_phomotopy (p a)),
apply eq_of_fn_eq_fn (pmap_eq_equiv _ _), esimp [pmap_eq_equiv],
refine !phomotopy_of_eq_con ⬝ _,
refine !phomotopy_of_eq_of_phomotopy ◾** idp ⬝ q,
end
definition pconst_pcompose_pconst (A B C : Type*) :
pconst_pcompose (pconst A B) = pcompose_pconst (pconst B C) :=
idp
definition pconst_pcompose_phomotopy_pconst {A B C : Type*} {f : A →* B} (p : f ~* pconst A B) :
pconst_pcompose f = pwhisker_left (pconst B C) p ⬝* pcompose_pconst (pconst B C) :=
begin
assert H : Π(p : pconst A B ~* f),
pconst_pcompose f = pwhisker_left (pconst B C) p⁻¹* ⬝* pcompose_pconst (pconst B C),
{ intro p, induction p using phomotopy_rec_on_idp, reflexivity },
refine H p⁻¹* ⬝ ap (pwhisker_left _) !symm_symm ◾** idp,
end
definition passoc_pconst_right {A B C D : Type*} (h : C →* D) (g : B →* C) :
passoc h g (pconst A B) ⬝* (pwhisker_left h (pcompose_pconst g) ⬝* pcompose_pconst h) =
pcompose_pconst (h ∘* g) :=
begin
fapply phomotopy_eq,
{ intro a, exact !idp_con },
{ induction h with h h₀, induction g with g g₀, induction D with D d₀, induction C with C c₀,
esimp at *, induction g₀, induction h₀, reflexivity }
end
definition passoc_pconst_middle {A A' B B' : Type*} (g : B →* B') (f : A' →* A) :
passoc g (pconst A B) f ⬝* (pwhisker_left g (pconst_pcompose f) ⬝* pcompose_pconst g) =
pwhisker_right f (pcompose_pconst g) ⬝* pconst_pcompose f :=
begin
fapply phomotopy_eq,
{ intro a, exact !idp_con ⬝ !idp_con },
{ induction g with g g₀, induction f with f f₀, induction B' with D d₀, induction A with C c₀,
esimp at *, induction g₀, induction f₀, reflexivity }
end
definition passoc_pconst_left {A B C D : Type*} (g : B →* C) (f : A →* B) :
phsquare (passoc (pconst C D) g f) (pconst_pcompose f)
(pwhisker_right f (pconst_pcompose g)) (pconst_pcompose (g ∘* f)) :=
begin
fapply phomotopy_eq,
{ intro a, exact !idp_con },
{ induction g with g g₀, induction f with f f₀, induction C with C c₀, induction B with B b₀,
esimp at *, induction g₀, induction f₀, reflexivity }
end
definition ppcompose_left_pcompose [constructor] {A B C D : Type*} (h : C →* D) (g : B →* C) :
@ppcompose_left A _ _ (h ∘* g) ~* ppcompose_left h ∘* ppcompose_left g :=
begin
fapply phomotopy_mk_ppmap,
{ exact passoc h g },
{ refine idp ◾** (!phomotopy_of_eq_con ⬝
(ap phomotopy_of_eq !pcompose_left_eq_of_phomotopy ⬝ !phomotopy_of_eq_of_phomotopy) ◾**
!phomotopy_of_eq_of_phomotopy) ⬝ _ ⬝ !phomotopy_of_eq_of_phomotopy⁻¹,
exact passoc_pconst_right h g }
end
definition ppcompose_right_pcompose [constructor] {A B C D : Type*} (g : B →* C) (f : A →* B) :
@ppcompose_right _ _ D (g ∘* f) ~* ppcompose_right f ∘* ppcompose_right g :=
begin
symmetry,
fapply phomotopy_mk_ppmap,
{ intro h, exact passoc h g f },
{ refine idp ◾** !phomotopy_of_eq_of_phomotopy ⬝ _ ⬝ (!phomotopy_of_eq_con ⬝
(ap phomotopy_of_eq !pcompose_right_eq_of_phomotopy ⬝ !phomotopy_of_eq_of_phomotopy) ◾** !phomotopy_of_eq_of_phomotopy)⁻¹,
exact passoc_pconst_left g f }
end
definition ppcompose_left_ppcompose_right {A A' B B' : Type*} (g : B →* B') (f : A' →* A) :
psquare (ppcompose_left g) (ppcompose_left g) (ppcompose_right f) (ppcompose_right f) :=
begin
fapply phomotopy_mk_ppmap,
{ intro h, exact passoc g h f },
{ refine idp ◾** (!phomotopy_of_eq_con ⬝
(ap phomotopy_of_eq !pcompose_left_eq_of_phomotopy ⬝ !phomotopy_of_eq_of_phomotopy) ◾**
!phomotopy_of_eq_of_phomotopy) ⬝ _ ⬝ (!phomotopy_of_eq_con ⬝
(ap phomotopy_of_eq !pcompose_right_eq_of_phomotopy ⬝ !phomotopy_of_eq_of_phomotopy) ◾**
!phomotopy_of_eq_of_phomotopy)⁻¹,
apply passoc_pconst_middle }
end
definition pcompose_pconst_phomotopy {A B C : Type*} {f f' : B →* C} (p : f ~* f') :
pwhisker_right (pconst A B) p ⬝* pcompose_pconst f' = pcompose_pconst f :=
begin
fapply phomotopy_eq,
{ intro a, exact to_homotopy_pt p },
{ induction p using phomotopy_rec_on_idp, induction C with C c₀, induction f with f f₀,
esimp at *, induction f₀, reflexivity }
end
definition pid_pconst (A B : Type*) : pcompose_pconst (pid B) = pid_pcompose (pconst A B) :=
by reflexivity
definition pid_pconst_pcompose {A B C : Type*} (f : A →* B) :
phsquare (pid_pcompose (pconst B C ∘* f))
(pcompose_pconst (pid C))
(pwhisker_left (pid C) (pconst_pcompose f))
(pconst_pcompose f) :=
begin
fapply phomotopy_eq,
{ reflexivity },
{ induction f with f f₀, induction B with B b₀, esimp at *, induction f₀, reflexivity }
end
definition ppcompose_left_pconst [constructor] (A B C : Type*) :
@ppcompose_left A _ _ (pconst B C) ~* pconst (ppmap A B) (ppmap A C) :=
begin
fapply phomotopy_mk_ppmap,
{ exact pconst_pcompose },
{ refine idp ◾** !phomotopy_of_eq_idp ⬝ !phomotopy_of_eq_of_phomotopy⁻¹ }
end
definition ppcompose_left_phomotopy [constructor] {A B C : Type*} {g g' : B →* C} (p : g ~* g') :
@ppcompose_left A _ _ g ~* ppcompose_left g' :=
begin
induction p using phomotopy_rec_on_idp,
reflexivity
end
definition ppcompose_right_phomotopy [constructor] {A B C : Type*} {f f' : A →* B} (p : f ~* f') :
@ppcompose_right _ _ C f ~* ppcompose_right f' :=
begin
induction p using phomotopy_rec_on_idp,
reflexivity
end
definition pppcompose [constructor] (A B C : Type*) : ppmap B C →* ppmap (ppmap A B) (ppmap A C) :=
pmap.mk ppcompose_left (eq_of_phomotopy !ppcompose_left_pconst)
section psquare
variables {A A' A₀₀ A₂₀ A₄₀ A₀₂ A₂₂ A₄₂ A₀₄ A₂₄ A₄₄ : Type*}
{f₁₀ f₁₀' : A₀₀ →* A₂₀} {f₃₀ : A₂₀ →* A₄₀}
{f₀₁ f₀₁' : A₀₀ →* A₀₂} {f₂₁ f₂₁' : A₂₀ →* A₂₂} {f₄₁ : A₄₀ →* A₄₂}
{f₁₂ f₁₂' : A₀₂ →* A₂₂} {f₃₂ : A₂₂ →* A₄₂}
{f₀₃ : A₀₂ →* A₀₄} {f₂₃ : A₂₂ →* A₂₄} {f₄₃ : A₄₂ →* A₄₄}
{f₁₄ : A₀₄ →* A₂₄} {f₃₄ : A₂₄ →* A₄₄}
definition ppcompose_left_psquare {A : Type*} (p : psquare f₁₀ f₁₂ f₀₁ f₂₁) :
psquare (@ppcompose_left A _ _ f₁₀) (ppcompose_left f₁₂)
(ppcompose_left f₀₁) (ppcompose_left f₂₁) :=
!ppcompose_left_pcompose⁻¹* ⬝* ppcompose_left_phomotopy p ⬝* !ppcompose_left_pcompose
definition ppcompose_right_psquare {A : Type*} (p : psquare f₁₀ f₁₂ f₀₁ f₂₁) :
psquare (@ppcompose_right _ _ A f₁₂) (ppcompose_right f₁₀)
(ppcompose_right f₂₁) (ppcompose_right f₀₁) :=
!ppcompose_right_pcompose⁻¹* ⬝* ppcompose_right_phomotopy p⁻¹* ⬝* !ppcompose_right_pcompose
definition trans_phomotopy_hconcat {f₀₁' f₀₁''}
(q₂ : f₀₁'' ~* f₀₁') (q₁ : f₀₁' ~* f₀₁) (p : psquare f₁₀ f₁₂ f₀₁ f₂₁) :
(q₂ ⬝* q₁) ⬝ph* p = q₂ ⬝ph* q₁ ⬝ph* p :=
idp ◾** (ap (pwhisker_left f₁₂) !trans_symm ⬝ !pwhisker_left_trans) ⬝ !trans_assoc⁻¹
definition symm_phomotopy_hconcat {f₀₁'} (q : f₀₁ ~* f₀₁')
(p : psquare f₁₀ f₁₂ f₀₁ f₂₁) : q⁻¹* ⬝ph* p = p ⬝* pwhisker_left f₁₂ q :=
idp ◾** ap (pwhisker_left f₁₂) !symm_symm
definition refl_phomotopy_hconcat (p : psquare f₁₀ f₁₂ f₀₁ f₂₁) : phomotopy.rfl ⬝ph* p = p :=
idp ◾** (ap (pwhisker_left _) !refl_symm ⬝ !pwhisker_left_refl) ⬝ !trans_refl
local attribute phomotopy.rfl [reducible]
theorem pwhisker_left_phomotopy_hconcat {f₀₁'} (r : f₀₁' ~* f₀₁)
(p : psquare f₁₀ f₁₂ f₀₁ f₂₁) (q : psquare f₁₂ f₁₄ f₀₃ f₂₃) :
pwhisker_left f₀₃ r ⬝ph* (p ⬝v* q) = (r ⬝ph* p) ⬝v* q :=
by induction r using phomotopy_rec_on_idp; rewrite [pwhisker_left_refl, +refl_phomotopy_hconcat]
theorem pvcompose_pwhisker_left {f₀₁'} (r : f₀₁ ~* f₀₁')
(p : psquare f₁₀ f₁₂ f₀₁ f₂₁) (q : psquare f₁₂ f₁₄ f₀₃ f₂₃) :
(p ⬝v* q) ⬝* (pwhisker_left f₁₄ (pwhisker_left f₀₃ r)) = (p ⬝* pwhisker_left f₁₂ r) ⬝v* q :=
by induction r using phomotopy_rec_on_idp; rewrite [+pwhisker_left_refl, + trans_refl]
definition phconcat2 {p p' : psquare f₁₀ f₁₂ f₀₁ f₂₁} {q q' : psquare f₃₀ f₃₂ f₂₁ f₄₁}
(r : p = p') (s : q = q') : p ⬝h* q = p' ⬝h* q' :=
ap011 phconcat r s
definition pvconcat2 {p p' : psquare f₁₀ f₁₂ f₀₁ f₂₁} {q q' : psquare f₁₂ f₁₄ f₀₃ f₂₃}
(r : p = p') (s : q = q') : p ⬝v* q = p' ⬝v* q' :=
ap011 pvconcat r s
definition phinverse2 {f₁₀ : A₀₀ ≃* A₂₀} {f₁₂ : A₀₂ ≃* A₂₂} {p p' : psquare f₁₀ f₁₂ f₀₁ f₂₁}
(r : p = p') : p⁻¹ʰ* = p'⁻¹ʰ* :=
ap phinverse r
definition pvinverse2 {f₀₁ : A₀₀ ≃* A₀₂} {f₂₁ : A₂₀ ≃* A₂₂} {p p' : psquare f₁₀ f₁₂ f₀₁ f₂₁}
(r : p = p') : p⁻¹ᵛ* = p'⁻¹ᵛ* :=
ap pvinverse r
definition phomotopy_hconcat2 {q q' : f₀₁' ~* f₀₁} {p p' : psquare f₁₀ f₁₂ f₀₁ f₂₁}
(r : q = q') (s : p = p') : q ⬝ph* p = q' ⬝ph* p' :=
ap011 phomotopy_hconcat r s
definition hconcat_phomotopy2 {p p' : psquare f₁₀ f₁₂ f₀₁ f₂₁} {q q' : f₂₁' ~* f₂₁}
(r : p = p') (s : q = q') : p ⬝hp* q = p' ⬝hp* q' :=
ap011 hconcat_phomotopy r s
definition phomotopy_vconcat2 {q q' : f₁₀' ~* f₁₀} {p p' : psquare f₁₀ f₁₂ f₀₁ f₂₁}
(r : q = q') (s : p = p') : q ⬝pv* p = q' ⬝pv* p' :=
ap011 phomotopy_vconcat r s
definition vconcat_phomotopy2 {p p' : psquare f₁₀ f₁₂ f₀₁ f₂₁} {q q' : f₁₂' ~* f₁₂}
(r : p = p') (s : q = q') : p ⬝vp* q = p' ⬝vp* q' :=
ap011 vconcat_phomotopy r s
-- for consistency, should there be a second star here?
infix ` ◾h* `:79 := phconcat2
infix ` ◾v* `:79 := pvconcat2
infixl ` ◾hp* `:79 := hconcat_phomotopy2
infixr ` ◾ph* `:79 := phomotopy_hconcat2
infixl ` ◾vp* `:79 := vconcat_phomotopy2
infixr ` ◾pv* `:79 := phomotopy_vconcat2
postfix `⁻²ʰ*`:(max+1) := phinverse2
postfix `⁻²ᵛ*`:(max+1) := pvinverse2
end psquare
/- a more explicit proof of ppcompose_left_phomotopy, which might be useful if we need to prove properties about it
-/
-- fapply phomotopy_mk_ppmap,
-- { intro f, exact pwhisker_right f p },
-- { refine ap (λx, _ ⬝* x) !phomotopy_of_eq_of_phomotopy ⬝ _ ⬝ !phomotopy_of_eq_of_phomotopy⁻¹,
-- exact pcompose_pconst_phomotopy p }
definition ppcompose_left_phomotopy_refl {A B C : Type*} (g : B →* C) :
ppcompose_left_phomotopy (phomotopy.refl g) = phomotopy.refl (@ppcompose_left A _ _ g) :=
!phomotopy_rec_on_idp_refl
-- definition pmap_eq_equiv {X Y : Type*} (f g : X →* Y) : (f = g) ≃ (f ~* g) :=
-- begin
@ -886,7 +38,7 @@ namespace pointed
ap (λx, eq_of_phomotopy (phomotopy.mk _ x)) !inv_inv ⬝ eq_of_phomotopy_refl f
definition pfunext (X Y : Type*) : ppmap X (Ω Y) ≃* Ω (ppmap X Y) :=
(loop_pmap_commute X Y)⁻¹ᵉ*
(loop_ppmap_commute X Y)⁻¹ᵉ*
definition loop_phomotopy [constructor] {A B : Type*} (f : A →* B) : Type* :=
pointed.MK (f ~* f) phomotopy.rfl
@ -900,21 +52,10 @@ namespace pointed
: loop_phomotopy f →* loop_phomotopy (g ∘* f) :=
pmap.mk (λq, pwhisker_left g q) !pwhisker_left_refl
definition ppcompose_left_loop_phomotopy_refl {A B C : Type*} (g : B →* C) (f : A →* B)
: ppcompose_left_loop_phomotopy g phomotopy.rfl ~* ppcompose_left_loop_phomotopy' g f :=
phomotopy.mk (λq, !refl_symm ◾** idp ◾** idp ⬝ !refl_trans ◾** idp ⬝ !trans_refl)
begin
esimp, exact sorry
end
definition loop_ppmap_pequiv' [constructor] (A B : Type*) :
Ω(ppmap A B) ≃* loop_phomotopy (pconst A B) :=
pequiv_of_equiv (pmap_eq_equiv _ _) idp
-- definition loop_ppmap (A B : Type*) : pointed.MK (pconst A B ~* pconst A B) phomotopy.rfl ≃*
-- pointed.MK (Σ(p : pconst A B ~ pconst A B), p pt ⬝ rfl = rfl) ⟨homotopy.rfl, idp⟩ :=
-- pequiv_of_equiv !phomotopy.sigma_char _
definition ppmap_loop_pequiv' [constructor] (A B : Type*) :
loop_phomotopy (pconst A B) ≃* ppmap A (Ω B) :=
pequiv_of_equiv (!phomotopy.sigma_char ⬝e !pmap.sigma_char⁻¹ᵉ) idp
@ -943,9 +84,6 @@ namespace pointed
induction X' with X' x₀', induction f with f f₀, esimp at f, esimp at f₀, induction f₀,
apply psquare_of_phomotopy,
exact sorry
-- fapply phomotopy.mk,
-- { esimp, esimp [pmap_eq_equiv], intro p, },
-- { }
end
definition ppmap_loop_pequiv'_natural_right {X X' : Type*} (A : Type*) (f : X →* X') :
@ -967,12 +105,12 @@ namespace pointed
end
definition loop_pmap_commute_natural_left {A A' : Type*} (X : Type*) (f : A' →* A) :
psquare (loop_pmap_commute A X) (loop_pmap_commute A' X)
psquare (loop_ppmap_commute A X) (loop_ppmap_commute A' X)
(Ω→ (ppcompose_right f)) (ppcompose_right f) :=
sorry
definition loop_pmap_commute_natural_right {X X' : Type*} (A : Type*) (f : X →* X') :
psquare (loop_pmap_commute A X) (loop_pmap_commute A X')
psquare (loop_ppmap_commute A X) (loop_ppmap_commute A X')
(Ω→ (ppcompose_left f)) (ppcompose_left (Ω→ f)) :=
loop_ppmap_pequiv'_natural_right A f ⬝h* ppmap_loop_pequiv'_natural_right A f
@ -1004,76 +142,5 @@ namespace pointed
-- definition phomotopy_eq_equiv_phomotopy2 : p = q ≃ p ~*2 q :=
-- sorry
variables {X X' Y Y' Z : Type*}
definition pap1 [constructor] (X Y : Type*) : ppmap X Y →* ppmap (Ω X) (Ω Y) :=
pmap.mk ap1 (eq_of_phomotopy !ap1_pconst)
definition ap1_gen_const {A B : Type} {a₁ a₂ : A} (b : B) (p : a₁ = a₂) :
ap1_gen (const A b) idp idp p = idp :=
ap1_gen_idp_left (const A b) p ⬝ ap_constant p b
definition ap1_gen_compose_const_left
{A B C : Type} (c : C) (f : A → B) {a₁ a₂ : A} (p : a₁ = a₂) :
ap1_gen_compose (const B c) f idp idp idp idp p ⬝
ap1_gen_const c (ap1_gen f idp idp p) =
ap1_gen_const c p :=
begin induction p, reflexivity end
definition ap1_gen_compose_const_right
{A B C : Type} (g : B → C) (b : B) {a₁ a₂ : A} (p : a₁ = a₂) :
ap1_gen_compose g (const A b) idp idp idp idp p ⬝
ap (ap1_gen g idp idp) (ap1_gen_const b p) =
ap1_gen_const (g b) p :=
begin induction p, reflexivity end
definition ap1_pcompose_pconst_left {A B C : Type*} (f : A →* B) :
phsquare (ap1_pcompose (pconst B C) f)
(ap1_pconst A C)
(ap1_phomotopy (pconst_pcompose f))
(pwhisker_right (Ω→ f) (ap1_pconst B C) ⬝* pconst_pcompose (Ω→ f)) :=
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₀,
refine idp ◾** !trans_refl ⬝ _ ⬝ !refl_trans⁻¹ ⬝ !ap1_phomotopy_refl⁻¹ ◾** idp,
fapply phomotopy_eq,
{ exact ap1_gen_compose_const_left c₀ f },
{ reflexivity }
end
definition ap1_pcompose_pconst_right {A B C : Type*} (g : B →* C) :
phsquare (ap1_pcompose g (pconst A B))
(ap1_pconst A C)
(ap1_phomotopy (pcompose_pconst g))
(pwhisker_left (Ω→ g) (ap1_pconst A B) ⬝* pcompose_pconst (Ω→ g)) :=
begin
induction A with A a₀, induction B with B b₀, induction C with C c₀, induction g with g g₀,
esimp at *, induction g₀,
refine idp ◾** !trans_refl ⬝ _ ⬝ !refl_trans⁻¹ ⬝ !ap1_phomotopy_refl⁻¹ ◾** idp,
fapply phomotopy_eq,
{ exact ap1_gen_compose_const_right g b₀ },
{ reflexivity }
end
definition pap1_natural_left [constructor] (f : X' →* X) :
psquare (pap1 X Y) (pap1 X' Y) (ppcompose_right f) (ppcompose_right (Ω→ f)) :=
begin
fapply phomotopy_mk_ppmap,
{ intro g, exact !ap1_pcompose⁻¹* },
{ refine idp ◾** (ap phomotopy_of_eq (!ap1_eq_of_phomotopy ◾ idp ⬝ !eq_of_phomotopy_trans⁻¹) ⬝
!phomotopy_of_eq_of_phomotopy) ⬝ _ ⬝ (ap phomotopy_of_eq (!pcompose_right_eq_of_phomotopy ◾
idp ⬝ !eq_of_phomotopy_trans⁻¹) ⬝ !phomotopy_of_eq_of_phomotopy)⁻¹,
apply symm_trans_eq_of_eq_trans, exact (ap1_pcompose_pconst_left f)⁻¹ }
end
definition pap1_natural_right [constructor] (f : Y →* Y') :
psquare (pap1 X Y) (pap1 X Y') (ppcompose_left f) (ppcompose_left (Ω→ f)) :=
begin
fapply phomotopy_mk_ppmap,
{ intro g, exact !ap1_pcompose⁻¹* },
{ refine idp ◾** (ap phomotopy_of_eq (!ap1_eq_of_phomotopy ◾ idp ⬝ !eq_of_phomotopy_trans⁻¹) ⬝
!phomotopy_of_eq_of_phomotopy) ⬝ _ ⬝ (ap phomotopy_of_eq (!pcompose_left_eq_of_phomotopy ◾
idp ⬝ !eq_of_phomotopy_trans⁻¹) ⬝ !phomotopy_of_eq_of_phomotopy)⁻¹,
apply symm_trans_eq_of_eq_trans, exact (ap1_pcompose_pconst_right f)⁻¹ }
end
end pointed