Homotopy Type Theory
group > history (Rev #6)
Definition
As a delooping of a pointed connected groupoid
A group is the type Aut ( G ) \mathrm{Aut}(G) of automorphisms in a pointed connected groupoid G G .
As a monoid
A group consists of
A type G G ,
A basepoint e : G e:G
A binary operation μ : G → G → G \mu : G \to G \to G
A unary operation ι : G → G \iota: G \to G
A contractible left unit identityc λ : ∏ ( a : G ) isContr ( μ ( e , a ) = a ) c_\lambda:\prod_{(a:G)} isContr(\mu(e,a)=a)
A contractible right unit identityc ρ : ∏ ( a : G ) isContr ( μ ( a , e ) = a ) c_\rho:\prod_{(a:G)} isContr(\mu(a,e)=a)
A contractible associative identityc α : ∏ ( a : G ) ∏ ( b : G ) ∏ ( c : G ) isContr ( μ ( μ ( a , b ) , c ) = μ ( a , μ ( b , c ) ) ) c_\alpha:\prod_{(a:G)} \prod_{(b:G)} \prod_{(c:G)} isContr(\mu(\mu(a, b),c)=\mu(a,\mu(b,c)))
A contractible left inverse identityc l : ∏ ( a : G ) isContr ( μ ( ι ( a ) , a ) = e ) c_l:\prod_{(a:G)} isContr(\mu(\iota(a), a)=e)
A contractible right inverse identityc r : ∏ ( a : G ) isContr ( μ ( a , ι ( a ) ) = e ) c_r:\prod_{(a:G)} isContr(\mu(a,\iota(a))=e)
A 0-truncatorτ 0 : ∏ ( a : G ) ∏ ( b : G ) isProp ( a = b ) \tau_0: \prod_{(a:G)} \prod_{(b:G)} isProp(a=b)
Examples
Every contractible magma ( M , μ ) (M, \mu) with a function f : M → M f:M \to M is a group.
The integers are a group.
Given a set A A , the type of automorphisms Aut ( A ) Aut(A) has the structure of a group, with basepoint id A id_A , binary operation function composition, and unary operation inverse automorphism ( − ) − 1 {(-)}^{-1} .
See also
References
Revision on May 1, 2022 at 21:53:11 by
Anonymous? .
See the history of this page for a list of all contributions to it.