feat(algebra): use infinity groups
This commit is contained in:
Floris van Doorn
parent
25ab404781
commit
5eafb1f6b2
5 changed files with 161 additions and 39 deletions
|
|
@ -87,6 +87,11 @@ attribute algebra._trans_of_Group_of_AbGroup_1
|
|||
algebra._trans_of_Group_of_AbGroup_3 [constructor]
|
||||
attribute algebra._trans_of_Group_of_AbGroup_2 [unfold 1]
|
||||
|
||||
definition ab_group_AbGroup [instance] (G : AbGroup) : ab_group G :=
|
||||
AbGroup.struct G
|
||||
|
||||
definition add_ab_group_AddAbGroup [instance] (G : AddAbGroup) : add_ab_group G :=
|
||||
AbGroup.struct G
|
||||
|
||||
-- structure AddSemigroup :=
|
||||
-- (carrier : Type) (struct : add_semigroup carrier)
|
||||
|
|
@ -123,4 +128,66 @@ attribute algebra._trans_of_Group_of_AbGroup_2 [unfold 1]
|
|||
|
||||
-- attribute AddAbGroup.carrier [coercion]
|
||||
-- attribute AddAbGroup.struct [instance]
|
||||
|
||||
|
||||
-- some bundled infinity-structures
|
||||
structure InfGroup :=
|
||||
(carrier : Type) (struct : inf_group carrier)
|
||||
|
||||
attribute InfGroup.carrier [coercion]
|
||||
attribute InfGroup.struct [instance]
|
||||
|
||||
section
|
||||
local attribute InfGroup.struct [instance]
|
||||
definition pType_of_InfGroup [constructor] [reducible] [coercion] (G : InfGroup) : Type* :=
|
||||
pType.mk G 1
|
||||
end
|
||||
|
||||
attribute algebra._trans_of_pType_of_InfGroup [unfold 1]
|
||||
|
||||
definition AddInfGroup : Type := InfGroup
|
||||
|
||||
definition AddInfGroup.mk [constructor] [reducible] (G : Type) (H : add_inf_group G) :
|
||||
AddInfGroup :=
|
||||
InfGroup.mk G H
|
||||
|
||||
definition AddInfGroup.struct [reducible] (G : AddInfGroup) : add_inf_group G :=
|
||||
InfGroup.struct G
|
||||
|
||||
attribute AddInfGroup.struct InfGroup.struct [instance] [priority 2000]
|
||||
|
||||
structure AbInfGroup :=
|
||||
(carrier : Type) (struct : ab_inf_group carrier)
|
||||
|
||||
attribute AbInfGroup.carrier [coercion]
|
||||
|
||||
definition AddAbInfGroup : Type := AbInfGroup
|
||||
|
||||
definition AddAbInfGroup.mk [constructor] [reducible] (G : Type) (H : add_ab_inf_group G) :
|
||||
AddAbInfGroup :=
|
||||
AbInfGroup.mk G H
|
||||
|
||||
definition AddAbInfGroup.struct [reducible] (G : AddAbInfGroup) : add_ab_inf_group G :=
|
||||
AbInfGroup.struct G
|
||||
|
||||
attribute AddAbInfGroup.struct AbInfGroup.struct [instance] [priority 2000]
|
||||
|
||||
definition InfGroup_of_AbInfGroup [coercion] [constructor] (G : AbInfGroup) : InfGroup :=
|
||||
InfGroup.mk G _
|
||||
|
||||
attribute algebra._trans_of_InfGroup_of_AbInfGroup_1 [constructor]
|
||||
attribute algebra._trans_of_InfGroup_of_AbInfGroup [unfold 1]
|
||||
|
||||
definition InfGroup_of_Group [constructor] (G : Group) : InfGroup :=
|
||||
InfGroup.mk G _
|
||||
|
||||
definition AddInfGroup_of_AddGroup [constructor] (G : AddGroup) : AddInfGroup :=
|
||||
AddInfGroup.mk G _
|
||||
|
||||
definition AbInfGroup_of_AbGroup [constructor] (G : AbGroup) : AbInfGroup :=
|
||||
AbInfGroup.mk G _
|
||||
|
||||
definition AddAbInfGroup_of_AddAbGroup [constructor] (G : AddAbGroup) : AddAbInfGroup :=
|
||||
AddAbInfGroup.mk G _
|
||||
|
||||
end algebra
|
||||
|
|
|
|||
|
|
@ -114,6 +114,9 @@ definition comm_monoid.to_add_comm_monoid {A : Type} [s : comm_monoid A] : add_c
|
|||
|
||||
structure group [class] (A : Type) extends monoid A, inf_group A
|
||||
|
||||
definition group_of_inf_group (A : Type) [s : inf_group A] [is_set A] : group A :=
|
||||
⦃group, s, is_set_carrier := _⦄
|
||||
|
||||
section group
|
||||
|
||||
variable [s : group A]
|
||||
|
|
@ -131,6 +134,9 @@ end group
|
|||
|
||||
structure ab_group [class] (A : Type) extends group A, comm_monoid A, ab_inf_group A
|
||||
|
||||
definition ab_group_of_ab_inf_group (A : Type) [s : ab_inf_group A] [is_set A] : ab_group A :=
|
||||
⦃ab_group, s, is_set_carrier := _⦄
|
||||
|
||||
/- additive group -/
|
||||
|
||||
definition add_group [class] : Type → Type := group
|
||||
|
|
@ -146,6 +152,10 @@ definition add_inf_group_of_add_group [reducible] [trans_instance] (A : Type)
|
|||
definition add_group.to_group {A : Type} [s : add_group A] : group A := s
|
||||
definition group.to_add_group {A : Type} [s : group A] : add_group A := s
|
||||
|
||||
definition add_group_of_add_inf_group (A : Type) [s : add_inf_group A] [is_set A] :
|
||||
add_group A :=
|
||||
⦃group, s, is_set_carrier := _⦄
|
||||
|
||||
section add_group
|
||||
|
||||
variables [s : add_group A]
|
||||
|
|
@ -178,6 +188,10 @@ definition add_ab_inf_group_of_add_ab_group [reducible] [trans_instance] (A : Ty
|
|||
definition add_ab_group.to_ab_group {A : Type} [s : add_ab_group A] : ab_group A := s
|
||||
definition ab_group.to_add_ab_group {A : Type} [s : ab_group A] : add_ab_group A := s
|
||||
|
||||
definition add_ab_group_of_add_ab_inf_group (A : Type) [s : add_ab_inf_group A] [is_set A] :
|
||||
add_ab_group A :=
|
||||
⦃ab_group, s, is_set_carrier := _⦄
|
||||
|
||||
definition group_of_add_group (A : Type) [G : add_group A] : group A :=
|
||||
⦃group,
|
||||
mul := has_add.add,
|
||||
|
|
|
|||
|
|
@ -404,6 +404,39 @@ namespace group
|
|||
mul_pt := mul_one,
|
||||
mul_left_inv_pt := mul.left_inv ⦄
|
||||
|
||||
-- infinity pgroups
|
||||
|
||||
structure inf_pgroup [class] (X : Type*) extends inf_semigroup X, has_inv X :=
|
||||
(pt_mul : Πa, mul pt a = a)
|
||||
(mul_pt : Πa, mul a pt = a)
|
||||
(mul_left_inv_pt : Πa, mul (inv a) a = pt)
|
||||
|
||||
definition inf_group_of_inf_pgroup [reducible] [instance] (X : Type*) [H : inf_pgroup X]
|
||||
: inf_group X :=
|
||||
⦃inf_group, H,
|
||||
one := pt,
|
||||
one_mul := inf_pgroup.pt_mul ,
|
||||
mul_one := inf_pgroup.mul_pt,
|
||||
mul_left_inv := inf_pgroup.mul_left_inv_pt⦄
|
||||
|
||||
definition inf_pgroup_of_inf_group (X : Type*) [H : inf_group X] (p : one = pt :> X) : inf_pgroup X :=
|
||||
begin
|
||||
cases X with X x, esimp at *, induction p,
|
||||
exact ⦃inf_pgroup, H,
|
||||
pt_mul := one_mul,
|
||||
mul_pt := mul_one,
|
||||
mul_left_inv_pt := mul.left_inv⦄
|
||||
end
|
||||
|
||||
definition inf_Group_of_inf_pgroup (G : Type*) [inf_pgroup G] : InfGroup :=
|
||||
InfGroup.mk G _
|
||||
|
||||
definition inf_pgroup_InfGroup [instance] (G : InfGroup) : inf_pgroup G :=
|
||||
⦃ inf_pgroup, InfGroup.struct G,
|
||||
pt_mul := one_mul,
|
||||
mul_pt := mul_one,
|
||||
mul_left_inv_pt := mul.left_inv ⦄
|
||||
|
||||
/- equality of groups and abelian groups -/
|
||||
|
||||
definition group.to_has_mul {A : Type} (H : group A) : has_mul A := _
|
||||
|
|
|
|||
|
|
@ -15,6 +15,17 @@ open nat eq pointed trunc is_trunc algebra group function equiv unit is_equiv na
|
|||
-- TODO: rename homotopy_group_functor_compose to homotopy_group_functor_pcompose
|
||||
namespace eq
|
||||
|
||||
definition inf_pgroup_loop [constructor] [instance] (A : Type*) : inf_pgroup (Ω A) :=
|
||||
inf_pgroup.mk concat con.assoc inverse idp_con con_idp con.left_inv
|
||||
|
||||
definition inf_group_loop [constructor] (A : Type*) : inf_group (Ω A) := _
|
||||
|
||||
definition ab_inf_group_loop [constructor] [instance] (A : Type*) : ab_inf_group (Ω (Ω A)) :=
|
||||
⦃ab_inf_group, inf_group_loop _, mul_comm := eckmann_hilton⦄
|
||||
|
||||
definition gloop [constructor] (A : Type*) : InfGroup :=
|
||||
InfGroup.mk (Ω A) (inf_group_loop A)
|
||||
|
||||
definition homotopy_group [reducible] [constructor] (n : ℕ) (A : Type*) : Set* :=
|
||||
ptrunc 0 (Ω[n] A)
|
||||
|
||||
|
|
@ -22,7 +33,7 @@ namespace eq
|
|||
|
||||
definition group_homotopy_group [instance] [constructor] [reducible] (n : ℕ) (A : Type*)
|
||||
: group (π[succ n] A) :=
|
||||
trunc_group concat inverse idp con.assoc idp_con con_idp con.left_inv
|
||||
trunc_group (Ω[succ n] A)
|
||||
|
||||
definition group_homotopy_group2 [instance] (k : ℕ) (A : Type*) :
|
||||
group (carrier (ptrunctype.to_pType (π[k + 1] A))) :=
|
||||
|
|
@ -30,7 +41,7 @@ namespace eq
|
|||
|
||||
definition ab_group_homotopy_group [constructor] [reducible] (n : ℕ) (A : Type*)
|
||||
: ab_group (π[succ (succ n)] A) :=
|
||||
trunc_ab_group concat inverse idp con.assoc idp_con con_idp con.left_inv eckmann_hilton
|
||||
trunc_ab_group (Ω[succ (succ n)] A)
|
||||
|
||||
local attribute ab_group_homotopy_group [instance]
|
||||
|
||||
|
|
|
|||
|
|
@ -6,99 +6,96 @@ Authors: Floris van Doorn
|
|||
truncating an ∞-group to a group
|
||||
-/
|
||||
|
||||
import hit.trunc algebra.group
|
||||
import hit.trunc algebra.bundled
|
||||
|
||||
open eq is_trunc trunc
|
||||
|
||||
namespace algebra
|
||||
|
||||
section
|
||||
parameters (n : trunc_index) {A : Type} (mul : A → A → A) (inv : A → A) (one : A)
|
||||
(mul_assoc : ∀a b c, mul (mul a b) c = mul a (mul b c))
|
||||
(one_mul : ∀a, mul one a = a) (mul_one : ∀a, mul a one = a)
|
||||
(mul_left_inv : ∀a, mul (inv a) a = one)
|
||||
parameters (n : trunc_index) {A : Type} [inf_group A]
|
||||
|
||||
local abbreviation G := trunc n A
|
||||
|
||||
include mul
|
||||
definition trunc_mul [unfold 9 10] (g h : G) : G :=
|
||||
begin
|
||||
induction g with p,
|
||||
induction h with q,
|
||||
exact tr (mul p q)
|
||||
exact tr (p * q)
|
||||
end
|
||||
|
||||
omit mul include inv
|
||||
definition trunc_inv [unfold 9] (g : G) : G :=
|
||||
begin
|
||||
induction g with p,
|
||||
exact tr (inv p)
|
||||
exact tr p⁻¹
|
||||
end
|
||||
|
||||
omit inv include one
|
||||
definition trunc_one [constructor] : G :=
|
||||
tr one
|
||||
tr 1
|
||||
|
||||
local notation 1 := trunc_one
|
||||
local postfix ⁻¹ := trunc_inv
|
||||
local infix * := trunc_mul
|
||||
|
||||
parameters {mul} {inv} {one}
|
||||
omit one include mul_assoc
|
||||
theorem trunc_mul_assoc (g₁ g₂ g₃ : G) : g₁ * g₂ * g₃ = g₁ * (g₂ * g₃) :=
|
||||
begin
|
||||
induction g₁ with p₁,
|
||||
induction g₂ with p₂,
|
||||
induction g₃ with p₃,
|
||||
exact ap tr !mul_assoc,
|
||||
exact ap tr !mul.assoc,
|
||||
end
|
||||
|
||||
omit mul_assoc include one_mul
|
||||
theorem trunc_one_mul (g : G) : 1 * g = g :=
|
||||
begin
|
||||
induction g with p,
|
||||
exact ap tr !one_mul
|
||||
end
|
||||
|
||||
omit one_mul include mul_one
|
||||
theorem trunc_mul_one (g : G) : g * 1 = g :=
|
||||
begin
|
||||
induction g with p,
|
||||
exact ap tr !mul_one
|
||||
end
|
||||
|
||||
omit mul_one include mul_left_inv
|
||||
theorem trunc_mul_left_inv (g : G) : g⁻¹ * g = 1 :=
|
||||
begin
|
||||
induction g with p,
|
||||
exact ap tr !mul_left_inv
|
||||
exact ap tr !mul.left_inv
|
||||
end
|
||||
|
||||
omit mul_left_inv
|
||||
theorem trunc_mul_comm (mul_comm : ∀a b, mul a b = mul b a) (g h : G)
|
||||
: g * h = h * g :=
|
||||
parameter (A)
|
||||
definition trunc_inf_group [constructor] [instance] : inf_group (trunc n A) :=
|
||||
⦃inf_group,
|
||||
mul := algebra.trunc_mul n,
|
||||
mul_assoc := algebra.trunc_mul_assoc n,
|
||||
one := algebra.trunc_one n,
|
||||
one_mul := algebra.trunc_one_mul n,
|
||||
mul_one := algebra.trunc_mul_one n,
|
||||
inv := algebra.trunc_inv n,
|
||||
mul_left_inv := algebra.trunc_mul_left_inv n⦄
|
||||
|
||||
definition trunc_group [constructor] : group (trunc 0 A) :=
|
||||
group_of_inf_group _
|
||||
|
||||
end
|
||||
|
||||
section
|
||||
variables (n : trunc_index) {A : Type} [ab_inf_group A]
|
||||
|
||||
theorem trunc_mul_comm (g h : trunc n A) : trunc_mul n g h = trunc_mul n h g :=
|
||||
begin
|
||||
induction g with p,
|
||||
induction h with q,
|
||||
exact ap tr !mul_comm
|
||||
exact ap tr !mul.comm
|
||||
end
|
||||
|
||||
parameters (mul) (inv) (one)
|
||||
variable (A)
|
||||
definition trunc_ab_inf_group [constructor] [instance] : ab_inf_group (trunc n A) :=
|
||||
⦃ab_inf_group, trunc_inf_group n A, mul_comm := algebra.trunc_mul_comm n⦄
|
||||
|
||||
definition trunc_group [constructor] : group (trunc 0 A) :=
|
||||
⦃group,
|
||||
mul := algebra.trunc_mul 0 mul,
|
||||
mul_assoc := algebra.trunc_mul_assoc 0 mul_assoc,
|
||||
one := algebra.trunc_one 0 one,
|
||||
one_mul := algebra.trunc_one_mul 0 one_mul,
|
||||
mul_one := algebra.trunc_mul_one 0 mul_one,
|
||||
inv := algebra.trunc_inv 0 inv,
|
||||
mul_left_inv := algebra.trunc_mul_left_inv 0 mul_left_inv,
|
||||
is_set_carrier := _⦄
|
||||
|
||||
definition trunc_ab_group [constructor] (mul_comm : ∀a b, mul a b = mul b a)
|
||||
: ab_group (trunc 0 A) :=
|
||||
⦃ab_group, trunc_group, mul_comm := algebra.trunc_mul_comm 0 mul_comm⦄
|
||||
definition trunc_ab_group [constructor] : ab_group (trunc 0 A) :=
|
||||
ab_group_of_ab_inf_group _
|
||||
|
||||
end
|
||||
|
||||
end algebra
|
||||
|
|
|
|||
Loading…
Reference in a new issue