module Algebra.Ring.Cat.Initial {ℓ} where

The initial ring🔗

We have, in the introduction to rings, mentioned offhand that the ring 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 is an object of the category of “rings in the zeroth universe”, whereas we would like any category of rings to have its own initial object. So, the first thing we must do is define a lifting of 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 there is a contractible space of homomorphisms 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 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 → ext (lemma x) 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 i.e., it sends sums of naturals to sums in and products of naturals to products in 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 extends to a function We want to define by sending to meaning that must respect the path constructor used in the definition of integers, i.e. we need 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 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 This, again, is slightly indirect: We know for a fact that, if we have some other homomorphism then it must enjoy just as our chosen embedding does. Now, no matter how trivial this coming observation may seem, do not brush it aside: The integer is the sum of 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 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 being the initial ring is that every abelian group admits a unique 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 “ structures on G” and “ring homomorphisms ” — 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 = Equiv→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 ↩