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

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

Definition

A ring is an abelian group RR with a an term element1:R1:R , and abilinear function ()():R×RR(-)\cdot(-):R \times R \to 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 , and b α : ( R a)(1)=a b:R \alpha(a)(1) = a, α(a)α(b)=α(ab)\alpha(a) \circ \alpha(b) = \alpha(a \cdot b)

  • 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 M as

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

Examples

See also

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