# Monoid actions

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

Created on 2022-05-08.

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