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

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 “$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.

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