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
}