Homotopy Type Theory ring > history (Rev #11)


A ring is an abelian group RR with an element 1:R1:R and a abelian group homomorphism α:R(R×R)\alpha:R \to (R \times R) such that

  • α(1)=id R\alpha(1) = \mathrm{id}_R

  • for all a:Ra:R, α(a)(1)=a\alpha(a)(1) = a

  • for all a:Ra:R, b:Rb:R, and c:Rc:R, (α(a)α(b))(c)=α(a)(α(b)(c))(\alpha(a) \circ \alpha(b))(c) = \alpha(a)(\alpha(b)(c))

We define the bilinear function ()():M×MM(-)\cdot(-):M \times M \to M as

abα(a)(b)a \cdot b \coloneqq \alpha(a)(b)


See also

Revision on June 15, 2022 at 22:59:25 by Anonymous?. See the history of this page for a list of all contributions to it.