Essential surjectivity of fiber functors

Let F : C ⥤ FintypeCat be a fiber functor of a Galois category C and denote by H the induced functor C ⥤ Action FintypeCat (Aut F).

In this file we show that the essential image of H consists of the finite Aut F-sets where the Aut F action is continuous.

Main results

• exists_lift_of_quotient_openSubgroup: If U is an open subgroup of Aut F, then there exists an object X such that F.obj X is isomorphic to Aut F ⧸ U as Aut F-sets.
• exists_lift_of_continuous: If X is a finite, discrete Aut F-set, then there exists an object A such that F.obj A is isomorphic to X as Aut F-sets.

Strategy

We first show that every finite, discrete Aut F-set Y has a decomposition into connected components and each connected component is of the form Aut F ⧸ U for an open subgroup U. Since H preserves finite coproducts, it hence suffices to treat the case Y = Aut F ⧸ U. For the case Y = Aut F ⧸ U we closely follow the second part of Stacks Project Tag 0BN4.

theorem CategoryTheory.PreGaloisCategory.has_decomp_quotients {G : Type u_1} [Group G] [TopologicalSpace G] [TopologicalGroup G] [CompactSpace G] (X : Action FintypeCat (MonCat.of G)) [TopologicalSpace ↑X.V] [DiscreteTopology ↑X.V] [ContinuousSMul G ↑X.V] : ∃ (ι : Type) (x : Finite ι) (f : ι → OpenSubgroup G), Nonempty ((∐ fun (i : ι) => Action.FintypeCat.ofMulAction G (FintypeCat.of (G ⧸ ↑(f i)))) ≅ X)

If X is a finite discrete G-set, it can be written as the finite disjoint union of quotients of the form G ⧸ Uᵢ for open subgroups (Uᵢ). Note that this is simply the decomposition into orbits.

def CategoryTheory.PreGaloisCategory.fiberIsoQuotientStabilizer {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] {F : CategoryTheory.Functor C FintypeCat} [CategoryTheory.GaloisCategory C] [CategoryTheory.PreGaloisCategory.FiberFunctor F] (X : C) [CategoryTheory.PreGaloisCategory.IsConnected X] (x : ↑(F.obj X)) : (CategoryTheory.PreGaloisCategory.functorToAction F).obj X ≅ Action.FintypeCat.ofMulAction (CategoryTheory.Aut F) (FintypeCat.of (CategoryTheory.Aut F ⧸ MulAction.stabilizer (CategoryTheory.Aut F) x))

If X is connected and x is in the fiber of X, F.obj X is isomorphic to the quotient of Aut F by the stabilizer of x as Aut F-sets.

Equations

• CategoryTheory.PreGaloisCategory.fiberIsoQuotientStabilizer X x = CategoryTheory.FintypeCat.isoQuotientStabilizerOfIsConnected ((CategoryTheory.PreGaloisCategory.functorToAction F).obj X) x

theorem CategoryTheory.PreGaloisCategory.exists_lift_of_quotient_openSubgroup {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] {F : CategoryTheory.Functor C FintypeCat} [CategoryTheory.GaloisCategory C] [CategoryTheory.PreGaloisCategory.FiberFunctor F] (V : OpenSubgroup (CategoryTheory.Aut F)) : ∃ (X : C), Nonempty ((CategoryTheory.PreGaloisCategory.functorToAction F).obj X ≅ Action.FintypeCat.ofMulAction (CategoryTheory.Aut F) (FintypeCat.of (CategoryTheory.Aut F ⧸ ↑V)))

For every open subgroup V of Aut F, there exists an X : C such that F.obj X ≅ Aut F ⧸ V as Aut F-sets.

theorem CategoryTheory.PreGaloisCategory.exists_lift_of_continuous {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] {F : CategoryTheory.Functor C FintypeCat} [CategoryTheory.GaloisCategory C] [CategoryTheory.PreGaloisCategory.FiberFunctor F] (X : Action FintypeCat (MonCat.of (CategoryTheory.Aut F))) [TopologicalSpace ↑X.V] [DiscreteTopology ↑X.V] [ContinuousSMul (CategoryTheory.Aut F) ↑X.V] : ∃ (A : C), 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.