module Algebra.Ring.Module where
Modulesπ
A module over a ring is an abelian group equipped with an action by . Modules generalise the idea of vector spaces, which may be familiar from linear algebra, by replacing the field of scalars by a ring of scalars. More pertinently, though, modules specialise functors: specifically, functors into the category .
For silly formalisation reasons, when defining modules, we do not take βan -functor into β as the definition: this correspondence is a theorem we prove later. Instead, we define a record packaging an -module structure on an abelian group:
record Module-on {β ββ²} (R : Ring β) (G : AbGroup ββ²) : Type (β β lsuc ββ²) where
Nicely typeset, the data of an -module structure on a group is given by a multiplication by , a function 1, such that:
- For every , the function is a group homomorphism : We have ;
- Left multiplication is a ring homomorphism onto : We have equalities , , and = r(sx)$.
Note: Even though we do not require all rings to be commutative, we only care about doing algebra with commutative rings. Because of this, we donβt differentiate between left and right modules.
field _β_ : β R β β G.β β G.β β-id : β x β R.1r β x β‘ x β-add-r : β r x y β r β (x G.+ y) β‘ (r β x) G.+ (r β y) β-add-l : β r s x β (r R.+ s) β x β‘ (r β x) G.+ (s β x) β-assoc : β r s x β r β (s β x) β‘ (r R.* s) β x
In much the same way that a monoid determines a 1-object category, a ring determines a 1-object -category, and a module in the above sense determines an -functor: so there should be a category of -modules, in the same way that there is a category of -functors (between fixed domain/codomain categories).
Modules can be considered in slightly more generality, however: Rather than considering only homomorphisms between -modules , for a fixed , we can define homomorphisms between modules over different rings, as long as we have a ring homomorphism to mediate the difference.
We formalise this construction by defining a βbig category of modulesβ as being displayed over the category . The objects over a ring are precisely the -modules, and the homomorphisms over a map are given by -module homomorphisms , where is the restriction of scalars, defined below.
Scalar-restriction : β {β ββ²} {G : AbGroup ββ²} {R S : Ring β} β Rings.Hom R S β Module-on S G β Module-on R G Scalar-restriction {G = G} f M = N where module M = Module-on M open Module-on
The idea behind restriction of scalars is much simpler than the fanciful name suggests: Given a map , we can transfer an -action on to an -action by precomposition with . Since weβre transporting it by _pre_composition, we get a little contravariance, as a treat.
N : Module-on _ G N ._β_ r m = f # r M.β m N .β-id x = ap (M._β x) (f .preserves .pres-id) β M.β-id x N .β-add-r r x y = M.β-add-r _ x y N .β-add-l r s x = ap (M._β x) (f .preserves .pres-+ _ _) β M.β-add-l _ _ x N .β-assoc r s x = M.β-assoc _ _ _ β ap (M._β x) (sym (f .preserves .pres-* r s))
We abbreviate the sentence βa linear map over a ring homomorphism β using the name --bilinear map, even though this might not be perfectly accurate to existing literature on commutative algebra. Being explicit, this is a function between the sets , satisfying the property
Since our modules are unital, this compressed definition still implies that is a homomorphism of abelian groups , as the following calculation shows:
Mods : β β ββ² β Displayed (Rings β) (β β lsuc ββ²) (β β ββ²) Ob[ Mods β ββ² ] R = Module ββ² R Hom[ Mods β ββ² ] f M N = Linear-map M N f Hom[ Mods β ββ² ]-set f x y = Linear-map-is-set Mods _ _ .idβ² .map x = x Mods _ _ .idβ² .linear r m s n = refl Mods _ _ ._ββ²_ f g .map x = f .map (g .map x) Mods _ _ ._ββ²_ f g .linear r m s n = ap (f .map) (g .linear r m s n) β f .linear _ _ _ _ Mods _ _ .idrβ² fβ² = Linear-map-path refl Mods _ _ .idlβ² fβ² = Linear-map-path refl Mods _ _ .assocβ² fβ² gβ² hβ² = Linear-map-path refl
The fibre of this displayed category over a ring is the category of -modules.
R-Mod : β {β} ββ² (R : Ring β) β Precategory (β β lsuc ββ²) (β β ββ²) R-Mod ββ² R = Fibreβ² (Mods _ ββ²) R fix coh where
module R-Mod {β ββ²} {R : Ring β} = Cat.Reasoning (R-Mod ββ² R)
As a fibrationπ
Let us prove that Mods is not just displayed over the category of rings, but fibred over it, too. But this is essentially something we have already done: the data of a Cartesian fibration is essentially that of a functorial reindexing of the fibres by morphisms in the base, but this is given exactly by the restriction of scalars we defined above.
Mods-fibration : β β ββ² β Cartesian-fibration (Mods β ββ²) Mods-fibration β ββ² = mods where open Cartesian-fibration open Cartesian-lift open is-cartesian
So, given a map and an -module , how do we find a universal -module making the following diagram cartesian? Well, Iβve already explained the answer, but our hand is essentially forced by the definition of maps-over in Mods. Since --bilinear maps over are defined as maps , the freest choice we can make is that which makes the identity function --bilinear: simply take .
mods : Cartesian-fibration (Mods β ββ²) mods .has-lift f N = the-lift where the-lift : Cartesian-lift (Mods β ββ²) f N the-lift .xβ² = N .fst , Scalar-restriction f (N .snd) the-lift .lifting .map x = x the-lift .lifting .linear r m s n = refl the-lift .cartesian .universal m hβ² .map = hβ² .map the-lift .cartesian .universal m hβ² .linear = hβ² .linear the-lift .cartesian .commutes {uβ² = uβ²} m hβ² = Linear-map-path refl the-lift .cartesian .unique {uβ² = uβ²} {m} mβ² p = Linear-map-path (ap map p)
It is straightforward to calculate that this choice indeed furnishes a Cartesian lift of .
Representable modulesπ
Analogously to how groups act on themselves (Cayleyβs theorem) and how precategories act on themselves (the Yoneda lemma), rings also act on themselves to give a notion of representable modules. can be regarded as an -module with underlying group given by βs additive group, and with multiplication exactly βs multiplication.
representable-module : β {β} (R : Ring β) β Module β R representable-module R = _ , mod where open Module-on hiding (module R ; module G) module R = Ring-on (R .snd) mod : Module-on R (restrict R.additive-group Ξ» _ _ β R.+-commutes) mod ._β_ = R._*_ mod .β-id x = R.*-idl mod .β-add-r r x y = R.*-distribl mod .β-add-l r s x = R.*-distribr mod .β-assoc r s x = R.*-associative
The construction of representable modules extends from a functor from the category of rings to the (big) category of modules β the total space of the fibration of modules.
Representable-modules : β {β} β Functor (Rings β) (β« (Mods β β)) Representable-modules .Fβ R = R , representable-module R Representable-modules .Fβ {x} {y} f = total-hom f $ record { map = f #_ ; linear = Ξ» r m s n β f .preserves .pres-+ _ _ β apβ (y .snd .Ring-on._+_) (f .preserves .pres-* r m) (f .preserves .pres-* s n) } Representable-modules .F-id {x} = total-hom-path _ refl $ Linear-map-path refl Representable-modules .F-β {x} {y} {z} f g = total-hom-path _ refl $ Linear-map-path refl
As actionsπ
Another presentation of modules, which might make more sense to some, is the following: In the same way that a monoid can act on a category (resp. a group can act on a groupoid), a ring can act on a ringoid: an -category. And, as usual, we have an adjunction: an action of on an -category can be described either as an -functor , or as a ring homomorphism , where is the object being acted on.
In the particular case where is the archetypal -category, these actions get a fancy name: modules. This is analogous to how monoid actions and group actions are fancy names for actions on the archetypal -category, which is itself.
module _ {β} (R : Ring β) where ModuleβAction : β G (M : Module-on R G) β Rings.Hom R (Endo Ab-ab G) ModuleβAction G M = rh where module M = Module-on M rh : Rings.Hom R (Endo Ab-ab G) rh .hom x .hom g = x M.β g rh .preserves .pres-id = Homomorphism-path (Ξ» x β M.β-id x) rh .preserves .pres-+ x y = Homomorphism-path (Ξ» x β M.β-add-l _ y x) rh .preserves .pres-* x y = Homomorphism-path (Ξ» x β sym (M.β-assoc _ _ _)) rh .hom x .preserves .Group-hom.pres-β g gβ² = M.β-add-r x g gβ² open Module-on ActionβModule : β G β Rings.Hom R (Endo Ab-ab G) β Module-on R G ActionβModule G rh ._β_ r g = (rh # r) .hom g ActionβModule G rh .β-id x = rh .preserves .pres-id #β x ActionβModule G rh .β-add-r x y z = (rh # x) .preserves .Group-hom.pres-β y z ActionβModule G rh .β-add-l x y z = rh .preserves .pres-+ x y #β z ActionβModule G rh .β-assoc x y z = sym $ rh .preserves .pres-* x y #β z
This correspondence between presentations β shuffling of data β is almost definitionally an equivalence, but in both cases, we need to appeal to some extensionality principles to βget atβ the data, even if it is unchanging.
ActionβModule : β G β Module-on R G β Rings.Hom R (Endo Ab-ab G) ActionβModule G = IsoβEquiv morp where open is-iso morp : Iso (Module-on R G) (Rings.Hom R (Endo Ab-ab G)) morp .fst = ModuleβAction G morp .snd .inv = ActionβModule G morp .snd .rinv x = Homomorphism-path Ξ» x β Homomorphism-path Ξ» y β refl morp .snd .linv x i ._β_ = x ._β_ morp .snd .linv x i .β-id = x .β-id morp .snd .linv x i .β-add-r = x .β-add-r morp .snd .linv x i .β-add-l = x .β-add-l morp .snd .linv x i .β-assoc = x .β-assoc
We generally elide the star and write only for .β©οΈ