feat(hott/algebra): define bundled additive groups as multiplicative groups
This commit is contained in:
Floris van Doorn
parent
c884e7bbb9
commit
554abe88c2
7 changed files with 66 additions and 78 deletions
|
|
@ -33,45 +33,37 @@ structure CommMonoid :=
|
|||
attribute CommMonoid.carrier [coercion]
|
||||
attribute CommMonoid.struct [instance]
|
||||
|
||||
abbreviation signature := interval
|
||||
structure Group (i : signature) :=
|
||||
structure Group :=
|
||||
(carrier : Type) (struct : group carrier)
|
||||
|
||||
definition MulGroup : Type := Group interval.zero
|
||||
definition AddGroup : Type := Group interval.one
|
||||
attribute Group.carrier [coercion]
|
||||
|
||||
definition MulGroup.mk [constructor] [reducible] (G : Type) (H : group G) : MulGroup :=
|
||||
Group.mk _ G _
|
||||
definition AddGroup : Type := Group
|
||||
|
||||
definition AddGroup.mk [constructor] [reducible] (G : Type) (H : add_group G) : AddGroup :=
|
||||
Group.mk _ G add_group.to_group
|
||||
Group.mk G H
|
||||
|
||||
definition MulGroup.struct [reducible] (G : MulGroup) : group G := Group.struct G
|
||||
definition AddGroup.struct [reducible] (G : AddGroup) : add_group G :=
|
||||
@group.to_add_group _ (Group.struct G)
|
||||
Group.struct G
|
||||
|
||||
attribute MulGroup.struct AddGroup.struct [instance] [priority 2000]
|
||||
attribute Group.struct [instance] [priority 800]
|
||||
attribute AddGroup.struct Group.struct [instance] [priority 2000]
|
||||
|
||||
structure CommGroup (i : signature) :=
|
||||
structure CommGroup :=
|
||||
(carrier : Type) (struct : comm_group carrier)
|
||||
|
||||
definition MulCommGroup : Type := CommGroup interval.zero
|
||||
definition AddCommGroup : Type := CommGroup interval.one
|
||||
attribute CommGroup.carrier [coercion]
|
||||
|
||||
definition MulCommGroup.mk [constructor] [reducible] (G : Type) (H : comm_group G) : MulCommGroup :=
|
||||
CommGroup.mk _ G _
|
||||
definition AddCommGroup : Type := CommGroup
|
||||
|
||||
definition AddCommGroup.mk [constructor] [reducible] (G : Type) (H : add_comm_group G) :
|
||||
AddCommGroup :=
|
||||
CommGroup.mk _ G add_comm_group.to_comm_group
|
||||
CommGroup.mk G H
|
||||
|
||||
definition MulCommGroup.struct [reducible] (G : MulCommGroup) : comm_group G := CommGroup.struct G
|
||||
definition AddCommGroup.struct [reducible] (G : AddCommGroup) : add_comm_group G :=
|
||||
@comm_group.to_add_comm_group _ (CommGroup.struct G)
|
||||
CommGroup.struct G
|
||||
|
||||
attribute AddCommGroup.struct CommGroup.struct [instance] [priority 2000]
|
||||
|
||||
attribute MulCommGroup.struct AddCommGroup.struct [instance] [priority 2000]
|
||||
attribute CommGroup.struct [instance] [priority 800]
|
||||
|
||||
-- structure AddSemigroup :=
|
||||
-- (carrier : Type) (struct : add_semigroup carrier)
|
||||
|
|
|
|||
|
|
@ -79,7 +79,7 @@ namespace category
|
|||
definition Groupoid.eta [unfold 1] (C : Groupoid) : Groupoid.mk C C = C :=
|
||||
Groupoid.rec (λob c, idp) C
|
||||
|
||||
definition Groupoid_of_Group [constructor] {i : signature} (G : Group i) : Groupoid :=
|
||||
definition Groupoid_of_Group [constructor] (G : Group) : Groupoid :=
|
||||
Groupoid.mk unit (groupoid_of_group G)
|
||||
|
||||
end category
|
||||
|
|
|
|||
|
|
@ -15,21 +15,20 @@ open eq algebra pointed function is_trunc pi category equiv is_equiv
|
|||
set_option class.force_new true
|
||||
|
||||
namespace group
|
||||
definition pointed_Group [instance] [constructor] {i : signature} (G : Group i) : pointed G :=
|
||||
definition pointed_Group [instance] [constructor] (G : Group) : pointed G :=
|
||||
pointed.mk 1
|
||||
definition pType_of_Group [constructor] [reducible] {i : signature} (G : Group i) : Type* :=
|
||||
definition pType_of_Group [constructor] [reducible] (G : Group) : Type* :=
|
||||
pointed.MK G 1
|
||||
definition Set_of_Group [constructor] {i : signature} (G : Group i) : Set := trunctype.mk G _
|
||||
definition Set_of_Group [constructor] (G : Group) : Set := trunctype.mk G _
|
||||
|
||||
definition Group_of_CommGroup [coercion] [constructor] {i : signature} (G : CommGroup i) :
|
||||
Group i :=
|
||||
Group.mk i G _
|
||||
definition Group_of_CommGroup [coercion] [constructor] (G : CommGroup) : Group :=
|
||||
Group.mk G _
|
||||
|
||||
definition comm_group_Group_of_CommGroup [instance] [constructor] [priority 900]
|
||||
{i : signature} (G : CommGroup i) : comm_group (Group_of_CommGroup G) :=
|
||||
(G : CommGroup) : comm_group (Group_of_CommGroup G) :=
|
||||
begin esimp, exact _ end
|
||||
|
||||
definition group_pType_of_Group [instance] [priority 900] {i : signature} (G : Group i) :
|
||||
definition group_pType_of_Group [instance] [priority 900] (G : Group) :
|
||||
group (pType_of_Group G) :=
|
||||
Group.struct G
|
||||
|
||||
|
|
@ -100,19 +99,18 @@ namespace group
|
|||
|
||||
end additive
|
||||
|
||||
structure homomorphism {i j : signature} (G₁ : Group i) (G₂ : Group j) : Type :=
|
||||
structure homomorphism (G₁ G₂ : Group) : Type :=
|
||||
(φ : G₁ → G₂)
|
||||
(p : is_homomorphism φ)
|
||||
|
||||
infix ` →g `:55 := homomorphism
|
||||
|
||||
definition group_fun [unfold 5] [coercion] := @homomorphism.φ
|
||||
definition homomorphism.struct [instance] [priority 900] {i j : signature}
|
||||
{G₁ : Group i} {G₂ : Group j} (φ : G₁ →g G₂)
|
||||
definition group_fun [unfold 3] [coercion] := @homomorphism.φ
|
||||
definition homomorphism.struct [instance] [priority 900] {G₁ : Group} {G₂ : Group} (φ : G₁ →g G₂)
|
||||
: is_homomorphism φ :=
|
||||
homomorphism.p φ
|
||||
|
||||
definition homomorphism.mulstruct [instance] [priority 2000] {G₁ G₂ : MulGroup } (φ : G₁ →g G₂)
|
||||
definition homomorphism.mulstruct [instance] [priority 2000] {G₁ G₂ : Group } (φ : G₁ →g G₂)
|
||||
: is_homomorphism φ :=
|
||||
homomorphism.p φ
|
||||
|
||||
|
|
@ -120,8 +118,7 @@ namespace group
|
|||
: is_add_homomorphism φ :=
|
||||
homomorphism.p φ
|
||||
|
||||
variables {i j k l : signature} {G : Group i} {G₁ : Group j} {G₂ : Group k} {G₃ : Group l}
|
||||
{g h : G₁} {ψ : G₂ →g G₃} {φ₁ φ₂ : G₁ →g G₂} (φ : G₁ →g G₂)
|
||||
variables {G G₁ G₂ G₃ : Group} {g h : G₁} {ψ : G₂ →g G₃} {φ₁ φ₂ : G₁ →g G₂} (φ : G₁ →g G₂)
|
||||
|
||||
definition to_respect_mul /- φ -/ (g h : G₁) : φ (g * h) = φ g * φ h :=
|
||||
respect_mul φ g h
|
||||
|
|
@ -173,7 +170,7 @@ namespace group
|
|||
end additive
|
||||
|
||||
section add_mul
|
||||
variables {H₁ : AddGroup} {H₂ : Group i} (χ : H₁ →g H₂)
|
||||
variables {H₁ : AddGroup} {H₂ : Group} (χ : H₁ →g H₂)
|
||||
definition to_respect_add_mul /- χ -/ (g h : H₁) : χ (g + h) = χ g * χ h :=
|
||||
to_respect_mul χ g h
|
||||
|
||||
|
|
@ -186,7 +183,7 @@ namespace group
|
|||
end add_mul
|
||||
|
||||
section mul_add
|
||||
variables {H₁ : Group i} {H₂ : AddGroup} (χ : H₁ →g H₂)
|
||||
variables {H₁ : Group} {H₂ : AddGroup} (χ : H₁ →g H₂)
|
||||
definition to_respect_mul_add /- χ -/ (g h : H₁) : χ (g * h) = χ g + χ h :=
|
||||
to_respect_mul χ g h
|
||||
|
||||
|
|
@ -211,7 +208,7 @@ namespace group
|
|||
infixr ` ∘g `:75 := homomorphism_compose
|
||||
notation 1 := homomorphism_id _
|
||||
|
||||
structure isomorphism {i j : signature} (A : Group i) (B : Group j) :=
|
||||
structure isomorphism (A B : Group) :=
|
||||
(to_hom : A →g B)
|
||||
(is_equiv_to_hom : is_equiv to_hom)
|
||||
|
||||
|
|
@ -230,10 +227,10 @@ namespace group
|
|||
(p : Πg₁ g₂, φ (g₁ * g₂) = φ g₁ * φ g₂) : G₁ ≃g G₂ :=
|
||||
isomorphism.mk (homomorphism.mk φ p) !to_is_equiv
|
||||
|
||||
definition eq_of_isomorphism {G₁ G₂ : Group i} (φ : G₁ ≃g G₂) : G₁ = G₂ :=
|
||||
definition eq_of_isomorphism {G₁ G₂ : Group} (φ : G₁ ≃g G₂) : G₁ = G₂ :=
|
||||
Group_eq (equiv_of_isomorphism φ) (respect_mul φ)
|
||||
|
||||
definition isomorphism_of_eq {G₁ G₂ : Group i} (φ : G₁ = G₂) : G₁ ≃g G₂ :=
|
||||
definition isomorphism_of_eq {G₁ G₂ : Group} (φ : G₁ = G₂) : G₁ ≃g G₂ :=
|
||||
isomorphism_of_equiv (equiv_of_eq (ap Group.carrier φ))
|
||||
begin intros, induction φ, reflexivity end
|
||||
|
||||
|
|
@ -256,11 +253,11 @@ namespace group
|
|||
isomorphism.mk (ψ ∘g φ) !is_equiv_compose
|
||||
|
||||
definition isomorphism.eq_trans [trans] [constructor]
|
||||
{G₁ G₂ : Group i} {G₃ : Group j} (φ : G₁ = G₂) (ψ : G₂ ≃g G₃) : G₁ ≃g G₃ :=
|
||||
{G₁ G₂ : Group} {G₃ : Group} (φ : G₁ = G₂) (ψ : G₂ ≃g G₃) : G₁ ≃g G₃ :=
|
||||
proof isomorphism.trans (isomorphism_of_eq φ) ψ qed
|
||||
|
||||
definition isomorphism.trans_eq [trans] [constructor]
|
||||
{G₁ : Group i} {G₂ G₃ : Group j} (φ : G₁ ≃g G₂) (ψ : G₂ = G₃) : G₁ ≃g G₃ :=
|
||||
{G₁ : Group} {G₂ G₃ : Group} (φ : G₁ ≃g G₂) (ψ : G₂ = G₃) : G₁ ≃g G₃ :=
|
||||
isomorphism.trans φ (isomorphism_of_eq ψ)
|
||||
|
||||
postfix `⁻¹ᵍ`:(max + 1) := isomorphism.symm
|
||||
|
|
@ -280,10 +277,10 @@ namespace group
|
|||
|
||||
/- category of groups -/
|
||||
|
||||
definition precategory_group [constructor] (i : signature) : precategory (Group i) :=
|
||||
definition precategory_group [constructor] : precategory Group :=
|
||||
precategory.mk homomorphism
|
||||
(@homomorphism_compose _ _ _)
|
||||
(@homomorphism_id _)
|
||||
@homomorphism_compose
|
||||
@homomorphism_id
|
||||
(λG₁ G₂ G₃ G₄ φ₃ φ₂ φ₁, homomorphism_eq (λg, idp))
|
||||
(λG₁ G₂ φ, homomorphism_eq (λg, idp))
|
||||
(λG₁ G₂ φ, homomorphism_eq (λg, idp))
|
||||
|
|
@ -349,7 +346,7 @@ namespace group
|
|||
{ intros, reflexivity}
|
||||
end
|
||||
|
||||
definition trivial_group_of_is_contr' (G : MulGroup) [H : is_contr G] : G = G0 :=
|
||||
definition trivial_group_of_is_contr' (G : Group) [H : is_contr G] : G = G0 :=
|
||||
eq_of_isomorphism (trivial_group_of_is_contr G)
|
||||
variable {G}
|
||||
|
||||
|
|
|
|||
|
|
@ -36,13 +36,13 @@ namespace eq
|
|||
|
||||
local attribute comm_group_homotopy_group [instance]
|
||||
|
||||
definition ghomotopy_group [constructor] (n : ℕ) (A : Type*) : MulGroup :=
|
||||
MulGroup.mk (π[succ n] A) _
|
||||
definition ghomotopy_group [constructor] (n : ℕ) (A : Type*) : Group :=
|
||||
Group.mk (π[succ n] A) _
|
||||
|
||||
definition cghomotopy_group [constructor] (n : ℕ) (A : Type*) : MulCommGroup :=
|
||||
MulCommGroup.mk (π[succ (succ n)] A) _
|
||||
definition cghomotopy_group [constructor] (n : ℕ) (A : Type*) : CommGroup :=
|
||||
CommGroup.mk (π[succ (succ n)] A) _
|
||||
|
||||
definition fundamental_group [constructor] (A : Type*) : MulGroup :=
|
||||
definition fundamental_group [constructor] (A : Type*) : Group :=
|
||||
ghomotopy_group zero A
|
||||
|
||||
notation `πg[`:95 n:0 ` +1]`:0 := ghomotopy_group n
|
||||
|
|
@ -249,7 +249,6 @@ namespace eq
|
|||
-- loop_space_succ_eq_in_concat, - + tr_compose],
|
||||
-- end
|
||||
|
||||
local attribute MulGroup MulCommGroup [reducible]
|
||||
definition is_homomorphism_inverse (A : Type*) (n : ℕ)
|
||||
: is_homomorphism (λp, p⁻¹ : (πag[n+2] A) → (πag[n+2] A)) :=
|
||||
begin
|
||||
|
|
|
|||
|
|
@ -15,8 +15,8 @@ namespace algebra
|
|||
definition trivial_group [constructor] : group unit :=
|
||||
group.mk (λx y, star) _ (λx y z, idp) star (unit.rec idp) (unit.rec idp) (λx, star) (λx, idp)
|
||||
|
||||
definition Trivial_group [constructor] : MulGroup :=
|
||||
MulGroup.mk _ trivial_group
|
||||
definition Trivial_group [constructor] : Group :=
|
||||
Group.mk _ trivial_group
|
||||
|
||||
abbreviation G0 := Trivial_group
|
||||
|
||||
|
|
@ -65,15 +65,15 @@ namespace algebra
|
|||
apply pathover_idp_of_eq, exact group_eq (resp_mul)
|
||||
end
|
||||
|
||||
definition Group_eq_of_eq {i : signature} {G H : Group i} (p : carrier G = carrier H)
|
||||
definition Group_eq_of_eq {G H : Group} (p : carrier G = carrier H)
|
||||
(resp_mul : Π(g h : G), cast p (g * h) = cast p g * cast p h) : G = H :=
|
||||
begin
|
||||
cases G with Gc G, cases H with Hc H,
|
||||
apply (apd011 (Group.mk i) p),
|
||||
apply (apd011 Group.mk p),
|
||||
exact group_pathover resp_mul
|
||||
end
|
||||
|
||||
definition Group_eq {i : signature} {G H : Group i} (f : carrier G ≃ carrier H)
|
||||
definition Group_eq {G H : Group} (f : carrier G ≃ carrier H)
|
||||
(resp_mul : Π(g h : G), f (g * h) = f g * f h) : G = H :=
|
||||
Group_eq_of_eq (ua f) (λg h, !cast_ua ⬝ resp_mul g h ⬝ ap011 mul !cast_ua⁻¹ !cast_ua⁻¹)
|
||||
|
||||
|
|
|
|||
|
|
@ -14,10 +14,10 @@ open algebra pointed nat eq category group algebra is_trunc iso pointed unit tru
|
|||
namespace EM
|
||||
open groupoid_quotient
|
||||
|
||||
variables {i : signature} {G : Group i}
|
||||
definition EM1 {i : signature} (G : Group i) : Type :=
|
||||
variables {G : Group}
|
||||
definition EM1 (G : Group) : Type :=
|
||||
groupoid_quotient (Groupoid_of_Group G)
|
||||
definition pEM1 [constructor] {i : signature} (G : Group i) : Type* :=
|
||||
definition pEM1 [constructor] (G : Group) : Type* :=
|
||||
pointed.MK (EM1 G) (elt star)
|
||||
|
||||
definition base : EM1 G := elt star
|
||||
|
|
@ -95,15 +95,15 @@ namespace EM
|
|||
end EM
|
||||
|
||||
attribute EM.base [constructor]
|
||||
attribute EM.rec EM.elim [unfold 8] [recursor 8]
|
||||
attribute EM.rec_on EM.elim_on [unfold 5]
|
||||
attribute EM.set_rec EM.set_elim [unfold 7]
|
||||
attribute EM.prop_rec EM.prop_elim EM.elim_set [unfold 6]
|
||||
attribute EM.rec EM.elim [unfold 7] [recursor 7]
|
||||
attribute EM.rec_on EM.elim_on [unfold 4]
|
||||
attribute EM.set_rec EM.set_elim [unfold 6]
|
||||
attribute EM.prop_rec EM.prop_elim EM.elim_set [unfold 5]
|
||||
|
||||
namespace EM
|
||||
open groupoid_quotient
|
||||
|
||||
variables {i : signature} (G : Group i)
|
||||
variables (G : Group)
|
||||
definition base_eq_base_equiv [constructor] : (base = base :> pEM1 G) ≃ G :=
|
||||
!elt_eq_elt_equiv
|
||||
|
||||
|
|
@ -142,7 +142,7 @@ end EM
|
|||
open hopf susp
|
||||
namespace EM
|
||||
-- The K(G,n+1):
|
||||
variables {i : signature} {G : CommGroup i} (n : ℕ)
|
||||
variables {G : CommGroup} (n : ℕ)
|
||||
|
||||
definition EM1_mul [unfold 2 3] (x x' : EM1 G) : EM1 G :=
|
||||
begin
|
||||
|
|
@ -211,7 +211,7 @@ namespace EM
|
|||
end
|
||||
|
||||
/- K(G, n) -/
|
||||
definition EM {i : signature} (G : CommGroup i) : ℕ → Type*
|
||||
definition EM (G : CommGroup) : ℕ → Type*
|
||||
| 0 := pType_of_Group G
|
||||
| (k+1) := EMadd1 G k
|
||||
|
||||
|
|
@ -248,7 +248,7 @@ namespace EM
|
|||
end
|
||||
|
||||
/- Uniqueness of K(G, 1) -/
|
||||
variable {H : Group i}
|
||||
variable {H : Group}
|
||||
definition pEM1_pmap [constructor] {X : Type*} (e : Ω X ≃ H)
|
||||
(r : Πp q, e (p ⬝ q) = e p * e q) [is_conn 0 X] [is_trunc 1 X] : pEM1 H →* X :=
|
||||
begin
|
||||
|
|
@ -270,7 +270,7 @@ namespace EM
|
|||
end
|
||||
|
||||
open trunc_index
|
||||
definition pEM1_pequiv'.{u} {i : signature} {G : Group.{u} i} {X : pType.{u}} (e : Ω X ≃ G)
|
||||
definition pEM1_pequiv'.{u} {G : Group.{u}} {X : pType.{u}} (e : Ω X ≃ G)
|
||||
(r : Πp q, e (p ⬝ q) = e p * e q) [is_conn 0 X] [is_trunc 1 X] : pEM1 G ≃* X :=
|
||||
begin
|
||||
apply pequiv_of_pmap (pEM1_pmap e r),
|
||||
|
|
@ -287,7 +287,7 @@ namespace EM
|
|||
do 2 exact trivial_homotopy_group_of_is_trunc _ (succ_lt_succ !zero_lt_succ)}}
|
||||
end
|
||||
|
||||
definition pEM1_pequiv.{u} {i : signature} {G : Group.{u} i} {X : pType.{u}} (e : π₁ X ≃g G)
|
||||
definition pEM1_pequiv.{u} {G : Group.{u}} {X : pType.{u}} (e : π₁ X ≃g G)
|
||||
[is_conn 0 X] [is_trunc 1 X] : pEM1 G ≃* X :=
|
||||
begin
|
||||
apply pEM1_pequiv' (!trunc_equiv⁻¹ᵉ ⬝e equiv_of_isomorphism e),
|
||||
|
|
@ -297,7 +297,7 @@ namespace EM
|
|||
definition pEM1_pequiv_type {X : Type*} [is_conn 0 X] [is_trunc 1 X] : pEM1 (π₁ X) ≃* X :=
|
||||
pEM1_pequiv !isomorphism.refl
|
||||
|
||||
definition EM_pequiv_1.{u} {i : signature} {G : CommGroup.{u} i} {X : pType.{u}} (e : π₁ X ≃g G)
|
||||
definition EM_pequiv_1.{u} {G : CommGroup.{u}} {X : pType.{u}} (e : π₁ X ≃g G)
|
||||
[is_conn 0 X] [is_trunc 1 X] : EM G 1 ≃* X :=
|
||||
begin
|
||||
refine _ ⬝e* pEM1_pequiv e,
|
||||
|
|
@ -309,7 +309,7 @@ namespace EM
|
|||
definition EMadd1_pequiv_pEM1 : EMadd1 G 0 ≃* pEM1 G :=
|
||||
begin apply ptrunc_pequiv, apply is_trunc_pEM1 end
|
||||
|
||||
definition EM1add1_pequiv_0.{u} {i : signature} {G : CommGroup.{u} i} {X : pType.{u}}
|
||||
definition EM1add1_pequiv_0.{u} {G : CommGroup.{u}} {X : pType.{u}}
|
||||
(e : π₁ X ≃g G) [is_conn 0 X] [is_trunc 1 X] : EMadd1 G 0 ≃* X :=
|
||||
EMadd1_pequiv_pEM1 G ⬝e* pEM1_pequiv e
|
||||
|
||||
|
|
|
|||
|
|
@ -723,12 +723,12 @@ namespace chain_complex
|
|||
| (fin.mk 2 H) := proof comm_group_homotopy_group n (pfiber f) qed
|
||||
| (fin.mk (k+3) H) := begin exfalso, apply lt_le_antisymm H, apply le_add_left end
|
||||
|
||||
definition Group_LES_of_homotopy_groups (x : +3ℕ) : MulGroup.{u} :=
|
||||
MulGroup.mk (LES_of_homotopy_groups (nat.succ (pr1 x), pr2 x))
|
||||
definition Group_LES_of_homotopy_groups (x : +3ℕ) : Group.{u} :=
|
||||
Group.mk (LES_of_homotopy_groups (nat.succ (pr1 x), pr2 x))
|
||||
(group_LES_of_homotopy_groups (pr1 x) (pr2 x))
|
||||
|
||||
definition CommGroup_LES_of_homotopy_groups (n : +3ℕ) : MulCommGroup.{u} :=
|
||||
MulCommGroup.mk (LES_of_homotopy_groups (pr1 n + 2, pr2 n))
|
||||
definition CommGroup_LES_of_homotopy_groups (n : +3ℕ) : CommGroup.{u} :=
|
||||
CommGroup.mk (LES_of_homotopy_groups (pr1 n + 2, pr2 n))
|
||||
(comm_group_LES_of_homotopy_groups (pr1 n) (pr2 n))
|
||||
|
||||
definition homomorphism_LES_of_homotopy_groups_fun : Π(k : +3ℕ),
|
||||
|
|
|
|||
Loading…
Reference in a new issue