Homotopy Type Theory abelian group > history (Rev #16, changes)

Showing changes from revision #15 to #16: Added | Removed | Changed

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 or 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)}\mathrm{isContr}(\mu (e,a)=a)$$ c_\lambda:\prod_{(a:G)} c_\lambda:\prod_{a:G} isContr(\mu(e,a)=a) \mu(e,a)=a
• A contractible right unit identity
  $$c_{\rho }:\prod _{(a:G)}\mathrm{isContr}(\mu (a,e)=a)$$ c_\rho:\prod_{(a:G)} c_\rho:\prod_{a:G} isContr(\mu(a,e)=a) \mu(a,e)=a
• A contractible associative identity
  $$c_{\alpha }:\prod _{(a:G)}\prod _{(b:G)}\prod _{(c:G)}\mathrm{isContr}(\mu (\mu (a,b),c)=\mu (a,\mu (b,c)))$$ c_\alpha:\prod_{(a:G)} c_\alpha:\prod_{a:G} \prod_{(b:G)} \prod_{b:G} \prod_{(c:G)} \prod_{c:G} isContr(\mu(\mu(a, \mu(\mu(a, b),c)=\mu(a,\mu(b,c))) b),c)=\mu(a,\mu(b,c))
• A contractible left inverse identity
  $$c_l:\prod _{(a:G)}\mathrm{isContr}(\mu (\iota (a),a)=e)$$ c_l:\prod_{(a:G)} c_l:\prod_{a:G} isContr(\mu(\iota(a), \mu(\iota(a), a)=e) a)=e
• A contractible right inverse identity
  $$c_r:\prod _{(a:G)}\mathrm{isContr}(\mu (a,\iota (a))=e)$$ c_r:\prod_{(a:G)} c_r:\prod_{a:G} isContr(\mu(a,\iota(a))=e) \mu(a,\iota(a))=e
• A contractible commutative identity
  $$c_{\kappa }:\prod _{(a:A)}\prod _{(b:A)}\mathrm{isContr}(\mu (a,b)=\mu (b,a))$$ c_\kappa:\prod_{(a:A)} c_\kappa:\prod_{a:A} \prod_{(b:A)} \prod_{b:A} isContr(\mu(a, \mu(a, b)=\mu(b, a)) a)
• A 0-truncator
  $${\tau }_0:\prod _{(a:\mathrm{<span><del\; class="diffmod">\; G</del><ins\; class="diffmod">\; A</ins></span>})}\prod _{(b:\mathrm{<span><del\; class="diffmod">\; G</del><ins\; class="diffmod">\; A</ins></span>})}\mathrm{isProp}\prod _{c:(a=b)}(\prod _{d:(a=b)}\mathrm{<span><del\; class="diffmod">\; a</del><ins\; class="diffmod">\; c</ins></span>}=\mathrm{<span><del\; class="diffmod">\; b</del><ins\; class="diffmod">\; d</ins></span>})$$ \tau_0: \prod_{(a:G)} \prod_{a:A} \prod_{(b:G)} \prod_{b:A} isProp(a=b) \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, Homotopy Type Theory – Univalent Foundations of Mathematics (2013)
• Marc Bezem, Ulrik Buchholtz, Pierre Cagne, Bjørn Ian Dundas, and Daniel R. Grayson, Symmetry book (2021)