module Algebra.Ring.Module.Action where
Modules as actionsπ
While the record Module-on
expresses the possible
-module
structures on a type
,
including the scalar multiplication and the addition making
into an abelian
group, itβs sometimes fruitful to consider the
-module
structures on an abelian group
,
which is then regarded as an indivisible unit.
The difference is in the quantification: the latter perspective, developed in this module, allows us to βfixβ the addition, and let only the scalar multiplication vary. The ordinary definition of -module, which is consistent with our other algebraic structures, only allows us to vary the underlying type (and the base ring).
module _ {β} (R : Ring β) where private module R = Ring-on (R .snd) open Additive-notation β¦ ... β¦
record Ring-action {βg} {T : Type βg} (G : Abelian-group-on T) : Type (β β βg) where instance _ = G field _β_ : β R β β T β T β-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
We refer to an β-module structure on an abelian group β as a ring action of on , for short. The definition is unsurprising: we bundle the scalar multiplication together with the proofs that this is, indeed, an -module structure.
ActionβModule-on : β {βg} {T : Type βg} {G : Abelian-group-on T} β Ring-action G β Module-on R T ActionβModule : β {βg} (G : Abelian-group βg) β Ring-action (G .snd) β Module R βg ActionβModule-on {G = G} act = mod where instance _ = G mod : Module-on R _ mod .Module-on._+_ = _ mod .Module-on._β_ = act .Ring-action._β_ mod .Module-on.has-is-mod = record { has-is-ab = G .Abelian-group-on.has-is-ab ; Ring-action act } ActionβModule G act .fst = G .fst ActionβModule G act .snd = ActionβModule-on act
The reason for allowing the extra dimension in quantification is the following theorem: There is an equivalence between actions of on and ring morphisms into the endomorphism ring of .
ActionβHom : (G : Abelian-group β) β Ring-action (G .snd) β Rings.Hom R (Endo Ab-ab-category G) HomβAction : (G : Abelian-group β) β Rings.Hom R (Endo Ab-ab-category G) β Ring-action (G .snd)
HomβAction G rhom .Ring-action._β_ x y = rhom # x # y HomβAction G rhom .Ring-action.β-distribl r x y = rhom .hom r .preserves .is-group-hom.pres-β _ _ HomβAction G rhom .Ring-action.β-distribr r s x = rhom .preserves .is-ring-hom.pres-+ r s #β x HomβAction G rhom .Ring-action.β-assoc r s x = sym (rhom .preserves .is-ring-hom.pres-* r s #β x) HomβAction G rhom .Ring-action.β-id x = rhom .preserves .is-ring-hom.pres-id #β x ActionβHom G act .hom r .hom = act .Ring-action._β_ r ActionβHom G act .hom r .preserves .is-group-hom.pres-β x y = act .Ring-action.β-distribl r x y ActionβHom G act .preserves .is-ring-hom.pres-id = Homomorphism-path Ξ» i β act .Ring-action.β-id _ ActionβHom G act .preserves .is-ring-hom.pres-+ x y = Homomorphism-path Ξ» i β act .Ring-action.β-distribr _ _ _ ActionβHom G act .preserves .is-ring-hom.pres-* r s = Homomorphism-path Ξ» x β sym (act .Ring-action.β-assoc _ _ _) ActionβHom : (G : Abelian-group β) β Ring-action (G .snd) β Rings.Hom R (Endo Ab-ab-category G) ActionβHom G = IsoβEquiv $ ActionβHom G , iso (HomβAction G) (Ξ» x β Homomorphism-path Ξ» _ β refl) (Ξ» x β refl)