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)
  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 β€œ 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    = ext Ξ» x β†’ act .Ring-action.⋆-id _
  Actionβ†’Hom G act .preserves .is-ring-hom.pres-+ x y = ext Ξ» x β†’ act .Ring-action.⋆-distribr _ _ _
  Actionβ†’Hom G act .preserves .is-ring-hom.pres-* r s = ext Ξ» 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)