Theorems · Theorem · category theory

CategoryTheory.PreGaloisCategory.exists_hom_from_galois_of_fiber_nonempty

∀ {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),
  Nonempty (F.obj X).obj → ∃ A x, CategoryTheory.PreGaloisCategory.IsGalois A

Any object with non-empty fiber admits a hom from a Galois object.

Defined in

Mathlib.CategoryTheory.Galois.Decomposition

Cited by

2 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.GaloisCategoryCategoryTheory.PreGaloisCategory.FiberFunctor