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

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

module Algebra.Ring.Module.Action where


# Modules as actionsπ

While the record Module-on expresses the possible structures on a type including the scalar multiplication and the addition making into an abelian group, itβs sometimes fruitful to consider the 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 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)

  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 β 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 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 # 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 β trivial!) (Ξ» x β refl)