English
Let X be a profinite (totally disconnected, compact) space and V a topological commutative monoid. Given any neighborhood S of the diagonal in V × V, there exist a finite index n, a family U of clopen subsets U(i) of X (i = 1,...,n), and elements v(i) ∈ V, such that for every x ∈ X the pair (f(x), ∏_{i=1}^n mulIndicator(U(i))(⋅ ↦ v(i)) x) lies in S. In words, a continuous map from a profinite space to V can be approximated by finite products of indicator functions of clopen sets.
Русский
Пусть X — профинитное (компактное, totally disconnected) пространство, а V — топологический коммутативный моноид. Для любого окрестностного множества S диагонали V × V существует конечное число n,U: Fin n → Clopens(X) и v: Fin n → V such that для каждого x ∈ X пара (f(x), ∏_{i=1}^n mulIndicator(U(i))(⋅ ↦ v(i)) x) принадлежит S. Говоря иначе, непрерывная карта f: X → V может быть аппроксимирована конечными произведениями индикаторов по клиопическим множествам.
LaTeX
$$$\\exists n \\in \\mathbb{N},\\ U: \\mathrm{Fin}(n) \\to \\mathrm{Clopens}(X),\\ v: \\mathrm{Fin}(n) \\to V,\\ \\forall x \\in X,\\ (f(x),\\ \\prod_{i: \\mathrm{Fin}(n)}\\mathrm{mulIndicator}(U(i))(\\lambda\\_.v(i))(x)) \\in S.$$$
Lean4
/-- If `f` is a continuous map from a profinite space to a topological space with a commutative monoid
structure, then we can approximate `f` by finite products of indicator functions of clopen sets.
(Note no compatibility is assumed between the monoid structure on `V` and the topology.)
-/
@[to_additive /-- If `f` is a continuous map from a profinite space to a topological space with a
commutative additive monoid structure, then we can approximate `f` by finite sums of indicator
functions of clopen sets.
(Note no compatibility is assumed between the monoid structure on `V` and the topology.) -/
]
theorem exists_finite_sum_const_mulIndicator_approximation_of_mem_nhds_diagonal [CommMonoid V]
(hS : S ∈ nhdsSet (diagonal V)) :
∃ (n : ℕ) (U : Fin n → Clopens X) (v : Fin n → V), ∀ x, (f x, ∏ n, mulIndicator (U n) (fun _ ↦ v n) x) ∈ S :=
by
obtain ⟨n, g, h, hg, hgh⟩ := exists_finite_approximation_of_mem_nhds_diagonal f hS
refine ⟨n, fun i ↦ ⟨_, (isClopen_discrete { i }).preimage hg⟩, h, fun x ↦ ?_⟩
convert hgh x
exact (Fintype.prod_eq_single _ fun i hi ↦ mulIndicator_of_notMem hi.symm _).trans (mulIndicator_of_mem rfl _)
