Principal group actions
Content created by Fredrik Bakke, Jonathan Prieto-Cubides, Egbert Rijke and Elisabeth Bonnevier.
Created on 2022-03-17.
Last modified on 2023-03-13.
module group-theory.principal-group-actions where
Imports
open import foundation.dependent-pair-types open import foundation.equivalence-extensionality open import foundation.universe-levels open import group-theory.group-actions open import group-theory.groups
Idea
The principal group action is the action of a group on itself by multiplication from the left
Definition
module _ {l1 : Level} (G : Group l1) where principal-Abstract-Group-Action : Abstract-Group-Action G l1 pr1 principal-Abstract-Group-Action = set-Group G pr1 (pr2 principal-Abstract-Group-Action) g = equiv-mul-Group G g pr2 (pr2 principal-Abstract-Group-Action) g h = eq-htpy-equiv (associative-mul-Group G g h)
Recent changes
- 2023-03-13. Jonathan Prieto-Cubides. More maintenance (#506).
- 2023-03-10. Fredrik Bakke. Additions to
fix-import
(#497). - 2023-03-09. Jonathan Prieto-Cubides. Add hooks (#495).
- 2023-03-07. Fredrik Bakke. Add blank lines between
<details>
tags and markdown syntax (#490). - 2023-03-07. Jonathan Prieto-Cubides. Show module declarations (#488).