Theorems · Theorem · category theory

CategoryTheory.PreGaloisCategory.exists_galois_representative

∀ {C : Type u₁} [inst : CategoryTheory.Category.{u₂, u₁} C] [inst_1 : CategoryTheory.GaloisCategory C]
  (F : CategoryTheory.Functor C FintypeCat) [CategoryTheory.PreGaloisCategory.FiberFunctor F] (X : C),
  ∃ A a,
    CategoryTheory.PreGaloisCategory.IsGalois A ∧
      Function.Bijective fun f => (CategoryTheory.ConcreteCategory.hom (F.map f)) a

The fiber of any object in a Galois category is represented by a Galois object.

Defined in

Mathlib.CategoryTheory.Galois.Decomposition

Cited by

2 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.GaloisCategoryCategoryTheory.PreGaloisCategory.FiberFunctor