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-09-15.
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 M
can act on a
set A
by a
monoid homomorphism hom M (A → A)
.
Definition
Monoid actions
Monoid-Action : {l1 : Level} (l : Level) (M : Monoid l1) → UU (l1 ⊔ lsuc l) Monoid-Action l M = Σ (Set l) (λ X → type-hom-Monoid M (endo-Monoid X)) module _ {l1 l2 : Level} (M : Monoid l1) (X : Monoid-Action l2 M) where set-Monoid-Action : Set l2 set-Monoid-Action = pr1 X type-Monoid-Action : UU l2 type-Monoid-Action = type-Set set-Monoid-Action is-set-type-Monoid-Action : is-set type-Monoid-Action is-set-type-Monoid-Action = is-set-type-Set set-Monoid-Action mul-Monoid-Action : type-Monoid M → type-Monoid-Action → type-Monoid-Action mul-Monoid-Action = pr1 (pr1 (pr2 X)) ap-mul-Monoid-Action : {m : type-Monoid M} {x y : type-Monoid-Action} → Id x y → Id (mul-Monoid-Action m x) (mul-Monoid-Action m y) ap-mul-Monoid-Action {m} = ap (mul-Monoid-Action m) ap-mul-Monoid-Action' : {m n : type-Monoid M} (p : Id m n) {x : type-Monoid-Action} → Id (mul-Monoid-Action m x) (mul-Monoid-Action n x) ap-mul-Monoid-Action' p {x} = ap (λ t → mul-Monoid-Action t x) p associative-mul-Monoid-Action : (x y : type-Monoid M) (z : type-Monoid-Action) → Id ( mul-Monoid-Action (mul-Monoid M x y) z) ( mul-Monoid-Action x (mul-Monoid-Action y z)) associative-mul-Monoid-Action x y = htpy-eq (pr2 (pr1 (pr2 X)) x y) unit-law-mul-Monoid-Action : (x : type-Monoid-Action) → Id (mul-Monoid-Action (unit-Monoid M) x) x unit-law-mul-Monoid-Action = htpy-eq (pr2 (pr2 X))
Recent changes
- 2023-09-15. Fredrik Bakke. Define representations of monoids (#765).
- 2023-06-10. Egbert Rijke and Fredrik Bakke. Cleaning up synthetic homotopy theory (#649).
- 2023-05-22. Fredrik Bakke, Victor Blanchi, Egbert Rijke and Jonathan Prieto-Cubides. Pre-commit stuff (#627).
- 2023-03-18. Egbert Rijke and Maša Žaucer. Central elements in semigroups, monoids, groups, semirings, and rings; ideals; nilpotent elements in semirings, rings, commutative semirings, and commutative rings; the nilradical of a commutative ring (#516).
- 2023-03-14. Fredrik Bakke. Remove all unused imports (#502).