Stabilizer groups

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

Created on 2022-03-17.
Last modified on 2023-03-13.

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 : Abstract-Group-Action G l2)

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

Recent changes