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

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

Definition

A ring is an abelian groupunital $\mathbb{Z}$-algebraRR with a term(A,+,,0,,1 ) :R (A, 1:R +, -, 0, \cdot, 1) , with 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

  • an associative identity for\cdot

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

    m α: (a:G) (b:G) (c:G)(ab)c=a(bc)m_\alpha:\prod_{(a:G)} \prod_{(b:G)} \prod_{(c:G)} (a\cdot b)\cdot c = a\cdot (b\cdot c)
  • for all a:Ra:R and b:Rb:R, α(a)α(b)=α(ab)\alpha(a) \circ \alpha(b) = \alpha(a \cdot b)

Examples

See also

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