open import Algebra.Group.Notation
open import Algebra.Group.Ab
open import Algebra.Group
open import Algebra.Ring

open import Cat.Displayed.Univalence.Thin
open import Cat.Prelude hiding (_+_)

import Cat.Reasoning

module Algebra.Ring.Module where

private variable
  β„“m β„“n : Level
  S T : Type β„“m

private module Mod {β„“} (R : Ring β„“) where
  private module R = Ring-on (R .snd)
  open Displayed
  open Total-hom
  open Functor

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, Ab\mathbf{Ab}-enriched 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 set up RR-modules as typical algebraic structures, as data (and property) attached to a type.

The structure of an RR-module on a type TT consists of an addition +:TΓ—Tβ†’T+ : T \times T \to T and a scalar multiplication ⋆:RΓ—Tβ†’T\star : R \times T \to T. In prose, we generally omit the star, writing rxrx rather than the wordlier r⋆xr \star x. These must satisfy the following properties:

  • ++ makes TT into an abelian group. Since we’ve already defined abelian groups, we can take this entire property as β€œindivisible”, saving some effort.

  • β‹…Β· is a ring homomorphism of RR onto (T,+)(T, +)’s endomorphism ring. In other words, we have:

    • 1x=x1x = x;
    • (rs)β‹…x=rβ‹…(sβ‹…x)(rs) \cdot x = r \cdot (s \cdot x);
    • (r+s)x=rx+sx(r + s)x = rx + sx; and
    • r(x+y)=rx+ryr(x + y) = rx + ry.
  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

    private
      ug : Group-on _
      ug = record { has-is-group = is-abelian-group.has-is-group has-is-ab }

    module ab = Additive-notation ug
    private module ab' = is-abelian-group has-is-ab renaming (commutes to +-comm)

    open ab using (-_ ; 0g ; +-invr ; +-invl ; +-assoc ; +-idl ; +-idr ; neg-0 ; neg-comm ; neg-neg ; has-is-set) public
    open ab' using (+-comm) public

    abstract
      ⋆-is-group-hom : βˆ€ {r} β†’ is-group-hom ug ug (r ⋆_)
      ⋆-is-group-hom .is-group-hom.pres-⋆ x y = ⋆-distribl _ x y

    private module ⋆gh {r} = is-group-hom (⋆-is-group-hom {r}) renaming (pres-id to ⋆-idr ; pres-inv to ⋆-invr)
    open ⋆gh public using (⋆-idr ; ⋆-invr)

  private unquoteDecl eqv = declare-record-iso eqv (quote is-module)

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-on→Group-on
    : βˆ€ {β„“m} {T : Type β„“m}
    β†’ Module-on T
    β†’ Group-on T
  Module-on→Group-on M = record { has-is-group = is-abelian-group.has-is-group (Module-on.has-is-ab M) }

  Module-on→Abelian-group-on
    : βˆ€ {β„“m} {T : Type β„“m}
    β†’ Module-on T
    β†’ Abelian-group-on T
  Module-on→Abelian-group-on M = record { has-is-ab = Module-on.has-is-ab M }

  abstract instance
    H-Level-is-module
      : βˆ€ {β„“'} {T : Type β„“'} {_+_ : T β†’ T β†’ T} {_⋆_ : ⌞ R ⌟ β†’ T β†’ T} {n}
      β†’ H-Level (is-module _+_ _⋆_) (suc n)
    H-Level-is-module {T = T} = prop-instance $ Ξ» x β†’
      let
        instance
          _ : H-Level T 2
          _ = basic-instance 2 (is-module.has-is-set x)
      in Iso→is-hlevel 1 eqv (hlevel 1) x

  open Module-on ⦃ ... ⦄ hiding (has-is-set)

  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 RR-modules is the linear map; in case we need to make the base ring RR clear, we shall call them RR-linear maps. Since the structure of RR-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:

    no-eta-equality
    private instance
      _ = M
      _ = N

    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

f(a+b)=f(1a+b)=1f(a)+f(b)=f(a)+f(b), f(a+b) = f(1a+b) = 1f(a)+f(b) = f(a)+f(b)\text{,}

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

f(ra)=f(ra+0)=rf(a)+f(0)=rf(a)+0=rf(a). f(ra) = f(ra + 0) = rf(a) + f(0) = rf(a) + 0 = rf(a)\text{.} 

    abstract
      has-is-gh : is-group-hom (Module-on→Group-on M) (Module-on→Group-on N) f
      has-is-gh .is-group-hom.pres-⋆ x y = ap f (apβ‚‚ _+_ (sym (⋆-id _)) refl) βˆ™ linear _ _ _ βˆ™ apβ‚‚ _+_ (⋆-id _) refl

    open is-group-hom has-is-gh
      renaming ( pres-⋆ to pres-+ ; pres-id to pres-0 ; pres-inv to pres-neg)
      public

    abstract
      pres-⋆ : βˆ€ r s β†’ f (r ⋆ s) ≑ r ⋆ f s
      pres-⋆ r s = ap f (sym +-idr) βˆ™ linear _ _ _ βˆ™ ap (r ⋆ f s +_) pres-0 βˆ™ +-idr

  private unquoteDecl eqv' = declare-record-iso eqv' (quote is-linear-map)
  open is-linear-map using (linear) public

  -- There are too many possible instances in scope for instance search
  -- to solve this one, but fortunately it's pretty short:

  abstract
    is-linear-map-is-prop
      : βˆ€ {M : Module-on T} {N : Module-on S} {f : T β†’ S}
      β†’ is-prop (is-linear-map f M N)
    is-linear-map-is-prop {S = S} {N = N} =
      Iso→is-hlevel 1 eqv' $
      Ξ -is-hlevelΒ³ 1 Ξ» _ _ _ β†’
      Module-on.ab.has-is-set N _ _

    instance
      H-Level-is-linear-map
        : βˆ€ {M : Module-on T} {N : Module-on S} {f : T β†’ S} {n}
        β†’ H-Level (is-linear-map f M N) (suc n)
      H-Level-is-linear-map = prop-instance is-linear-map-is-prop

  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-Mod{R}\text{-}\mathbf{Mod}. R-Mod{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.

  private unquoteDecl eqv'' = declare-record-iso eqv'' (quote Linear-map)
  abstract
    Linear-map-is-set
      : βˆ€ {β„“' β„“''} {M : Module β„“'} {N : Module β„“''}
      β†’ is-set (Linear-map M N)
    Linear-map-is-set {N = N} =
      Iso→is-hlevel 2 eqv'' $
        Σ-is-hlevel 2 (fun-is-hlevel 2 (N .fst .is-tr)) λ x → is-prop→is-set (hlevel 1)

    instance
      H-Level-Linear-map
        : βˆ€ {β„“' β„“''} {M : Module β„“'} {N : Module β„“''} {n}
        β†’ H-Level (Linear-map M N) (suc (suc n))
      H-Level-Linear-map {N = N} {n = n} = basic-instance (suc (suc zero)) Linear-map-is-set

  open Linear-map public

  Linear-map-path
    : βˆ€ {M : Module β„“m} {N : Module β„“n} {f g : Linear-map M N}
    β†’ (βˆ€ x β†’ f .map x ≑ g .map x)
    β†’ f ≑ g
  Linear-map-path p i .map x = p x i
  Linear-map-path {M = M} {N} {f} {g} p i .lin =
    is-prop→pathp (λ i → hlevel {T = is-linear-map (λ x → p x i) (M .snd) (N .snd)} 1)
      (f .lin) (g .lin) i

  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

  R-Mod : βˆ€ β„“m β†’ Precategory (lsuc β„“m βŠ” β„“) (β„“m βŠ” β„“)
  R-Mod β„“m = Structured-objects (R-Mod-structure {β„“m})

  Forget-module : βˆ€ β„“m β†’ Functor (R-Mod β„“m) (Sets β„“m)
  Forget-module _ = Forget-structure R-Mod-structure

  record make-module {β„“m} (M : Type β„“m) : Type (β„“m βŠ” β„“) where
    field
      has-is-set : is-set M
      _+_ : M β†’ M β†’ M
      inv : M β†’ M
      0g  : M

      +-assoc : βˆ€ x y z β†’ x + (y + z) ≑ (x + y) + z
      +-invl  : βˆ€ x β†’ inv x + x ≑ 0g
      +-idl   : βˆ€ x β†’ 0g + x ≑ x
      +-comm  : βˆ€ x y β†’ x + y ≑ y + x

      _⋆_ : ⌞ R ⌟ β†’ M β†’ M

      ⋆-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

  to-module-on : βˆ€ {β„“m} {M : Type β„“m} β†’ make-module M β†’ Module-on M
  to-module-on m .Module-on._+_ = make-module._+_ m
  to-module-on m .Module-on._⋆_ = make-module._⋆_ m
  to-module-on m .Module-on.has-is-mod = mod where
    gr : Group-on _
    gr = to-group-on Ξ» where
      .make-group.group-is-set β†’ make-module.has-is-set m
      .make-group.unit β†’ make-module.0g m
      .make-group.mul β†’ make-module._+_ m
      .make-group.inv β†’ make-module.inv m
      .make-group.assoc β†’ make-module.+-assoc m
      .make-group.invl β†’ make-module.+-invl m
      .make-group.idl β†’ make-module.+-idl m

    mod : is-module _ _
    mod .is-module.has-is-ab .is-abelian-group.has-is-group = gr .Group-on.has-is-group
    mod .is-module.has-is-ab .is-abelian-group.commutes = make-module.+-comm m _ _
    mod .is-module.⋆-distribl = make-module.⋆-distribl m
    mod .is-module.⋆-distribr = make-module.⋆-distribr m
    mod .is-module.⋆-assoc = make-module.⋆-assoc m
    mod .is-module.⋆-id = make-module.⋆-id m

  to-module : βˆ€ {β„“m} {M : Type β„“m} β†’ make-module M β†’ Module β„“m
  ∣ to-module m .fst ∣ = _
  to-module m .fst .is-tr = make-module.has-is-set m
  to-module m .snd = to-module-on m

β€œRepresentable” modulesπŸ”—

A prototypical example of RR-module is.. RR 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 RR as an Ab\mathbf{Ab}-category with a single object, this construction corresponds to the functor HomR(βˆ’,βˆ™)\mathbf{Hom}_R(-,\bull) β€” the β€œYoneda embedding” of RR’s unique object. Stretching the analogy, we refer to RR-as-an-RR-module as the β€œrepresentable” RR-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 RR as the space of β€œ1-dimensional vectors” over itself. Following this line of reasoning one can define the module of nn-dimensional vectors over RR.

-- Hide the constructions that take the base ring as an explicit
-- argument:
open Mod
  hiding
    ( Linear-map
    ; Linear-map-path
    ; is-linear-map
    ; to-module
    ; to-module-on
    ; Module-on→Group-on
    ; Module-on→Abelian-group-on
    )
  public

-- And open them here where R is implicit instead:
module _ {β„“} {R : Ring β„“} where
  open Mod R
    using
      ( Linear-map
      ; Linear-map-path
      ; is-linear-map
      ; to-module
      ; to-module-on
      ; Module-on→Group-on
      ; Module-on→Abelian-group-on
      )
    public

module R-Mod {β„“ β„“m} {R : Ring β„“} = Cat.Reasoning (R-Mod R β„“m)

hom→linear-map
  : βˆ€ {β„“ β„“m} {R : Ring β„“} {M N : Module R β„“m}
  β†’ R-Mod.Hom M N
  β†’ Linear-map M N
hom→linear-map h .map = h .hom
hom→linear-map h .lin = h .preserves

linear-map→hom
  : βˆ€ {β„“ β„“m} {R : Ring β„“} {M N : Module R β„“m}
  β†’ Linear-map M N
  β†’ R-Mod.Hom M N
linear-map→hom h .hom       = h .map
linear-map→hom h .preserves = h .lin