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] [IsTopologicalGroup G] [CompactSpace G] (X : Action FintypeCat G) [TopologicalSpace X.V.carrier] [DiscreteTopology X.V.carrier] [ContinuousSMul G X.V.carrier] : ∃ (ι : 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₁} [Category.{u₂, u₁} C] {F : Functor C FintypeCat} [GaloisCategory C] [FiberFunctor F] (X : C) [IsConnected X] (x : (F.obj X).carrier) : (functorToAction F).obj X ≅ Action.FintypeCat.ofMulAction (Aut F) (FintypeCat.of (Aut F ⧸ MulAction.stabilizer (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₁} [Category.{u₂, u₁} C] {F : Functor C FintypeCat} [GaloisCategory C] [FiberFunctor F] (V : OpenSubgroup (Aut F)) : ∃ (X : C), Nonempty ((functorToAction F).obj X ≅ Action.FintypeCat.ofMulAction (Aut F) (FintypeCat.of (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₁} [Category.{u₂, u₁} C] {F : Functor C FintypeCat} [GaloisCategory C] [FiberFunctor F] (X : Action FintypeCat (Aut F)) [TopologicalSpace X.V.carrier] [DiscreteTopology X.V.carrier] [ContinuousSMul (Aut F) X.V.carrier] : ∃ (A : C), Nonempty ((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.

Stacks Tag 0BN4 (Essential surjectivity part)