Homotopy Type Theory abelian group > history (Rev #7)

Definition

As a group

An abelian group or $\mathbb{Z}$-module consists of

• A type $G$,
• A basepoint $e:G$
• A binary operation $\mu : G \to G \to G$
• A unary operation $\iota: G \to G$
• A contractible left unit identity
  $$c_\lambda:\prod_{(a:G)} isContr(\mu(e,a)=a)$$
• A contractible right unit identity
  $$c_\rho:\prod_{(a:G)} isContr(\mu(a,e)=a)$$
• A contractible associative identity
  $$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 identity
  $$c_l:\prod_{(a:G)} isContr(\mu(\iota(a), a)=e)$$
• A contractible right inverse identity
  $$c_r:\prod_{(a:G)} isContr(\mu(a,\iota(a))=e)$$
• A contractible commutative identity
  $$c_\kappa:\prod_{(a:A)} \prod_{(b:A)} isContr(\mu(a, b)=\mu(b, a))$$
• A 0-truncator
  $$\tau_0: \prod_{(a:G)} \prod_{(b:G)} isProp(a=b)$$

As a module

An abelian group or $\mathbb{Z}$-module is a set $S$ with a term $0:S$ and a binary function $(-)+(-):S \times S \to S$, and a left multiplicative $\mathbb{Z}$-action $(-)\cdot_l(-):\mathbb{Z} \times S \to S$, such that

We define the functions $-:S \to S$ and $(-)\cdot_r(-):S \times \mathbb{Z} \to S$ to be

and $S$ is an abelian group and a $\mathbb{Z}$-bimodule

Examples

• Every contractible magma $(M, \mu)$ with a function $f:M \to M$ is an abelian group.

• The integers are an abelian group.

See also

• Higher algebra
• commutative monoid
• group
• Z-algebra
• ordered abelian group
• abelian group homomorphism