open import Algebra.Ring.Module open import Algebra.Group.Ab open import Algebra.Prelude open import Algebra.Group open import Algebra.Ring open import Cat.Diagram.Initial open import Data.Int import Data.Nat as Nat import Prim.Data.Nat as Nat module Algebra.Ring.Cat.Initial {β} where

# The initial ringπ

We have, in the introduction to rings, mentioned offhand that the ring ${\mathbb{Z}}$ is an initial object. This turns out to be a fairly nontrivial theorem to formalise, so we have decided to do so in this module. For starters, note that the ring ${\mathbb{Z}}$ is an object of the category of βrings in the zeroth universeβ, whereas we would like any category of $\kappa$-compact rings to have its own initial object. So, the first thing we must do is define a lifting of ${\mathbb{Z}}$ to larger universes:

Liftβ€ : Ring β Liftβ€ = from-make-ring mr where open make-ring mr : make-ring (Lift β Int) mr .ring-is-set = hlevel 2 mr .1R = lift 1 mr .0R = lift 0 mr .-_ (lift x) = lift (negate x) mr ._+_ (lift x) (lift y) = lift (x +β€ y) mr ._*_ (lift x) (lift y) = lift (x *β€ y)

With that set up out of the way, we can now proceed to the
*actual* theorem weβre interested in: For a ring
$R$,
there is a contractible space of homomorphisms
${\mathbb{Z}}\to R$.
The definition of this construction is *fairly* involved, as
algebra tends to be, so letβs see it in parts: The first thing we must
do is write a procedure to turn natural numbers into elements of
$R$.
Thereβs really only one choice^{1}, so here it is:

Int-is-initial : is-initial (Rings β) Liftβ€ Int-is-initial R = contr zβr Ξ» x β Homomorphism-path Ξ» { (lift i) β lemma x i } where module R = Ring-on (R .snd)

Note that we treat 1 with care: we could have this map 1 to
`1r + 0r`

, but this results in worse definitional behaviour
when actually using the embedding. This will result in a bit more work
right now, but is work worth doing.

e : Nat β β R β e zero = R.0r e (suc zero) = R.1r e (suc (suc x)) = R.1r R.+ e (suc x)

Zero gets sent to zero, and βadding oneβ gets sent to adding one. Is anyone surprised? I know Iβm not. Anyway, this operation is a semiring homomorphism from the natural numbers to $R$, i.e., it sends sums of naturals to sums in $R$, and products of naturals to products in $R$. Weβll need this later.

e-suc : β n β e (suc n) β‘ R.1r R.+ e n e-add : β m n β e (m Nat.+ n) β‘ e m R.+ e n e-mul : β m n β e (m Nat.* n) β‘ e m R.* e n

The last thing we need is a little lemma that will be used in showing
that our embedding
$e : {\mathbb{N}}{\hookrightarrow}R$
extends to a function
$f : {\mathbb{Z}}\to R$:
We want to define
$f$
by sending
$[a - b]$
to
$e(a) - e(b)$,
meaning that
$e$
must respect the path constructor used in the definition of integers,
i.e.Β we need
$e(m) - e(n) = e(1 + m) - e(1 + n)$.
This is annoying to show, but not *too* annoying:

e-tr : β m n β e m R.- e n β‘ e (suc m) R.- e (suc n) e-tr m n = sym $ (e (suc m) R.- e (suc n)) β‘β¨ apβ R._-_ (e-suc m) (e-suc n) β©β‘ (R.1r R.+ e m) R.- (R.1r R.+ e n) β‘β¨ apβ R._+_ refl (R.a.inv-comm β R.a.commutative) β R.+-associative β©β‘ R.1r R.+ e m R.+ (R.- R.1r) R.+ (R.- e n) β‘β¨ apβ R._+_ (R.pullr R.+-commutes β R.pulll refl) refl β©β‘ R.1r R.+ (R.- R.1r) R.+ e m R.+ (R.- e n) β‘β¨ apβ R._+_ (R.eliml R.+-invr) refl β©β‘ e m R.- e n β

We can now build the embedding ${\mathbb{Z}}{\hookrightarrow}R$. It remains to show that this is a ring homomorphismβ¦ which involves a mountain of annoying algebra, so I wonβt comment on it too much: it can be worked out on paper, following the ring laws.

Note that we special case `diff x 0`

here for better
definitional behaviour of the embedding.

β€βͺR : Int β β R β β€βͺR (diff x zero) = e x β€βͺR (diff x (suc y)) = e x R.- e (suc y) β€βͺR (Int.quot m zero i) = along i $ e m β‘β¨ R.intror R.+-invr β©β‘ e m R.+ (R.1r R.- R.1r) β‘β¨ R.+-associative β©β‘ (e m R.+ R.1r) R.- R.1r β‘β¨ ap (R._- R.1r) R.+-commutes β©β‘ (R.1r R.+ e m) R.- R.1r β‘Λβ¨ ap (R._- R.1r) (e-suc m) β©β‘Λ e (suc m) R.- R.1r β β€βͺR (Int.quot m (suc n) i) = e-tr m (suc n) i open is-ring-hom β€βͺR-diff : β m n β β€βͺR (diff m n) β‘ e m R.- e n β€βͺR-diff m zero = R.intror R.inv-unit β€βͺR-diff m (suc n) = refl zβr : Rings.Hom Liftβ€ R zβr .hom (lift x) = β€βͺR x

The last thing we must show is that this is the *unique* ring
homomorphism from the integers to
$R$.
This, again, is slightly indirect: We know for a fact that, if we have
some *other* homomorphism
$f : {\mathbb{Z}}\to R$,
then it must enjoy
$f(1) = 1$,
just as our chosen embedding does. Now, no matter how trivial this
coming observation may seem, do not brush it aside: The integer
$n$
is the sum of
$n$
copies of the number 1. This is actually precisely what we need to
establish the result! Thatβs because we have

$f(n) = f(1 + \cdots + 1) = f(1) + \cdots + f(1) = 1 + \cdots + 1\text{,}$

and that last expression is pretty exactly what our canonical map evaluates to on $n$. So weβre done!

lemma : β (f : Rings.Hom Liftβ€ R) i β zβr # lift i β‘ f # lift i lemma f = Int-elim-prop (Ξ» _ β hlevel 1) Ξ» a b β sym $ f # lift (diff a b) β‘β¨ ap (f #_) (ap lift (p a b)) β©β‘ f # lift (diff a 0 +β€ diff 0 b) β‘β¨ f .preserves .pres-+ (lift (diff a 0)) (lift (diff 0 b)) β©β‘ f # lift (diff a 0) R.+ f # lift (diff 0 b) β‘β¨ apβ R._+_ (q a) (Group-hom.pres-inv gh {x = lift (diff b 0)} β ap R.-_ (q b)) β©β‘ (e a) R.+ (R.- e b) β‘Λβ¨ β€βͺR-diff a b β©β‘Λ zβr # lift (diff a b) β where p : β a b β diff a b β‘ diff a 0 +β€ diff 0 b p a b = ap (Ξ» e β diff e b) (sym (Nat.+-zeror a)) gh : Group-hom (Ring-on.additive-group (Liftβ€ .snd) .snd) (Ring-on.additive-group (R .snd) .snd) _ gh = record { pres-β = f .preserves .pres-+ } q : β a β f # lift (diff a 0) β‘ e a q zero = Group-hom.pres-id gh q (suc n) = f # lift (diff (suc n) 0) β‘β¨ f .preserves .pres-+ (lift (diff 1 0)) (lift (diff n 0)) β©β‘ f # lift 1 R.+ f # lift (diff n 0) β‘β¨ apβ R._+_ (f .preserves .pres-id) (q n) β©β‘ R.1r R.+ (e n) β‘Λβ¨ e-suc n β©β‘Λ e (suc n) β

## Abelian groups as Z-modulesπ

A fun consequence of ${\mathbb{Z}}$ being the initial ring is that every abelian group admits a unique ${\mathbb{Z}}$-module structure. This is, if you ask me, rather amazing! The correspondence is as follows: Because of the delooping-endomorphism ring adjunction, we have a correspondence between β$R$-module structures on Gβ and βring homomorphisms $R \to {\mathrm{Endo}}(G)$β β and since the latter is contractible, so is the former!

β€-module-unique : β (G : AbGroup β) β is-contr (Module-on Liftβ€ G) β€-module-unique G = is-hlevelβ 0 (ActionβModule Liftβ€ G) (Int-is-initial _)

though the fact that thereβs only one choice is sorta the theorem we are trying to proveβ¦β©οΈ