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 -compact 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)
mr .*-idl {lift x} = ap lift $ *β€-idl x mr .*-idr {lift x} = ap lift $ *β€-idr x mr .+-idl {lift x} = ap lift $ +β€-zerol x mr .+-invr {lift x} = ap lift $ +β€-inverser x mr .+-comm {lift x} {lift y} = ap lift $ +β€-commutative x y mr .+-assoc {lift x} {lift y} {lift z} = ap lift $ +β€-associative 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 $ *β€-distrib-+β€-l x y z mr .*-distribr {lift x} {lift y} {lift z} = ap lift $ *β€-distrib-+β€-r 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 , 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 β 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 , 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
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 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 -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 β-module 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 = is-hlevelβ 0 (ActionβHom Liftβ€ G) (Int-is-initial _)
though the fact that thereβs only one choice is sorta the theorem we are trying to proveβ¦β©οΈ