English
Every finite, discrete Aut F-set with a continuous Aut F-action is in the essential image of functorToContAction; i.e., there exists X in C with (functorToAction F).obj X ≅ X-set.
Русский
Каждое конечное дискретное множество с непрерывным действием Aut F на себя находится в образе функторa: существует X в C с эквивалентностью вида (functorToAction F).obj X ≅ X.
LaTeX
$$$\\forall X: \\mathrm{Action}\\;\\mathrm{FintypeCat}(\\mathrm{Aut}\\,F),\\ \\exists A: C, (\\mathrm{functorToAction}\n F).obj A \\cong X$$$
Lean4
instance {F : C ⥤ FintypeCat.{u₁}} [FiberFunctor F] : (functorToContAction F).EssSurj where
mem_essImage
X := by
have : ContinuousSMul (Aut F) X.obj.V.carrier := X.2
obtain ⟨A, ⟨i⟩⟩ := exists_lift_of_continuous (F := F) X
exact ⟨A, ⟨ObjectProperty.isoMk _ i⟩⟩
