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

1. We generally elide the star and write only $rx$ for $r \star x$.↩︎