# Stabilizers of concrete group actions

Content created by Egbert Rijke, Fredrik Bakke, Jonathan Prieto-Cubides, Julian KG, fernabnor and louismntnu.

Created on 2022-07-09.

module group-theory.stabilizer-groups-concrete-group-actions where

Imports
open import foundation.0-connected-types
open import foundation.dependent-pair-types
open import foundation.function-types
open import foundation.mere-equality
open import foundation.propositional-truncations
open import foundation.sets
open import foundation.subtypes
open import foundation.type-arithmetic-dependent-pair-types
open import foundation.universe-levels

open import group-theory.concrete-group-actions
open import group-theory.concrete-groups
open import group-theory.subgroups-concrete-groups
open import group-theory.transitive-concrete-group-actions


## Idea

The stabilizer of an element x : X point of a concrete G-set X : BG → Set is the connected component of point , x in the type of orbits of X. Its loop space is indeed the type of elements g : G such that g x = x.

## Definition

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

action-stabilizer-action-Concrete-Group :
type-action-Concrete-Group G X → action-Concrete-Group (l1 ⊔ l2) G
action-stabilizer-action-Concrete-Group x u =
set-subset
( X u)
( λ y → mere-eq-Prop (shape-Concrete-Group G , x) (u , y))

is-transitive-action-stabilizer-action-Concrete-Group :
(x : type-action-Concrete-Group G X) →
is-transitive-action-Concrete-Group G
( action-stabilizer-action-Concrete-Group x)
is-transitive-action-stabilizer-action-Concrete-Group x =
is-0-connected-equiv'
( associative-Σ
( classifying-type-Concrete-Group G)
( type-Set ∘ X)
( mere-eq (shape-Concrete-Group G , x)))
( is-0-connected-mere-eq
( ( shape-Concrete-Group G , x) ,
( refl-mere-eq (shape-Concrete-Group G , x)))
( λ (uy , p) →
apply-universal-property-trunc-Prop p
( mere-eq-Prop
( ( shape-Concrete-Group G , x) ,
( refl-mere-eq (shape-Concrete-Group G , x)))
( uy , p))
( λ q →
unit-trunc-Prop
( eq-type-subtype
( mere-eq-Prop (shape-Concrete-Group G , x))
( q)))))

subgroup-stabilizer-action-Concrete-Group :
(x : type-action-Concrete-Group G X) → subgroup-Concrete-Group (l1 ⊔ l2) G
pr1 (pr1 (subgroup-stabilizer-action-Concrete-Group x)) =
action-stabilizer-action-Concrete-Group x
pr2 (pr1 (subgroup-stabilizer-action-Concrete-Group x)) =
is-transitive-action-stabilizer-action-Concrete-Group x
pr1 (pr2 (subgroup-stabilizer-action-Concrete-Group x)) = x
pr2 (pr2 (subgroup-stabilizer-action-Concrete-Group x)) =
refl-mere-eq (shape-Concrete-Group G , x)