Monoid actions

Content created by Egbert Rijke, Fredrik Bakke, Jonathan Prieto-Cubides, Maša Žaucer and Victor Blanchi.

Created on 2022-05-08.
Last modified on 2023-11-24.

module group-theory.monoid-actions where
open import foundation.action-on-identifications-functions
open import foundation.dependent-pair-types
open import foundation.endomorphisms
open import foundation.function-extensionality
open import foundation.identity-types
open import foundation.sets
open import foundation.universe-levels

open import group-theory.homomorphisms-monoids
open import group-theory.monoids


A monoid action of a monoid M on a set X is a monoid homomorphism from M into the monoid of endomorphisms X → X. The fact that monoid homomorphisms preserve the monoid operation and the unit implies that a monoid action μ of M on X satisfies the following laws:

  μ mn x = μ m (μ n x)
   μ 1 x = x.


Monoid actions

action-Monoid : {l1 : Level} (l : Level) (M : Monoid l1)  UU (l1  lsuc l)
action-Monoid l M = Σ (Set l)  X  hom-Monoid M (endo-Monoid X))

module _
  {l1 l2 : Level} (M : Monoid l1) (X : action-Monoid l2 M)

  set-action-Monoid : Set l2
  set-action-Monoid = pr1 X

  type-action-Monoid : UU l2
  type-action-Monoid = type-Set set-action-Monoid

  is-set-type-action-Monoid : is-set type-action-Monoid
  is-set-type-action-Monoid = is-set-type-Set set-action-Monoid

  mul-hom-monoid-action-Monoid : hom-Monoid M (endo-Monoid set-action-Monoid)
  mul-hom-monoid-action-Monoid = pr2 X

  mul-action-Monoid : type-Monoid M  type-action-Monoid  type-action-Monoid
  mul-action-Monoid =
    map-hom-Monoid M
      ( endo-Monoid set-action-Monoid)
      ( mul-hom-monoid-action-Monoid)

  ap-mul-action-Monoid :
    {m : type-Monoid M} {x y : type-action-Monoid} 
    x  y  mul-action-Monoid m x  mul-action-Monoid m y
  ap-mul-action-Monoid {m} = ap (mul-action-Monoid m)

  ap-mul-action-Monoid' :
    {m n : type-Monoid M} (p : m  n) {x : type-action-Monoid} 
    mul-action-Monoid m x  mul-action-Monoid n x
  ap-mul-action-Monoid' p {x} = ap  t  mul-action-Monoid t x) p

  associative-mul-action-Monoid :
    (x y : type-Monoid M) (z : type-action-Monoid) 
    mul-action-Monoid (mul-Monoid M x y) z 
    mul-action-Monoid x (mul-action-Monoid y z)
  associative-mul-action-Monoid x y =
      ( preserves-mul-hom-Monoid M
        ( endo-Monoid set-action-Monoid)
        ( mul-hom-monoid-action-Monoid))

  unit-law-mul-action-Monoid :
    (x : type-action-Monoid)  mul-action-Monoid (unit-Monoid M) x  x
  unit-law-mul-action-Monoid =
      ( preserves-unit-hom-Monoid M
        ( endo-Monoid set-action-Monoid)
        ( mul-hom-monoid-action-Monoid))

Recent changes