module Algebra.Ring.Module.Action where

Modules as actions🔗

While the record Module-on expresses the possible $R$ -module structures on a type $T$ , including the scalar multiplication and the addition making $T$ into an abelian group, it’s sometimes fruitful to consider the $R$ -module structures on an abelian group $G$ , 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 $R$ -module, 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 “ $R$ -module structure on an abelian group $G$ ” as a ring action of $R$ on $G$ , for short. The definition is unsurprising: we bundle the scalar multiplication together with the proofs that this is, indeed, an $R$ -module structure.

The reason for allowing the extra dimension in quantification is the following theorem: There is an equivalence between actions of $R$ on $G$ and ring morphisms $R \to [G,G]$ into the endomorphism ring of $G$ .

  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)