[[!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__ is the type $\mathrm{Aut}(\mathrm{Aut}(G))$ of automorphisms of automorphisms in $G$. ### As a group ### An __abelian group__ 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 left unit identity $$c_\lambda:\prod_{a:G} \mu(e,a)=a$$ * A right unit identity $$c_\rho:\prod_{a:G} \mu(a,e)=a$$ * A associative identity $$c_\alpha:\prod_{a:G} \prod_{b:G} \prod_{c:G} \mu(\mu(a, b),c)=\mu(a,\mu(b,c))$$ * A left inverse identity $$c_l:\prod_{a:G} \mu(\iota(a), a)=e$$ * A right inverse identity $$c_r:\prod_{a:G} \mu(a,\iota(a))=e$$ * A commutative identity $$c_\kappa:\prod_{a:A} \prod_{b:A} \mu(a, b)=\mu(b, a)$$ * A 0-truncator $$\tau_0: \prod_{a:A} \prod_{b:A} \prod_{c:(a = b)} \prod_{d:(a = b)} c = d$$ ## Examples ## * The [[integers]] are an abelian group. ## See also ## * [[commutative monoid]] * [[group]] * [[divisible group]] * [[rationalization of an abelian group]] * [[ordered abelian group]] * [[abelian group homomorphism]] * [[ring]] ## 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) category: not redirected to nlab yet