This is an archived version pinned as of the submission of my master's thesis. An up-to-date version may be found online.

Stabilizer groups

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)