English
Any locally constant map from the cofiltered limit to Fin 2 factors through one component at some stage of the diagram.
Русский
Любой локально константный отображение с предела к Fin 2 факorizуется через одну компоненту на некотором этапе диаграммы.
LaTeX
$$$\\exists j:\\,J,\\exists g:\\mathrm{LocallyConstant}(F(j),\\mathrm{Fin}\\,2),\\ f= g\\circ (C.\\pi.app j).hom$$$
Lean4
theorem exists_locallyConstant_fin_two (hC : IsLimit C) (f : LocallyConstant C.pt (Fin 2)) :
∃ (j : J) (g : LocallyConstant (F.obj j) (Fin 2)), f = g.comap (C.π.app _).hom :=
by
let U := f ⁻¹' {0}
have hU : IsClopen U := f.isLocallyConstant.isClopen_fiber _
obtain ⟨j, V, hV, h⟩ := exists_isClopen_of_cofiltered C hC hU
classical
use j, LocallyConstant.ofIsClopen hV
apply LocallyConstant.locallyConstant_eq_of_fiber_zero_eq
simp only [Fin.isValue, Functor.const_obj_obj, LocallyConstant.coe_comap, Set.preimage_comp,
LocallyConstant.ofIsClopen_fiber_zero]
exact h
