Theorems · Theorem · category theory

CategoryTheory.PreGaloisCategory.exists_lift_of_mono_of_isConnected

∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (F : CategoryTheory.Functor C FintypeCat)
  [inst_1 : CategoryTheory.GaloisCategory C] [CategoryTheory.PreGaloisCategory.FiberFunctor F] (X : C)
  (Y : Action FintypeCat (CategoryTheory.Aut F)) (i : Y ⟶ (CategoryTheory.PreGaloisCategory.functorToAction F).obj X)
  [CategoryTheory.Mono i] [CategoryTheory.PreGaloisCategory.IsConnected Y],
  ∃ Z f u,
    CategoryTheory.PreGaloisCategory.IsConnected Z ∧
      CategoryTheory.Mono f ∧
        i = CategoryTheory.CategoryStruct.comp u.hom ((CategoryTheory.PreGaloisCategory.functorToAction F).map f)

Let X be an object of a Galois category with fiber functor F and Y a sub-Aut F-set of F.obj X, on which Aut F acts transitively (i.e. which is connected in the Galois category of finite Aut F-sets). Then there exists a connected sub-object Z of X and an isomorphism Y ≅ F.obj X as Aut F-sets such that the obvious triangle commutes. For a version without the connectedness assumption, see exists_lift_of_mono.

Defined in

Mathlib.CategoryTheory.Galois.Full

Cited by

1 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.GaloisCategoryCategoryTheory.PreGaloisCategory.FiberFunctorCategoryTheory.MonoCategoryTheory.PreGaloisCategory.IsConnected