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, $\mathbf{Ab}\text{-enriched}$ functors into the category $\mathbf{Ab}\text{.}$

For silly formalisation reasons, when defining modules, we do not take “an $\mathbf{Ab}\text{-functor}$ into $\mathbf{Ab}$” as the definition: this correspondence is a theorem we prove later. Instead, we set up $R\text{-modules}$ as typical algebraic structures, as data (and property) attached to a type.

The structure of an $R\text{-module}$ on a type $T$ consists of an addition $+:T\times T\to T$ and a scalar multiplication $\star :R\times T\to T\text{.}$ In prose, we generally omit the star, writing $rx$ rather than the wordlier $r\star x\text{.}$ These must satisfy the following properties:

• $+$ makes $T$ into an abelian group. Since we’ve already defined abelian groups, we can take this entire property as “indivisible”, saving some effort.

• $\cdot$ is a ring homomorphism of $R$ onto $(T,+)\text{’s}$ endomorphism ring. In other words, we have:

  • $1x=x\text{;}$
  • $(rs)\cdot x=r\cdot (s\cdot x)\text{;}$
  • $(r+s)x=rx+sx\text{;}$ and
  • $r(x+y)=rx+ry\text{.}$

  record is-module {ℓ'} {T : Type ℓ'} (_+_ : T → T → T) (_⋆_ : ⌞ R ⌟ → T → T) : Type (ℓ ⊔ ℓ') where
    no-eta-equality
    field
      has-is-ab  : is-abelian-group _+_
      ⋆-distribl : ∀ r x y → r ⋆ (x + y)   ≡ (r ⋆ x) + (r ⋆ y)
      ⋆-distribr : ∀ r s x → (r R.+ s) ⋆ x ≡ (r ⋆ x) + (s ⋆ x)
      ⋆-assoc    : ∀ r s x → r ⋆ (s ⋆ x)   ≡ (r R.* s) ⋆ x
      ⋆-id       : ∀ x     → R.1r ⋆ x      ≡ x

Correspondingly, a module structure on a type packages the addition, the scalar multiplication, and the proofs that these behave as we set above. A module is a type equipped with a module structure.

  record Module-on {ℓ'} (T : Type ℓ') : Type (ℓ ⊔ ℓ') where
    no-eta-equality
    field
      _+_        : T → T → T
      _⋆_        : ⌞ R ⌟ → T → T
      has-is-mod : is-module _+_ _⋆_

    infixl 25 _+_
    infixr 27 _⋆_

    open is-module has-is-mod public

  Module : ∀ ℓm → Type (lsuc ℓm ⊔ ℓ)
  Module ℓm = Σ (Set ℓm) λ X → Module-on ∣ X ∣

  record is-linear-map (f : S → T) (M : Module-on S) (N : Module-on T)
    : Type (ℓ ⊔ level-of S ⊔ level-of T) where

Linear maps🔗

The correct notion of morphism between $R\text{-modules}$ is the linear map; in case we need to make the base ring $R$ clear, we shall call them $R\text{-linear}$ maps. Since the structure of $R\text{-modules}$ are their additions and their scalar multiplications, it stands to reason that these are what homomorphisms should preserve. Rather than separately asking for preservation of addition and of multiplication, the following single assumption suffices:

    field linear : ∀ r s t → f (r ⋆ s + t) ≡ r ⋆ f s + f t

Any map which satisfies this equation must preserve addition, since we have

and standard lemmas about group homomorphisms ensure that $f$ will also preserve negation, and, more importantly, zero. We can then derive that $f$ preserves the scalar multiplication, by calculating

  record Linear-map (M : Module ℓm) (N : Module ℓn) : Type (ℓ ⊔ ℓm ⊔ ℓn) where
    no-eta-equality
    field
      map : ⌞ M ⌟ → ⌞ N ⌟
      lin : is-linear-map map (M .snd) (N .snd)
    open is-linear-map lin public

The collection of linear maps forms a set, whose identity type is given by pointwise identity of the underlying maps. Therefore, we may take these to be the morphisms of a category $R\text{-}\mathbf{Mod}\text{.}$ $R\text{-}\mathbf{Mod}$ is a very standard category, so very standard constructions can set up the category, the functor witnessing its concreteness, and a proof that it is univalent.

  R-Mod-structure : ∀ {ℓ} → Thin-structure _ Module-on
  R-Mod-structure {ℓ} = rms where
    rms : Thin-structure _ Module-on
    ∣ rms .is-hom f M N ∣    = is-linear-map {ℓ} {_} {ℓ} f M N
    rms .is-hom f M N .is-tr = is-linear-map-is-prop

    rms .id-is-hom        .linear r s t = refl
    rms .∘-is-hom f g α β .linear r s t =
      ap f (β .linear r s t) ∙ α .linear _ _ _

    rms .id-hom-unique {s = s} {t = t} α _ = r where
      module s = Module-on s
      module t = Module-on t

      r : s ≡ t
      r i .Module-on._+_ x y = is-linear-map.pres-+ α x y i
      r i .Module-on._⋆_ x y = is-linear-map.pres-⋆ α x y i
      r i .Module-on.has-is-mod =
        is-prop→pathp (λ i → hlevel {T = is-module
          (λ x y → is-linear-map.pres-+ α x y i)
          (λ x y → is-linear-map.pres-⋆ α x y i)} 1)
          (Module-on.has-is-mod s) (Module-on.has-is-mod t) i

“Representable” modules🔗

A prototypical example of $R\text{-module}$ is.. $R$ itself! A ring has an underlying abelian group, and the multiplication operation can certainly be considered a special kind of “scalar multiplication”. If we treat $R$ as an $\mathbf{Ab}\text{-category}$ with a single object, this construction corresponds to the functor ${\mathbf{Hom}}_R(-,\bullet )$ — the “Yoneda embedding” of $R\text{’s}$ unique object. Stretching the analogy, we refer to $R\text{-as-an-}$$R\text{-module}$ as the “representable” $R\text{-module.}$

  representable-module : Module ℓ
  representable-module .fst = R .fst
  representable-module .snd = to-module-on record
    { has-is-set = R.has-is-set
    ; _+_ = R._+_
    ; inv = R.-_
    ; 0g = R.0r
    ; +-assoc = λ x y z → R.+-associative
    ; +-invl = λ x → R.+-invl
    ; +-idl = λ x → R.+-idl
    ; +-comm = λ x y → R.+-commutes
    ; _⋆_ = R._*_
    ; ⋆-distribl = λ x y z → R.*-distribl
    ; ⋆-distribr = λ x y z → R.*-distribr
    ; ⋆-assoc    = λ x y z → R.*-associative
    ; ⋆-id       = λ x → R.*-idl
    }

Another perspective on this construction is that we are regarding $R$ as the space of “1-dimensional vectors” over itself. Following this line of reasoning one can define the module of $n\text{-dimensional}$ vectors over $R\text{.}$