Fiber functors are (faithfully) full

Any (fiber) functor F : C ⥤ FintypeCat factors via the forgetful functor from finite Aut F-sets to finite sets. The induced functor H : C ⥤ Action FintypeCat (MonCat.of (Aut F)) is faithfully full. The faithfulness follows easily from the faithfulness of F. In this file we show that H is also full.

Main results

• PreGaloisCategory.exists_lift_of_mono: If Y is a sub-Aut F-set of F.obj X, there exists a sub-object Z of X such that F.obj Z ≅ Y as Aut F-sets.
• PreGaloisCategory.functorToAction_full: The induced functor H from above is full.

The main input for this is that the induced functor H : C ⥤ Action FintypeCat (MonCat.of (Aut F)) preserves connectedness, which translates to the fact that Aut F acts transitively on the fibers of connected objects.

Implementation details

We only show this for small categories, because the preservation of connectedness result as it is currently in Mathlib is only shown for (C : Type u₁) [Category.{u₂} C] (F : C ⥤ FintypeCat.{u₂}) and by the definition of Action, this forces u₁ = u₂ for the definition of functorToAction. Mathematically there should be no obstruction to generalizing the results of this file to arbitrary universes.

theorem CategoryTheory.PreGaloisCategory.exists_lift_of_mono_of_isConnected {C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor C FintypeCat) [CategoryTheory.GaloisCategory C] [CategoryTheory.PreGaloisCategory.FiberFunctor F] (X : C) (Y : Action FintypeCat (MonCat.of (CategoryTheory.Aut F))) (i : Y ⟶ (CategoryTheory.PreGaloisCategory.functorToAction F).obj X) [CategoryTheory.Mono i] [CategoryTheory.PreGaloisCategory.IsConnected Y] : ∃ (Z : C) (f : Z ⟶ X) (u : Y ≅ (CategoryTheory.PreGaloisCategory.functorToAction F).obj Z), 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.

theorem CategoryTheory.PreGaloisCategory.exists_lift_of_mono {C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor C FintypeCat) [CategoryTheory.GaloisCategory C] [CategoryTheory.PreGaloisCategory.FiberFunctor F] (X : C) (Y : Action FintypeCat (MonCat.of (CategoryTheory.Aut F))) (i : Y ⟶ (CategoryTheory.PreGaloisCategory.functorToAction F).obj X) [CategoryTheory.Mono i] : ∃ (Z : C) (f : Z ⟶ X) (u : Y ≅ (CategoryTheory.PreGaloisCategory.functorToAction F).obj Z), CategoryTheory.Mono f ∧ CategoryTheory.CategoryStruct.comp u.hom ((CategoryTheory.PreGaloisCategory.functorToAction F).map f) = i

Let X be an object of a Galois category with fiber functor F and Y a sub-Aut F-set of F.obj X. Then there exists a sub-object Z of X and an isomorphism Y ≅ F.obj X as Aut F-sets such that the obvious triangle commutes.

instance CategoryTheory.PreGaloisCategory.functorToAction_full {C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor C FintypeCat) [CategoryTheory.GaloisCategory C] [CategoryTheory.PreGaloisCategory.FiberFunctor F] : (CategoryTheory.PreGaloisCategory.functorToAction F).Full

The by a fiber functor F : C ⥤ FintypeCat induced functor functorToAction F to finite Aut F-sets is full.