Theorems · Theorem · category theory

CategoryTheory.PreGaloisCategory.exists_lift_of_quotient_openSubgroup

∀ {C : Type u₁} [inst : CategoryTheory.Category.{u₂, u₁} C] {F : CategoryTheory.Functor C FintypeCat}
  [inst_1 : CategoryTheory.GaloisCategory C] [CategoryTheory.PreGaloisCategory.FiberFunctor F]
  (V : OpenSubgroup (CategoryTheory.Aut F)),
  ∃ X,
    Nonempty
      ((CategoryTheory.PreGaloisCategory.functorToAction F).obj X ≅
        Action.FintypeCat.ofMulAction (CategoryTheory.Aut F) (FintypeCat.of (CategoryTheory.Aut F ⧸ ↑V)))

For every open subgroup V of Aut F, there exists an X : C such that F.obj X ≅ Aut F ⧸ V as Aut F-sets.

Defined in

Mathlib.CategoryTheory.Galois.EssSurj

Cited by

1 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.GaloisCategoryCategoryTheory.PreGaloisCategory.FiberFunctor