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β€¦β†©οΈŽ