open import Algebra.Group.Ab
open import Algebra.Group
open import Algebra.Ring

open import Cat.Displayed.Univalence.Thin
open import Cat.Diagram.Initial
open import Cat.Prelude hiding (_+_ ; _*_)

open import Data.Int.Properties
open import Data.Int.Base

import Algebra.Ring.Reasoning as Kit

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 \text{-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ℤ = to-ring mr where
  open make-ring
  mr : make-ring (Lift ℓ Int)
  mr .ring-is-set = hlevel 
  mr .1R = lift 
  mr .0R = lift 
  mr .-_  (lift x)          = lift (negℤ x)
  mr ._+_ (lift x) (lift y) = lift (x +ℤ y)
  mr ._*_ (lift x) (lift y) = lift (x *ℤ y)

  mr .*-idl      (lift x)                   = ap lift $ *ℤ-onel x
  mr .*-idr      (lift x)                   = ap lift $ *ℤ-oner x
  mr .+-idl      (lift x)                   = ap lift $ +ℤ-zerol x
  mr .+-invr     (lift x)                   = ap lift $ +ℤ-invr x
  mr .+-comm     (lift x) (lift y)          = ap lift $ +ℤ-commutative x y
  mr .+-assoc    (lift x) (lift y) (lift z) = ap lift $ +ℤ-assoc x y z
  mr .*-assoc    (lift x) (lift y) (lift z) = ap lift $ *ℤ-associative x y z
  mr .*-distribl (lift x) (lift y) (lift z) = ap lift $ *ℤ-distribl x y z
  mr .*-distribr (lift x) (lift y) (lift z) = ap lift $ *ℤ-distribr x y z

With that set up out of the way, we can now proceed to the actual theorem we’re interested in: For a ring $R\text{,}$ there is a contractible space of homomorphisms $\mathbb{Z}\to R\text{.}$ 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\text{.}$ There’s really only one choice¹, so here it is:

Int-is-initial : is-initial (Rings ℓ) Liftℤ
Int-is-initial R = contr z→r λ x → ext (lemma x) where
  module R = Kit R

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\text{,}$ i.e., it sends sums of naturals to sums in $R\text{,}$ and products of naturals to products in $R\text{.}$ 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

  e-suc zero = sym R.+-idr
  e-suc (suc n) = refl

  e-add zero n = sym R.+-idl
  e-add (suc m) n =
    e (suc m Nat.+ n)      ≡⟨ e-suc (m Nat.+ n) ⟩≡
    R.1r R.+ e (m Nat.+ n) ≡⟨ ap (R.1r R.+_) (e-add m n) ⟩≡
    R.1r R.+ (e m R.+ e n) ≡⟨ R.+-associative ⟩≡
    (R.1r R.+ e m) R.+ e n ≡˘⟨ ap (R._+ e n) (e-suc m) ⟩≡˘
    e (suc m) R.+ e n ∎

  e-mul zero n = sym R.*-zerol
  e-mul (suc m) n =
    e (suc m Nat.* n)            ≡⟨ e-add n (m Nat.* n) ⟩≡
    e n R.+ e (m Nat.* n)        ≡⟨ ap (e n R.+_) (e-mul m n) ⟩≡
    e n R.+ e m R.* e n          ≡˘⟨ ap (R._+ (e m R.* e n)) R.*-idl ⟩≡˘
    R.1r R.* e n R.+ e m R.* e n ≡˘⟨ R.*-distribr ⟩≡˘
    (R.1r R.+ e m) R.* e n       ≡˘⟨ ap (R._* e n) (e-suc m) ⟩≡˘
    (e (suc 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\text{:}$ We want to define $f$ by sending $[a-b]$ to $e(a)-e(b)\text{,}$ 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)\text{.}$ 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.+-commutes) ∙ 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\text{.}$ 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.

  ℤ↪R : Int → ⌞ R ⌟
  ℤ↪R (pos x) = e x
  ℤ↪R (negsuc x) = R.- (e (suc x))

  open is-ring-hom

  z-natdiff : ∀ x y → ℤ↪R (x ℕ- y) ≡ e x R.- e y
  z-natdiff x zero = R.intror R.inv-unit
  z-natdiff zero (suc y) = R.introl refl
  z-natdiff (suc x) (suc y) = z-natdiff x y ∙ e-tr x y

  z-add : ∀ x y → ℤ↪R (x +ℤ y) ≡ ℤ↪R x R.+ ℤ↪R y
  z-add (pos x) (pos y) = e-add x y
  z-add (pos x) (negsuc y) = z-natdiff x (suc y)
  z-add (negsuc x) (pos y) = z-natdiff y (suc x) ∙ R.+-commutes
  z-add (negsuc x) (negsuc y) =
    R.- (e  R.+ e (suc x Nat.+ y))         ≡⟨ ap R.-_ (ap₂ R._+_ refl (e-add (suc x) y) ∙ R.extendl R.+-commutes) ⟩≡
    R.- (e (suc x) R.+ (e  R.+ e y))       ≡⟨ R.a.inv-comm ⟩≡
    (R.- (e  R.+ e y)) R.+ (R.- e (suc x)) ≡⟨ R.+-commutes ⟩≡
    (R.- e (suc x)) R.+ (R.- (e  R.+ e y)) ≡⟨ ap₂ R._+_ refl (ap R.-_ (sym (e-add  y))) ⟩≡
    (R.- e (suc x)) R.+ (R.- e ( Nat.+ y)) ∎

  z-mul : ∀ x y → ℤ↪R (x *ℤ y) ≡ ℤ↪R x R.* ℤ↪R y
  z-mul (pos x) (pos y) =
    ℤ↪R (assign pos (x Nat.* y)) ≡⟨ ap ℤ↪R (assign-pos (x Nat.* y)) ⟩≡
    e (x Nat.* y)                ≡⟨ e-mul x y ⟩≡
    (e x R.* e y)                ∎
  z-mul (posz) (negsuc y) = sym R.*-zerol
  z-mul (possuc x) (negsuc y) =
    R.- e (suc x Nat.* suc y)     ≡⟨ ap R.-_ (e-mul (suc x) (suc y)) ⟩≡
    R.- (e (suc x) R.* e (suc y)) ≡˘⟨ R.*-negater ⟩≡˘
    e (suc x) R.* (R.- e (suc y)) ∎
  z-mul (negsuc x) (posz) =
    ℤ↪R (assign neg (x Nat.* )) ≡⟨ ap ℤ↪R (ap (assign neg) (Nat.*-zeror x)) ⟩≡
    ℤ↪R                         ≡⟨ sym R.*-zeror ⟩≡
    ℤ↪R (negsuc x) R.* R.0r      ∎
  z-mul (negsuc x) (possuc y) =
    R.- e (suc x Nat.* suc y)     ≡⟨ ap R.-_ (e-mul (suc x) (suc y)) ⟩≡
    R.- (e (suc x) R.* e (suc y)) ≡⟨ sym R.*-negatel ⟩≡
    (R.- e (suc x)) R.* e (suc y) ∎
  z-mul (negsuc x) (negsuc y) =
    e (suc x Nat.* suc y)               ≡⟨ e-mul (suc x) (suc y) ⟩≡
    e (suc x) R.* e (suc y)             ≡˘⟨ R.inv-inv ⟩≡˘
    R.- (R.- (e (suc x) R.* e (suc y))) ≡˘⟨ ap R.-_ R.*-negater ⟩≡˘
    R.- (e (suc x) R.* ℤ↪R (negsuc y))  ≡˘⟨ R.*-negatel ⟩≡˘
    ℤ↪R (negsuc x) R.* ℤ↪R (negsuc y)   ∎

  z→r : Rings.Hom Liftℤ R
  z→r .hom (lift x) = ℤ↪R x
  z→r .preserves .pres-id = refl
  z→r .preserves .pres-+ (lift x) (lift y) = z-add x y
  z→r .preserves .pres-* (lift x) (lift y) = z-mul x y

The last thing we must show is that this is the unique ring homomorphism from the integers to $R\text{.}$ This, again, is slightly indirect: We know for a fact that, if we have some other homomorphism $f:\mathbb{Z}\to R\text{,}$ then it must enjoy $f(1)=1\text{,}$ 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

and that last expression is pretty exactly what our canonical map evaluates to on $n\text{.}$ So we’re done!

  module _ (f : Rings.Hom Liftℤ R) where
    private module f = is-ring-hom (f .preserves)

    f-pos : ∀ x → e x ≡ f .hom (lift (pos x))
    f-pos zero = sym f.pres-0
    f-pos (suc x) = e-suc x ∙ sym (f.pres-+ (lift ) (lift (pos x)) ∙ ap₂ R._+_ f.pres-id (sym (f-pos x)))

    lemma : (i : Int) → z→r # lift i ≡ f # lift i
    lemma (pos x) = f-pos x
    lemma (negsuc x) = sym (f.pres-neg {lift (possuc x)} ∙ ap R.-_ (sym (f-pos (suc x))))