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 (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 (Aut F) preserves connectedness, which translates to the fact that Aut F acts transitively on the fibers of connected objects.

theorem CategoryTheory.PreGaloisCategory.exists_lift_of_mono_of_isConnected {C : Type u_1} [Category.{u_2, u_1} C] (F : Functor C FintypeCat) [GaloisCategory C] [FiberFunctor F] (X : C) (Y : Action FintypeCat (Aut F)) (i : Y ⟶ (functorToAction F).obj X) [Mono i] [IsConnected Y] : ∃ (Z : C) (f : Z ⟶ X) (u : Y ≅ (functorToAction F).obj Z), IsConnected Z ∧ Mono f ∧ i = CategoryStruct.comp u.hom ((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_1} [Category.{u_2, u_1} C] (F : Functor C FintypeCat) [GaloisCategory C] [FiberFunctor F] (X : C) (Y : Action FintypeCat (Aut F)) (i : Y ⟶ (functorToAction F).obj X) [Mono i] : ∃ (Z : C) (f : Z ⟶ X) (u : Y ≅ (functorToAction F).obj Z), Mono f ∧ CategoryStruct.comp u.hom ((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_1} [Category.{u_2, u_1} C] (F : Functor C FintypeCat) [GaloisCategory C] [FiberFunctor F] : (functorToAction F).Full

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