open import Algebra.Group.Ab
open import Algebra.Prelude
open import Algebra.Group

module Algebra.Ring.Base where

RingsπŸ”—

The ring is one of the basic objects of study in algebra, which abstracts the best bits of the common algebraic structures: The integers Z\bb{Z}, the rationals Q\bb{Q}, the reals R\bb{R}, and the complex numbers C\bb{C} are all rings, as are the collections of polynomials with coefficients in any of those. Less familiar examples of rings include square matrices (with values in a ring) and the integral cohomology ring of a topological space: that these are so far from being β€œnumber-like” indicates the incredible generality of rings.

A ring is an abelian group RR, together with a distinguished point 1:R1 : R to be called the multiplicative unit, and a multiplication homomorphism β‹…:RβŠ—Rβ†’RΒ· : R \otimes R \to R, such that β‹…Β· has 11 as a left/right unit, and it is associative. That is: A ring is a monoid, but described β€œon an abelian group” rather than β€œon a set”

record Ring β„“ : Type (lsuc β„“) where
  no-eta-equality
  field
    group : AbGroup β„“
  field
    1R  : R
    *-hom : Ab.Hom (group βŠ— group) group

The fact that _*_ is defined as a map out of the tensor product abelian group means that it is a bilinear map β€” meaning that multiplication and addition satisfy a distributivity equality, which is familiar from our example of Z\bb{Z} before: x(y+z)=xy+xzx(y + z) = xy + xz. Since rings are not necessarily commutative, we note that the symmetric equation holds as well: (y+z)x=yz+xz(y+z)x = yz + xz.

  _*_ : R β†’ R β†’ R
  x * y = *-hom .fst (x :, y)

  field
    *-idl : βˆ€ {x} β†’ 1R * x ≑ x
    *-idr : βˆ€ {x} β†’ x * 1R ≑ x
    *-assoc : βˆ€ {x y z} β†’ (x * y) * z ≑ x * (y * z)

  *-distribl : βˆ€ {x y z} β†’ x * (y + z) ≑ (x * y) + (x * z)
  *-distribl {x} {y} {z} =
    x * (y + z)                       β‰‘βŸ¨βŸ©
    *-hom .fst (x :, (y + z))         β‰‘βŸ¨ ap (*-hom .fst) (sym t-fixl) βŸ©β‰‘
    *-hom .fst ((x :, y) :+ (x :, z)) β‰‘βŸ¨ *-hom .snd .Group-hom.pres-⋆ _ _ βŸ©β‰‘
    (x * y) + (x * z)                 ∎

  *-distribr : βˆ€ {x y z} β†’ (y + z) * x ≑ (y * x) + (z * x)
  *-distribr {x} {y} {z} =
    (y + z) * x                       β‰‘βŸ¨βŸ©
    *-hom .fst ((y + z) :, x)         β‰‘βŸ¨ ap (*-hom .fst) (sym t-fixr) βŸ©β‰‘
    *-hom .fst ((y :, x) :+ (z :, x)) β‰‘βŸ¨ *-hom .snd .Group-hom.pres-⋆ _ _ βŸ©β‰‘
    (y * x) + (z * x)                 ∎

The elementary descriptionπŸ”—

We give a more elementary description of rings, which is suitable for constructing values of the record type Ring above. This re-expresses the data included in the definition of a ring with the least amount of redundancy possible, in the most direct terms possible: A ring is a set, equipped with two binary operations βˆ—* and ++, such that βˆ—* distributes over ++ on either side; ++ is an abelian group; and βˆ—* is a monoid.

record make-ring {β„“} (R : Type β„“) : Type β„“ where
  no-eta-equality
  field
    ring-is-set : is-set R

    -- R is an abelian group:
    0R      : R
    _+_     : R β†’ R β†’ R
    -_      : R β†’ R
    +-idl   : βˆ€ {x} β†’ 0R + x ≑ x
    +-invr  : βˆ€ {x} β†’ x + (- x) ≑ 0R
    +-assoc : βˆ€ {x y z} β†’ (x + y) + z ≑ x + (y + z)
    +-comm  : βˆ€ {x y} β†’ x + y ≑ y + x

    -- R is a monoid:
    1R      : R
    _*_     : R β†’ R β†’ R
    *-idl   : βˆ€ {x} β†’ 1R * x ≑ x
    *-idr   : βˆ€ {x} β†’ x * 1R ≑ x
    *-assoc : βˆ€ {x y z} β†’ (x * y) * z ≑ x * (y * z)

    -- Multiplication is bilinear:
    *-distribl : βˆ€ {x y z} β†’ x * (y + z) ≑ (x * y) + (x * z)
    *-distribr : βˆ€ {x y z} β†’ (y + z) * x ≑ (y * x) + (z * x)

This data is missing (by design, actually!) one condition which we would expect: 0β‰ 10 \ne 1. We exploit this to give our first example of a ring, the zero ring, which has carrier set the unit β€” the type with one object.

Despite the name, the zero ring is not the zero object in the category of rings: it is the terminal object. In the category of rings, the initial object is the ring Z\bb{Z}, which is very far (infinitely far!) from having a single element. It’s called the β€œzero ring” because it has one element xx, which must be the additive identity, hence we call it 00. But it’s also the multiplicative identity, so we might also call the ring {βˆ—}\{*\} the One Ring, which would be objectively cooler.

Zero-ring : Ring lzero
Zero-ring = from-make-ring {R = ⊀} $ record
  { ring-is-set = Ξ» _ _ _ _ _ _ β†’ tt
  ; 0R         = tt
  ; _+_        = Ξ» _ _ β†’ tt
  ; -_         = Ξ» _ β†’ tt
  ; +-idl      = Ξ» _ β†’ tt
  ; +-invr     = Ξ» _ β†’ tt
  ; +-assoc    = Ξ» _ β†’ tt
  ; +-comm     = Ξ» _ β†’ tt
  ; 1R         = tt
  ; _*_        = Ξ» _ _ β†’ tt
  ; *-idl      = Ξ» _ β†’ tt
  ; *-idr      = Ξ» _ β†’ tt
  ; *-assoc    = Ξ» _ β†’ tt
  ; *-distribl = Ξ» _ β†’ tt
  ; *-distribr = Ξ» _ β†’ tt
  }

Ring homomorphismsπŸ”—

There is a natural notion of ring homomorphism, which we get by smashing together that of monoid homomorphism (for the multiplicative part) and of group homomorphism; Every map of rings has an underlying map of groups which preserves the addition operation, and it must also preserve the multiplication.

record Ring-hom {β„“} (R S : Ring β„“) : Type β„“ where
  no-eta-equality
  private
    module R = Ring R
    module S = Ring S

  field
    map : R.R β†’ S.R
    pres-* : βˆ€ x y β†’ map (x R.* y) ≑ map x S.* map y
    pres-+ : βˆ€ x y β†’ map (x R.+ y) ≑ map x S.+ map y
    pres-1 : map R.1R ≑ S.1R

  group-hom : Ab.Hom R.group S.group
  group-hom = map , record { pres-⋆ = pres-+ }

  open Group-hom (group-hom .snd) hiding (pres-⋆)
    renaming ( pres-id to pres-0 ; pres-inv to pres-neg ; pres-diff to pres-sub )
    public

open Ring-hom

It follows, by standard equational nonsense, that rings and ring homomorphisms form a precategory β€” for instance, we have f(g(1R))=f(1S)=1Tf(g(1_R)) = f(1_S) = 1_T.

Rings : βˆ€ β„“ β†’ Precategory (lsuc β„“) β„“