Principal group actions

Content created by Fredrik Bakke, Jonathan Prieto-Cubides, Egbert Rijke and Elisabeth Stenholm.

Created on 2022-03-17.
Last modified on 2023-11-24.

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-action-Group : action-Group G l1
  pr1 principal-action-Group = set-Group G
  pr1 (pr2 principal-action-Group) g = equiv-mul-Group G g
  pr2 (pr2 principal-action-Group) {g} {h} =
    eq-htpy-equiv (associative-mul-Group G g h)

Recent changes