English
There exists a functor from the category C to the category of finite, discrete Aut F-sets, sending each object X to the Aut F-action on its fiber F(X). Morphisms are sent to equivariant maps between these Aut F-sets.
Русский
Существует функтор из категории C в категорию конечных дискретных множеств-aut(F), который каждому объекту X сопоставляет действие Aut F на волокно F(X). Морфизмы переходят в эквивариантные отображения между этими Aut F-множестями.
LaTeX
$$$\\exists \\mathcal{F}: \\mathcal{C} \\to \\mathrm{ContAction}(\\mathrm{FintypeCat}, \\mathrm{Aut}\\,F)\\;\\text{such that}\\; \\mathcal{F}(X) \\cong (\\mathrm{Aut}\\,F) \\curvearrowright F(X) \\quad$$$
Lean4
/-- The induced functor from `C` to the category of finite, discrete `Aut F`-sets. -/
@[simps! obj_obj map]
def functorToContAction : C ⥤ ContAction FintypeCat (Aut F) :=
ObjectProperty.lift _ (functorToAction F) (fun X ↦ continuousSMul_aut_fiber F X)
