# 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.

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.

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

## Instances For

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.

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.