Stabilizer groups

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

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

module group-theory.stabilizer-groups where
open import foundation.dependent-pair-types
open import foundation.identity-types
open import foundation.universe-levels

open import
open import group-theory.groups


Given a G-set X, the stabilizer group at an element x of X is the subgroup of elements g of G that keep x fixed.


module _
  {l1 l2 : Level} (G : Group l1) (X : action-Group G l2)

  type-stabilizer-action-Group : type-action-Group G X  UU (l1  l2)
  type-stabilizer-action-Group x =
    Σ (type-Group G)  g  mul-action-Group G X g x  x)

Recent changes