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 Z{\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 Z{\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 Z{\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 RR, there is a contractible space of homomorphisms Zβ†’R{\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 RR. There’s really only one choice1, 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 RR, i.e., it sends sums of naturals to sums in RR, and products of naturals to products in RR. 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:Nβ†ͺRe : {\mathbb{N}}{\hookrightarrow}R extends to a function f:Zβ†’Rf : {\mathbb{Z}}\to R: We want to define ff by sending [aβˆ’b][a - b] to e(a)βˆ’e(b)e(a) - e(b), meaning that ee 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)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 Zβ†ͺR{\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 RR. This, again, is slightly indirect: We know for a fact that, if we have some other homomorphism f:Zβ†’Rf : {\mathbb{Z}}\to R, then it must enjoy f(1)=1f(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 nn is the sum of nn 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+β‹―+1)=f(1)+β‹―+f(1)=1+β‹―+1, 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 nn. 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 Z{\mathbb{Z}} being the initial ring is that every abelian group admits a unique Z{\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 β€œRR-module structures on G” and β€œring homomorphisms Rβ†’Endo(G)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 _)

  1. though the fact that there’s only one choice is sorta the theorem we are trying to proveβ€¦β†©οΈŽ