English
For a closed set C, any locally constant f on C factors through a finite restriction to some s: there exist s and g such that f = g ∘ ProjRestrict.
Русский
Пусть C замкнуто. Любая локально-константная функция f на C факторизуется через проекцию на конечное множество координат: существует конечное s и функция g, такая что f = g ∘ ProjRestrict.
LaTeX
$$$ \exists s : Finset I,\; \exists g : LocallyConstant (\pi C (\cdot \in s))\mathbb{Z},\; f = g \circ \langle \mathrm{ProjRestrict} C (\cdot \in s), \mathrm{continuous_projRestrict} _ _ \rangle $$$
Lean4
theorem fin_comap_jointlySurjective (hC : IsClosed C) (f : LocallyConstant C ℤ) :
∃ (s : Finset I) (g : LocallyConstant (π C (· ∈ s)) ℤ),
f = g.comap ⟨(ProjRestrict C (· ∈ s)), continuous_projRestrict _ _⟩ :=
by
obtain ⟨J, g, h⟩ :=
@Profinite.exists_locallyConstant (Finset I)ᵒᵖ _ _ _ (spanCone hC.isCompact) ℤ (spanCone_isLimit hC.isCompact) f
exact ⟨(Opposite.unop J), g, h⟩
