Theorems · Definition · category theory

CategoryTheory.PreGaloisCategory.fiberIsoQuotientStabilizer

{C : Type u₁} →
  [inst : CategoryTheory.Category.{u₂, u₁} C] →
    {F : CategoryTheory.Functor C FintypeCat} →
      [inst_1 : CategoryTheory.GaloisCategory C] →
        [CategoryTheory.PreGaloisCategory.FiberFunctor F] →
          (X : C) →
            [CategoryTheory.PreGaloisCategory.IsConnected X] →
              (x : (F.obj X).obj) →
                (CategoryTheory.PreGaloisCategory.functorToAction F).obj X ≅
                  Action.FintypeCat.ofMulAction (CategoryTheory.Aut F)
                    (FintypeCat.of (CategoryTheory.Aut F ⧸ MulAction.stabilizer (CategoryTheory.Aut F) x))

If X is connected and x is in the fiber of X, F.obj X is isomorphic to the quotient of Aut F by the stabilizer of x as Aut F-sets.

Defined in

Mathlib.CategoryTheory.Galois.EssSurj

Cited by

1 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.GaloisCategoryCategoryTheory.PreGaloisCategory.FiberFunctorCategoryTheory.PreGaloisCategory.IsConnected