Homotopy Type Theory ring > history (Rev #10, changes)

Showing changes from revision #9 to #10: Added | Removed | Changed

Definition

A ring is an abelian groupRRabelian group with an element1:R 1:R R and with a an element1: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 binary operation()():M×MM(-)\cdot(-):M \times M \to Mbilinear function ()():M×MM(-)\cdot(-):M \times M \to M as

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

Examples

See also

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