open import Algebra.Semigroup open import Algebra.Group.Ab open import Algebra.Prelude open import Algebra.Monoid open import Algebra.Group module Algebra.Ring 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
$\bb{Z}$,
the rationals
$\bb{Q}$,
the reals
$\bb{R}$,
and the complex numbers
$\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
$R$
(which we call the **additive group** of
$R$),
together with the data of a monoid on
$R$
(the **multiplicative monoid**), where the multiplication
of the monoid *distributes over* the addition. Weβll see why this
compatibility condition is required afterwards. Check out what it means
for a triple
$(1, *, +)$
to be a ring structure on a type:

record is-ring {β} {R : Type β} (1R : R) (_*_ _+_ : R β R β R) : Type β where no-eta-equality field *-monoid : is-monoid 1R _*_ +-group : is-group _+_ +-commutes : β {x y} β x + y β‘ y + x *-distribl : β {x y z} β x * (y + z) β‘ (x * y) + (x * z) *-distribr : β {x y z} β (y + z) * x β‘ (y * x) + (z * x)

There is a natural notion of ring homomorphism, which we get by smashing together that of a 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. This encodes the view of a ring as an βabelian group with a monoid structureβ.

record is-ring-hom {β} (A B : Ring β) (f : A .fst β B .fst) : Type β where private module A = Ring-on (A .snd) module B = Ring-on (B .snd) field pres-id : f A.1R β‘ B.1R pres-+ : β x y β f (x A.+ y) β‘ f x B.+ f y pres-* : β x y β f (x A.* y) β‘ f x B.* f y

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

Rings : β β β Precategory (lsuc β) β

## In componentsπ

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 \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
$\bb{Z}$,
which is very far (infinitely far!) from having a single element. Itβs
called the βzero ringβ because it has one element
$x$,
which must be the additive identity, hence we call it
$0$.
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 }