module Algebra.Ring.Module where

ModulesπŸ”—

A module over a ring RR is an abelian group GG equipped with an action by RR. 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 Ab{{\mathbf{Ab}}}.

For silly formalisation reasons, when defining modules, we do not take β€œan Ab{{\mathbf{Ab}}}-functor into Ab{{\mathbf{Ab}}}” as the definition: this correspondence is a theorem we prove later. Instead, we define a record packaging an RR-module structure on an abelian group:

record Module-on {β„“ β„“β€²} (R : Ring β„“) (G : AbGroup β„“β€²) : Type (β„“ βŠ” lsuc β„“β€²) where

Nicely typeset, the data of an RR-module structure on a group GG is given by a multiplication by RR, a function ⋆:Rβ†’Gβ†’G\star : R \to G \to G1, such that:

  • For every r:Rr : R, the function rβ‹†βˆ’r \star - is a group homomorphism Gβ†’GG \to G: We have r(x+y)=rx+ryr(x + y) = rx + ry;
  • Left multiplication is a ring homomorphism onto Gβ†’GG \to G: We have equalities 1x=x1x = x, (r+s)x=rx+sx(r+s)x = rx + sx, and (rs)x(rs)x = 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 Ab{{\mathbf{Ab}}}-category, and a module in the above sense determines an Ab{{\mathbf{Ab}}}-functor: so there should be a category of RR-modules, in the same way that there is a category of Ab{{\mathbf{Ab}}}-functors (between fixed domain/codomain categories).

Modules can be considered in slightly more generality, however: Rather than considering only homomorphisms between RR-modules M→NM \to N, for a fixed RR, 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 Rings{{\mathbf{Rings}}}. The objects over a ring RR are precisely the RR-modules, and the homomorphisms Mβ†’NM \to N over a map f:Rβ†’Sf : R \to S are given by RR-module homomorphisms Mβ†’fβˆ—(N)M \to f^*(N), where fβˆ—(N)f^*(N) 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 f:Rβ†’Sf : R \to S, we can transfer an SS-action on GG to an RR-action by precomposition with ff. 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 Mβ†’NM \to N over a ring homomorphism f:Rβ†’Sf : R \to S” using the name RR-SS-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 Mβ†’fβˆ—(N)M \to f^*(N), satisfying the property

f(rm+sn)=rf(m)+sf(n). f(rm + sn) = rf(m) + sf(n)\text{.}

Since our modules are unital, this compressed definition still implies that ff is a homomorphism of abelian groups M→NM \to N, as the following calculation shows:

f(m+n)=f(1m+1n)=1f(m)+1f(n)=f(m)+f(n). f(m + n) = f(1m + 1n) = 1f(m) + 1f(n) = f(m) + f(n)\text{.} 

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 RR is the category of RR-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 f:Rβ†’Sf : R \to S and an SS-module NN, how do we find a universal RR-module XX 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 RR-SS-bilinear maps over f:Rβ†’Sf : R \to S are defined as maps Xβ†’fβˆ—(N)X \to f^*(N), the freest choice we can make is that which makes the identity function RR-SS-bilinear: simply take X=fβˆ—(N)X = f^*(N).

  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 ff.

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. RR can be regarded as an RR-module with underlying group given by RR’s additive group, and with multiplication exactly RR’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 Ab{{\mathbf{Ab}}}-category. And, as usual, we have an adjunction: an action of RR on an Ab{{\mathbf{Ab}}}-category A\mathcal{A} can be described either as an Ab{{\mathbf{Ab}}}-functor B(R)→A{\mathbf{B}}(R) \to \mathcal{A}, or as a ring homomorphism R→EndoA(x)R \to {\mathrm{Endo}}_\mathcal{A}(x), where xx is the object being acted on.

In the particular case where A=Ab\mathcal{A} = {{\mathbf{Ab}}} is the archetypal Ab{{\mathbf{Ab}}}-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 Sets{{\mathbf{Sets}}}-category, which is Sets{{\mathbf{Sets}}} 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

  1. We generally elide the star and write only rxrx for r⋆xr \star x.β†©οΈŽ