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).

  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.

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)