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)
External links
- stabilizer group at Lab
- Fixed points and stabilizer subgroups at Wikipedia
- Isotropy Group at Wolfram Mathworld
- Isotropy group at Encyclopedia of Mathematics
Recent changes
- 2023-11-24. Fredrik Bakke. The orbit category of a group (#935).
- 2023-11-24. Egbert Rijke. Abelianization (#877).
- 2023-03-13. Jonathan Prieto-Cubides. More maintenance (#506).
- 2023-03-10. Fredrik Bakke. Additions to
fix-import
(#497). - 2023-03-09. Jonathan Prieto-Cubides. Add hooks (#495).