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

move things to the Lean library, and update after changes in the Lean library

Browse source
This commit is contained in:
Floris van Doorn 2016-11-23 23:54:57 -05:00
parent 4f1db25e16
commit b08457c77f
21 changed files with 200 additions and 2194 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

16
algebra/arrow_group.hlean
View file

@ -21,12 +21,12 @@ namespace group
definition Group_arrow (A : Type) (G : Group) : Group :=
Group.mk (A → G) _
definition comm_group_arrow [instance] (A B : Type) [comm_group B] : comm_group (A → B) :=
⦃comm_group, group_arrow A B,
definition ab_group_arrow [instance] (A B : Type) [ab_group B] : ab_group (A → B) :=
⦃ab_group, group_arrow A B,
mul_comm := by intros; apply eq_of_homotopy; intro a; apply mul.comm⦄
definition CommGroup_arrow (A : Type) (G : CommGroup) : CommGroup :=
CommGroup.mk (A → G) _
definition AbGroup_arrow (A : Type) (G : AbGroup) : AbGroup :=
AbGroup.mk (A → G) _
definition pgroup_ppmap [instance] (A B : Type*) [pgroup B] : pgroup (ppmap A B) :=
begin
@ -44,12 +44,12 @@ namespace group
definition Group_pmap (A : Type*) (G : Group) : Group :=
Group_of_pgroup (ppmap A (pType_of_Group G))
definition CommGroup_pmap (A : Type*) (G : CommGroup) : CommGroup :=
CommGroup.mk (A →* pType_of_Group G)
⦃ comm_group, Group.struct (Group_pmap A G),
definition AbGroup_pmap (A : Type*) (G : AbGroup) : AbGroup :=
AbGroup.mk (A →* pType_of_Group G)
⦃ ab_group, Group.struct (Group_pmap A G),
mul_comm := by intro f g; apply pmap_eq_of_homotopy; intro a; apply mul.comm ⦄
definition Group_pmap_homomorphism [constructor] {A A' : Type*} (f : A' →* A) (G : CommGroup) :
definition Group_pmap_homomorphism [constructor] {A A' : Type*} (f : A' →* A) (G : AbGroup) :
Group_pmap A G →g Group_pmap A' G :=
begin
fapply homomorphism.mk,

18
algebra/direct_sum.hlean
View file

@ -13,21 +13,21 @@ open eq algebra is_trunc set_quotient relation sigma prod sum list trunc functio
namespace group
variables {G G' : Group} (H : subgroup_rel G) (N : normal_subgroup_rel G) {g g' h h' k : G}
{A B : CommGroup}
{A B : AbGroup}
variables (X : Set) {l l' : list (X ⊎ X)}
section
parameters {I : Set} (Y : I → CommGroup)
variables {A' : CommGroup}
parameters {I : Set} (Y : I → AbGroup)
variables {A' : AbGroup}
definition dirsum_carrier : CommGroup := free_comm_group (trunctype.mk (Σi, Y i) _)
local abbreviation ι [constructor] := @free_comm_group_inclusion
definition dirsum_carrier : AbGroup := free_ab_group (trunctype.mk (Σi, Y i) _)
local abbreviation ι [constructor] := @free_ab_group_inclusion
inductive dirsum_rel : dirsum_carrier → Type :=
| rmk : Πi y₁ y₂, dirsum_rel (ι ⟨i, y₁⟩ * ι ⟨i, y₂⟩ * (ι ⟨i, y₁ * y₂⟩)⁻¹)
definition dirsum : CommGroup := quotient_comm_group_gen dirsum_carrier (λg, ∥dirsum_rel g∥)
definition dirsum : AbGroup := quotient_ab_group_gen dirsum_carrier (λg, ∥dirsum_rel g∥)
-- definition dirsum_carrier_incl [constructor] (i : I) : Y i →g dirsum_carrier :=
@ -36,7 +36,7 @@ namespace group
begin intro g h, symmetry, apply gqg_eq_of_rel, apply tr, apply dirsum_rel.rmk end
definition dirsum_elim_resp_quotient (f : Πi, Y i →g A') (g : dirsum_carrier)
(r : ∥dirsum_rel g∥) : free_comm_group_elim (λv, f v.1 v.2) g = 1 :=
(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_mul, to_respect_inv], apply mul_inv_eq_of_eq_mul,
@ -44,7 +44,7 @@ namespace group
end
definition dirsum_elim [constructor] (f : Πi, Y i →g A') : dirsum →g A' :=
gqg_elim _ (free_comm_group_elim (λv, f v.1 v.2)) (dirsum_elim_resp_quotient f)
gqg_elim _ (free_ab_group_elim (λv, f v.1 v.2)) (dirsum_elim_resp_quotient f)
definition dirsum_elim_compute (f : Πi, Y i →g A') (i : I) :
dirsum_elim f ∘g dirsum_incl i ~ f i :=
@ -56,7 +56,7 @@ namespace group
(H : Πi, k ∘g dirsum_incl i ~ f i) : k ~ dirsum_elim f :=
begin
apply gqg_elim_unique,
apply free_comm_group_elim_unique,
apply free_ab_group_elim_unique,
intro x, induction x with i y, exact H i y
end

24
algebra/exact_couple.hlean
View file

@ -11,13 +11,13 @@ import algebra.group_theory hit.set_quotient types.sigma types.list types.sum .q
open eq algebra is_trunc set_quotient relation sigma sigma.ops prod prod.ops sum list trunc function group trunc
equiv
structure is_exact {A B C : CommGroup} (f : A →g B) (g : B →g C) :=
structure is_exact {A B C : AbGroup} (f : A →g B) (g : B →g C) :=
( im_in_ker : Π(a:A), g (f a) = 1)
( ker_in_im : Π(b:B), (g b = 1) → ∃(a:A), f a = b)
definition is_differential {B : CommGroup} (d : B →g B) := Π(b:B), d (d b) = 1
definition is_differential {B : AbGroup} (d : B →g B) := Π(b:B), d (d b) = 1
definition image_subgroup_of_diff {B : CommGroup} (d : B →g B) (H : is_differential d) : subgroup_rel (comm_kernel d) :=
definition image_subgroup_of_diff {B : AbGroup} (d : B →g B) (H : is_differential d) : subgroup_rel (ab_kernel d) :=
subgroup_rel_of_subgroup (image_subgroup d) (kernel_subgroup d)
begin
intro g p,
@ -27,19 +27,19 @@ definition image_subgroup_of_diff {B : CommGroup} (d : B →g B) (H : is_differe
exact H h
end
definition homology {B : CommGroup} (d : B →g B) (H : is_differential d) : CommGroup :=
@quotient_comm_group (comm_kernel d) (image_subgroup_of_diff d H)
definition homology {B : AbGroup} (d : B →g B) (H : is_differential d) : AbGroup :=
@quotient_ab_group (ab_kernel d) (image_subgroup_of_diff d H)
structure exact_couple (A B : CommGroup) : Type :=
structure exact_couple (A B : AbGroup) : Type :=
( i : A →g A) (j : A →g B) (k : B →g A)
( exact_ij : is_exact i j)
( exact_jk : is_exact j k)
( exact_ki : is_exact k i)
definition differential {A B : CommGroup} (EC : exact_couple A B) : B →g B :=
definition differential {A B : AbGroup} (EC : exact_couple A B) : B →g B :=
(exact_couple.j EC) ∘g (exact_couple.k EC)
definition differential_is_differential {A B : CommGroup} (EC : exact_couple A B) : is_differential (differential EC) :=
definition differential_is_differential {A B : AbGroup} (EC : exact_couple A B) : is_differential (differential EC) :=
begin
induction EC,
induction exact_jk,
@ -49,12 +49,12 @@ definition differential_is_differential {A B : CommGroup} (EC : exact_couple A B
section derived_couple
variables {A B : CommGroup} (EC : exact_couple A B)
variables {A B : AbGroup} (EC : exact_couple A B)
definition derived_couple_A : CommGroup :=
comm_subgroup (image_subgroup (exact_couple.i EC))
definition derived_couple_A : AbGroup :=
ab_subgroup (image_subgroup (exact_couple.i EC))
definition derived_couple_B : CommGroup :=
definition derived_couple_B : AbGroup :=
homology (differential EC) (differential_is_differential EC)
definition derived_couple_i : derived_couple_A EC →g derived_couple_A EC :=

40
algebra/free_commutative_group.hlean
View file

@ -12,12 +12,12 @@ open eq algebra is_trunc set_quotient relation sigma sigma.ops prod sum list tru
namespace group
variables {G G' : Group} {g g' h h' k : G} {A B : CommGroup}
variables {G G' : Group} {g g' h h' k : G} {A B : AbGroup}
variables (X : Set) {l l' : list (X ⊎ X)}
/- Free Commutative Group of a set -/
namespace free_comm_group
/- Free Abelian Group of a set -/
namespace free_ab_group
inductive fcg_rel : list (X ⊎ X) → list (X ⊎ X) → Type :=
| rrefl : Πl, fcg_rel l l
@ -133,22 +133,22 @@ namespace group
rewrite [-append_concat], apply IH}
end
end
end free_comm_group open free_comm_group
end free_ab_group open free_ab_group
variables (X)
definition group_free_comm_group [constructor] : comm_group (fcg_carrier X) :=
comm_group.mk fcg_mul _ fcg_mul_assoc fcg_one fcg_one_mul fcg_mul_one
definition group_free_ab_group [constructor] : ab_group (fcg_carrier X) :=
ab_group.mk fcg_mul _ fcg_mul_assoc fcg_one fcg_one_mul fcg_mul_one
fcg_inv fcg_mul_left_inv fcg_mul_comm
definition free_comm_group [constructor] : CommGroup :=
CommGroup.mk _ (group_free_comm_group X)
definition free_ab_group [constructor] : AbGroup :=
AbGroup.mk _ (group_free_ab_group X)
/- The universal property of the free commutative group -/
variables {X A}
definition free_comm_group_inclusion [constructor] (x : X) : free_comm_group X :=
definition free_ab_group_inclusion [constructor] (x : X) : free_ab_group X :=
class_of [inl x]
theorem fgh_helper_respect_comm_rel (f : X → A) (r : fcg_rel X l l')
theorem fgh_helper_respect_fcg_rel (f : X → A) (r : fcg_rel X l l')
: Π(g : A), foldl (fgh_helper f) g l = foldl (fgh_helper f) g l' :=
begin
induction r with l x x x y l₁ l₂ l₃ l₄ r₁ r₂ IH₁ IH₂ l₁ l₂ l₃ r₁ r₂ IH₁ IH₂: intro g,
@ -160,22 +160,22 @@ namespace group
{ exact !IH₁ ⬝ !IH₂}
end
definition free_comm_group_elim [constructor] (f : X → A) : free_comm_group X →g A :=
definition free_ab_group_elim [constructor] (f : X → A) : free_ab_group X →g A :=
begin
fapply homomorphism.mk,
{ intro g, refine set_quotient.elim _ _ g,
{ intro l, exact foldl (fgh_helper f) 1 l},
{ intro l l' r, esimp at *, refine trunc.rec _ r, clear r, intro r,
exact fgh_helper_respect_comm_rel f r 1}},
exact fgh_helper_respect_fcg_rel f r 1}},
{ refine set_quotient.rec_prop _, intro l, refine set_quotient.rec_prop _, intro l',
esimp, refine !foldl_append ⬝ _, esimp, apply fgh_helper_mul}
end
definition fn_of_free_comm_group_elim [unfold_full] (φ : free_comm_group X →g A) : X → A :=
φ ∘ free_comm_group_inclusion
definition fn_of_free_ab_group_elim [unfold_full] (φ : free_ab_group X →g A) : X → A :=
φ ∘ free_ab_group_inclusion
definition free_comm_group_elim_unique [constructor] (f : X → A) (k : free_comm_group X →g A)
(H : k ∘ free_comm_group_inclusion ~ f) : k ~ free_comm_group_elim f :=
definition free_ab_group_elim_unique [constructor] (f : X → A) (k : free_ab_group X →g A)
(H : k ∘ free_ab_group_inclusion ~ f) : k ~ free_ab_group_elim f :=
begin
refine set_quotient.rec_prop _, intro l, esimp,
induction l with s l IH,
@ -187,13 +187,13 @@ namespace group
end
variables (X A)
definition free_comm_group_elim_equiv_fn [constructor] : (free_comm_group X →g A) ≃ (X → A) :=
definition free_ab_group_elim_equiv_fn [constructor] : (free_ab_group X →g A) ≃ (X → A) :=
begin
fapply equiv.MK,
{ exact fn_of_free_comm_group_elim},
{ exact free_comm_group_elim},
{ exact fn_of_free_ab_group_elim},
{ exact free_ab_group_elim},
{ intro f, apply eq_of_homotopy, intro x, esimp, unfold [foldl], apply one_mul},
{ intro k, symmetry, apply homomorphism_eq, apply free_comm_group_elim_unique,
{ intro k, symmetry, apply homomorphism_eq, apply free_ab_group_elim_unique,
reflexivity }
end

2
algebra/free_group.hlean
View file

@ -12,7 +12,7 @@ open eq algebra is_trunc set_quotient relation sigma sigma.ops prod sum list tru
namespace group
variables {G G' : Group} {g g' h h' k : G} {A B : CommGroup}
variables {G G' : Group} {g g' h h' k : G} {A B : AbGroup}
/- Free Group of a set -/
variables (X : Set) {l l' : list (X ⊎ X)}

16
algebra/group_constructions.hlean
View file

@ -11,29 +11,29 @@ import .free_commutative_group
open eq algebra is_trunc sigma sigma.ops prod trunc function equiv
namespace group
variables {G G' : Group} {g g' h h' k : G} {A B : CommGroup}
variables {G G' : Group} {g g' h h' k : G} {A B : AbGroup}
/- Tensor group (WIP) -/
/- namespace tensor_group
variables {A B}
local abbreviation ι := @free_comm_group_inclusion
local abbreviation ι := @free_ab_group_inclusion
inductive tensor_rel_type : free_comm_group (Set_of_Group A ×t Set_of_Group B) → Type :=
inductive tensor_rel_type : free_ab_group (Set_of_Group A ×t Set_of_Group B) → Type :=
| mul_left : Π(a₁ a₂ : A) (b : B), tensor_rel_type (ι (a₁, b) * ι (a₂, b) * (ι (a₁ * a₂, b))⁻¹)
| mul_right : Π(a : A) (b₁ b₂ : B), tensor_rel_type (ι (a, b₁) * ι (a, b₂) * (ι (a, b₁ * b₂))⁻¹)
open tensor_rel_type
definition tensor_rel' (x : free_comm_group (Set_of_Group A ×t Set_of_Group B)) : Prop :=
definition tensor_rel' (x : free_ab_group (Set_of_Group A ×t Set_of_Group B)) : Prop :=
∥ tensor_rel_type x ∥
definition tensor_group_rel (A B : CommGroup)
: normal_subgroup_rel (free_comm_group (Set_of_Group A ×t Set_of_Group B)) :=
definition tensor_group_rel (A B : AbGroup)
: normal_subgroup_rel (free_ab_group (Set_of_Group A ×t Set_of_Group B)) :=
sorry /- relation generated by tensor_rel'-/
definition tensor_group [constructor] : CommGroup :=
quotient_comm_group (tensor_group_rel A B)
definition tensor_group [constructor] : AbGroup :=
quotient_ab_group (tensor_group_rel A B)
end tensor_group-/

10
algebra/module.hlean
View file

@ -17,7 +17,7 @@ infixl ` • `:73 := has_scalar.smul
/- modules over a ring -/
structure left_module (R M : Type) [ringR : ring R] extends has_scalar R M, comm_group M renaming
structure left_module (R M : Type) [ringR : ring R] extends has_scalar R M, ab_group M renaming
mul→add mul_assoc→add_assoc one→zero one_mul→zero_add mul_one→add_zero inv→neg
mul_left_inv→add_left_inv mul_comm→add_comm :=
(smul_left_distrib : Π (r : R) (x y : M), smul r (add x y) = (add (smul r x) (smul r y)))
@ -26,12 +26,12 @@ structure left_module (R M : Type) [ringR : ring R] extends has_scalar R M, comm
(one_smul : Π x, smul one x = x)
/- we make it a class now (and not as part of the structure) to avoid
left_module.to_comm_group to be an instance -/
left_module.to_ab_group to be an instance -/
attribute left_module [class]
definition add_comm_group_of_left_module [reducible] [trans_instance] (R M : Type) [K : ring R]
[H : left_module R M] : add_comm_group M :=
@left_module.to_comm_group R M K H
definition add_ab_group_of_left_module [reducible] [trans_instance] (R M : Type) [K : ring R]
[H : left_module R M] : add_ab_group M :=
@left_module.to_ab_group R M K H
definition has_scalar_of_left_module [reducible] [trans_instance] (R M : Type) [K : ring R]
[H : left_module R M] : has_scalar R M :=

12
algebra/product_group.hlean
View file

@ -13,7 +13,7 @@ open eq algebra is_trunc set_quotient relation sigma sigma.ops prod prod.ops sum
namespace group
variables {G G' : Group} (H : subgroup_rel G) (N : normal_subgroup_rel G) {g g' h h' k : G}
{A B : CommGroup}
{A B : AbGroup}
/- Binary products (direct product) of Groups -/
definition product_one [constructor] : G × G' := (one, one)
@ -39,7 +39,7 @@ namespace group
theorem product_mul_left_inv (g : G × G') : g⁻¹ * g = 1 :=
prod_eq !mul.left_inv !mul.left_inv
theorem product_mul_comm {G G' : CommGroup} (g h : G × G') : g * h = h * g :=
theorem product_mul_comm {G G' : AbGroup} (g h : G × G') : g * h = h * g :=
prod_eq !mul.comm !mul.comm
end
@ -52,11 +52,11 @@ namespace group
definition product [constructor] : Group :=
Group.mk _ (group_prod G G')
definition comm_group_prod [constructor] (G G' : CommGroup) : comm_group (G × G') :=
⦃comm_group, group_prod G G', mul_comm := product_mul_comm⦄
definition ab_group_prod [constructor] (G G' : AbGroup) : ab_group (G × G') :=
⦃ab_group, group_prod G G', mul_comm := product_mul_comm⦄
definition comm_product [constructor] (G G' : CommGroup) : CommGroup :=
CommGroup.mk _ (comm_group_prod G G')
definition ab_product [constructor] (G G' : AbGroup) : AbGroup :=
AbGroup.mk _ (ab_group_prod G G')
infix ` ×g `:30 := group.product

62
algebra/quotient_group.hlean
View file

@ -13,7 +13,7 @@ open eq algebra is_trunc set_quotient relation sigma sigma.ops prod trunc functi
namespace group
variables {G G' : Group} (H : subgroup_rel G) (N : normal_subgroup_rel G) {g g' h h' k : G}
variables {A B : CommGroup}
variables {A B : AbGroup}
/- Quotient Group -/
@ -113,7 +113,7 @@ namespace group
exact ap class_of !mul.left_inv
end
theorem quotient_mul_comm {G : CommGroup} {N : normal_subgroup_rel G} (g h : qg N)
theorem quotient_mul_comm {G : AbGroup} {N : normal_subgroup_rel G} (g h : qg N)
: g * h = h * g :=
begin
refine set_quotient.rec_prop _ g, clear g, intro g,
@ -131,18 +131,18 @@ namespace group
definition quotient_group [constructor] : Group :=
Group.mk _ (group_qg N)
definition comm_group_qg [constructor] {G : CommGroup} (N : normal_subgroup_rel G)
: comm_group (qg N) :=
⦃comm_group, group_qg N, mul_comm := quotient_mul_comm⦄
definition ab_group_qg [constructor] {G : AbGroup} (N : normal_subgroup_rel G)
: ab_group (qg N) :=
⦃ab_group, group_qg N, mul_comm := quotient_mul_comm⦄
definition quotient_comm_group [constructor] {G : CommGroup} (N : subgroup_rel G)
: CommGroup :=
CommGroup.mk _ (comm_group_qg (normal_subgroup_rel_comm N))
definition quotient_ab_group [constructor] {G : AbGroup} (N : subgroup_rel G)
: AbGroup :=
AbGroup.mk _ (ab_group_qg (normal_subgroup_rel_ab N))
definition qg_map [constructor] : G →g quotient_group N :=
homomorphism.mk class_of (λ g h, idp)
definition comm_gq_map {G : CommGroup} (N : subgroup_rel G) : G →g quotient_comm_group N :=
definition ab_gq_map {G : AbGroup} (N : subgroup_rel G) : G →g quotient_ab_group N :=
begin
fapply homomorphism.mk,
exact class_of,
@ -166,7 +166,7 @@ namespace group
unfold quotient_rel, rewrite e, exact H
end
definition comm_gq_map_eq_one {K : subgroup_rel A} (g :A) (H : K g) : comm_gq_map K g = 1 :=
definition ab_gq_map_eq_one {K : subgroup_rel A} (g :A) (H : K g) : ab_gq_map K g = 1 :=
begin
apply eq_of_rel,
have e : (g * 1⁻¹ = g),
@ -237,17 +237,17 @@ namespace group
{fapply is_prop.elimo} }
end
definition comm_group_quotient_homomorphism (A B : CommGroup)(K : subgroup_rel A)(L : subgroup_rel B) (f : A →g B)
(p : Π(a:A), K(a) → L(f a)) : quotient_comm_group K →g quotient_comm_group L :=
definition ab_group_quotient_homomorphism (A B : AbGroup)(K : subgroup_rel A)(L : subgroup_rel B) (f : A →g B)
(p : Π(a:A), K(a) → L(f a)) : quotient_ab_group K →g quotient_ab_group L :=
begin
fapply quotient_group_elim,
exact (comm_gq_map L) ∘g f,
exact (ab_gq_map L) ∘g f,
intro a,
intro k,
exact @comm_gq_map_eq_one B L (f a) (p a k),
exact @ab_gq_map_eq_one B L (f a) (p a k),
end
definition comm_group_first_iso_thm (A B : CommGroup) (f : A →g B) : quotient_comm_group (kernel_subgroup f) ≃g comm_image f :=
definition ab_group_first_iso_thm (A B : AbGroup) (f : A →g B) : quotient_ab_group (kernel_subgroup f) ≃g ab_image f :=
begin
fapply isomorphism.mk,
fapply quotient_group_elim,
@ -260,7 +260,7 @@ definition comm_group_first_iso_thm (A B : CommGroup) (f : A →g B) : quotient_
-- show that the above map is injective and surjective.
end
definition comm_group_kernel_factor {A B C: CommGroup} (f : A →g B)(g : A →g C){i : C →g B}(H : f = i ∘g g )
definition ab_group_kernel_factor {A B C: AbGroup} (f : A →g B)(g : A →g C){i : C →g B}(H : f = i ∘g g )
: Π a:A , kernel_subgroup(g)(a) → kernel_subgroup(f)(a) :=
begin
intro a,
@ -271,12 +271,12 @@ definition comm_group_kernel_factor {A B C: CommGroup} (f : A →g B)(g : A →g
... = 1 : respect_one i
end
definition comm_group_kernel_equivalent {A B : CommGroup} (C : CommGroup) (f : A →g B)(g : A →g C)(i : C →g B)(H : f = i ∘g g )(K : is_embedding i)
definition ab_group_kernel_equivalent {A B : AbGroup} (C : AbGroup) (f : A →g B)(g : A →g C)(i : C →g B)(H : f = i ∘g g )(K : is_embedding i)
: Π a:A , kernel_subgroup(g)(a) ↔ kernel_subgroup(f)(a) :=
begin
intro a,
fapply iff.intro,
exact comm_group_kernel_factor f g H a,
exact ab_group_kernel_factor f g H a,
intro p,
apply @is_injective_of_is_embedding _ _ i _ (g a) 1,
exact calc
@ -285,23 +285,23 @@ begin
... = i 1 : (respect_one i)⁻¹
end
definition comm_group_kernel_image_lift (A B : CommGroup) (f : A →g B)
definition ab_group_kernel_image_lift (A B : AbGroup) (f : A →g B)
: Π a : A, kernel_subgroup(image_lift(f))(a) ↔ kernel_subgroup(f)(a) :=
begin
fapply comm_group_kernel_equivalent (comm_image f) (f) (image_lift(f)) (image_incl(f)),
fapply ab_group_kernel_equivalent (ab_image f) (f) (image_lift(f)) (image_incl(f)),
exact image_factor f,
exact is_embedding_of_is_injective (image_incl_injective(f)),
end
definition comm_group_kernel_quotient_to_image {A B : CommGroup} (f : A →g B)
: quotient_comm_group (kernel_subgroup f) →g comm_image (f) :=
definition ab_group_kernel_quotient_to_image {A B : AbGroup} (f : A →g B)
: quotient_ab_group (kernel_subgroup f) →g ab_image (f) :=
begin
fapply quotient_group_elim (image_lift f), intro a, intro p,
apply iff.mpr (comm_group_kernel_image_lift _ _ f a) p
apply iff.mpr (ab_group_kernel_image_lift _ _ f a) p
end
definition is_surjective_kernel_quotient_to_image {A B : CommGroup} (f : A →g B)
: is_surjective (comm_group_kernel_quotient_to_image f) :=
definition is_surjective_kernel_quotient_to_image {A B : AbGroup} (f : A →g B)
: is_surjective (ab_group_kernel_quotient_to_image f) :=
begin
intro b, exact sorry
-- have H : is_surjective (image_lift f)
@ -312,8 +312,8 @@ print iff.mpr
section
parameters {A₁ : CommGroup} (S : A₁ → Prop)
variable {A₂ : CommGroup}
parameters {A₁ : AbGroup} (S : A₁ → Prop)
variable {A₂ : AbGroup}
inductive generating_relation' : A₁ → Type :=
| rincl : Π{g}, S g → generating_relation' g
@ -337,9 +337,9 @@ print iff.mpr
Rmul := gr_mul⦄
parameter (A₁)
definition quotient_comm_group_gen : CommGroup := quotient_comm_group normal_generating_relation
definition quotient_ab_group_gen : AbGroup := quotient_ab_group normal_generating_relation
definition gqg_map [constructor] : A₁ →g quotient_comm_group_gen :=
definition gqg_map [constructor] : A₁ →g quotient_ab_group_gen :=
qg_map _
parameter {A₁}
@ -347,7 +347,7 @@ print iff.mpr
eq_of_rel (tr (rincl H))
definition gqg_elim [constructor] (f : A₁ →g A₂) (H : Π⦃g⦄, S g → f g = 1)
: quotient_comm_group_gen →g A₂ :=
: quotient_ab_group_gen →g A₂ :=
begin
apply quotient_group_elim f,
intro g r, induction r with r,
@ -365,7 +365,7 @@ print iff.mpr
end
definition gqg_elim_unique (f : A₁ →g A₂) (H : Π⦃g⦄, S g → f g = 1)
(k : quotient_comm_group_gen →g A₂) : ( k ∘g gqg_map ~ f ) → k ~ gqg_elim f H :=
(k : quotient_ab_group_gen →g A₂) : ( k ∘g gqg_map ~ f ) → k ~ gqg_elim f H :=
!gelim_unique
end

30
algebra/subgroup.hlean
View file

@ -130,12 +130,12 @@ namespace group
abbreviation is_normal_subgroup [unfold 2] := @normal_subgroup_rel.is_normal_subgroup
variables {G G' : Group} (H : subgroup_rel G) (N : normal_subgroup_rel G) {g g' h h' k : G}
{A B : CommGroup}
{A B : AbGroup}
theorem is_normal_subgroup' (h : G) (r : N g) : N (h⁻¹ * g * h) :=
inv_inv h ▸ is_normal_subgroup N h⁻¹ r
definition normal_subgroup_rel_comm.{u} [constructor] (R : subgroup_rel.{_ u} A)
definition normal_subgroup_rel_ab.{u} [constructor] (R : subgroup_rel.{_ u} A)
: normal_subgroup_rel.{_ u} A :=
⦃normal_subgroup_rel, R,
is_normal_subgroup := abstract begin
@ -209,7 +209,7 @@ namespace group
theorem subgroup_mul_left_inv (g : sg H) : g⁻¹ * g = 1 :=
subtype_eq !mul.left_inv
theorem subgroup_mul_comm {G : CommGroup} {H : subgroup_rel G} (g h : sg H)
theorem subgroup_mul_comm {G : AbGroup} {H : subgroup_rel G} (g h : sg H)
: g * h = h * g :=
subtype_eq !mul.comm
@ -223,17 +223,17 @@ namespace group
definition subgroup [constructor] : Group :=
Group.mk _ (group_sg H)
definition comm_group_sg [constructor] {G : CommGroup} (H : subgroup_rel G)
: comm_group (sg H) :=
⦃comm_group, group_sg H, mul_comm := subgroup_mul_comm⦄
definition ab_group_sg [constructor] {G : AbGroup} (H : subgroup_rel G)
: ab_group (sg H) :=
⦃ab_group, group_sg H, mul_comm := subgroup_mul_comm⦄
definition comm_subgroup [constructor] {G : CommGroup} (H : subgroup_rel G)
: CommGroup :=
CommGroup.mk _ (comm_group_sg H)
definition ab_subgroup [constructor] {G : AbGroup} (H : subgroup_rel G)
: AbGroup :=
AbGroup.mk _ (ab_group_sg H)
definition kernel {G H : Group} (f : G →g H) : Group := subgroup (kernel_subgroup f)
definition comm_kernel {G H : CommGroup} (f : G →g H) : CommGroup := comm_subgroup (kernel_subgroup f)
definition ab_kernel {G H : AbGroup} (f : G →g H) : AbGroup := ab_subgroup (kernel_subgroup f)
definition incl_of_subgroup [constructor] {G : Group} (H : subgroup_rel G) : subgroup H →g G :=
begin
@ -258,19 +258,19 @@ namespace group
definition image {G H : Group} (f : G →g H) : Group :=
subgroup (image_subgroup f)
definition CommGroup_of_Group.{u} (G : Group.{u}) (H : Π (g h : G), mul g h = mul h g) : CommGroup.{u} :=
definition AbGroup_of_Group.{u} (G : Group.{u}) (H : Π (g h : G), mul g h = mul h g) : AbGroup.{u} :=
begin
induction G,
induction struct,
fapply CommGroup.mk,
fapply AbGroup.mk,
exact carrier,
fapply comm_group.mk,
fapply ab_group.mk,
repeat assumption,
exact H
end
definition comm_image {G : CommGroup} {H : Group} (f : G →g H) : CommGroup :=
CommGroup_of_Group (image f)
definition ab_image {G : AbGroup} {H : Group} (f : G →g H) : AbGroup :=
AbGroup_of_Group (image f)
begin
intro g h,
induction g with x t, induction h with y s,

2
colim.hlean
View file

@ -389,7 +389,7 @@ namespace seq_colim
rewrite [▸*, +ap_con, ap_inv, +succ_add_tr_rep_succ, con_inv, inv_con_inv_right, +con.assoc],
apply whisker_left,
rewrite [- +con.assoc], apply whisker_right, rewrite [- +ap_compose'],
note s := (eq_top_of_square (natural_square
note s := (eq_top_of_square (natural_square_tr
(λx, fn_tr_eq_tr_fn (succ_add n k) f x ⬝ (tr_ap A succ (succ_add n k) (f x))⁻¹) p))⁻¹,
rewrite [inv_con_inv_right at s, -con.assoc at s], exact s
end

317
homotopy/EM.hlean
View file

@ -1,317 +0,0 @@
/-
Copyright (c) 2016 Floris van Doorn. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Floris van Doorn
Eilenberg MacLane spaces
-/
import homotopy.EM .spectrum
open eq is_equiv equiv is_conn is_trunc unit function pointed nat group algebra trunc trunc_index
fiber prod pointed susp EM.ops
namespace EM
/- Functorial action of Eilenberg-Maclane spaces -/
definition pEM1_functor [constructor] {G H : Group} (φ : G →g H) : pEM1 G →* pEM1 H :=
begin
fconstructor,
{ intro g, induction g,
{ exact base },
{ exact pth (φ g) },
{ exact ap pth (respect_mul φ g h) ⬝ resp_mul (φ g) (φ h) }},
{ reflexivity }
end
definition EMadd1_functor [constructor] {G H : CommGroup} (φ : G →g H) (n : ℕ) :
EMadd1 G n →* EMadd1 H n :=
begin
apply ptrunc_functor,
apply iterate_psusp_functor,
apply pEM1_functor,
exact φ
end
definition EM_functor [unfold 4] {G H : CommGroup} (φ : G →g H) (n : ℕ) :
K G n →* K H n :=
begin
cases n with n,
{ exact pmap_of_homomorphism φ },
{ exact EMadd1_functor φ n }
end
-- TODO: (K G n →* K H n) ≃ (G →g H)
/- Equivalence of Groups and pointed connected 1-truncated types -/
definition pEM1_pequiv_ptruncconntype (X : 1-Type*[0]) : pEM1 (π₁ X) ≃* X :=
pEM1_pequiv_type
definition Group_equiv_ptruncconntype [constructor] : Group ≃ 1-Type*[0] :=
equiv.MK (λG, ptruncconntype.mk (pEM1 G) _ pt !is_conn_pEM1)
(λX, π₁ X)
begin intro X, apply ptruncconntype_eq, esimp, exact pEM1_pequiv_type end
begin intro G, apply eq_of_isomorphism, apply fundamental_group_pEM1 end
/- Higher EM-spaces -/
/- K(G, 2) is unique (see below for general case) -/
definition loopn_EMadd1 (G : CommGroup) (n : ℕ) : Ω[succ n] (EMadd1 G n) ≃* pType_of_Group G :=
begin
refine _ ⬝e* loop_pEM1 G,
cases n with n,
{ refine !loop_ptrunc_pequiv ⬝e* _, refine ptrunc_pequiv _ _ _,
apply is_trunc_eq, apply is_trunc_EM1},
induction n with n IH,
{ exact loop_pequiv_loop (loop_EM2 G)},
refine _ ⬝e* IH,
refine !homotopy_group_pequiv_loop_ptrunc⁻¹ᵉ* ⬝e* _ ⬝e* !homotopy_group_pequiv_loop_ptrunc,
apply iterate_psusp_stability_pequiv,
rexact add_mul_le_mul_add n 1 1
end
definition EM2_map [unfold 7] {G : CommGroup} {X : Type*} (e : Ω[2] X ≃ G)
(r : Π(p q : Ω[2] X), e (@concat (Ω X) idp idp idp p q) = e p * e q)
[is_conn 1 X] [is_trunc 2 X] : EMadd1 G 1 → X :=
begin
change trunc 2 (susp (EM1 G)) → X, intro x,
induction x with x, induction x with x,
{ exact pt},
{ exact pt},
{ change carrier (Ω X), refine EM1_map e r x}
end
definition pEM2_pmap [constructor] {G : CommGroup} {X : Type*} (e : Ω[2] X ≃ G)
(r : Π(p q : Ω[2] X), e (@concat (Ω X) idp idp idp p q) = e p * e q)
[is_conn 1 X] [is_trunc 2 X] : EMadd1 G 1 →* X :=
pmap.mk (EM2_map e r) idp
definition loop_pEM2_pmap {G : CommGroup} {X : Type*} (e : Ω[2] X ≃ G)
(r : Π(p q : Ω[2] X), e (@concat (Ω X) idp idp idp p q) = e p * e q)
[is_conn 1 X] [is_trunc 2 X] :
Ω→[2](pEM2_pmap e r) ~ e⁻¹ᵉ ∘ loopn_EMadd1 G 1 :=
begin
exact sorry
end
-- TODO: make arguments in trivial_homotopy_group_of_is_trunc implicit
attribute is_conn_EMadd1 is_trunc_EMadd1 [instance]
definition pEM2_pequiv' {G : CommGroup} {X : Type*} (e : Ω[2] X ≃ G)
(r : Π(p q : Ω[2] X), e (@concat (Ω X) idp idp idp p q) = e p * e q)
[is_conn 1 X] [is_trunc 2 X] : EMadd1 G 1 ≃* X :=
begin
apply pequiv_of_pmap (pEM2_pmap e r),
have is_conn 0 (EMadd1 G 1), from !is_conn_of_is_conn_succ,
have is_trunc 2 (EMadd1 G 1), from !is_trunc_EMadd1,
refine whitehead_principle_pointed 2 _ _,
intro k, apply @nat.lt_by_cases k 2: intro H,
{ apply @is_equiv_of_is_contr,
do 2 exact trivial_homotopy_group_of_is_conn _ (le_of_lt_succ H)},
{ cases H, esimp, apply is_equiv_trunc_functor, esimp,
apply is_equiv.homotopy_closed, rotate 1,
{ symmetry, exact loop_pEM2_pmap _ _},
apply is_equiv_compose, apply pequiv.to_is_equiv, apply to_is_equiv},
{ apply @is_equiv_of_is_contr,
exact trivial_homotopy_group_of_is_trunc _ H,
apply @trivial_homotopy_group_of_is_trunc, rotate 1, exact H, exact _inst_2}
end
definition pEM2_pequiv {G : CommGroup} {X : Type*} (e : πg[1+1] X ≃g G)
[is_conn 1 X] [is_trunc 2 X] : EMadd1 G 1 ≃* X :=
begin
have is_set (Ω[2] X), from !is_trunc_eq,
apply pEM2_pequiv' (!trunc_equiv⁻¹ᵉ ⬝e equiv_of_isomorphism e),
intro p q, esimp, exact to_respect_mul e (tr p) (tr q)
end
-- general case
definition EMadd1_map [unfold 8] {G : CommGroup} {X : Type*} {n : ℕ} (e : Ω[succ n] X ≃ G)
(r : Π(p q : Ω (Ω[n] X)), e (p ⬝ q) = e p * e q)
[H1 : is_conn n X] [H2 : is_trunc (n.+1) X] : EMadd1 G n → X :=
begin
revert X e r H1 H2, induction n with n f: intro X e r H1 H2,
{ change trunc 1 (EM1 G) → X, intro x, induction x with x, exact EM1_map e r x},
change trunc (n.+2) (susp (iterate_psusp n (pEM1 G))) → X, intro x,
induction x with x, induction x with x,
{ exact pt},
{ exact pt},
change carrier (Ω X), refine f _ _ _ _ _ (tr x),
{ refine _⁻¹ᵉ ⬝e e, apply equiv_of_pequiv, apply loopn_succ_in},
exact abstract begin
intro p q, refine _ ⬝ !r, apply ap e, esimp,
apply inv_eq_of_eq,
refine _⁻¹ ⬝ !loopn_succ_in_con⁻¹,
exact to_right_inv (loopn_succ_in X (succ n)) p ◾ to_right_inv (loopn_succ_in X (succ n)) q
end end
end
definition pEMadd1_pmap [constructor] {G : CommGroup} {X : Type*} {n : ℕ} (e : Ω[succ n] X ≃ G)
(r : Π(p q : Ω[succ n] X), e (@concat (Ω[n] X) pt pt pt p q) = e p * e q)
[H1 : is_conn n X] [H2 : is_trunc (n.+1) X] : EMadd1 G n →* X :=
pmap.mk (EMadd1_map e r) begin cases n with n: reflexivity end
definition loopn_pEMadd1_pmap {G : CommGroup} {X : Type*} {n : ℕ} (e : Ω[succ n] X ≃ G)
(r : Π(p q : Ω[succ n] X), e (@concat (Ω[n] X) pt pt pt p q) = e p * e q)
[H1 : is_conn n X] [H2 : is_trunc (n.+1) X] :
Ω→[succ n](pEMadd1_pmap e r) ~ e⁻¹ᵉ ∘ loopn_EMadd1 G n :=
begin
apply homotopy_of_inv_homotopy_pre (loopn_EMadd1 G n),
intro g, esimp at *,
revert X e r H1 H2, induction n with n IH: intro X e r H1 H2,
{ refine !idp_con ⬝ _, refine !ap_compose'⁻¹ ⬝ _, apply elim_pth},
{ replace (succ (succ n)) with ((succ n) + 1), rewrite [apn_succ],
exact sorry}
-- exact !idp_con ⬝ !elim_pth
end
-- definition is_conn_of_le (n : ℕ₋₂) (A : Type) [is_conn (n.+1) A] :
-- is_conn n A :=
-- is_trunc_trunc_of_le A -2 (trunc_index.self_le_succ n)
-- attribute is_conn_EMadd1 is_trunc_EMadd1 [instance]
definition pEMadd1_pequiv' {G : CommGroup} {X : Type*} {n : ℕ} (e : Ω[succ n] X ≃ G)
(r : Π(p q : Ω[succ n] X), e (@concat (Ω[n] X) pt pt pt p q) = e p * e q)
[H1 : is_conn n X] [H2 : is_trunc (n.+1) X] : EMadd1 G n ≃* X :=
begin
apply pequiv_of_pmap (pEMadd1_pmap e r),
have is_conn 0 (EMadd1 G n), from is_conn_of_le _ (zero_le_of_nat n),
have is_trunc (n.+1) (EMadd1 G n), from !is_trunc_EMadd1,
refine whitehead_principle_pointed (n.+1) _ _,
intro k, apply @nat.lt_by_cases k (succ n): intro H,
{ apply @is_equiv_of_is_contr,
do 2 exact trivial_homotopy_group_of_is_conn _ (le_of_lt_succ H)},
{ cases H, esimp, apply is_equiv_trunc_functor, esimp,
apply is_equiv.homotopy_closed, rotate 1,
{ symmetry, exact loopn_pEMadd1_pmap _ _},
apply is_equiv_compose, apply pequiv.to_is_equiv},
{ apply @is_equiv_of_is_contr,
do 2 exact trivial_homotopy_group_of_is_trunc _ H}
end
definition pEMadd1_pequiv {G : CommGroup} {X : Type*} {n : ℕ} (e : πg[n+1] X ≃g G)
[H1 : is_conn n X] [H2 : is_trunc (n.+1) X] : EMadd1 G n ≃* X :=
begin
have is_set (Ω[succ n] X), from !is_set_loopn,
apply pEMadd1_pequiv' (!trunc_equiv⁻¹ᵉ ⬝e equiv_of_isomorphism e),
intro p q, esimp, exact to_respect_mul e (tr p) (tr q)
end
definition EM_pequiv_succ {G : CommGroup} {X : Type*} {n : ℕ} (e : πg[n+1] X ≃g G)
[H1 : is_conn n X] [H2 : is_trunc (n.+1) X] : EM G (succ n) ≃* X :=
pEMadd1_pequiv e
definition EM_pequiv_zero {G : CommGroup} {X : Type*} (e : X ≃* pType_of_Group G) : EM G 0 ≃* X :=
proof e⁻¹ᵉ* qed
/- uniqueness of K(G,n), method 2: -/
-- definition freudenthal_homotopy_group_pequiv (A : Type*) {n k : ℕ} [is_conn n A] (H : k ≤ 2 * n)
-- : π[k + 1] (psusp A) ≃* π[k] A :=
-- calc
-- π[k + 1] (psusp A) ≃* π[k] (Ω (psusp A)) : homotopy_group_succ_in
-- ... ≃* Ω[k] (ptrunc k (Ω (psusp A))) : homotopy_group_pequiv_loop_ptrunc k (Ω (psusp A))
-- ... ≃* Ω[k] (ptrunc k A) : loopn_pequiv_loopn k (freudenthal_pequiv A H)
-- ... ≃* π[k] A : (homotopy_group_pequiv_loop_ptrunc k A)⁻¹ᵉ*
definition iterate_psusp_succ_pequiv (n : ℕ) (A : Type*) :
iterate_psusp (succ n) A ≃* iterate_psusp n (psusp A) :=
begin
induction n with n IH,
{ reflexivity},
{ exact psusp_equiv IH}
end
definition is_conn_psusp [instance] (n : trunc_index) (A : Type*)
[H : is_conn n A] : is_conn (n .+1) (psusp A) :=
is_conn_susp n A
definition iterated_freudenthal_pequiv (A : Type*) {n k m : ℕ} [HA : is_conn n A] (H : k ≤ 2 * n)
: ptrunc k A ≃* ptrunc k (Ω[m] (iterate_psusp m A)) :=
begin
revert A n k HA H, induction m with m IH: intro A n k HA H,
{ reflexivity},
{ have H2 : succ k ≤ 2 * succ n,
from calc
succ k ≤ succ (2 * n) : succ_le_succ H
... ≤ 2 * succ n : self_le_succ,
exact calc
ptrunc k A ≃* ptrunc k (Ω (psusp A)) : freudenthal_pequiv A H
... ≃* Ω (ptrunc (succ k) (psusp A)) : loop_ptrunc_pequiv
... ≃* Ω (ptrunc (succ k) (Ω[m] (iterate_psusp m (psusp A)))) :
loop_pequiv_loop (IH (psusp A) (succ n) (succ k) _ H2)
... ≃* ptrunc k (Ω[succ m] (iterate_psusp m (psusp A))) : loop_ptrunc_pequiv
... ≃* ptrunc k (Ω[succ m] (iterate_psusp (succ m) A)) :
ptrunc_pequiv_ptrunc _ (loopn_pequiv_loopn _ !iterate_psusp_succ_pequiv)}
end
definition pmap_eq_of_phomotopy {A B : Type*} {f g : A →* B} (p : f ~* g) : f = g :=
pmap_eq (to_homotopy p) (to_homotopy_pt p)⁻¹
definition pmap_equiv_pmap_right {A B : Type*} (C : Type*) (f : A ≃* B) : C →* A ≃ C →* B :=
begin
fapply equiv.MK,
{ exact pcompose f},
{ exact pcompose f⁻¹ᵉ*},
{ intro f, apply pmap_eq_of_phomotopy,
exact !passoc⁻¹* ⬝* pwhisker_right _ !pright_inv ⬝* !pid_pcompose},
{ intro f, apply pmap_eq_of_phomotopy,
exact !passoc⁻¹* ⬝* pwhisker_right _ !pleft_inv ⬝* !pid_pcompose}
end
definition iterate_psusp_adjoint_loopn [constructor] (X Y : Type*) (n : ℕ) :
iterate_psusp n X →* Y ≃ X →* Ω[n] Y :=
begin
revert X Y, induction n with n IH: intro X Y,
{ reflexivity},
{ refine !susp_adjoint_loop ⬝e !IH ⬝e _, apply pmap_equiv_pmap_right,
symmetry, apply loopn_succ_in}
end
/- new method of uniqueness, define K(G,n+1) as the truncation of the suspension of K(G,n) -/
definition EMadd2 (G : CommGroup) (n : ℕ) : Type* := ptrunc (n.+2) (psusp (EMadd1 G n))
definition EMadd2_map [constructor] {G : CommGroup} {X : Type*} {n : ℕ} (e : Ω[n+2] X ≃ G)
(r : Π(p q : Ω[n+2] X), e (@concat (Ω[n+1] X) pt pt pt p q) = e p * e q)
[H1 : is_conn (n.+1) X] [H2 : is_trunc (n.+2) X] : EMadd2 G n → X :=
begin
intro x, induction x with x, induction x with x,
{ exact pt },
{ exact pt },
{ refine EMadd1_map ((loopn_succ_in _ (n+1))⁻¹ᵉ ⬝e e) _ x,
exact abstract begin
intro p q, refine _ ⬝ !r, apply ap e, esimp,
refine @inv_eq_of_eq _ _ (pequiv.to_equiv (loopn_succ_in X (n + 1))) _ _ _ _,
refine _⁻¹ ⬝ !loopn_succ_in_con⁻¹,
exact to_right_inv (loopn_succ_in X (succ n)) p ◾ to_right_inv (loopn_succ_in X (succ n)) q
end end }
end
-- -- general case
-- definition EMadd1_map [unfold 8] {G : CommGroup} {X : Type*} {n : ℕ} (e : Ω[succ n] X ≃ G)
-- (r : Π(p q : Ω (Ω[n] X)), e (p ⬝ q) = e p * e q)
-- [H1 : is_conn n X] [H2 : is_trunc (n.+1) X] : EMadd1 G n → X :=
-- begin
-- revert X e r H1 H2, induction n with n f: intro X e r H1 H2,
-- { change trunc 1 (EM1 G) → X, intro x, induction x with x, exact EM1_map e r x},
-- change trunc (n.+2) (susp (iterate_psusp n (pEM1 G))) → X, intro x,
-- induction x with x, induction x with x,
-- { exact pt},
-- { exact pt},
-- change carrier (Ω X), refine f _ _ _ _ _ (tr x),
-- { refine _⁻¹ᵉ ⬝e e, apply equiv_of_pequiv, apply loopn_succ_in},
-- exact abstract begin
-- intro p q, refine _ ⬝ !r, apply ap e, esimp,
-- apply inv_eq_of_eq,
-- refine _⁻¹ ⬝ !loopn_succ_in_con⁻¹,
-- exact to_right_inv (loopn_succ_in X (succ n)) p ◾ to_right_inv (loopn_succ_in X (succ n)) q
-- end end
-- end
end EM
-- cohomology ∥ X → K(G,n) ∥
-- reduced cohomology ∥ X →* K(G,n) ∥
-- but we probably want to do this for any spectrum

518
homotopy/EMnew.hlean
View file

@ -1,518 +0,0 @@
/-
Copyright (c) 2016 Floris van Doorn. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Floris van Doorn
Eilenberg MacLane spaces
This file replaces the file in the HoTT library
-/
import hit.groupoid_quotient homotopy.hopf homotopy.freudenthal homotopy.homotopy_group
..move_to_lib
open algebra pointed nat eq category group is_trunc iso unit trunc equiv is_conn function is_equiv
trunc_index
local attribute pType_of_Group [coercion]
namespace EMnew
open groupoid_quotient
variables {G : Group}
definition EM1' (G : Group) : Type :=
groupoid_quotient (Groupoid_of_Group G)
definition EM1 [constructor] (G : Group) : Type* :=
pointed.MK (EM1' G) (elt star)
definition base : EM1' G := elt star
definition pth : G → base = base := pth
definition resp_mul (g h : G) : pth (g * h) = pth g ⬝ pth h := resp_comp h g
definition resp_one : pth (1 : G) = idp :=
resp_id star
definition resp_inv (g : G) : pth (g⁻¹) = (pth g)⁻¹ :=
resp_inv g
local attribute pointed.MK pointed.carrier EM1 EM1' [reducible]
protected definition rec {P : EM1' G → Type} [H : Π(x : EM1' G), is_trunc 1 (P x)]
(Pb : P base) (Pp : Π(g : G), Pb =[pth g] Pb)
(Pmul : Π(g h : G), change_path (resp_mul g h) (Pp (g * h)) = Pp g ⬝o Pp h) (x : EM1' G) : P x :=
begin
induction x,
{ induction g, exact Pb},
{ induction a, induction b, exact Pp f},
{ induction a, induction b, induction c, exact Pmul f g}
end
protected definition rec_on {P : EM1' G → Type} [H : Π(x : EM1' G), is_trunc 1 (P x)]
(x : EM1' G) (Pb : P base) (Pp : Π(g : G), Pb =[pth g] Pb)
(Pmul : Π(g h : G), change_path (resp_mul g h) (Pp (g * h)) = Pp g ⬝o Pp h) : P x :=
EMnew.rec Pb Pp Pmul x
protected definition set_rec {P : EM1' G → Type} [H : Π(x : EM1' G), is_set (P x)]
(Pb : P base) (Pp : Π(g : G), Pb =[pth g] Pb) (x : EM1' G) : P x :=
EMnew.rec Pb Pp !center x
protected definition prop_rec {P : EM1' G → Type} [H : Π(x : EM1' G), is_prop (P x)]
(Pb : P base) (x : EM1' G) : P x :=
EMnew.rec Pb !center !center x
definition rec_pth {P : EM1' G → Type} [H : Π(x : EM1' G), is_trunc 1 (P x)]
{Pb : P base} {Pp : Π(g : G), Pb =[pth g] Pb}
(Pmul : Π(g h : G), change_path (resp_mul g h) (Pp (g * h)) = Pp g ⬝o Pp h)
(g : G) : apd (EMnew.rec Pb Pp Pmul) (pth g) = Pp g :=
proof !rec_pth qed
protected definition elim {P : Type} [is_trunc 1 P] (Pb : P) (Pp : Π(g : G), Pb = Pb)
(Pmul : Π(g h : G), Pp (g * h) = Pp g ⬝ Pp h) (x : EM1' G) : P :=
begin
induction x,
{ exact Pb},
{ exact Pp f},
{ exact Pmul f g}
end
protected definition elim_on [reducible] {P : Type} [is_trunc 1 P] (x : EM1' G)
(Pb : P) (Pp : G → Pb = Pb) (Pmul : Π(g h : G), Pp (g * h) = Pp g ⬝ Pp h) : P :=
EMnew.elim Pb Pp Pmul x
protected definition set_elim [reducible] {P : Type} [is_set P] (Pb : P) (Pp : G → Pb = Pb)
(x : EM1' G) : P :=
EMnew.elim Pb Pp !center x
protected definition prop_elim [reducible] {P : Type} [is_prop P] (Pb : P) (x : EM1' G) : P :=
EMnew.elim Pb !center !center x
definition elim_pth {P : Type} [is_trunc 1 P] {Pb : P} {Pp : G → Pb = Pb}
(Pmul : Π(g h : G), Pp (g * h) = Pp g ⬝ Pp h) (g : G) : ap (EMnew.elim Pb Pp Pmul) (pth g) = Pp g :=
proof !elim_pth qed
protected definition elim_set.{u} (Pb : Set.{u}) (Pp : Π(g : G), Pb ≃ Pb)
(Pmul : Π(g h : G) (x : Pb), Pp (g * h) x = Pp h (Pp g x)) (x : EM1' G) : Set.{u} :=
groupoid_quotient.elim_set (λu, Pb) (λu v, Pp) (λu v w g h, proof Pmul h g qed) x
theorem elim_set_pth {Pb : Set} {Pp : Π(g : G), Pb ≃ Pb}
(Pmul : Π(g h : G) (x : Pb), Pp (g * h) x = Pp h (Pp g x)) (g : G) :
transport (EMnew.elim_set Pb Pp Pmul) (pth g) = Pp g :=
!elim_set_pth
end EMnew
attribute EMnew.base [constructor]
attribute EMnew.rec EMnew.elim [unfold 7] [recursor 7]
attribute EMnew.rec_on EMnew.elim_on [unfold 4]
attribute EMnew.set_rec EMnew.set_elim [unfold 6]
attribute EMnew.prop_rec EMnew.prop_elim EMnew.elim_set [unfold 5]
namespace EMnew
open groupoid_quotient
variables (G : Group)
definition base_eq_base_equiv : (base = base :> EM1 G) ≃ G :=
!elt_eq_elt_equiv
definition fundamental_group_EM1 : π₁ (EM1 G) ≃g G :=
begin
fapply isomorphism_of_equiv,
{ exact trunc_equiv_trunc 0 !base_eq_base_equiv ⬝e trunc_equiv 0 G},
{ intros g h, induction g with p, induction h with q,
exact encode_con p q}
end
proposition is_trunc_EM1 [instance] : is_trunc 1 (EM1 G) :=
!is_trunc_groupoid_quotient
proposition is_trunc_EM1' [instance] : is_trunc 1 (EM1' G) :=
!is_trunc_groupoid_quotient
proposition is_conn_EM1' [instance] : is_conn 0 (EM1' G) :=
by apply @is_conn_groupoid_quotient; esimp; exact _
proposition is_conn_EM1 [instance] : is_conn 0 (EM1 G) :=
is_conn_EM1' G
variable {G}
definition EM1_map [unfold 7] {X : Type*} (e : G → Ω X)
(r : Πg h, e (g * h) = e g ⬝ e h) [is_conn 0 X] [is_trunc 1 X] : EM1 G → X :=
begin
intro x, induction x using EMnew.elim,
{ exact Point X },
{ exact e g },
{ exact r g h }
end
/- Uniqueness of K(G, 1) -/
definition EM1_pmap [constructor] {X : Type*} (e : G → Ω X)
(r : Πg h, e (g * h) = e g ⬝ e h) [is_conn 0 X] [is_trunc 1 X] : EM1 G →* X :=
pmap.mk (EM1_map e r) idp
variable (G)
definition loop_EM1 [constructor] : G ≃* Ω (EM1 G) :=
(pequiv_of_equiv (base_eq_base_equiv G) idp)⁻¹ᵉ*
variable {G}
definition loop_EM1_pmap {X : Type*} (e : G →* Ω X)
(r : Πg h, e (g * h) = e g ⬝ e h) [is_conn 0 X] [is_trunc 1 X] :
Ω→(EM1_pmap e r) ∘* loop_EM1 G ~* e :=
begin
fapply phomotopy.mk,
{ intro g, refine !idp_con ⬝ elim_pth r g },
{ apply is_set.elim }
end
definition EM1_pequiv'.{u} {G : Group.{u}} {X : pType.{u}} (e : G ≃* Ω X)
(r : Πg h, e (g * h) = e g ⬝ e h) [is_conn 0 X] [is_trunc 1 X] : EM1 G ≃* X :=
begin
apply pequiv_of_pmap (EM1_pmap e r),
apply whitehead_principle_pointed 1,
intro k, cases k with k,
{ apply @is_equiv_of_is_contr,
all_goals (esimp; exact _)},
{ cases k with k,
{ apply is_equiv_trunc_functor, esimp,
apply is_equiv.homotopy_closed, rotate 1,
{ symmetry, exact phomotopy_pinv_right_of_phomotopy (loop_EM1_pmap _ _) },
apply is_equiv_compose e },
{ apply @is_equiv_of_is_contr,
do 2 exact trivial_homotopy_group_of_is_trunc _ (succ_lt_succ !zero_lt_succ)}}
end
definition EM1_pequiv.{u} {G : Group.{u}} {X : pType.{u}} (e : G ≃g π₁ X)
[is_conn 0 X] [is_trunc 1 X] : EM1 G ≃* X :=
begin
apply EM1_pequiv' (pequiv_of_isomorphism e ⬝e* ptrunc_pequiv _ _ _),
refine is_equiv.preserve_binary_of_inv_preserve _ mul concat _,
intro p q,
exact to_respect_mul e⁻¹ᵍ (tr p) (tr q)
end
definition EM1_pequiv_type (X : Type*) [is_conn 0 X] [is_trunc 1 X] : EM1 (π₁ X) ≃* X :=
EM1_pequiv !isomorphism.refl
end EMnew
open hopf new_susp susp
namespace EMnew
/- EM1 G is an h-space if G is an abelian group. This allows us to construct K(G,n) for n ≥ 2 -/
variables {G : CommGroup} (n : ℕ)
definition EM1_mul [unfold 2 3] (x x' : EM1' G) : EM1' G :=
begin
induction x,
{ exact x'},
{ induction x' using EMnew.set_rec,
{ exact pth g},
{ exact abstract begin apply loop_pathover, apply square_of_eq,
refine !resp_mul⁻¹ ⬝ _ ⬝ !resp_mul,
exact ap pth !mul.comm end end}},
{ refine EMnew.prop_rec _ x', apply resp_mul }
end
variable (G)
definition EM1_mul_one (x : EM1' G) : EM1_mul x base = x :=
begin
induction x using EMnew.set_rec,
{ reflexivity},
{ apply eq_pathover_id_right, apply hdeg_square, refine EMnew.elim_pth _ g}
end
definition h_space_EM1 [constructor] [instance] : h_space (EM1' G) :=
begin
fapply h_space.mk,
{ exact EM1_mul},
{ exact base},
{ intro x', reflexivity},
{ apply EM1_mul_one}
end
/- K(G, n+1) -/
definition EMadd1 : ℕ → Type*
| 0 := EM1 G
| (n+1) := ptrunc (n+2) (psusp (EMadd1 n))
definition EMadd1_succ [unfold_full] (n : ℕ) :
EMadd1 G (succ n) = ptrunc (n.+2) (psusp (EMadd1 G n)) :=
idp
definition loop_EM2 : Ω[1] (EMadd1 G 1) ≃* EM1 G :=
hopf.delooping (EM1' G) idp
definition is_conn_EMadd1 [instance] (n : ℕ) : is_conn n (EMadd1 G n) :=
begin
induction n with n IH,
{ apply is_conn_EM1 },
{ rewrite EMadd1_succ, esimp, exact _ }
end
definition is_trunc_EMadd1 [instance] (n : ℕ) : is_trunc (n+1) (EMadd1 G n) :=
begin
cases n with n,
{ apply is_trunc_EM1 },
{ apply is_trunc_trunc }
end
/- loops of an EM-space -/
definition loop_EMadd1 (n : ℕ) : EMadd1 G n ≃* Ω (EMadd1 G (succ n)) :=
begin
cases n with n,
{ exact !loop_EM2⁻¹ᵉ* },
{ rewrite [EMadd1_succ G (succ n)],
refine (ptrunc_pequiv (succ n + 1) _ _)⁻¹ᵉ* ⬝e* _ ⬝e* (loop_ptrunc_pequiv _ _)⁻¹ᵉ*,
have succ n + 1 ≤ 2 * succ n, from add_mul_le_mul_add n 1 1,
refine freudenthal_pequiv _ this }
end
definition loopn_EMadd1_pequiv_EM1 (G : CommGroup) (n : ℕ) : EM1 G ≃* Ω[n] (EMadd1 G n) :=
begin
induction n with n e,
{ reflexivity },
{ refine _ ⬝e* !loopn_succ_in⁻¹ᵉ*,
refine _ ⬝e* loopn_pequiv_loopn n !loop_EMadd1,
exact e }
end
-- use loopn_EMadd1_pequiv_EM1 in this definition?
definition loopn_EMadd1 (G : CommGroup) (n : ℕ) : G ≃* Ω[succ n] (EMadd1 G n) :=
begin
induction n with n e,
{ apply loop_EM1 },
{ refine _ ⬝e* !loopn_succ_in⁻¹ᵉ*,
refine _ ⬝e* loopn_pequiv_loopn (succ n) !loop_EMadd1,
exact e }
end
definition loopn_EMadd1_succ [unfold_full] (G : CommGroup) (n : ℕ) : loopn_EMadd1 G (succ n) ~*
!loopn_succ_in⁻¹ᵉ* ∘* apn (succ n) !loop_EMadd1 ∘* loopn_EMadd1 G n :=
by reflexivity
definition EM_up {G : CommGroup} {X : Type*} {n : ℕ} (e : Ω[succ (succ n)] X ≃* G)
: Ω[succ n] (Ω X) ≃* G :=
!loopn_succ_in⁻¹ᵉ* ⬝e* e
definition is_homomorphism_EM_up {G : CommGroup} {X : Type*} {n : ℕ}
(e : Ω[succ (succ n)] X ≃* G)
(r : Π(p q : Ω[succ (succ n)] X), e (p ⬝ q) = e p * e q)
(p q : Ω[succ n] (Ω X)) : EM_up e (p ⬝ q) = EM_up e p * EM_up e q :=
begin
refine _ ⬝ !r, apply ap e, esimp, apply apn_con
end
definition EMadd1_pmap [unfold 8] {G : CommGroup} {X : Type*} (n : ℕ)
(e : Ω[succ n] X ≃* G)
(r : Πp q, e (p ⬝ q) = e p * e q)
[H1 : is_conn n X] [H2 : is_trunc (n.+1) X] : EMadd1 G n →* X :=
begin
revert X e r H1 H2, induction n with n f: intro X e r H1 H2,
{ exact EM1_pmap e⁻¹ᵉ* (equiv.inv_preserve_binary e concat mul r) },
rewrite [EMadd1_succ],
exact ptrunc.elim ((succ n).+1)
(psusp.elim (f _ (EM_up e) (is_homomorphism_EM_up e r) _ _)),
end
definition EMadd1_pmap_succ {G : CommGroup} {X : Type*} (n : ℕ) (e : Ω[succ (succ n)] X ≃* G)
r [H1 : is_conn (succ n) X] [H2 : is_trunc ((succ n).+1) X] : EMadd1_pmap (succ n) e r =
ptrunc.elim ((succ n).+1) (psusp.elim (EMadd1_pmap n (EM_up e) (is_homomorphism_EM_up e r))) :=
by reflexivity
definition loop_EMadd1_pmap {G : CommGroup} {X : Type*} {n : ℕ} (e : Ω[succ (succ n)] X ≃* G)
(r : Πp q, e (p ⬝ q) = e p * e q)
[H1 : is_conn (succ n) X] [H2 : is_trunc ((succ n).+1) X] :
Ω→(EMadd1_pmap (succ n) e r) ∘* loop_EMadd1 G n ~*
EMadd1_pmap n (EM_up e) (is_homomorphism_EM_up e r) :=
begin
cases n with n,
{ apply hopf_delooping_elim },
{ refine !passoc⁻¹* ⬝* _,
rewrite [EMadd1_pmap_succ (succ n)],
refine pwhisker_right _ !ap1_ptrunc_elim ⬝* _,
refine !passoc⁻¹* ⬝* _,
refine pwhisker_right _ (ptrunc_elim_freudenthal_pequiv
(succ n) (succ (succ n)) (add_mul_le_mul_add n 1 1) _) ⬝* _,
reflexivity }
end
definition loopn_EMadd1_pmap' {G : CommGroup} {X : Type*} {n : ℕ} (e : Ω[succ n] X ≃* G)
(r : Πp q, e (p ⬝ q) = e p * e q)
[H1 : is_conn n X] [H2 : is_trunc (n.+1) X] :
Ω→[succ n](EMadd1_pmap n e r) ∘* loopn_EMadd1 G n ~* e⁻¹ᵉ* :=
begin
revert X e r H1 H2, induction n with n IH: intro X e r H1 H2,
{ apply loop_EM1_pmap },
refine pwhisker_left _ !loopn_EMadd1_succ ⬝* _,
refine !passoc⁻¹* ⬝* _,
refine pwhisker_right _ !loopn_succ_in_inv_natural ⬝* _,
refine !passoc ⬝* _,
refine pwhisker_left _ (!passoc⁻¹* ⬝*
pwhisker_right _ (!apn_pcompose⁻¹* ⬝* apn_phomotopy _ !loop_EMadd1_pmap) ⬝*
!IH ⬝* !pinv_trans_pinv_left) ⬝* _,
apply pinv_pcompose_cancel_left
end
definition EMadd1_pequiv' {G : CommGroup} {X : Type*} (n : ℕ) (e : Ω[succ n] X ≃* G)
(r : Π(p q : Ω[succ n] X), e (p ⬝ q) = e p * e q)
[H1 : is_conn n X] [H2 : is_trunc (n.+1) X] : EMadd1 G n ≃* X :=
begin
apply pequiv_of_pmap (EMadd1_pmap n e r),
have is_conn 0 (EMadd1 G n), from is_conn_of_le _ (zero_le_of_nat n),
have is_trunc (n.+1) (EMadd1 G n), from !is_trunc_EMadd1,
refine whitehead_principle_pointed (n.+1) _ _,
intro k, apply @nat.lt_by_cases k (succ n): intro H,
{ apply @is_equiv_of_is_contr,
do 2 exact trivial_homotopy_group_of_is_conn _ (le_of_lt_succ H)},
{ cases H, esimp, apply is_equiv_trunc_functor, esimp,
apply is_equiv.homotopy_closed, rotate 1,
{ symmetry, exact phomotopy_pinv_right_of_phomotopy (loopn_EMadd1_pmap' _ _) },
apply is_equiv_compose (e⁻¹ᵉ*)},
{ apply @is_equiv_of_is_contr,
do 2 exact trivial_homotopy_group_of_is_trunc _ H}
end
definition EMadd1_pequiv {G : CommGroup} {X : Type*} (n : ℕ) (e : πg[n+1] X ≃g G)
[H1 : is_conn n X] [H2 : is_trunc (n.+1) X] : EMadd1 G n ≃* X :=
begin
have is_set (Ω[succ n] X), from !is_set_loopn,
apply EMadd1_pequiv' n ((ptrunc_pequiv _ _ _)⁻¹ᵉ* ⬝e* pequiv_of_isomorphism e),
intro p q, esimp, exact to_respect_mul e (tr p) (tr q)
end
definition EMadd1_pequiv_succ {G : CommGroup} {X : Type*} (n : ℕ) (e : πag[n+2] X ≃g G)
[H1 : is_conn (n.+1) X] [H2 : is_trunc (n.+2) X] : EMadd1 G (succ n) ≃* X :=
EMadd1_pequiv (succ n) e
definition ghomotopy_group_EMadd1 (n : ℕ) : πg[n+1] (EMadd1 G n) ≃g G :=
begin
change π₁ (Ω[n] (EMadd1 G n)) ≃g G,
refine homotopy_group_isomorphism_of_pequiv 0 (loopn_EMadd1_pequiv_EM1 G n)⁻¹ᵉ* ⬝g _,
apply fundamental_group_EM1,
end
definition EMadd1_pequiv_type (X : Type*) (n : ℕ) [is_conn (n+1) X] [is_trunc (n+1+1) X]
: EMadd1 (πag[n+2] X) (succ n) ≃* X :=
EMadd1_pequiv_succ n !isomorphism.refl
/- K(G, n) -/
definition EM (G : CommGroup) : ℕ → Type*
| 0 := G
| (k+1) := EMadd1 G k
namespace ops
abbreviation K := @EM
end ops
open ops
definition homotopy_group_EM (n : ℕ) : π[n] (EM G n) ≃* G :=
begin
cases n with n,
{ rexact ptrunc_pequiv 0 (G) _},
{ exact pequiv_of_isomorphism (ghomotopy_group_EMadd1 G n)}
end
definition ghomotopy_group_EM (n : ℕ) : πg[n+1] (EM G (n+1)) ≃g G :=
ghomotopy_group_EMadd1 G n
definition is_conn_EM [instance] (n : ℕ) : is_conn (n.-1) (EM G n) :=
begin
cases n with n,
{ apply is_conn_minus_one, apply tr, unfold [EM], exact 1},
{ apply is_conn_EMadd1}
end
definition is_conn_EM_succ [instance] (n : ℕ) : is_conn n (EM G (succ n)) :=
is_conn_EM G (succ n)
definition is_trunc_EM [instance] (n : ℕ) : is_trunc n (EM G n) :=
begin
cases n with n,
{ unfold [EM], apply semigroup.is_set_carrier},
{ apply is_trunc_EMadd1}
end
definition loop_EM (n : ℕ) : Ω (K G (succ n)) ≃* K G n :=
begin
cases n with n,
{ refine _ ⬝e* pequiv_of_isomorphism (fundamental_group_EM1 G),
symmetry, apply ptrunc_pequiv, exact _},
{ exact !loop_EMadd1⁻¹ᵉ* }
end
open circle int
definition EM_pequiv_circle : K agℤ 1 ≃* S¹* :=
EM1_pequiv fundamental_group_of_circle⁻¹ᵍ
/- Functorial action of Eilenberg-Maclane spaces -/
definition EM1_functor [constructor] {G H : Group} (φ : G →g H) : EM1 G →* EM1 H :=
begin
fconstructor,
{ intro g, induction g,
{ exact base },
{ exact pth (φ g) },
{ exact ap pth (to_respect_mul φ g h) ⬝ resp_mul (φ g) (φ h) }},
{ reflexivity }
end
definition EMadd1_functor [constructor] {G H : CommGroup} (φ : G →g H) (n : ℕ) :
EMadd1 G n →* EMadd1 H n :=
begin
induction n with n ψ,
{ exact EM1_functor φ },
{ apply ptrunc_functor, apply psusp_functor, exact ψ }
end
definition EM_functor [unfold 4] {G H : CommGroup} (φ : G →g H) (n : ℕ) :
K G n →* K H n :=
begin
cases n with n,
{ exact pmap_of_homomorphism φ },
{ exact EMadd1_functor φ n }
end
-- TODO: (K G n →* K H n) ≃ (G →g H)
/- Equivalence of Groups and pointed connected 1-truncated types -/
definition ptruncconntype10_pequiv (X Y : 1-Type*[0]) (e : π₁ X ≃g π₁ Y) : X ≃* Y :=
(EM1_pequiv !isomorphism.refl)⁻¹ᵉ* ⬝e* EM1_pequiv e
definition EM1_pequiv_ptruncconntype10 (X : 1-Type*[0]) : EM1 (π₁ X) ≃* X :=
EM1_pequiv_type X
definition Group_equiv_ptruncconntype10 [constructor] : Group ≃ 1-Type*[0] :=
equiv.MK (λG, ptruncconntype.mk (EM1 G) _ pt !is_conn_EM1)
(λX, π₁ X)
begin intro X, apply ptruncconntype_eq, esimp, exact EM1_pequiv_type X end
begin intro G, apply eq_of_isomorphism, apply fundamental_group_EM1 end
/- Equivalence of CommGroups and pointed n-connected (n+1)-truncated types (n ≥ 1) -/
open trunc_index
definition ptruncconntype_pequiv : Π(n : ℕ) (X Y : (n.+1)-Type*[n])
(e : πg[n+1] X ≃g πg[n+1] Y), X ≃* Y
| 0 X Y e := ptruncconntype10_pequiv X Y e
| (succ n) X Y e :=
begin
refine (EMadd1_pequiv_succ n _)⁻¹ᵉ* ⬝e* EMadd1_pequiv_succ n !isomorphism.refl,
exact e
end
definition EM1_pequiv_ptruncconntype (n : ℕ) (X : (n+1+1)-Type*[n+1]) :
EMadd1 (πag[n+2] X) (succ n) ≃* X :=
EMadd1_pequiv_type X n
definition CommGroup_equiv_ptruncconntype' [constructor] (n : ℕ) :
CommGroup ≃ (n + 1 + 1)-Type*[n+1] :=
equiv.MK
(λG, ptruncconntype.mk (EMadd1 G (n+1)) _ pt _)
(λX, πag[n+2] X)
begin intro X, apply ptruncconntype_eq, apply EMadd1_pequiv_type end
begin intro G, apply CommGroup_eq_of_isomorphism, exact ghomotopy_group_EMadd1 G (n+1) end
definition CommGroup_equiv_ptruncconntype [constructor] (n : ℕ) :
CommGroup ≃ (n.+2)-Type*[n.+1] :=
CommGroup_equiv_ptruncconntype' n
print axioms CommGroup_equiv_ptruncconntype
end EMnew

18
homotopy/cohomology.hlean
View file

@ -6,29 +6,29 @@ Authors: Floris van Doorn
Reduced cohomology
-/
import .EM algebra.arrow_group .spectrum
import algebra.arrow_group .spectrum homotopy.EM
open eq spectrum int trunc pointed EM group algebra circle sphere nat EM.ops
definition EM_spectrum /-[constructor]-/ (G : CommGroup) : spectrum :=
definition EM_spectrum /-[constructor]-/ (G : AbGroup) : spectrum :=
spectrum.Mk (K G) (λn, (loop_EM G n)⁻¹ᵉ*)
definition cohomology (X : Type*) (Y : spectrum) (n : ℤ) : CommGroup :=
CommGroup_pmap X (πag[2] (Y (2+n)))
definition cohomology (X : Type*) (Y : spectrum) (n : ℤ) : AbGroup :=
AbGroup_pmap X (πag[2] (Y (2+n)))
definition ordinary_cohomology [reducible] (X : Type*) (G : CommGroup) (n : ℤ) : CommGroup :=
definition ordinary_cohomology [reducible] (X : Type*) (G : AbGroup) (n : ℤ) : AbGroup :=
cohomology X (EM_spectrum G) n
definition ordinary_cohomology_Z [reducible] (X : Type*) (n : ℤ) : CommGroup :=
definition ordinary_cohomology_Z [reducible] (X : Type*) (n : ℤ) : AbGroup :=
ordinary_cohomology X agℤ n
notation `H^` n `[`:0 X:0 `, ` Y:0 `]`:0 := cohomology X Y n
notation `H^` n `[`:0 X:0 `]`:0 := ordinary_cohomology_Z X n
check H^3[S¹*,EM_spectrum agℤ]
check H^3[S¹*]
-- check H^3[S¹*,EM_spectrum agℤ]
-- check H^3[S¹*]
definition unpointed_cohomology (X : Type) (Y : spectrum) (n : ℤ) : CommGroup :=
definition unpointed_cohomology (X : Type) (Y : spectrum) (n : ℤ) : AbGroup :=
cohomology X₊ Y n
definition cohomology_homomorphism [constructor] {X X' : Type*} (f : X' →* X) (Y : spectrum)

2
homotopy/degree.hlean
View file

@ -55,7 +55,7 @@ namespace sphere
definition deg_id (n : ℕ) [H : is_succ n] : deg (pid (S* n)) = (1 : ℤ) :=
by induction H with n;
exact ap (πnSn n) (phomotopy_group_functor_pid (succ n) (S* (succ n)) (tr surf)) ⬝ πnSn_surf n
exact ap (πnSn n) (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 :=

2
homotopy/sample.hlean
View file

@ -175,7 +175,7 @@ namespace homotopy
apply trunc.rec,
intro a',
apply pathover_of_tr_eq,
rewrite [transport_eq_Fr,idp_con],
rewrite [eq_transport_Fr,idp_con],
revert H, induction n with [n, IH],
{ intro H, apply is_prop.elim },
{ intros H,

202
homotopy/smash.hlean
View file

@ -1,181 +1,9 @@
-- Authors: Floris van Doorn
/-
In this file we define the smash type. This is the cofiber of the map
wedge A B → A × B
However, we define it (equivalently) as the pushout of the maps A + B → 2 and A + B → A × B.
-/
import homotopy.circle homotopy.join types.pointed homotopy.cofiber ..move_to_lib
import homotopy.smash
open bool pointed eq equiv is_equiv sum bool prod unit circle cofiber prod.ops wedge
namespace smash
variables {A B : Type*}
section
open pushout
definition prod_of_sum [unfold 3] (u : A + B) : A × B :=
by induction u with a b; exact (a, pt); exact (pt, b)
definition bool_of_sum [unfold 3] (u : A + B) : bool :=
by induction u; exact ff; exact tt
definition smash' (A B : Type*) : Type := pushout (@prod_of_sum A B) (@bool_of_sum A B)
protected definition mk (a : A) (b : B) : smash' A B := inl (a, b)
definition pointed_smash' [instance] [constructor] (A B : Type*) : pointed (smash' A B) :=
pointed.mk (smash.mk pt pt)
definition smash [constructor] (A B : Type*) : Type* :=
pointed.mk' (smash' A B)
definition auxl : smash A B := inr ff
definition auxr : smash A B := inr tt
definition gluel (a : A) : smash.mk a pt = auxl :> smash A B := glue (inl a)
definition gluer (b : B) : smash.mk pt b = auxr :> smash A B := glue (inr b)
end
definition gluel' (a a' : A) : smash.mk a pt = smash.mk a' pt :> smash A B :=
gluel a ⬝ (gluel a')⁻¹
definition gluer' (b b' : B) : smash.mk pt b = smash.mk pt b' :> smash A B :=
gluer b ⬝ (gluer b')⁻¹
definition glue (a : A) (b : B) : smash.mk a pt = smash.mk pt b :=
gluel' a pt ⬝ gluer' pt b
definition glue_pt_left (b : B) : glue (Point A) b = gluer' pt b :=
whisker_right !con.right_inv _ ⬝ !idp_con
definition glue_pt_right (a : A) : glue a (Point B) = gluel' a pt :=
proof whisker_left _ !con.right_inv qed
definition ap_mk_left {a a' : A} (p : a = a') : ap (λa, smash.mk a (Point B)) p = gluel' a a' :=
by induction p; exact !con.right_inv⁻¹
definition ap_mk_right {b b' : B} (p : b = b') : ap (smash.mk (Point A)) p = gluer' b b' :=
by induction p; exact !con.right_inv⁻¹
protected definition rec {P : smash A B → Type} (Pmk : Πa b, P (smash.mk a b))
(Pl : P auxl) (Pr : P auxr) (Pgl : Πa, Pmk a pt =[gluel a] Pl)
(Pgr : Πb, Pmk pt b =[gluer b] Pr) (x : smash' A B) : P x :=
begin
induction x with x b u,
{ induction x with a b, exact Pmk a b },
{ induction b, exact Pl, exact Pr },
{ induction u: esimp,
{ apply Pgl },
{ apply Pgr }}
end
-- a rec which is easier to prove, but with worse computational properties
protected definition rec' {P : smash A B → Type} (Pmk : Πa b, P (smash.mk a b))
(Pg : Πa b, Pmk a pt =[glue a b] Pmk pt b) (x : smash' A B) : P x :=
begin
induction x using smash.rec,
{ apply Pmk },
{ exact gluel pt ▸ Pmk pt pt },
{ exact gluer pt ▸ Pmk pt pt },
{ refine change_path _ (Pg a pt ⬝o !pathover_tr),
refine whisker_right !glue_pt_right _ ⬝ _, esimp, refine !con.assoc ⬝ _,
apply whisker_left, apply con.left_inv },
{ refine change_path _ ((Pg pt b)⁻¹ᵒ ⬝o !pathover_tr),
refine whisker_right !glue_pt_left⁻² _ ⬝ _,
refine whisker_right !inv_con_inv_right _ ⬝ _, refine !con.assoc ⬝ _,
apply whisker_left, apply con.left_inv }
end
theorem rec_gluel {P : smash A B → Type} {Pmk : Πa b, P (smash.mk a b)}
{Pl : P auxl} {Pr : P auxr} (Pgl : Πa, Pmk a pt =[gluel a] Pl)
(Pgr : Πb, Pmk pt b =[gluer b] Pr) (a : A) :
apd (smash.rec Pmk Pl Pr Pgl Pgr) (gluel a) = Pgl a :=
!pushout.rec_glue
theorem rec_gluer {P : smash A B → Type} {Pmk : Πa b, P (smash.mk a b)}
{Pl : P auxl} {Pr : P auxr} (Pgl : Πa, Pmk a pt =[gluel a] Pl)
(Pgr : Πb, Pmk pt b =[gluer b] Pr) (b : B) :
apd (smash.rec Pmk Pl Pr Pgl Pgr) (gluer b) = Pgr b :=
!pushout.rec_glue
theorem rec_glue {P : smash A B → Type} {Pmk : Πa b, P (smash.mk a b)}
{Pl : P auxl} {Pr : P auxr} (Pgl : Πa, Pmk a pt =[gluel a] Pl)
(Pgr : Πb, Pmk pt b =[gluer b] Pr) (a : A) (b : B) :
apd (smash.rec Pmk Pl Pr Pgl Pgr) (glue a b) =
(Pgl a ⬝o (Pgl pt)⁻¹ᵒ) ⬝o (Pgr pt ⬝o (Pgr b)⁻¹ᵒ) :=
by rewrite [↑glue, ↑gluel', ↑gluer', +apd_con, +apd_inv, +rec_gluel, +rec_gluer]
protected definition elim {P : Type} (Pmk : Πa b, P) (Pl Pr : P)
(Pgl : Πa : A, Pmk a pt = Pl) (Pgr : Πb : B, Pmk pt b = Pr) (x : smash' A B) : P :=
smash.rec Pmk Pl Pr (λa, pathover_of_eq _ (Pgl a)) (λb, pathover_of_eq _ (Pgr b)) x
-- an elim which is easier to prove, but with worse computational properties
protected definition elim' {P : Type} (Pmk : Πa b, P) (Pg : Πa b, Pmk a pt = Pmk pt b)
(x : smash' A B) : P :=
smash.rec' Pmk (λa b, pathover_of_eq _ (Pg a b)) x
theorem elim_gluel {P : Type} {Pmk : Πa b, P} {Pl Pr : P}
(Pgl : Πa : A, Pmk a pt = Pl) (Pgr : Πb : B, Pmk pt b = Pr) (a : A) :
ap (smash.elim Pmk Pl Pr Pgl Pgr) (gluel a) = Pgl a :=
begin
apply eq_of_fn_eq_fn_inv !(pathover_constant (@gluel A B a)),
rewrite [▸*,-apd_eq_pathover_of_eq_ap,↑smash.elim,rec_gluel],
end
theorem elim_gluer {P : Type} {Pmk : Πa b, P} {Pl Pr : P}
(Pgl : Πa : A, Pmk a pt = Pl) (Pgr : Πb : B, Pmk pt b = Pr) (b : B) :
ap (smash.elim Pmk Pl Pr Pgl Pgr) (gluer b) = Pgr b :=
begin
apply eq_of_fn_eq_fn_inv !(pathover_constant (@gluer A B b)),
rewrite [▸*,-apd_eq_pathover_of_eq_ap,↑smash.elim,rec_gluer],
end
theorem elim_glue {P : Type} {Pmk : Πa b, P} {Pl Pr : P}
(Pgl : Πa : A, Pmk a pt = Pl) (Pgr : Πb : B, Pmk pt b = Pr) (a : A) (b : B) :
ap (smash.elim Pmk Pl Pr Pgl Pgr) (glue a b) = (Pgl a ⬝ (Pgl pt)⁻¹) ⬝ (Pgr pt ⬝ (Pgr b)⁻¹) :=
by rewrite [↑glue, ↑gluel', ↑gluer', +ap_con, +ap_inv, +elim_gluel, +elim_gluer]
end smash
open smash
attribute smash.mk auxl auxr [constructor]
attribute smash.rec smash.elim [unfold 9] [recursor 9]
attribute smash.rec' smash.elim' [unfold 6]
namespace smash
variables {A B : Type*}
definition of_smash_pbool [unfold 2] (x : smash A pbool) : A :=
begin
induction x,
{ induction b, exact pt, exact a },
{ exact pt },
{ exact pt },
{ reflexivity },
{ induction b: reflexivity }
end
definition smash_pbool_equiv [constructor] (A : Type*) : smash A pbool ≃* A :=
begin
fapply pequiv_of_equiv,
{ fapply equiv.MK,
{ exact of_smash_pbool },
{ intro a, exact smash.mk a tt },
{ intro a, reflexivity },
{ exact abstract begin intro x, induction x using smash.rec',
{ induction b, exact (glue a tt)⁻¹, reflexivity },
{ apply eq_pathover_id_right, induction b: esimp,
{ refine ap02 _ !glue_pt_right ⬝ph _,
refine ap_compose (λx, smash.mk x _) _ _ ⬝ph _,
refine ap02 _ (!ap_con ⬝ (!elim_gluel ◾ (!ap_inv ⬝ !elim_gluel⁻²))) ⬝ph _,
apply hinverse, apply square_of_eq,
esimp, refine (!glue_pt_right ◾ !glue_pt_left)⁻¹ },
{ apply square_of_eq, refine !con.left_inv ⬝ _, esimp, symmetry,
refine ap_compose (λx, smash.mk x _) _ _ ⬝ _,
exact ap02 _ !elim_glue }} end end }},
{ reflexivity }
end
/- smash A (susp B) = susp (smash A B) <- this follows from associativity and smash with S¹-/
/- To prove: Σ(X × Y) ≃ ΣX ∨ ΣY ∨ Σ(X ∧ Y) (notation means suspension, wedge, smash),
@ -185,7 +13,11 @@ namespace smash
/- smash A B ≃ pcofiber (pprod_of_pwedge A B) -/
definition prod_of_wedge [unfold 3] (v : pwedge' A B) : A × B :=
namespace smash
variables {A B : Type*}
definition prod_of_wedge [unfold 3] (v : pwedge A B) : A × B :=
begin
induction v with a b ,
{ exact (a, pt) },
@ -194,7 +26,7 @@ namespace smash
end
variables (A B)
definition pprod_of_pwedge [constructor] : pwedge' A B →* A ×* B :=
definition pprod_of_pwedge [constructor] : pwedge A B →* A ×* B :=
begin
fconstructor,
{ exact prod_of_wedge },
@ -203,7 +35,7 @@ namespace smash
variables {A B}
attribute pcofiber [constructor]
definition pcofiber_of_smash [unfold 3] (x : smash A B) : pcofiber' (@pprod_of_pwedge A B) :=
definition pcofiber_of_smash [unfold 3] (x : smash A B) : pcofiber (@pprod_of_pwedge A B) :=
begin
induction x,
{ exact pushout.inr (a, b) },
@ -218,7 +50,7 @@ namespace smash
(p : x = x') : ap (λx, f (g x) (h x)) p = ap011 f (ap g p) (ap h p) :=
by induction p; reflexivity
definition smash_of_pcofiber_glue [unfold 3] (x : pwedge' A B) :
definition smash_of_pcofiber_glue [unfold 3] (x : pwedge A B) :
Point (smash A B) = smash.mk (prod_of_wedge x).1 (prod_of_wedge x).2 :=
begin
induction x with a b: esimp,
@ -231,7 +63,7 @@ namespace smash
exact !con.right_inv ⬝ !con.right_inv⁻¹ }
end
definition smash_of_pcofiber [unfold 3] (x : pcofiber' (pprod_of_pwedge A B)) : smash A B :=
definition smash_of_pcofiber [unfold 3] (x : pcofiber (pprod_of_pwedge A B)) : smash A B :=
begin
induction x with x x,
{ exact smash.mk pt pt },
@ -239,7 +71,7 @@ namespace smash
{ exact smash_of_pcofiber_glue x }
end
definition pcofiber_of_smash_of_pcofiber (x : pcofiber' (pprod_of_pwedge A B)) :
definition pcofiber_of_smash_of_pcofiber (x : pcofiber (pprod_of_pwedge A B)) :
pcofiber_of_smash (smash_of_pcofiber x) = x :=
begin
induction x with x x,
@ -257,16 +89,16 @@ namespace smash
{ apply gluer },
{ apply eq_pathover_id_right, refine ap_compose smash_of_pcofiber _ _ ⬝ph _,
refine ap02 _ !elim_gluel ⬝ph _, refine !ap_inv ⬝ph _, refine !pushout.elim_glue⁻² ⬝ph _,
esimp, apply square_of_eq, refine !idp_con ⬝ _ ⬝ whisker_right !inv_con_inv_right⁻¹ _,
esimp, apply square_of_eq, refine !idp_con ⬝ _ ⬝ whisker_right _ !inv_con_inv_right⁻¹,
exact !inv_con_cancel_right⁻¹ },
{ apply eq_pathover_id_right, refine ap_compose smash_of_pcofiber _ _ ⬝ph _,
refine ap02 _ !elim_gluer ⬝ph _, refine !ap_inv ⬝ph _, refine !pushout.elim_glue⁻² ⬝ph _,
esimp, apply square_of_eq, refine !idp_con ⬝ _ ⬝ whisker_right !inv_con_inv_right⁻¹ _,
esimp, apply square_of_eq, refine !idp_con ⬝ _ ⬝ whisker_right _ !inv_con_inv_right⁻¹,
exact !inv_con_cancel_right⁻¹ },
end
variables (A B)
definition smash_pequiv_pcofiber : smash A B ≃* pcofiber' (pprod_of_pwedge A B) :=
definition smash_pequiv_pcofiber : smash A B ≃* pcofiber (pprod_of_pwedge A B) :=
begin
fapply pequiv_of_equiv,
{ fapply equiv.MK,
@ -315,7 +147,7 @@ exit -- the definitions below compile, but take a long time to do so and have so
apply square_of_eq, rewrite [+con.assoc], apply whisker_left, apply whisker_left,
symmetry, apply con_eq_of_eq_inv_con, esimp, apply con_eq_of_eq_con_inv,
refine _⁻² ⬝ !con_inv, refine _ ⬝ !con.assoc,
refine _ ⬝ whisker_right !inv_con_cancel_right⁻¹ _, refine _ ⬝ !con.right_inv⁻¹,
refine _ ⬝ whisker_right _ !inv_con_cancel_right⁻¹, refine _ ⬝ !con.right_inv⁻¹,
refine !con.right_inv ◾ _, refine _ ◾ !con.right_inv,
refine !ap_mk_right ⬝ !con.right_inv end end }
end
@ -328,7 +160,7 @@ exit -- the definitions below compile, but take a long time to do so and have so
begin
refine ap02 _ !elim_gluer ⬝ph _,
induction b,
{ apply square_of_eq, exact whisker_right !con.right_inv _ },
{ apply square_of_eq, exact whisker_right _ !con.right_inv },
{ apply square_pathover', exact sorry }
end
@ -361,7 +193,7 @@ exit -- the definitions below compile, but take a long time to do so and have so
refine ap_compose smash_pcircle_of_psusp _ _ ⬝ph _,
refine ap02 _ !elim_gluer ⬝ph _,
induction b,
{ apply square_of_eq, exact whisker_right !con.right_inv _ },
{ apply square_of_eq, exact whisker_right _ !con.right_inv },
{ exact sorry}
}}},
{ reflexivity }

24
homotopy/spectrum.hlean
View file

@ -6,6 +6,7 @@ Authors: Michael Shulman, Floris van Doorn
-/
import homotopy.LES_of_homotopy_groups .splice homotopy.susp ..move_to_lib ..colim
..pointed_pi
open eq nat int susp pointed pmap sigma is_equiv equiv fiber algebra trunc trunc_index pi group
seq_colim
@ -190,7 +191,7 @@ namespace spectrum
-- Suspension prespectra are one that's naturally indexed on the natural numbers
definition psp_susp (X : Type*) : gen_prespectrum +ℕ :=
gen_prespectrum.mk (λn, psuspn n X) (λn, loop_susp_unit (psuspn n X))
gen_prespectrum.mk (λn, psuspn n X) (λn, loop_psusp_unit (psuspn n X))
/- Truncations -/
@ -210,7 +211,7 @@ namespace spectrum
-- read off the homotopy groups without any tedious case-analysis of
-- n. We increment by 2 in order to ensure that they are all
-- automatically abelian groups.
definition shomotopy_group [constructor] (n : ℤ) (E : spectrum) : CommGroup := πag[0+2] (E (2 - n))
definition shomotopy_group [constructor] (n : ℤ) (E : spectrum) : AbGroup := πag[0+2] (E (2 - n))
notation `πₛ[`:95 n:0 `]`:0 := shomotopy_group n
@ -234,9 +235,10 @@ namespace spectrum
-- Sections of parametrized spectra
----------------------------------------
definition spi {N : succ_str} (A : Type) (E : A -> gen_spectrum N) : gen_spectrum N :=
spectrum.MK (λn, ppi (λa, E a n))
(λn, (loop_ppi_commute (λa, E a (S n)))⁻¹ᵉ* ∘*ᵉ equiv_ppi_right (λa, equiv_glue (E a) n))
-- this definition must be changed to use dependent maps respecting the basepoint, presumably
-- definition spi {N : succ_str} (A : Type) (E : A -> gen_spectrum N) : gen_spectrum N :=
-- spectrum.MK (λn, ppi (λa, E a n))
-- (λn, (loop_ppi_commute (λa, E a (S n)))⁻¹ᵉ* ∘*ᵉ equiv_ppi_right (λa, equiv_glue (E a) n))
/-----------------------------------------
Fibers and long exact sequences
@ -311,12 +313,12 @@ namespace spectrum
example (n : ℤ) : cc_to_fn LES_of_shomotopy_groups (n, 1) = πₛ→[n] (spoint f) := idp
-- the maps are ugly for (n, 2)
definition comm_group_LES_of_shomotopy_groups : Π(v : +3ℤ), comm_group (LES_of_shomotopy_groups v)
| (n, fin.mk 0 H) := proof CommGroup.struct (πₛ[n] Y) qed
| (n, fin.mk 1 H) := proof CommGroup.struct (πₛ[n] X) qed
| (n, fin.mk 2 H) := proof CommGroup.struct (πₛ[n] (sfiber f)) qed
definition ab_group_LES_of_shomotopy_groups : Π(v : +3ℤ), ab_group (LES_of_shomotopy_groups v)
| (n, fin.mk 0 H) := proof AbGroup.struct (πₛ[n] Y) qed
| (n, fin.mk 1 H) := proof AbGroup.struct (πₛ[n] X) qed
| (n, fin.mk 2 H) := proof AbGroup.struct (πₛ[n] (sfiber f)) qed
| (n, fin.mk (k+3) H) := begin exfalso, apply lt_le_antisymm H, apply le_add_left end
local attribute comm_group_LES_of_shomotopy_groups [instance]
local attribute ab_group_LES_of_shomotopy_groups [instance]
definition is_homomorphism_LES_of_shomotopy_groups :
Π(v : +3ℤ), is_homomorphism (cc_to_fn LES_of_shomotopy_groups v)
@ -330,7 +332,7 @@ namespace spectrum
-- In the comments below is a start on an explicit description of the LES for spectra
-- Maybe it's slightly nicer to work with than the above version
-- definition shomotopy_groups [reducible] : -3ℤ → CommGroup
-- definition shomotopy_groups [reducible] : -3ℤ → AbGroup
-- | (n, fin.mk 0 H) := πₛ[n] Y
-- | (n, fin.mk 1 H) := πₛ[n] X
-- | (n, fin.mk k H) := πₛ[n] (sfiber f)

2
homotopy/spherical_fibrations.hlean
View file

@ -90,7 +90,7 @@ namespace spherical_fibrations
definition BF_mul {n m : ℕ} (X : BF n) (Y : BF m) : BF (n + m) :=
begin
cases X with X hX, cases Y with Y hY,
apply sigma.mk (psmash X Y),
apply sigma.mk (smash X Y),
induction hX with fX, induction hY with fY, apply tr,
exact sorry -- needs smash.spheres : psmash (S. n) (S. m) ≃ S. (n + m)
end

1038
move_to_lib.hlean
View file

File diff suppressed because it is too large Load diff

13
pointed_pi.hlean
View file

@ -24,13 +24,6 @@ open eq pointed equiv sigma
namespace pointed
-- needs another name! (one more p?)
structure ppi (A : Type*) (P : A → Type*) :=
(to_fun : Π a : A, P a)
(resp_pt : to_fun (Point A) = Point (P (Point A)))
attribute ppi.to_fun [coercion]
abbreviation ppi_resp_pt [unfold 3] := @ppi.resp_pt
definition pointed_ppi [instance] [constructor] {A : Type*}
@ -79,7 +72,7 @@ namespace pointed
esimp at *,
fapply apd011 ppi.mk,
{ apply eq_of_homotopy h },
{ esimp, apply concato_eq, apply pathover_eq_Fl, apply inv_con_eq_of_eq_con,
{ esimp, apply concato_eq, apply eq_pathover_Fl, apply inv_con_eq_of_eq_con,
rewrite [ap_eq_apd10, apd10_eq_of_homotopy], exact r }
end
@ -105,11 +98,11 @@ namespace pointed
... ≃ Σ(p : ppi.to_fun f = ppi.to_fun g),
ppi_resp_pt f = ap (λh, h pt) p ⬝ ppi_resp_pt g
: sigma_equiv_sigma_right
(λp, pathover_eq_equiv_Fl p (ppi_resp_pt f) (ppi_resp_pt g))
(λp, eq_pathover_equiv_Fl p (ppi_resp_pt f) (ppi_resp_pt g))
... ≃ Σ(p : ppi.to_fun f = ppi.to_fun g),
ppi_resp_pt f = apd10 p pt ⬝ ppi_resp_pt g
: sigma_equiv_sigma_right
(λp, equiv_eq_closed_right _ (whisker_right (ap_eq_apd10 p _) _))
(λp, equiv_eq_closed_right _ (whisker_right _ (ap_eq_apd10 p _)))
... ≃ Σ(p : f ~ g), ppi_resp_pt f = p pt ⬝ ppi_resp_pt g
: sigma_equiv_sigma_left' eq_equiv_homotopy
... ≃ Σ(p : f ~ g), p pt ⬝ ppi_resp_pt g = ppi_resp_pt f