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 is an abelian group equipped with an action by . 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

For silly formalisation reasons, when defining modules, we do not take βan into β as the definition: this correspondence is a theorem we prove later. Instead, we set up as typical algebraic structures, as data (and property) attached to a type.

The structure of an on a type consists of an addition and a scalar multiplication In prose, we generally omit the star, writing rather than the wordlier These must satisfy the following properties:

• makes 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 onto endomorphism ring. In other words, we have:

• and
  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 is the linear map; in case we need to make the base ring clear, we shall call them maps. Since the structure of 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 and standard lemmas about group homomorphisms ensure that will also preserve negation, and, more importantly, zero. We can then derive that preserves the scalar multiplication, by calculating  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 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}) R-ModβͺSets : β βm β Functor (R-Mod βm) (Sets βm) R-ModβͺSets _ = 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 is.. 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 as an with a single object, this construction corresponds to the functor β the βYoneda embeddingβ of unique object. Stretching the analogy, we refer to as the βrepresentableβ  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 as the space of β1-dimensional vectorsβ over itself. Following this line of reasoning one can define the module of vectors over -- 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 ; H-Level-is-linear-map ; H-Level-is-module ; H-Level-Linear-map ) 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 ; H-Level-is-linear-map ; H-Level-is-module ; H-Level-Linear-map ) public instance Extensional-linear-map : β {βr} {M : Module R βm} {N : Module R βn} β β¦ ext : Extensional (β M β β β N β) βr β¦ β Extensional (Linear-map M N) βr Extensional-linear-map β¦ ext β¦ = injectionβextensional! (Ξ» p β Linear-map-path (happly p)) ext 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 extensional-mod-hom : β {β βrel} {R : Ring β} {M : Module R βm} {N : Module R βm} β β¦ ext : Extensional (Linear-map M N) βrel β¦ β Extensional (R-Mod R _ .Precategory.Hom M N) βrel extensional-mod-hom β¦ ei β¦ = injectionβextensional! {f = homβlinear-map} (Ξ» p β ext Ξ» e β ap map p$β e) ei

instance Extensional-mod-hom = extensional-mod-hom
{-# OVERLAPS Extensional-mod-hom #-}