English
If X is a finite, discrete Aut F-set with a continuous Aut F-action, there exists A in C with F.obj A isomorphic to X as Aut F-sets.
Русский
Если X — конечное дискретное Aut F-множество с непрерывным действием Aut F, существо A в C таково, что F.obj A изоморфно X как Aut F-множество.
LaTeX
$$$\\exists A:\\, C, \\ (\\mathrm{functorToAction} F).obj A \\cong X$$$
Lean4
/-- 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 0BN4 "Essential surjectivity part"]
theorem exists_lift_of_continuous (X : Action FintypeCat (Aut F)) [TopologicalSpace X.V] [DiscreteTopology X.V]
[ContinuousSMul (Aut F) X.V] : ∃ A, Nonempty ((functorToAction F).obj A ≅ X) :=
by
obtain ⟨ι, hfin, f, ⟨u⟩⟩ := has_decomp_quotients X
choose g gu using (fun i ↦ exists_lift_of_quotient_openSubgroup (f i))
exact ⟨∐ g, ⟨PreservesCoproduct.iso (functorToAction F) g ≪≫ Sigma.mapIso (fun i ↦ (gu i).some) ≪≫ u⟩⟩
