Theorems · Definition · category theory

CategoryTheory.FintypeCat.isoQuotientStabilizerOfIsConnected

{G : Type u} →
  [inst : Group G] →
    (X : Action FintypeCat G) →
      [CategoryTheory.PreGaloisCategory.IsConnected X] →
        (x : X.V.obj) →
          [inst_2 : Fintype (G ⧸ MulAction.stabilizer G x)] →
            X ≅ Action.FintypeCat.ofMulAction G (FintypeCat.of (G ⧸ MulAction.stabilizer G x))

If X is a connected G-set and x is an element of X, X is isomorphic to the quotient of G by the stabilizer of x as G-sets.

Defined in

Mathlib.CategoryTheory.Galois.Examples

Cited by

1 results in Mathlib

Foundations

Depth 84 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

GroupCategoryTheory.PreGaloisCategory.IsConnectedFintype