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
Imports 
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

Idea

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.

Definition

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

  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 =
    htpy-eq
      ( 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 =
    htpy-eq
      ( preserves-unit-hom-Monoid M
        ( endo-Monoid set-action-Monoid)
        ( mul-hom-monoid-action-Monoid))

Recent changes