English
Any morphism from the limit object to a finite object factors through some stage of the diagram.
Русский
Любой морфизм из предельного объекта в конечный объект факторизуется через некоторый этап диаграммы.
LaTeX
$$$\\exists i:\\,I,\\exists g:\\;\\mathrm{LocallyConstant}(F(i),\\mathrm{Finite}),\\ f=\\mathrm{(π.app i)}\\,\\\\cdot\, g$$$
Lean4
/-- A continuous map from a profinite set to a finite set factors through one of the components of
the profinite set when written as a cofiltered limit of finite sets.
-/
theorem exists_hom (hc : IsLimit c) {X : FintypeCat} (f : c.pt ⟶ toProfinite.obj X) :
∃ (i : I) (g : F.obj i ⟶ X), f = c.π.app i ≫ toProfinite.map g :=
by
let _ : TopologicalSpace X := ⊥
have : DiscreteTopology (toProfinite.obj X) := ⟨rfl⟩
let f' : LocallyConstant c.pt (toProfinite.obj X) := ⟨f, (IsLocallyConstant.iff_continuous _).mpr f.hom.continuous⟩
obtain ⟨i, g, h⟩ := exists_locallyConstant.{_, u} c hc f'
refine ⟨i, (g : _ → _), ?_⟩
ext x
exact LocallyConstant.congr_fun h x
