Disjoint covers of profinite spaces

We prove various results about covering profinite spaces by disjoint clopens, including

• TopologicalSpace.IsOpenCover.exists_finite_nonempty_disjoint_clopen_cover: any open cover of a profinite space can be refined to a finite cover by pairwise disjoint nonempty clopens.

• ContinuousMap.exists_finite_approximation_of_mem_nhds_diagonal: if f : X → V is continuous with X profinite, and S is a neighbourhood of the diagonal in V × V, then f can be S-approximated by a function factoring through Fin n for some n.

theorem TopologicalSpace.IsOpenCover.exists_finite_clopen_cover {ι : Type u_1} {X : Type u_2} [TopologicalSpace X] [TotallyDisconnectedSpace X] [T2Space X] [CompactSpace X] {U : ι → Opens X} (hU : IsOpenCover U) : ∃ (n : ℕ) (V : Fin n → Clopens X), (∀ (j : Fin n), ∃ (i : ι), ↑(V j) ⊆ ↑(U i)) ∧ Set.univ ⊆ ⋃ (j : Fin n), ↑(V j)

Any open cover of a profinite space can be refined to a finite cover by clopens.

theorem TopologicalSpace.IsOpenCover.exists_finite_nonempty_disjoint_clopen_cover {ι : Type u_1} {X : Type u_2} [TopologicalSpace X] [TotallyDisconnectedSpace X] [T2Space X] [CompactSpace X] {U : ι → Opens X} (hU : IsOpenCover U) : ∃ (n : ℕ) (W : Fin n → Clopens X), (∀ (j : Fin n), W j ≠ ⊥ ∧ ∃ (i : ι), ↑(W j) ⊆ ↑(U i)) ∧ Set.univ ⊆ ⋃ (j : Fin n), ↑(W j) ∧ Pairwise (Function.onFun Disjoint W)

Any open cover of a profinite space can be refined to a finite cover by pairwise disjoint nonempty clopens.

theorem TopologicalSpace.exists_open_prod_subset_of_mem_nhds_diagonal {X : Type u_1} [TopologicalSpace X] {S : Set (X × X)} (hS : S ∈ nhdsSet (Set.diagonal X)) (x : X) : ∃ (U : Set X), IsOpen U ∧ x ∈ U ∧ U ×ˢ U ⊆ S

If S is any neighbourhood of the diagonal in a topological space X, any point of X has an open neighbourhood U such that U ×ˢ U ⊆ S.

theorem TopologicalSpace.exists_finite_open_cover_prod_subset_of_mem_nhds_diagonal_of_compact {X : Type u_1} [TopologicalSpace X] {S : Set (X × X)} [CompactSpace X] (hS : S ∈ nhdsSet (Set.diagonal X)) : ∃ (t : Finset X) (U : { x : X // x ∈ t } → Opens X), IsOpenCover U ∧ ∀ (i : { x : X // x ∈ t }), ↑(U i) ×ˢ ↑(U i) ⊆ S

If S is any neighbourhood of the diagonal in a compact topological space X, then there exists a finite cover of X by opens U i such that U i ×ˢ U i ⊆ S for all i.

That the indexing set is a finset of X is an artifact of the proof; it could be any finite type.

theorem ContinuousMap.exists_disjoint_nonempty_clopen_cover_of_mem_nhds_diagonal {X : Type u_1} {V : Type u_2} [TopologicalSpace X] [TopologicalSpace V] [TotallyDisconnectedSpace X] [T2Space X] [CompactSpace X] {S : Set (V × V)} (f : C(X, V)) (hS : S ∈ nhdsSet (Set.diagonal V)) : ∃ (n : ℕ) (D : Fin n → TopologicalSpace.Clopens X), (∀ (i : Fin n), D i ≠ ⊥) ∧ (∀ (i : Fin n), ∀ y ∈ D i, ∀ z ∈ D i, (f y, f z) ∈ S) ∧ Set.univ ⊆ ⋃ (i : Fin n), ↑(D i) ∧ Pairwise (Function.onFun Disjoint D)

For any continuous function f : X → V, with X profinite, and S a neighbourhood of the diagonal in V × V, there exists a finite cover of X by pairwise-disjoint nonempty clopens, on each of which f varies within S.

theorem ContinuousMap.exists_finite_approximation_of_mem_nhds_diagonal {X : Type u_1} {V : Type u_2} [TopologicalSpace X] [TopologicalSpace V] [TotallyDisconnectedSpace X] [T2Space X] [CompactSpace X] {S : Set (V × V)} (f : C(X, V)) (hS : S ∈ nhdsSet (Set.diagonal V)) : ∃ (n : ℕ) (g : X → Fin n) (h : Fin n → V), Continuous g ∧ ∀ (x : X), (f x, h (g x)) ∈ S

For any continuous function f : X → V, with X profinite, and S a neighbourhood of the diagonal in V × V, the function f can be S-approximated by a function factoring through Fin n, for some n.

theorem ContinuousMap.exists_finite_sum_const_mulIndicator_approximation_of_mem_nhds_diagonal {X : Type u_1} {V : Type u_2} [TopologicalSpace X] [TopologicalSpace V] [TotallyDisconnectedSpace X] [T2Space X] [CompactSpace X] {S : Set (V × V)} (f : C(X, V)) [CommMonoid V] (hS : S ∈ nhdsSet (Set.diagonal V)) : ∃ (n : ℕ) (U : Fin n → TopologicalSpace.Clopens X) (v : Fin n → V), ∀ (x : X), (f x, ∏ n : Fin n, (↑(U n)).mulIndicator (fun (x : X) => v n) x) ∈ S

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.)

theorem ContinuousMap.exists_finite_sum_const_indicator_approximation_of_mem_nhds_diagonal {X : Type u_1} {V : Type u_2} [TopologicalSpace X] [TopologicalSpace V] [TotallyDisconnectedSpace X] [T2Space X] [CompactSpace X] {S : Set (V × V)} (f : C(X, V)) [AddCommMonoid V] (hS : S ∈ nhdsSet (Set.diagonal V)) : ∃ (n : ℕ) (U : Fin n → TopologicalSpace.Clopens X) (v : Fin n → V), ∀ (x : X), (f x, ∑ n : Fin n, (↑(U n)).indicator (fun (x : X) => v n) x) ∈ S

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.)