[[!redirects Z-module]] ## Definition ## ### As a twice-delooping of a pointed simply connected 2-groupoid ### A pointed simply connected 2-groupoid consists of * A type $G$ * A basepoint $e:G$ * A 1-connector $$\kappa_1:\prod_{f:G \to \mathbb{1}} \prod_{a:\mathbb{1}} \mathrm{isContr}(\left[\mathrm{fiber}(f, a)\right]_{1})$$ * A 2-truncator: $$\tau_2:\mathrm{isTwoGroupoid}(G)$$ An __abelian group__ or __$\mathbb{Z}$-module__ is the type $\mathrm{Aut}(\mathrm{Aut}(G))$ of automorphisms of automorphisms in $G$. ### 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 $$\prod_{a:S} \prod_{b:S} a + b = b + a$$ $$\prod_{a:S} \prod_{b:S} \prod_{c:S} a + (b + c) = (a + b) + c$$ $$\prod_{a:S} 1 \cdot_l a = a$$ $$\prod_{a:\mathbb{Z}} \prod_{b:\mathbb{Z}} \prod_{c:S} (a \cdot b) \cdot_l c = a \cdot_l (b \cdot_l c)$$ $$\prod_{a:S} 0 \cdot_l a = 0$$ $$\prod_{a:\mathbb{Z}} \prod_{b:S} \prod_{c:S} a \cdot_l (b + c) = a \cdot_l b + a \cdot_l c$$ $$\prod_{a:\mathbb{Z}} \prod_{b:\mathbb{Z}} \prod_{c:S} (a + b) \cdot_l c = a \cdot_l c + b \cdot_l c$$ We define the functions $-:S \to S$ and $(-)\cdot_r(-):S \times \mathbb{Z} \to S$ to be $$-a \coloneqq (-1) \cdot_l a$$ $$a \cdot_r b \coloneqq b \cdot_l a$$ and $S$ is an [[abelian group]] and a $\mathbb{Z}$-[[bimodule]] $$a = 1 \cdot_1 a = (1 + 0) \cdot_1 a = (1 \cdot_1 a) + (0 \cdot_1 a) = a + 0$$ $$a = 1 \cdot_1 a = (0 + 1) \cdot_1 a = (0 \cdot_1 a) + (1 \cdot_1 a) = 0 + a$$ $$0 = 0 \cdot_1 a = (1 + -1) \cdot_1 a = (1 \cdot_1 a) + (-1 \cdot_1 a) = a + -a$$ $$0 = 0 \cdot_1 a = (-1 + 1) \cdot_1 a = (-1 \cdot_1 a) + (1 \cdot_1 a) = -a + a$$ ## 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]] * [[divisible group]] * [[ordered abelian group]] * [[abelian group homomorphism]] ## References ## * Univalent Foundations Project, [[HoTT book|Homotopy Type Theory – Univalent Foundations of Mathematics]] (2013) * Marc Bezem, Ulrik Buchholtz, Pierre Cagne, Bjørn Ian Dundas, and Daniel R. Grayson, [Symmetry book](https://unimath.github.io/SymmetryBook/book.pdf) (2021)