module Algebra.Ring.Module where

# Modulesπ

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

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

record Module-on {β ββ²} (R : Ring β) (G : AbGroup ββ²) : Type (β β lsuc ββ²) where

Nicely typeset, the data of an
$R$-module
structure on a group
$G$
is given by a *multiplication* by
$R$,
a function
$\star : R \to G \to G$^{1}, such that:

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

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

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

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

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

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

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

We generally elide the star and write only $rx$ for $r \star x$.β©οΈ