English
If X is connected and x ∈ F.obj X, then F.obj X is isomorphic to Aut F modulo the stabilizer of x, as Aut F-sets.
Русский
Если X связно и x ∈ F.obj X, то F.obj X изоморфно Aut F / стабилизатор(x) как Aut F-множества.
LaTeX
$$$\\text{If } X \\text{ is connected and } x \\in F.obj X,\\; (\\mathrm{functorToAction} F).obj X \\cong \\mathrm{Aut}F \\,/\\, \\mathrm{stabilizer}_{\\mathrm{Aut}F}(x)$$$
Lean4
/-- 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. -/
def fiberIsoQuotientStabilizer (X : C) [IsConnected X] (x : F.obj X) :
(functorToAction F).obj X ≅ Aut F ⧸ₐ MulAction.stabilizer (Aut F) x :=
haveI : IsConnected ((functorToAction F).obj X) := PreservesIsConnected.preserves
letI : Fintype (Aut F ⧸ MulAction.stabilizer (Aut F) x) := fintypeQuotientStabilizer x
FintypeCat.isoQuotientStabilizerOfIsConnected ((functorToAction F).obj X) x
