Theorems · Theorem · category theory

CategoryTheory.PreGaloisCategory.exists_lift_of_continuous

∀ {C : Type u₁} [inst : CategoryTheory.Category.{u₂, u₁} C] {F : CategoryTheory.Functor C FintypeCat}
  [inst_1 : CategoryTheory.GaloisCategory C] [CategoryTheory.PreGaloisCategory.FiberFunctor F]
  (X : Action FintypeCat (CategoryTheory.Aut F)) [inst_3 : TopologicalSpace X.V.obj] [DiscreteTopology X.V.obj]
  [ContinuousSMul (CategoryTheory.Aut F) X.V.obj],
  ∃ A, Nonempty ((CategoryTheory.PreGaloisCategory.functorToAction F).obj A ≅ X)

If X is a finite, discrete Aut F-set with continuous Aut F-action, then there exists A : C such that F.obj A ≅ X as Aut F-sets.

Defined in

Mathlib.CategoryTheory.Galois.EssSurj

Cited by

0 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.GaloisCategoryCategoryTheory.PreGaloisCategory.FiberFunctorTopologicalSpaceDiscreteTopologyContinuousSMul