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â„€ = to-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.+-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 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
  z→r .preserves .pres-id = refl
  z→r .preserves .pres-+ (lift x) (lift y) =
    Int-elim₂-prop {P = λ x y → â„€â†ȘR (x +â„€ y) ≡ â„€â†ȘR x R.+ â„€â†ȘR y}
      (λ _ _ → hlevel 1)
      pf
      x y
      where abstract
        pf : ∀ a b x y → â„€â†ȘR (diff (a Nat.+ x) (b Nat.+ y)) ≡ (â„€â†ȘR (diff a b)) R.+ (â„€â†ȘR (diff x y))
        pf a b x y =
          â„€â†ȘR (diff (a Nat.+ x) (b Nat.+ y))    ≡⟹ â„€â†ȘR-diff (a Nat.+ x) (b Nat.+ y) âŸ©â‰Ą
          e (a Nat.+ x) R.- e (b Nat.+ y)       ≡⟹ ap₂ R._-_ (e-add a x) (e-add b y) âŸ©â‰Ą
          (e a R.+ e x) R.- (e b R.+ e y)       ≡⟹ ap₂ R._+_ refl (R.inv-comm ∙ R.+-commutes) âŸ©â‰Ą
          (e a R.+ e x) R.+ ((R.- e b) R.- e y) ≡⟹ R.extendl (R.extendr R.+-commutes) âŸ©â‰Ą
          (e a R.- e b) R.+ (e x R.- e y)       ≡˘⟹ ap₂ R._+_ (â„€â†ȘR-diff a b) (â„€â†ȘR-diff x y) âŸ©â‰ĄË˜
          â„€â†ȘR (diff a b) R.+ â„€â†ȘR (diff x y)     ∎
  z→r .preserves .pres-* (lift x) (lift y) =
    Int-elim₂-prop {P = λ x y → â„€â†ȘR (x *â„€ y) ≡ â„€â†ȘR x R.* â„€â†ȘR y}
      (λ _ _ → hlevel 1)
      pf
      x y
    where abstract
      swizzle : ∀ a b x y
                → (a R.- b) R.* (x R.- y)
                ≡ (a R.* x R.+ b R.* y) R.- (a R.* y R.+ b R.* x)
      swizzle a b x y =
        (a R.- b) R.* (x R.- y)                                                       ≡⟹ R.*-distribl âŸ©â‰Ą
        ((a R.- b) R.* x) R.+ ((a R.- b) R.* (R.- y))                                 ≡⟹ ap₂ R._+_ refl (sym R.neg-*-r) âŸ©â‰Ą
        ((a R.- b) R.* x) R.- ((a R.- b) R.* y)                                       ≡⟹ ap₂ R._-_ R.*-distribr R.*-distribr âŸ©â‰Ą
        (a R.* x R.+ (R.- b) R.* x) R.- (a R.* y R.+ (R.- b) R.* y)                   ≡⟹ ap₂ R._+_ refl (R.a.inv-comm ∙ R.+-commutes) âŸ©â‰Ą
        (a R.* x R.+ (R.- b) R.* x) R.+ ((R.- (a R.* y)) R.+ ⌜ R.- ((R.- b) R.* y) ⌝) ≡⟹ ap! (ap R.a._⁻Âč (sym R.neg-*-l) ∙ R.a.inv-inv) âŸ©â‰Ą
        (a R.* x R.+ (R.- b) R.* x) R.+ ((R.- (a R.* y)) R.+ (b R.* y))               ≡⟹ R.pulll (R.extendr R.+-commutes) âŸ©â‰Ą
        (a R.* x) R.+ (R.- (a R.* y)) R.+ ((R.- b) R.* x) R.+ (b R.* y)               ≡⟹ R.pullr R.+-commutes ·· R.extendl (R.pullr R.+-commutes) ·· R.pulll (R.pulll refl) ∙ R.pullr (ap₂ R._+_ refl (sym R.neg-*-l) ·· sym R.a.inv-comm ·· ap R.a._⁻Âč R.+-commutes) âŸ©â‰Ą
        (a R.* x R.+ b R.* y) R.- (a R.* y R.+ b R.* x)                               ∎

      pf : ∀ a b x y → â„€â†ȘR (diff a b *â„€ diff x y) ≡ (â„€â†ȘR (diff a b) R.* â„€â†ȘR (diff x y))
      pf a b x y =
        â„€â†ȘR (diff (a Nat.* x Nat.+ b Nat.* y) (a Nat.* y Nat.+ b Nat.* x))      ≡⟹ â„€â†ȘR-diff (a Nat.* x Nat.+ b Nat.* y) (a Nat.* y Nat.+ b Nat.* x) âŸ©â‰Ą
        e (a Nat.* x Nat.+ b Nat.* y) R.- e (a Nat.* y Nat.+ b Nat.* x)         ≡⟹ ap₂ R._-_ (e-add (a Nat.* x) (b Nat.* y)) (e-add (a Nat.* y) (b Nat.* x)) âŸ©â‰Ą
        (e (a Nat.* x) R.+ e (b Nat.* y)) R.- (e (a Nat.* y) R.+ e (b Nat.* x)) ≡⟹ ap₂ R._-_ (ap₂ R._+_ (e-mul a x) (e-mul b y)) (ap₂ R._+_ (e-mul a y) (e-mul b x)) âŸ©â‰Ą
        ((e a R.* e x) R.+ (e b R.* e y)) R.- ((e a R.* e y) R.+ (e b R.* e x)) ≡˘⟹ swizzle (e a) (e b) (e x) (e y) âŸ©â‰ĄË˜
        (e a R.- e b) R.* (e x R.- e y)                                         ≡˘⟹ ap₂ R._*_ (â„€â†ȘR-diff a b) (â„€â†ȘR-diff x y) âŸ©â‰ĄË˜
        â„€â†ȘR (diff a b) R.* â„€â†ȘR (diff x y) ∎

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) (is-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 : is-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 = is-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 : Abelian-group ℓ) → is-contr (Ring-action Liftâ„€ (G .snd))
â„€-module-unique G = is-hlevel≃ 0 (Action≃Hom Liftâ„€ G) (Int-is-initial _)

  1. though the fact that there’s only one choice is sorta the theorem we are trying to prove ↩