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

Merge branch 'master' of https://github.com/cmu-phil/Spectral

Browse source
This commit is contained in:
Egbert Rijke 2016-12-01 14:39:23 -05:00
commit c0a6e581e6
20 changed files with 339 additions and 1343 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,

36
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 ι := @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 :=
@ -35,26 +35,30 @@ namespace group
homomorphism.mk (λy, class_of (ι ⟨i, y⟩))
begin intro g h, symmetry, apply gqg_eq_of_rel, apply tr, apply dirsum_rel.rmk end
definition dirsum_elim [constructor] (f : Πi, Y i →g A') : dirsum →g A' :=
definition dirsum_elim_resp_quotient (f : Πi, Y i →g A') (g : dirsum_carrier)
(r : ∥dirsum_rel g∥) : free_ab_group_elim (λv, f v.1 v.2) g = 1 :=
begin
refine homomorphism.mk (gqg_elim _ (free_comm_group_elim (λv, f v.1 v.2)) _) _,
{ intro g r, induction r with r, induction r,
rewrite [to_respect_mul, to_respect_inv], apply mul_inv_eq_of_eq_mul,
rewrite [one_mul], apply ap (free_comm_group_elim (λ v, group_fun (f v.1) v.2)),
exact sorry
},
{ exact sorry }
induction r with r, induction r,
rewrite [to_respect_mul, to_respect_inv], apply mul_inv_eq_of_eq_mul,
rewrite [one_mul, to_respect_mul, ▸*, ↑foldl, +one_mul, to_respect_mul]
end
definition dirsum_elim [constructor] (f : Πi, Y i →g A') : dirsum →g A' :=
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 :=
begin
intro g, exact sorry
intro g, apply one_mul
end
definition dirsum_elim_unique (f : Πi, Y i →g A') (k : dirsum →g A')
(H : Πi, k ∘g dirsum_incl i ~ f i) : k ~ dirsum_elim f :=
sorry
begin
apply gqg_elim_unique,
apply free_ab_group_elim_unique,
intro x, induction x with i y, exact H i y
end
end

36
algebra/exact_couple.hlean
View file

@ -11,50 +11,50 @@ 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)
( 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,
intro g p,
induction p with f, induction f with h p,
rewrite [p⁻¹],
rewrite [p⁻¹],
esimp,
exact H h
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,
induction EC,
induction exact_jk,
intro b,
exact (ap (group_fun j) (im_in_ker (group_fun k b))) ⬝ (respect_one j)
end
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 :=

55
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,34 +160,41 @@ 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_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,
{ esimp [foldl], exact to_respect_one k},
{ rewrite [foldl_cons, fgh_helper_mul],
refine to_respect_mul k (class_of [s]) (class_of l) ⬝ _,
rewrite [IH], apply ap (λx, x * _), induction s: rewrite [▸*, one_mul, -H a],
apply to_respect_inv }
end
variables (X A)
definition free_comm_group_elim_equiv_fn : (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 φ, apply homomorphism_eq, refine set_quotient.rec_prop _, intro l, esimp,
induction l with s l IH,
{ esimp [foldl], symmetry, exact to_respect_one φ},
{ rewrite [foldl_cons, fgh_helper_mul],
refine _ ⬝ (to_respect_mul φ (class_of [s]) (class_of l))⁻¹,
rewrite [▸*,IH], induction s: rewrite [▸*, one_mul], apply ap (λx, x * _),
exact !to_respect_inv⁻¹}}
{ intro k, symmetry, apply homomorphism_eq, apply free_ab_group_elim_unique,
reflexivity }
end
end group

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

126
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 -/
@ -37,7 +37,7 @@ namespace group
have H2 : (g * h⁻¹) * (h * k⁻¹) = g * k⁻¹, from calc
(g * h⁻¹) * (h * k⁻¹) = ((g * h⁻¹) * h) * k⁻¹ : by rewrite [mul.assoc (g * h⁻¹)]
... = g * k⁻¹ : by rewrite inv_mul_cancel_right,
show N (g * k⁻¹), from H2 ▸ H1
show N (g * k⁻¹), by rewrite [-H2]; exact H1
theorem is_equivalence_quotient_rel : is_equivalence (quotient_rel N) :=
is_equivalence.mk quotient_rel_refl
@ -53,7 +53,7 @@ namespace group
g⁻¹ * (h * g⁻¹) * g = g⁻¹ * h * g⁻¹ * g : by rewrite -mul.assoc
... = g⁻¹ * h : inv_mul_cancel_right
... = g⁻¹ * h⁻¹⁻¹ : by rewrite algebra.inv_inv,
show N (g⁻¹ * h⁻¹⁻¹), from H2 ▸ H1
show N (g⁻¹ * h⁻¹⁻¹), by rewrite [-H2]; exact H1
theorem quotient_rel_resp_mul (r : quotient_rel N g h) (r' : quotient_rel N g' h')
: quotient_rel N (g * g') (h * h') :=
@ -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),
@ -187,26 +187,33 @@ namespace group
apply rel_of_eq _ H
end
definition quotient_group_elim (f : G →g G') (H : Π⦃g⦄, N g → f g = 1) : quotient_group N →g G' :=
definition quotient_group_elim_fun [unfold 6] (f : G →g G') (H : Π⦃g⦄, N g → f g = 1)
(g : quotient_group N) : G' :=
begin
refine set_quotient.elim f _ g,
intro g h K,
apply eq_of_mul_inv_eq_one,
have e : f (g * h⁻¹) = f g * (f h)⁻¹,
from calc
f (g * h⁻¹) = f g * (f h⁻¹) : to_respect_mul
... = f g * (f h)⁻¹ : to_respect_inv,
rewrite (inverse e),
apply H, exact K
end
definition quotient_group_elim [constructor] (f : G →g G') (H : Π⦃g⦄, N g → f g = 1) : quotient_group N →g G' :=
begin
fapply homomorphism.mk,
-- define function
{ apply set_quotient.elim f,
intro g h K,
apply eq_of_mul_inv_eq_one,
have e : f (g * h⁻¹) = f g * (f h)⁻¹,
from calc
f (g * h⁻¹) = f g * (f h⁻¹) : to_respect_mul
... = f g * (f h)⁻¹ : to_respect_inv,
rewrite (inverse e),
apply H, exact K},
{ exact quotient_group_elim_fun f H },
{ intro g h, induction g using set_quotient.rec_prop with g,
induction h using set_quotient.rec_prop with h,
krewrite (inverse (to_respect_mul (qg_map N) g h)),
unfold qg_map, esimp, exact to_respect_mul f g h }
end
definition quotient_group_compute (f : G →g G') (H : Π⦃g⦄, N g → f g = 1) : quotient_group_elim f H ∘g qg_map N ~ f :=
definition quotient_group_compute (f : G →g G') (H : Π⦃g⦄, N g → f g = 1) :
quotient_group_elim f H ∘g qg_map N ~ f :=
begin
intro g, reflexivity
end
@ -215,7 +222,6 @@ namespace group
: ( k ∘g qg_map N ~ f ) → k ~ quotient_group_elim f H :=
begin
intro K cg, induction cg using set_quotient.rec_prop with g,
krewrite (quotient_group_compute f),
exact K g
end
@ -231,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,
@ -254,12 +260,60 @@ 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 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,
intro p,
exact calc
f a = i (g a) : homotopy_of_eq (ap group_fun H) a
... = i 1 : ap i p
... = 1 : respect_one i
end
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 ab_group_kernel_factor f g H a,
intro p,
apply @is_injective_of_is_embedding _ _ i _ (g a) 1,
exact calc
i (g a) = f a : (homotopy_of_eq (ap group_fun H) a)⁻¹
... = 1 : p
... = i 1 : (respect_one i)⁻¹
end
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 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 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 (ab_group_kernel_image_lift _ _ f a) p
end
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)
end
print iff.mpr
/- set generating normal subgroup -/
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
@ -283,17 +337,17 @@ definition comm_group_first_iso_thm (A B : CommGroup) (f : A →g B) : quotient_
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₁}
definition gqg_eq_of_rel {g h : A₁} (H : S (g * h⁻¹)) : gqg_map g = gqg_map h :=
eq_of_rel (tr (rincl H))
definition gqg_elim (f : A₁ →g A₂) (H : Π⦃g⦄, S g → f g = 1)
: quotient_comm_group_gen →g A₂ :=
definition gqg_elim [constructor] (f : A₁ →g A₂) (H : Π⦃g⦄, S g → f g = 1)
: quotient_ab_group_gen →g A₂ :=
begin
apply quotient_group_elim f,
intro g r, induction r with r,
@ -311,7 +365,7 @@ definition comm_group_first_iso_thm (A B : CommGroup) (f : A →g B) : quotient_
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

40
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,24 +258,24 @@ 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,
repeat assumption,
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,
fapply subtype_eq,
induction t with p, induction s with q, induction p with g p, induction q with h q, induction p, induction q,
induction t with p, induction s with q, induction p with g p, induction q with h q, induction p, induction q,
refine (((respect_mul f g h)⁻¹ ⬝ _) ⬝ (respect_mul f h g)),
apply (ap f),
induction G, induction struct, apply mul_comm
@ -299,9 +299,9 @@ namespace group
definition image_lift {G H : Group} (f : G →g H) : G →g image f :=
begin
fapply hom_lift f,
intro g,
intro g,
apply tr,
fapply fiber.mk,
fapply fiber.mk,
exact g, reflexivity
end
@ -317,7 +317,7 @@ namespace group
intro p,
fapply subtype_eq,
exact p
end
end
definition image_incl_eq_one {G H : Group} (f : G →g H) : Π (x : image f), (image_incl f x = 1) → x = 1 :=
begin

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

279
homotopy/EM.hlean
View file

@ -1,279 +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 loop_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 loop_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
definition EM_spectrum /-[constructor]-/ (G : CommGroup) : spectrum :=
spectrum.Mk (K G) (λn, (loop_EM G n)⁻¹ᵉ*)
/- 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)) : pequiv_of_eq (homotopy_group_succ_in (psusp A) k)
-- ... ≃* Ω[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
end EM
-- cohomology ∥ X → K(G,n) ∥
-- reduced cohomology ∥ X →* K(G,n) ∥
-- but we probably want to do this for any spectrum

21
homotopy/cohomology.hlean
View file

@ -6,26 +6,29 @@ Authors: Floris van Doorn
Reduced cohomology
-/
import .EM algebra.arrow_group
import algebra.arrow_group .spectrum homotopy.EM
open eq spectrum int trunc pointed EM group algebra circle sphere nat
open eq spectrum int trunc pointed EM group algebra circle sphere nat EM.ops
definition cohomology (X : Type*) (Y : spectrum) (n : ℤ) : CommGroup :=
CommGroup_pmap X (πag[2] (Y (2+n)))
definition EM_spectrum /-[constructor]-/ (G : AbGroup) : spectrum :=
spectrum.Mk (K G) (λn, (loop_EM G n)⁻¹ᵉ*)
definition ordinary_cohomology [reducible] (X : Type*) (G : CommGroup) (n : ℤ) : CommGroup :=
definition cohomology (X : Type*) (Y : spectrum) (n : ℤ) : AbGroup :=
AbGroup_pmap X (πag[2] (Y (2+n)))
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)

6
homotopy/degree.hlean
View file

@ -51,11 +51,11 @@ namespace sphere
end
definition deg {n : ℕ} [H : is_succ n] (f : S* n →* S* n) : ℤ :=
by induction H with n; exact πnSn n ((π→g[n+1] f) (tr surf))
by induction H with n; exact πnSn n (π→g[n+1] f (tr surf))
definition deg_id (n : ℕ) [H : is_succ n] : deg (pid (S* n)) = (1 : ℤ) :=
by induction H with n;
exact ap (πnSn n) (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 :=
@ -94,7 +94,7 @@ namespace sphere
apply eq_one_or_eq_neg_one_of_mul_eq_one (deg f⁻¹ᵉ*),
refine !deg_compose⁻¹ ⬝ _,
refine deg_phomotopy (pright_inv f) ⬝ _,
apply deg_id,
apply deg_id
end
end sphere

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,

261
homotopy/smash.hlean
View file

@ -1,179 +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 smash [constructor] (A B : Type*) : Type* :=
pointed.MK (smash' A B) (smash.mk pt pt)
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),
@ -183,7 +13,11 @@ namespace smash
/- smash A B ≃ pcofiber (pprod_of_pwedge A B) -/
definition prod_of_pwedge [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) },
@ -191,18 +25,17 @@ namespace smash
{ reflexivity }
end
definition pprod_of_pwedge [constructor] : pwedge' A B →* A ×* B :=
variables (A B)
definition pprod_of_pwedge [constructor] : pwedge A B →* A ×* B :=
begin
fconstructor,
{ intro v, induction v with a b ,
{ exact (a, pt) },
{ exact (pt, b) },
{ reflexivity }},
{ exact prod_of_wedge },
{ reflexivity }
end
variables {A B}
attribute pcofiber [constructor]
definition pcofiber_of_smash (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) },
@ -212,26 +45,72 @@ namespace smash
{ symmetry, exact pushout.glue (pushout.inr b) }
end
-- move
definition ap_eq_ap011 {A B C X : Type} (f : A → B → C) (g : X → A) (h : X → B) {x x' : X}
(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 (x : pcofiber' (@pprod_of_pwedge A B)) : smash 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,
{ apply gluel' },
{ apply gluer' },
{ apply eq_pathover_constant_left, refine _ ⬝hp (ap_eq_ap011 smash.mk _ _ _)⁻¹,
rewrite [ap_compose' prod.pr1, ap_compose' prod.pr2],
-- TODO: define elim_glue for wedges and remove k in krewrite
krewrite [pushout.elim_glue], esimp, apply vdeg_square,
exact !con.right_inv ⬝ !con.right_inv⁻¹ }
end
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 },
{ exact smash.mk x.1 x.2 },
{ induction x with a b: esimp,
{ apply gluel' },
{ apply gluer' },
{ apply eq_pathover_constant_left, refine _ ⬝hp (ap_eq_ap011 smash.mk _ _ _)⁻¹,
unfold [wedge.elim],
rewrite [ap_compose' prod.pr1, ap_compose' prod.pr2],
-- TODO: define elim_glue for wedges and remove krewrite
krewrite [pushout.elim_glue], esimp, apply vdeg_square,
exact !con.right_inv ⬝ !con.right_inv⁻¹ }}
{ exact smash_of_pcofiber_glue x }
end
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,
{ refine (pushout.glue pt)⁻¹ },
{ exact sorry },
{ exact sorry }
end
definition smash_of_pcofiber_of_smash (x : smash A B) :
smash_of_pcofiber (pcofiber_of_smash x) = x :=
begin
induction x,
{ reflexivity },
{ apply gluel },
{ 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⁻¹,
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⁻¹,
exact !inv_con_cancel_right⁻¹ },
end
variables (A B)
definition smash_pequiv_pcofiber : smash A B ≃* pcofiber (pprod_of_pwedge A B) :=
begin
fapply pequiv_of_equiv,
{ fapply equiv.MK,
{ apply pcofiber_of_smash },
{ apply smash_of_pcofiber },
{ exact pcofiber_of_smash_of_pcofiber },
{ exact smash_of_pcofiber_of_smash }},
{ esimp, symmetry, apply pushout.glue pt }
end
variables {A B}
/- smash A S¹ = susp A -/
open susp
@ -268,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
@ -281,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
@ -314,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

721
move_to_lib.hlean
View file

@ -5,80 +5,27 @@ import homotopy.sphere2 homotopy.cofiber homotopy.wedge
open eq nat int susp pointed pmap sigma is_equiv equiv fiber algebra trunc trunc_index pi group
is_trunc function sphere
attribute equiv.symm equiv.trans is_equiv.is_equiv_ap fiber.equiv_postcompose
fiber.equiv_precompose pequiv.to_pmap pequiv._trans_of_to_pmap ghomotopy_group_succ_in
isomorphism_of_eq pmap_bool_equiv sphere_equiv_bool psphere_pequiv_pbool fiber_eq_equiv int.equiv_succ
[constructor]
attribute is_equiv.eq_of_fn_eq_fn' [unfold 3]
attribute isomorphism._trans_of_to_hom [unfold 3]
attribute homomorphism.struct [unfold 3]
attribute pequiv.trans pequiv.symm [constructor]
namespace sigma
definition sigma_equiv_sigma_left' [constructor] {A A' : Type} {B : A' → Type} (Hf : A ≃ A') : (Σa, B (Hf a)) ≃ (Σa', B a') :=
sigma_equiv_sigma Hf (λa, erfl)
end sigma
open sigma
namespace group
open is_trunc
-- some extra instances for type class inference
definition is_homomorphism_comm_homomorphism [instance] {G G' : CommGroup} (φ : G →g G')
: @is_homomorphism G G' (@comm_group.to_group _ (CommGroup.struct G))
(@comm_group.to_group _ (CommGroup.struct G')) φ :=
homomorphism.struct φ
-- definition is_homomorphism_comm_homomorphism [instance] {G G' : AbGroup} (φ : G →g G')
-- : @is_homomorphism G G' (@ab_group.to_group _ (AbGroup.struct G))
-- (@ab_group.to_group _ (AbGroup.struct G')) φ :=
-- homomorphism.struct φ
definition is_homomorphism_comm_homomorphism1 [instance] {G G' : CommGroup} (φ : G →g G')
: @is_homomorphism G G' _
(@comm_group.to_group _ (CommGroup.struct G')) φ :=
homomorphism.struct φ
-- definition is_homomorphism_comm_homomorphism1 [instance] {G G' : AbGroup} (φ : G →g G')
-- : @is_homomorphism G G' _
-- (@ab_group.to_group _ (AbGroup.struct G')) φ :=
-- homomorphism.struct φ
definition is_homomorphism_comm_homomorphism2 [instance] {G G' : CommGroup} (φ : G →g G')
: @is_homomorphism G G' (@comm_group.to_group _ (CommGroup.struct G)) _ φ :=
homomorphism.struct φ
theorem inv_eq_one {A : Type} [group A] {a : A} (H : a = 1) : a⁻¹ = 1 :=
iff.mpr (inv_eq_one_iff_eq_one a) H
definition pSet_of_Group (G : Group) : Set* := ptrunctype.mk G _ 1
definition pmap_of_isomorphism [constructor] {G₁ : Group} {G₂ : Group}
(φ : G₁ ≃g G₂) : pType_of_Group G₁ →* pType_of_Group G₂ :=
pequiv_of_isomorphism φ
definition pequiv_of_isomorphism_of_eq {G₁ G₂ : Group} (p : G₁ = G₂) :
pequiv_of_isomorphism (isomorphism_of_eq p) = pequiv_of_eq (ap pType_of_Group p) :=
begin
induction p,
apply pequiv_eq,
fapply pmap_eq,
{ intro g, reflexivity},
{ apply is_prop.elim}
end
definition homomorphism_change_fun [constructor] {G₁ G₂ : Group}
(φ : G₁ →g G₂) (f : G₁ → G₂) (p : φ ~ f) : G₁ →g G₂ :=
homomorphism.mk f (λg h, (p (g * h))⁻¹ ⬝ to_respect_mul φ g h ⬝ ap011 mul (p g) (p h))
definition Group_of_pgroup (G : Type*) [pgroup G] : Group :=
Group.mk G _
definition pgroup_pType_of_Group [instance] (G : Group) : pgroup (pType_of_Group G) :=
⦃ pgroup, Group.struct G,
pt_mul := one_mul,
mul_pt := mul_one,
mul_left_inv_pt := mul.left_inv ⦄
definition comm_group_pType_of_Group [instance] (G : CommGroup) : comm_group (pType_of_Group G) :=
CommGroup.struct G
abbreviation gid [constructor] := @homomorphism_id
-- definition is_homomorphism_comm_homomorphism2 [instance] {G G' : AbGroup} (φ : G →g G')
-- : @is_homomorphism G G' (@ab_group.to_group _ (AbGroup.struct G)) _ φ :=
-- homomorphism.struct φ
end group open group
namespace pi -- move to types.arrow
definition pmap_eq_idp {X Y : Type*} (f : X →* Y) :
@ -110,335 +57,30 @@ end pi open pi
namespace eq
-- types.eq
definition loop_equiv_eq_closed [constructor] {A : Type} {a a' : A} (p : a = a')
: (a = a) ≃ (a' = a') :=
eq_equiv_eq_closed p p
-- init.path
definition tr_ap {A B : Type} {x y : A} (P : B → Type) (f : A → B) (p : x = y) (z : P (f x)) :
transport P (ap f p) z = transport (P ∘ f) p z :=
(tr_compose P f p z)⁻¹
definition pathover_eq_Fl' {A B : Type} {f : A → B} {a₁ a₂ : A} {b : B} (p : a₁ = a₂) (q : f a₂ = b) : (ap f p) ⬝ q =[p] q :=
by induction p; induction q; exact idpo
-- this should be renamed square_pathover. The one in cubical.cube should be renamed
definition square_pathover' {A B : Type} {a a' : A} {b₁ b₂ b₃ b₄ : A → B}
{f₁ : b₁ ~ b₂} {f₂ : b₃ ~ b₄} {f₃ : b₁ ~ b₃} {f₄ : b₂ ~ b₄} {p : a = a'}
{q : square (f₁ a) (f₂ a) (f₃ a) (f₄ a)}
{r : square (f₁ a') (f₂ a') (f₃ a') (f₄ a')}
(s : cube (natural_square_tr f₁ p) (natural_square_tr f₂ p)
(natural_square_tr f₃ p) (natural_square_tr f₄ p) q r) : q =[p] r :=
by induction p; apply pathover_idp_of_eq; exact eq_of_deg12_cube s
-- define natural_square_tr this way. Also, natural_square_tr and natural_square should swap names
definition natural_square_tr_eq {A B : Type} {a a' : A} {f g : A → B}
(p : f ~ g) (q : a = a') : natural_square_tr p q = square_of_pathover (apd p q) :=
by induction q; reflexivity
section
variables {A : Type} {a₀₀₀ a₂₀₀ a₀₂₀ a₂₂₀ a₀₀₂ a₂₀₂ a₀₂₂ a₂₂₂ : A}
{p₁₀₀ : a₀₀₀ = a₂₀₀} {p₀₁₀ : a₀₀₀ = a₀₂₀} {p₀₀₁ : a₀₀₀ = a₀₀₂}
{p₁₂₀ : a₀₂₀ = a₂₂₀} {p₂₁₀ : a₂₀₀ = a₂₂₀} {p₂₀₁ : a₂₀₀ = a₂₀₂}
{p₁₀₂ : a₀₀₂ = a₂₀₂} {p₀₁₂ : a₀₀₂ = a₀₂₂} {p₀₂₁ : a₀₂₀ = a₀₂₂}
{p₁₂₂ : a₀₂₂ = a₂₂₂} {p₂₁₂ : a₂₀₂ = a₂₂₂} {p₂₂₁ : a₂₂₀ = a₂₂₂}
{s₁₁₀ : square p₀₁₀ p₂₁₀ p₁₀₀ p₁₂₀}
{s₁₁₂ : square p₀₁₂ p₂₁₂ p₁₀₂ p₁₂₂}
{s₀₁₁ : square p₀₁₀ p₀₁₂ p₀₀₁ p₀₂₁}
{s₂₁₁ : square p₂₁₀ p₂₁₂ p₂₀₁ p₂₂₁}
{s₁₀₁ : square p₁₀₀ p₁₀₂ p₀₀₁ p₂₀₁}
{s₁₂₁ : square p₁₂₀ p₁₂₂ p₀₂₁ p₂₂₁}
-- move to cubical.cube
definition eq_concat1 {s₀₁₁' : square p₀₁₀ p₀₁₂ p₀₀₁ p₀₂₁} (r : s₀₁₁' = s₀₁₁)
(c : cube s₀₁₁ s₂₁₁ s₁₀₁ s₁₂₁ s₁₁₀ s₁₁₂) : cube s₀₁₁' s₂₁₁ s₁₀₁ s₁₂₁ s₁₁₀ s₁₁₂ :=
by induction r; exact c
definition concat1_eq {s₂₁₁' : square p₂₁₀ p₂₁₂ p₂₀₁ p₂₂₁}
(c : cube s₀₁₁ s₂₁₁ s₁₀₁ s₁₂₁ s₁₁₀ s₁₁₂) (r : s₂₁₁ = s₂₁₁')
: cube s₀₁₁ s₂₁₁' s₁₀₁ s₁₂₁ s₁₁₀ s₁₁₂ :=
by induction r; exact c
definition eq_concat2 {s₁₀₁' : square p₁₀₀ p₁₀₂ p₀₀₁ p₂₀₁} (r : s₁₀₁' = s₁₀₁)
(c : cube s₀₁₁ s₂₁₁ s₁₀₁ s₁₂₁ s₁₁₀ s₁₁₂) : cube s₀₁₁ s₂₁₁ s₁₀₁' s₁₂₁ s₁₁₀ s₁₁₂ :=
by induction r; exact c
definition concat2_eq {s₁₂₁' : square p₁₂₀ p₁₂₂ p₀₂₁ p₂₂₁}
(c : cube s₀₁₁ s₂₁₁ s₁₀₁ s₁₂₁ s₁₁₀ s₁₁₂) (r : s₁₂₁ = s₁₂₁')
: cube s₀₁₁ s₂₁₁ s₁₀₁ s₁₂₁' s₁₁₀ s₁₁₂ :=
by induction r; exact c
definition eq_concat3 {s₁₁₀' : square p₀₁₀ p₂₁₀ p₁₀₀ p₁₂₀} (r : s₁₁₀' = s₁₁₀)
(c : cube s₀₁₁ s₂₁₁ s₁₀₁ s₁₂₁ s₁₁₀ s₁₁₂) : cube s₀₁₁ s₂₁₁ s₁₀₁ s₁₂₁ s₁₁₀' s₁₁₂ :=
by induction r; exact c
definition concat3_eq {s₁₁₂' : square p₀₁₂ p₂₁₂ p₁₀₂ p₁₂₂}
(c : cube s₀₁₁ s₂₁₁ s₁₀₁ s₁₂₁ s₁₁₀ s₁₁₂) (r : s₁₁₂ = s₁₁₂')
: cube s₀₁₁ s₂₁₁ s₁₀₁ s₁₂₁ s₁₁₀ s₁₁₂' :=
by induction r; exact c
end
infix ` ⬝1 `:75 := cube_concat1
infix ` ⬝2 `:75 := cube_concat2
infix ` ⬝3 `:75 := cube_concat3
infix ` ⬝p1 `:75 := eq_concat1
infix ` ⬝1p `:75 := concat1_eq
infix ` ⬝p2 `:75 := eq_concat3
infix ` ⬝2p `:75 := concat2_eq
infix ` ⬝p3 `:75 := eq_concat3
infix ` ⬝3p `:75 := concat3_eq
-- definition natural_square_tr_eq {A B : Type} {a a' : A} {f g : A → B}
-- (p : f ~ g) (q : a = a') : natural_square p q = square_of_pathover (apd p q) :=
-- idp
end eq open eq
namespace pointed
-- in init.pointed `pointed_carrier` should be [unfold 1] instead of [constructor]
definition ptransport [constructor] {A : Type} (B : A → Type*) {a a' : A} (p : a = a')
: B a →* B a' :=
pmap.mk (transport B p) (apdt (λa, Point (B a)) p)
-- /- the pointed type of (unpointed) dependent maps -/
-- definition pupi [constructor] {A : Type} (P : A → Type*) : Type* :=
-- pointed.mk' (Πa, P a)
definition ptransport_change_eq [constructor] {A : Type} (B : A → Type*) {a a' : A} {p q : a = a'}
(r : p = q) : ptransport B p ~* ptransport B q :=
phomotopy.mk (λb, ap (λp, transport B p b) r) begin induction r, exact !idp_con end
-- definition loop_pupi_commute {A : Type} (B : A → Type*) : Ω(pupi B) ≃* pupi (λa, Ω (B a)) :=
-- pequiv_of_equiv eq_equiv_homotopy rfl
definition pnatural_square {A B : Type} (X : B → Type*) {f g : A → B}
(h : Πa, X (f a) →* X (g a)) {a a' : A} (p : a = a') :
h a' ∘* ptransport X (ap f p) ~* ptransport X (ap g p) ∘* h a :=
by induction p; exact !pcompose_pid ⬝* !pid_pcompose⁻¹*
definition pequiv_ap [constructor] {A : Type} (B : A → Type*) {a a' : A} (p : a = a')
: B a ≃* B a' :=
pequiv_of_pmap (ptransport B p) !is_equiv_tr
definition pequiv_compose {A B C : Type*} (g : B ≃* C) (f : A ≃* B) : A ≃* C :=
pequiv_of_pmap (g ∘* f) (is_equiv_compose g f)
infixr ` ∘*ᵉ `:60 := pequiv_compose
definition pmap.sigma_char [constructor] {A B : Type*} : (A →* B) ≃ Σ(f : A → B), f pt = pt :=
begin
fapply equiv.MK : intros f,
{ exact ⟨to_fun f , resp_pt f⟩ },
all_goals cases f with f p,
{ exact pmap.mk f p },
all_goals reflexivity
end
definition is_trunc_pmap [instance] (n : ℕ₋₂) (A B : Type*) [is_trunc n B] : is_trunc n (A →* B) :=
is_trunc_equiv_closed_rev _ !pmap.sigma_char
definition is_trunc_ppmap [instance] (n : ℕ₋₂) {A B : Type*} [is_trunc n B] :
is_trunc n (ppmap A B) :=
!is_trunc_pmap
definition pmap_eq_of_homotopy {A B : Type*} {f g : A →* B} [is_set B] (p : f ~ g) : f = g :=
pmap_eq p !is_set.elim
definition phomotopy.sigma_char [constructor] {A B : Type*} (f g : A →* B) : (f ~* g) ≃ Σ(p : f ~ g), p pt ⬝ resp_pt g = resp_pt f :=
begin
fapply equiv.MK : intros h,
{ exact ⟨h , to_homotopy_pt h⟩ },
all_goals cases h with h p,
{ exact phomotopy.mk h p },
all_goals reflexivity
end
definition pmap_eq_equiv {A B : Type*} (f g : A →* B) : (f = g) ≃ (f ~* g) :=
calc (f = g) ≃ pmap.sigma_char f = pmap.sigma_char g
: eq_equiv_fn_eq pmap.sigma_char f g
... ≃ Σ(p : pmap.to_fun f = pmap.to_fun g), pathover (λh, h pt = pt) (resp_pt f) p (resp_pt g)
: sigma_eq_equiv _ _
... ≃ Σ(p : pmap.to_fun f = pmap.to_fun g), resp_pt f = ap (λh, h pt) p ⬝ resp_pt g
: sigma_equiv_sigma_right (λp, pathover_eq_equiv_Fl p (resp_pt f) (resp_pt g))
... ≃ Σ(p : pmap.to_fun f = pmap.to_fun g), resp_pt f = ap10 p pt ⬝ resp_pt g
: sigma_equiv_sigma_right (λp, equiv_eq_closed_right _ (whisker_right (ap_eq_apd10 p _) _))
... ≃ Σ(p : pmap.to_fun f ~ pmap.to_fun g), resp_pt f = p pt ⬝ resp_pt g
: sigma_equiv_sigma_left' eq_equiv_homotopy
... ≃ Σ(p : pmap.to_fun f ~ pmap.to_fun g), p pt ⬝ resp_pt g = resp_pt f
: sigma_equiv_sigma_right (λp, eq_equiv_eq_symm _ _)
... ≃ (f ~* g) : phomotopy.sigma_char f g
definition loop_pmap_commute (A B : Type*) : Ω(ppmap A B) ≃* (ppmap A (Ω B)) :=
pequiv_of_equiv
(calc Ω(ppmap A B) /- ≃ (pconst A B = pconst A B) : erfl
... -/ ≃ (pconst A B ~* pconst A B) : pmap_eq_equiv _ _
... ≃ Σ(p : pconst A B ~ pconst A B), p pt ⬝ rfl = rfl : phomotopy.sigma_char
... /- ≃ Σ(f : A → Ω B), f pt = pt : erfl
... -/ ≃ (A →* Ω B) : pmap.sigma_char)
(by reflexivity)
-- definition ppcompose_left {A B C : Type*} (g : B →* C) : ppmap A B →* ppmap A C :=
-- pmap.mk (pcompose g) (eq_of_phomotopy (phomotopy.mk (λa, resp_pt g) (idp_con _)⁻¹))
-- definition is_equiv_ppcompose_left [instance] {A B C : Type*} (g : B →* C) [H : is_equiv g] : is_equiv (@ppcompose_left A B C g) :=
-- begin
-- fapply is_equiv.adjointify,
-- { exact (ppcompose_left (pequiv_of_pmap g H)⁻¹ᵉ*) },
-- all_goals (intros f; esimp; apply eq_of_phomotopy),
-- { exact calc g ∘* ((pequiv_of_pmap g H)⁻¹ᵉ* ∘* f) ~* (g ∘* (pequiv_of_pmap g H)⁻¹ᵉ*) ∘* f : passoc
-- ... ~* pid _ ∘* f : pwhisker_right f (pright_inv (pequiv_of_pmap g H))
-- ... ~* f : pid_pcompose f },
-- { exact calc (pequiv_of_pmap g H)⁻¹ᵉ* ∘* (g ∘* f) ~* ((pequiv_of_pmap g H)⁻¹ᵉ* ∘* g) ∘* f : passoc
-- ... ~* pid _ ∘* f : pwhisker_right f (pleft_inv (pequiv_of_pmap g H))
-- ... ~* f : pid_pcompose f }
-- end
-- definition pequiv_ppcompose_left {A B C : Type*} (g : B ≃* C) : ppmap A B ≃* ppmap A C :=
-- pequiv_of_pmap (ppcompose_left g) _
-- definition pcompose_pconst {A B C : Type*} (f : B →* C) : f ∘* pconst A B ~* pconst A C :=
-- phomotopy.mk (λa, respect_pt f) (idp_con _)⁻¹
-- definition pconst_pcompose {A B C : Type*} (f : A →* B) : pconst B C ∘* f ~* pconst A C :=
-- phomotopy.mk (λa, rfl) (ap_constant _ _)⁻¹
definition ap1_pconst (A B : Type*) : Ω→(pconst A B) ~* pconst (Ω A) (Ω B) :=
phomotopy.mk (λp, idp_con _ ⬝ ap_constant p pt) rfl
definition apn_pconst (A B : Type*) (n : ℕ) :
apn n (pconst A B) ~* pconst (Ω[n] A) (Ω[n] B) :=
begin
induction n with n IH,
{ reflexivity },
{ exact ap1_phomotopy IH ⬝* !ap1_pconst }
end
definition loop_ppi_commute {A : Type} (B : A → Type*) : Ω(ppi B) ≃* Π*a, Ω (B a) :=
pequiv_of_equiv eq_equiv_homotopy rfl
definition equiv_ppi_right {A : Type} {P Q : A → Type*} (g : Πa, P a ≃* Q a)
: (Π*a, P a) ≃* (Π*a, Q a) :=
pequiv_of_equiv (pi_equiv_pi_right g)
begin esimp, apply eq_of_homotopy, intros a, esimp, exact (respect_pt (g a)) end
definition pcast_commute [constructor] {A : Type} {B C : A → Type*} (f : Πa, B a →* C a)
{a₁ a₂ : A} (p : a₁ = a₂) : pcast (ap C p) ∘* f a₁ ~* f a₂ ∘* pcast (ap B p) :=
phomotopy.mk
begin induction p, reflexivity end
begin induction p, esimp, refine !idp_con ⬝ !idp_con ⬝ !ap_id⁻¹ end
definition pequiv_of_eq_commute [constructor] {A : Type} {B C : A → Type*} (f : Πa, B a →* C a)
{a₁ a₂ : A} (p : a₁ = a₂) : pequiv_of_eq (ap C p) ∘* f a₁ ~* f a₂ ∘* pequiv_of_eq (ap B p) :=
pcast_commute f p
definition papply [constructor] {A : Type*} (B : Type*) (a : A) : ppmap A B →* B :=
pmap.mk (λ(f : A →* B), f a) idp
definition papply_pcompose [constructor] {A : Type*} (B : Type*) (a : A) : ppmap A B →* B :=
pmap.mk (λ(f : A →* B), f a) idp
open bool --also rename pmap_bool_equiv -> pmap_pbool_equiv
definition pbool_pmap [constructor] {A : Type*} (a : A) : pbool →* A :=
pmap.mk (bool.rec pt a) idp
definition pmap_pbool_pequiv [constructor] (B : Type*) : ppmap pbool B ≃* B :=
begin
fapply pequiv.MK,
{ exact papply B tt },
{ exact pbool_pmap },
{ intro f, fapply pmap_eq,
{ intro b, cases b, exact !respect_pt⁻¹, reflexivity },
{ exact !con.left_inv⁻¹ }},
{ intro b, reflexivity },
end
definition papn_pt [constructor] (n : ℕ) (A B : Type*) : ppmap A B →* ppmap (Ω[n] A) (Ω[n] B) :=
pmap.mk (λf, apn n f) (eq_of_phomotopy !apn_pconst)
definition papn_fun [constructor] {n : ℕ} {A : Type*} (B : Type*) (p : Ω[n] A) :
ppmap A B →* Ω[n] B :=
papply _ p ∘* papn_pt n A B
definition loopn_succ_in_natural {A B : Type*} (n : ℕ) (f : A →* B) :
loopn_succ_in B n ∘* Ω→[n+1] f ~* Ω→[n] (Ω→ f) ∘* loopn_succ_in A n :=
!apn_succ_phomotopy_in
definition loopn_succ_in_inv_natural {A B : Type*} (n : ℕ) (f : A →* B) :
Ω→[n + 1] f ∘* (loopn_succ_in A n)⁻¹ᵉ* ~* (loopn_succ_in B n)⁻¹ᵉ* ∘* Ω→[n] (Ω→ f):=
begin
apply pinv_right_phomotopy_of_phomotopy,
refine _ ⬝* !passoc⁻¹*,
apply phomotopy_pinv_left_of_phomotopy,
apply apn_succ_phomotopy_in
end
-- definition equiv_pupi_right {A : Type} {P Q : A → Type*} (g : Πa, P a ≃* Q a)
-- : pupi P ≃* pupi Q :=
-- pequiv_of_equiv (pi_equiv_pi_right g)
-- begin esimp, apply eq_of_homotopy, intros a, esimp, exact (respect_pt (g a)) end
end pointed open pointed
namespace fiber
definition pfiber.sigma_char [constructor] {A B : Type*} (f : A →* B)
: pfiber f ≃* pointed.MK (Σa, f a = pt) ⟨pt, respect_pt f⟩ :=
pequiv_of_equiv (fiber.sigma_char f pt) idp
definition ppoint_sigma_char [constructor] {A B : Type*} (f : A →* B)
: ppoint f ~* pmap.mk pr1 idp ∘* pfiber.sigma_char f :=
!phomotopy.refl
definition pfiber_loop_space {A B : Type*} (f : A →* B) : pfiber (Ω→ f) ≃* Ω (pfiber f) :=
pequiv_of_equiv
(calc pfiber (Ω→ f) ≃ Σ(p : Point A = Point A), ap1 f p = rfl
: (fiber.sigma_char (ap1 f) (Point (Ω B)))
... ≃ Σ(p : Point A = Point A), (respect_pt f) = ap f p ⬝ (respect_pt f)
: (sigma_equiv_sigma_right (λp,
calc (ap1 f p = rfl) ≃ !respect_pt⁻¹ ⬝ (ap f p ⬝ !respect_pt) = rfl
: equiv_eq_closed_left _ (con.assoc _ _ _)
... ≃ ap f p ⬝ (respect_pt f) = (respect_pt f)
: eq_equiv_inv_con_eq_idp
... ≃ (respect_pt f) = ap f p ⬝ (respect_pt f)
: eq_equiv_eq_symm))
... ≃ fiber.mk (Point A) (respect_pt f) = fiber.mk pt (respect_pt f)
: fiber_eq_equiv
... ≃ Ω (pfiber f)
: erfl)
(begin cases f with f p, cases A with A a, cases B with B b, esimp at p, esimp at f,
induction p, reflexivity end)
definition pfiber_equiv_of_phomotopy {A B : Type*} {f g : A →* B} (h : f ~* g)
: pfiber f ≃* pfiber g :=
begin
fapply pequiv_of_equiv,
{ refine (fiber.sigma_char f pt ⬝e _ ⬝e (fiber.sigma_char g pt)⁻¹ᵉ),
apply sigma_equiv_sigma_right, intros a,
apply equiv_eq_closed_left, apply (to_homotopy h) },
{ refine (fiber_eq rfl _),
change (h pt)⁻¹ ⬝ respect_pt f = idp ⬝ respect_pt g,
rewrite idp_con, apply inv_con_eq_of_eq_con, symmetry, exact (to_homotopy_pt h) }
end
definition transport_fiber_equiv [constructor] {A B : Type} (f : A → B) {b1 b2 : B} (p : b1 = b2)
: fiber f b1 ≃ fiber f b2 :=
calc fiber f b1 ≃ Σa, f a = b1 : fiber.sigma_char
... ≃ Σa, f a = b2 : sigma_equiv_sigma_right (λa, equiv_eq_closed_right (f a) p)
... ≃ fiber f b2 : fiber.sigma_char
definition pequiv_postcompose {A B B' : Type*} (f : A →* B) (g : B ≃* B')
: pfiber (g ∘* f) ≃* pfiber f :=
begin
fapply pequiv_of_equiv, esimp,
refine transport_fiber_equiv (g ∘* f) (respect_pt g)⁻¹ ⬝e fiber.equiv_postcompose f g (Point B),
esimp, apply (ap (fiber.mk (Point A))), refine !con.assoc ⬝ _, apply inv_con_eq_of_eq_con,
rewrite [con.assoc, con.right_inv, con_idp, -ap_compose'], apply ap_con_eq_con
end
definition pequiv_precompose {A A' B : Type*} (f : A →* B) (g : A' ≃* A)
: pfiber (f ∘* g) ≃* pfiber f :=
begin
fapply pequiv_of_equiv, esimp,
refine fiber.equiv_precompose f g (Point B),
esimp, apply (eq_of_fn_eq_fn (fiber.sigma_char _ _)), fapply sigma_eq: esimp,
{ apply respect_pt g },
{ apply pathover_eq_Fl' }
end
definition pfiber_equiv_of_square {A B C D : Type*} {f : A →* B} {g : C →* D} (h : A ≃* C)
(k : B ≃* D) (s : k ∘* f ~* g ∘* h) : pfiber f ≃* pfiber g :=
calc pfiber f ≃* pfiber (k ∘* f) : pequiv_postcompose
... ≃* pfiber (g ∘* h) : pfiber_equiv_of_phomotopy s
... ≃* pfiber g : pequiv_precompose
definition ap1_ppoint_phomotopy {A B : Type*} (f : A →* B)
: Ω→ (ppoint f) ∘* pfiber_loop_space f ~* ppoint (Ω→ f) :=
@ -453,125 +95,6 @@ namespace fiber
end fiber
namespace eq --algebra.homotopy_group
definition phomotopy_group_functor_pid (n : ℕ) (A : Type*) : π→[n] (pid A) ~* pid (π[n] A) :=
ptrunc_functor_phomotopy 0 !apn_pid ⬝* !ptrunc_functor_pid
end eq
namespace susp
definition iterate_psusp_functor (n : ℕ) {A B : Type*} (f : A →* B) :
iterate_psusp n A →* iterate_psusp n B :=
begin
induction n with n g,
{ exact f },
{ exact psusp_functor g }
end
end susp
namespace is_conn -- homotopy.connectedness
structure conntype (n : ℕ₋₂) : Type :=
(carrier : Type)
(struct : is_conn n carrier)
notation `Type[`:95 n:0 `]`:0 := conntype n
attribute conntype.carrier [coercion]
attribute conntype.struct [instance] [priority 1300]
section
universe variable u
structure pconntype (n : ℕ₋₂) extends conntype.{u} n, pType.{u}
notation `Type*[`:95 n:0 `]`:0 := pconntype n
/-
There are multiple coercions from pconntype to Type. Type class inference doesn't recognize
that all of them are definitionally equal (for performance reasons). One instance is
automatically generated, and we manually add the missing instances.
-/
definition is_conn_pconntype [instance] {n : ℕ₋₂} (X : Type*[n]) : is_conn n X :=
conntype.struct X
/- Now all the instances work -/
example {n : ℕ₋₂} (X : Type*[n]) : is_conn n X := _
example {n : ℕ₋₂} (X : Type*[n]) : is_conn n (pconntype.to_pType X) := _
example {n : ℕ₋₂} (X : Type*[n]) : is_conn n (pconntype.to_conntype X) := _
example {n : ℕ₋₂} (X : Type*[n]) : is_conn n (pconntype._trans_of_to_pType X) := _
example {n : ℕ₋₂} (X : Type*[n]) : is_conn n (pconntype._trans_of_to_conntype X) := _
structure truncconntype (n k : ℕ₋₂) extends trunctype.{u} n,
conntype.{u} k renaming struct→conn_struct
notation n `-Type[`:95 k:0 `]`:0 := truncconntype n k
definition is_conn_truncconntype [instance] {n k : ℕ₋₂} (X : n-Type[k]) :
is_conn k (truncconntype._trans_of_to_trunctype X) :=
conntype.struct X
definition is_trunc_truncconntype [instance] {n k : ℕ₋₂} (X : n-Type[k]) : is_trunc n X :=
trunctype.struct X
structure ptruncconntype (n k : ℕ₋₂) extends ptrunctype.{u} n,
pconntype.{u} k renaming struct→conn_struct
notation n `-Type*[`:95 k:0 `]`:0 := ptruncconntype n k
attribute ptruncconntype._trans_of_to_pconntype ptruncconntype._trans_of_to_ptrunctype
ptruncconntype._trans_of_to_pconntype_1 ptruncconntype._trans_of_to_ptrunctype_1
ptruncconntype._trans_of_to_pconntype_2 ptruncconntype._trans_of_to_ptrunctype_2
ptruncconntype.to_pconntype ptruncconntype.to_ptrunctype
truncconntype._trans_of_to_conntype truncconntype._trans_of_to_trunctype
truncconntype.to_conntype truncconntype.to_trunctype [unfold 3]
attribute pconntype._trans_of_to_conntype pconntype._trans_of_to_pType
pconntype.to_pType pconntype.to_conntype [unfold 2]
definition is_conn_ptruncconntype [instance] {n k : ℕ₋₂} (X : n-Type*[k]) :
is_conn k (ptruncconntype._trans_of_to_ptrunctype X) :=
conntype.struct X
definition is_trunc_ptruncconntype [instance] {n k : ℕ₋₂} (X : n-Type*[k]) :
is_trunc n (ptruncconntype._trans_of_to_pconntype X) :=
trunctype.struct X
definition ptruncconntype_eq {n k : ℕ₋₂} {X Y : n-Type*[k]} (p : X ≃* Y) : X = Y :=
begin
induction X with X Xt Xp Xc, induction Y with Y Yt Yp Yc,
note q := pType_eq_elim (eq_of_pequiv p),
cases q with r s, esimp at *, induction r,
exact ap0111 (ptruncconntype.mk X) !is_prop.elim (eq_of_pathover_idp s) !is_prop.elim
end
end
end is_conn
namespace succ_str
variables {N : succ_str}
protected definition add [reducible] (n : N) (k : ℕ) : N :=
iterate S k n
infix ` +' `:65 := succ_str.add
definition add_succ (n : N) (k : ℕ) : n +' (k + 1) = (S n) +' k :=
by induction k with k p; reflexivity; exact ap S p
end succ_str
namespace join
definition pjoin [constructor] (A B : Type*) : Type* := pointed.MK (join A B) (inl pt)
end join
namespace circle
@ -582,11 +105,11 @@ namespace circle
to the square which defined H on the path constructor
-/
definition natural_square_tr_elim_loop {A : Type} {f g : S¹ → A} (p : f base = g base)
definition natural_square_elim_loop {A : Type} {f g : S¹ → A} (p : f base = g base)
(q : square p p (ap f loop) (ap g loop))
: natural_square_tr (circle.rec p (eq_pathover q)) loop = q :=
: natural_square (circle.rec p (eq_pathover q)) loop = q :=
begin
refine !natural_square_tr_eq ⬝ _,
-- refine !natural_square_eq ⬝ _,
refine ap square_of_pathover !rec_loop ⬝ _,
exact to_right_inv !eq_pathover_equiv_square q
end
@ -594,162 +117,8 @@ namespace circle
end circle
-- this should replace various definitions in homotopy.susp, lines 241 - 338
namespace new_susp
variables {X Y Z : Type*}
definition loop_psusp_unit [constructor] (X : Type*) : X →* Ω(psusp X) :=
begin
fconstructor,
{ intro x, exact merid x ⬝ (merid pt)⁻¹ },
{ apply con.right_inv },
end
definition loop_psusp_unit_natural (f : X →* Y)
: loop_psusp_unit Y ∘* f ~* ap1 (psusp_functor f) ∘* loop_psusp_unit X :=
begin
induction X with X x, induction Y with Y y, induction f with f pf, esimp at *, induction pf,
fconstructor,
{ intro x', esimp [psusp_functor], symmetry,
exact
!idp_con ⬝
(!ap_con ⬝
whisker_left _ !ap_inv) ⬝
(!elim_merid ◾ (inverse2 !elim_merid)) },
{ rewrite [▸*,idp_con (con.right_inv _)],
apply inv_con_eq_of_eq_con,
refine _ ⬝ !con.assoc',
rewrite inverse2_right_inv,
refine _ ⬝ !con.assoc',
rewrite [ap_con_right_inv],
xrewrite [idp_con_idp, -ap_compose (concat idp)] },
end
definition loop_psusp_counit [constructor] (X : Type*) : psusp (Ω X) →* X :=
begin
fconstructor,
{ intro x, induction x, exact pt, exact pt, exact a },
{ reflexivity },
end
definition loop_psusp_counit_natural (f : X →* Y)
: f ∘* loop_psusp_counit X ~* loop_psusp_counit Y ∘* (psusp_functor (ap1 f)) :=
begin
induction X with X x, induction Y with Y y, induction f with f pf, esimp at *, induction pf,
fconstructor,
{ intro x', induction x' with p,
{ reflexivity },
{ reflexivity },
{ esimp, apply eq_pathover, apply hdeg_square,
xrewrite [ap_compose' f, ap_compose' (susp.elim (f x) (f x) (λ (a : f x = f x), a)),▸*],
xrewrite [+elim_merid,▸*,idp_con] }},
{ reflexivity }
end
definition loop_psusp_counit_unit (X : Type*)
: ap1 (loop_psusp_counit X) ∘* loop_psusp_unit (Ω X) ~* pid (Ω X) :=
begin
induction X with X x, fconstructor,
{ intro p, esimp,
refine !idp_con ⬝
(!ap_con ⬝
whisker_left _ !ap_inv) ⬝
(!elim_merid ◾ inverse2 !elim_merid) },
{ rewrite [▸*,inverse2_right_inv (elim_merid id idp)],
refine !con.assoc ⬝ _,
xrewrite [ap_con_right_inv (susp.elim x x (λa, a)) (merid idp),idp_con_idp,-ap_compose] }
end
definition loop_psusp_unit_counit (X : Type*)
: loop_psusp_counit (psusp X) ∘* psusp_functor (loop_psusp_unit X) ~* pid (psusp X) :=
begin
induction X with X x, fconstructor,
{ intro x', induction x',
{ reflexivity },
{ exact merid pt },
{ apply eq_pathover,
xrewrite [▸*, ap_id, ap_compose' (susp.elim north north (λa, a)), +elim_merid,▸*],
apply square_of_eq, exact !idp_con ⬝ !inv_con_cancel_right⁻¹ }},
{ reflexivity }
end
-- TODO: rename to psusp_adjoint_loop (also in above lemmas)
definition psusp_adjoint_loop_unpointed [constructor] (X Y : Type*) : psusp X →* Y ≃ X →* Ω Y :=
begin
fapply equiv.MK,
{ intro f, exact ap1 f ∘* loop_psusp_unit X },
{ intro g, exact loop_psusp_counit Y ∘* psusp_functor g },
{ intro g, apply eq_of_phomotopy, esimp,
refine !pwhisker_right !ap1_pcompose ⬝* _,
refine !passoc ⬝* _,
refine !pwhisker_left !loop_psusp_unit_natural⁻¹* ⬝* _,
refine !passoc⁻¹* ⬝* _,
refine !pwhisker_right !loop_psusp_counit_unit ⬝* _,
apply pid_pcompose },
{ intro f, apply eq_of_phomotopy, esimp,
refine !pwhisker_left !psusp_functor_compose ⬝* _,
refine !passoc⁻¹* ⬝* _,
refine !pwhisker_right !loop_psusp_counit_natural⁻¹* ⬝* _,
refine !passoc ⬝* _,
refine !pwhisker_left !loop_psusp_unit_counit ⬝* _,
apply pcompose_pid },
end
definition psusp_adjoint_loop_pconst (X Y : Type*) :
psusp_adjoint_loop_unpointed X Y (pconst (psusp X) Y) ~* pconst X (Ω Y) :=
begin
refine pwhisker_right _ !ap1_pconst ⬝* _,
apply pconst_pcompose
end
definition psusp_adjoint_loop [constructor] (X Y : Type*) : ppmap (psusp X) Y ≃* ppmap X (Ω Y) :=
begin
apply pequiv_of_equiv (psusp_adjoint_loop_unpointed X Y),
apply eq_of_phomotopy,
apply psusp_adjoint_loop_pconst
end
end new_susp open new_susp
-- this should replace corresponding definitions in homotopy.sphere
namespace new_sphere
open sphere sphere.ops
-- the definition was wrong for n = 0
definition new.surf {n : ℕ} : Ω[n] (S* n) :=
begin
induction n with n s,
{ exact south },
{ exact (loopn_succ_in (S* (succ n)) n)⁻¹ᵉ* (apn n (equator n) s), }
end
definition psphere_pmap_pequiv' (A : Type*) (n : ℕ) : ppmap (S* n) A ≃* Ω[n] A :=
begin
revert A, induction n with n IH: intro A,
{ refine _ ⬝e* !pmap_pbool_pequiv, exact pequiv_ppcompose_right psphere_pequiv_pbool⁻¹ᵉ* },
{ refine psusp_adjoint_loop (S* n) A ⬝e* IH (Ω A) ⬝e* !loopn_succ_in⁻¹ᵉ* }
end
definition psphere_pmap_pequiv (A : Type*) (n : ℕ) : ppmap (S* n) A ≃* Ω[n] A :=
begin
fapply pequiv_change_fun,
{ exact psphere_pmap_pequiv' A n },
{ exact papn_fun A new.surf },
{ revert A, induction n with n IH: intro A,
{ reflexivity },
{ intro f, refine ap !loopn_succ_in⁻¹ᵉ* (IH (Ω A) _ ⬝ !apn_pcompose _) ⬝ _,
exact !loopn_succ_in_inv_natural⁻¹* _ }}
end
end new_sphere
namespace sphere
open sphere.ops new_sphere
-- definition constant_sphere_map_sphere {n m : ℕ} (H : n < m) (f : S* n →* S* m) :
-- f ~* pconst (S* n) (S* m) :=
-- begin
@ -761,39 +130,3 @@ namespace sphere
-- end
end sphere
namespace cofiber
-- replace with the definition of pcofiber (and remove primes in homotopy.smash)
definition pcofiber' [constructor] {A B : Type*} (f : A →* B) : Type* :=
pointed.MK (cofiber f) !cofiber.base
attribute pcofiber [constructor]
-- move ppushout attribute out namespace
protected definition elim {A : Type} {B : Type} {f : A → B} {P : Type}
(Pinl : P) (Pinr : B → P) (Pglue : Π (x : A), Pinl = Pinr (f x)) (y : cofiber f) : P :=
begin
induction y using pushout.elim with x x x, induction x, exact Pinl, exact Pinr x, exact Pglue x,
end
end cofiber
attribute cofiber.rec cofiber.elim [recursor 8] [unfold 8]
namespace wedge
open pushout unit
definition wedge (A B : Type*) : Type := ppushout (pconst punit A) (pconst punit B)
local attribute wedge [reducible]
definition pwedge' (A B : Type*) : Type* := pointed.mk' (wedge A B)
protected definition rec {A B : Type*} {P : wedge A B → Type} (Pinl : Π(x : A), P (inl x))
(Pinr : Π(x : B), P (inr x)) (Pglue : pathover P (Pinl pt) (glue ⋆) (Pinr pt))
(y : wedge A B) : P y :=
by induction y; apply Pinl; apply Pinr; induction x; exact Pglue
protected definition elim {A B : Type*} {P : Type} (Pinl : A → P)
(Pinr : B → P) (Pglue : Pinl pt = Pinr pt) (y : wedge A B) : P :=
by induction y with a b x; exact Pinl a; exact Pinr b; induction x; exact Pglue
end wedge
attribute wedge.rec wedge.elim [recursor 7] [unfold 7]

15
pointed_pi.hlean
View file

@ -13,7 +13,7 @@ open eq pointed equiv sigma
of the type of pointed maps, giving the connectivity of
the domain and the truncation level of the codomain.
This is is_trunc_pmap at the end.
First we define the type of dependent pointed maps
as a tool, because these appear in the more general
statement is_trunc_ppi (the generality needed for induction).
@ -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