open import Algebra.Ring.Module open import Algebra.Group.Ab open import Algebra.Group open import Algebra.Ring open import Cat.Abelian.Instances.Ab open import Cat.Abelian.Base open import Cat.Prelude module Algebra.Ring.Module.Category {β} (R : Ring β) where
The category R-Modπ
Let us investigate the structure of the category -Mod, for whatever your favourite ring is1. The first thing weβll show is that it admits an -enrichment. This is the usual βpointwiseβ group structure, but proving that the pointwise sum is a still a linear map is, ahem, very annoying. See for yourself:
R-Mod-ab-category : β {ββ²} β Ab-category (R-Mod ββ² R) R-Mod-ab-category .Group-on-hom A B = to-group-on grp where module A = Module A module B = Module B grp : make-group (R-Mod.Hom A B) grp .group-is-set = R-Mod.Hom-set _ _ grp .mul f g .map x = f .map x B.+ g .map x grp .mul f g .linear r m s n = fβ (r A.β m A.+ s A.β n) B.+ gβ (r A.β m A.+ s A.β n) β‘β¨ apβ B._+_ (f .linear _ _ _ _) (g .linear _ _ _ _) β©β‘ (r B.β fβ m B.+ s B.β fβ n) B.+ (r B.β gβ m B.+ s B.β gβ n) β‘β¨ B.G.pullr (B.G.pulll B.G.commutative) β©β‘ r B.β fβ m B.+ (r B.β gβ m B.+ s B.β fβ n) B.+ s B.β gβ n β‘β¨ B.G.pulll (B.G.pulll (sym (B.β-add-r r _ _))) β©β‘ (r B.β (fβ m B.+ gβ m) B.+ (s B.β fβ n)) B.+ (s B.β gβ n) β‘β¨ B.G.pullr (sym (B.β-add-r s _ _)) β©β‘ r B.β (fβ m B.+ gβ m) B.+ s B.β (fβ n B.+ gβ n) β where fβ = f .map gβ = g .map
The rest of the construction is also Just Like That, so Iβm
going to keep it in this <details>
element out of decency.
grp .unit .map x = B.G.unit grp .unit .linear r m s n = B.G.unit β‘Λβ¨ B.β-group-hom.pres-id _ β©β‘Λ s B.β B.G.unit β‘Λβ¨ B.G.eliml (B.β-group-hom.pres-id _) β©β‘Λ r B.β B.G.unit B.+ s B.β B.G.unit β grp .inv f .map x = B.G.inverse (f .map x) grp .inv f .linear r m s n = ap B.G.inverse (f .linear r m s n) Β·Β· B.G.inv-comm Β·Β· B.G.commutative β apβ B._+_ (sym (B.β-group-hom.pres-inv _)) (sym (B.β-group-hom.pres-inv _)) grp .assoc x y z = Linear-map-path (funext Ξ» x β sym B.G.associative) grp .invl x = Linear-map-path (funext Ξ» x β B.G.inversel) grp .invr x = Linear-map-path (funext Ξ» x β B.G.inverser) grp .idl x = Linear-map-path (funext Ξ» x β B.G.idl) R-Mod-ab-category .Hom-grp-ab A B f g = Linear-map-path (funext Ξ» x β Module.G.commutative B) R-Mod-ab-category .β-linear-l {C = C} f g h = Linear-map-path refl R-Mod-ab-category .β-linear-r {B = B} {C} f g h = Linear-map-path $ funext Ξ» x β f .map (g .map x) C.+ f .map (h .map x) β‘β¨ apβ C._+_ (sym (C.β-id _)) (sym (C.β-id _)) β©β‘ R.1r C.β f .map (g .map x) C.+ (R.1r C.β f .map (h .map x)) β‘β¨ sym (f .linear R.1r (g .map x) R.1r (h .map x)) β©β‘ f .map (R.1r B.β g .map x B.+ R.1r B.β h .map x) β‘β¨ ap (f .map) (apβ B._+_ (B.β-id _) (B.β-id _)) β©β‘ f .map (g .map x B.+ h .map x) β where module C = Module C module B = Module B
Finite biproductsπ
Letβs now prove that -Mod is a preadditive category. This is exactly as in : The zero object is the zero group, equipped with its unique choice of -module structure, and direct products are given by direct products of the underlying groups with the canonical choice of -module structure.
The zero object is simple, because the unit type is so well-behaved2 when it comes to definitional equality: Everything is constantly the unit, including the paths, which are all reflexivity.
R-Mod-is-additive : is-additive (R-Mod _ R) R-Mod-is-additive .has-ab = R-Mod-ab-category R-Mod-is-additive .has-terminal = record { top = _ , β α΄Ή ; hasβ€ = Ξ» x β contr (record { map = Ξ» _ β lift tt ; linear = Ξ» _ _ _ _ β refl }) (Ξ» _ β Linear-map-path refl) } where β α΄Ή : Module-on R (Ab-is-additive .has-terminal .Terminal.top) β α΄Ή .Module-on._β_ = Ξ» _ _ β lift tt β α΄Ή .Module-on.β-id _ = refl β α΄Ή .Module-on.β-add-r _ _ _ = refl β α΄Ή .Module-on.β-add-l _ _ _ = refl β α΄Ή .Module-on.β-assoc _ _ _ = refl
For the direct products, on the other hand, we have to do a bit more work. Like we mentioned before, the direct product of modules is built on the direct product of abelian groups (which is, in turn, built on the Cartesian product of types). The module action, and its laws, are defined pointwise using the -module structures of and :
R-Mod-is-additive .has-prods M N = prod where module P = is-additive.Product Ab-is-additive (Ab-is-additive .has-prods (M .fst) (N .fst)) module M = Module M module N = Module N Mβα΅£N : Module-on R P.apex Mβα΅£N .Module-on._β_ r (a , b) = r M.β a , r N.β b Mβα΅£N .Module-on.β-id _ = Ξ£-pathp (M.β-id _) (N.β-id _) Mβα΅£N .Module-on.β-add-r _ _ _ = Ξ£-pathp (M.β-add-r _ _ _) (N.β-add-r _ _ _) Mβα΅£N .Module-on.β-add-l _ _ _ = Ξ£-pathp (M.β-add-l _ _ _) (N.β-add-l _ _ _) Mβα΅£N .Module-on.β-assoc _ _ _ = Ξ£-pathp (M.β-assoc _ _ _) (N.β-assoc _ _ _)
We can readily define the universal cone: The projection maps are the projection maps of the underlying type, which are definitionally linear. Proving that this cone is actually universal involves a bit of path-mangling, but itβs nothing too bad:
open Ab-category.is-product open Ab-category.Product prod : Ab-category.Product R-Mod-ab-category M N prod .apex = _ , Mβα΅£N prod .Οβ .map (a , _) = a prod .Οβ .linear r m s n = refl prod .Οβ .map (_ , b) = b prod .Οβ .linear r m s n = refl prod .has-is-product .β¨_,_β© f g .map x = f .map x , g .map x prod .has-is-product .β¨_,_β© f g .linear r m s n = Ξ£-pathp (f .linear _ _ _ _) (g .linear _ _ _ _) prod .has-is-product .Οββfactor = Linear-map-path refl prod .has-is-product .Οββfactor = Linear-map-path refl prod .has-is-product .unique other p q = Linear-map-path {ββ² = lzero} $ funext Ξ» x β Ξ£-pathp (ap map p $β x) (ap map q $β x)