Theorems · Theorem · category theory

CategoryTheory.PreGaloisCategory.exists_hom_from_galois_of_fiber

∀ {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)
  (x : (F.obj X).obj),
  ∃ A f a, CategoryTheory.PreGaloisCategory.IsGalois A ∧ (CategoryTheory.ConcreteCategory.hom (F.map f)) a = x

Any element in the fiber of an object X is the evaluation of a morphism from a Galois object.

Defined in

Mathlib.CategoryTheory.Galois.Decomposition

Cited by

3 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.GaloisCategoryCategoryTheory.PreGaloisCategory.FiberFunctor