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 RR-module structures on a type TT, including the scalar multiplication and the addition making TT into an abelian group, it’s sometimes fruitful to consider the RR-module structures on an abelian group GG, 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 RR-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 β€œRR-module structure on an abelian group GG” as a ring action of RR on GG, for short. The definition is unsurprising: we bundle the scalar multiplication together with the proofs that this is, indeed, an RR-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 RR on GG and ring morphisms R→[G,G]R \to [G,G] into the endomorphism ring of GG.

  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)