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
Imports 
open import foundation.dependent-pair-types
open import foundation.identity-types
open import foundation.universe-levels

open import group-theory.group-actions
open import group-theory.groups

Idea

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.

Definition

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

  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