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, -enriched functors into the category .
For silly formalisation reasons, when defining modules, we do not take βan -functor into β as the definition: this correspondence is a theorem we prove later. Instead, we set up -modules as typical algebraic structures, as data (and property) attached to a type.
The structure of an -module 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 βs 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 -modules is the linear map; in case we need to make the base ring clear, we shall call them -linear maps. Since the structure of -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 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}) 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 -module 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 -category with a single object, this construction corresponds to the functor β the βYoneda embeddingβ of βs unique object. Stretching the analogy, we refer to -as-an--module as the βrepresentableβ -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 as the space of β1-dimensional vectorsβ over itself. Following this line of reasoning one can define the module of -dimensional 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 ) 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