feat(Topology): clopen subsets of products of compact spaces are unio…

…ns of clopen boxes (#8678)






Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>

Mathlib.lean

@@ -3550,6 +3550,7 @@ import Mathlib.Topology.Category.TopCat.Opens
 import Mathlib.Topology.Category.TopCommRingCat
 import Mathlib.Topology.Category.UniformSpace
 import Mathlib.Topology.Clopen
+import Mathlib.Topology.ClopenBox
 import Mathlib.Topology.CompactOpen
 import Mathlib.Topology.Compactification.OnePoint
 import Mathlib.Topology.Compactness.Compact

Mathlib/Topology/ClopenBox.lean

@@ -0,0 +1,75 @@
+/-
+Copyright (c) 2023 Dagur Asgeirsson. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Dagur Asgeirsson
+-/
+import Mathlib.Topology.CompactOpen
+import Mathlib.Topology.Sets.Closeds
+
+/-!
+# Clopen subsets in cartesian products
+
+In general, a clopen subset in a cartesian product of topological spaces
+cannot be written as a union of "clopen boxes",
+i.e. products of clopen subsets of the components (see [buzyakovaClopenBox] for counterexamples).
+
+However, when one of the factors is compact, a clopen subset can be written as such a union.
+Our argument in `TopologicalSpace.Clopens.exists_prod_subset`
+follows the one given in [buzyakovaClopenBox].
+
+We deduce that in a product of compact spaces, a clopen subset is a finite union of clopen boxes,
+and use that to prove that the property of having countably many clopens is preserved by taking
+cartesian products of compact spaces (this is relevant to the theory of light profinite sets).
+
+## References
+
+- [buzyakovaClopenBox]: *On clopen sets in Cartesian products*, 2001.
+- [engelking1989]: *General Topology*, 1989.
+
+-/
+
+open Function Set Filter TopologicalSpace
+open scoped Topology
+
+variable {X Y : Type*} [TopologicalSpace X] [TopologicalSpace Y] [CompactSpace Y]
+
+theorem TopologicalSpace.Clopens.exists_prod_subset (W : Clopens (X × Y)) {a : X × Y} (h : a ∈ W) :
+    ∃ U : Clopens X, a.1 ∈ U ∧ ∃ V : Clopens Y, a.2 ∈ V ∧ U ×ˢ V ≤ W := by
+  have hp : Continuous (fun y : Y ↦ (a.1, y)) := Continuous.Prod.mk _
+  let V : Set Y := {y | (a.1, y) ∈ W}
+  have hV : IsCompact V := (W.2.2.preimage hp).isCompact
+  let U : Set X := {x | MapsTo (Prod.mk x) V W}
+  have hUV : U ×ˢ V ⊆ W := fun ⟨_, _⟩ hw ↦ hw.1 hw.2
+  exact ⟨⟨U, (ContinuousMap.isClopen_setOf_mapsTo hV W.2).preimage
+    (ContinuousMap.id (X × Y)).curry.2⟩, by simp [MapsTo], ⟨V, W.2.preimage hp⟩, h, hUV⟩
+
+variable [CompactSpace X]
+
+/-- Every clopen set in a product of two compact spaces
+is a union of finitely many clopen boxes. -/
+theorem TopologicalSpace.Clopens.exists_finset_eq_sup_prod (W : Clopens (X × Y)) :
+    ∃ (I : Finset (Clopens X × Clopens Y)), W = I.sup fun i ↦ i.1 ×ˢ i.2 := by
+  choose! U hxU V hxV hUV using fun x ↦ W.exists_prod_subset (a := x)
+  rcases W.2.2.isCompact.elim_nhds_subcover (fun x ↦ U x ×ˢ V x) (fun x hx ↦
+    (U x ×ˢ V x).2.isOpen.mem_nhds ⟨hxU x hx, hxV x hx⟩) with ⟨I, hIW, hWI⟩
+  classical
+  use I.image fun x ↦ (U x, V x)
+  rw [Finset.sup_image]
+  refine le_antisymm (fun x hx ↦ ?_) (Finset.sup_le fun x hx ↦ ?_)
+  · rcases Set.mem_iUnion₂.1 (hWI hx) with ⟨i, hi, hxi⟩
+    exact SetLike.le_def.1 (Finset.le_sup hi) hxi
+  · exact hUV _ <| hIW _ hx
+
+lemma TopologicalSpace.Clopens.surjective_finset_sup_prod :
+    Surjective fun I : Finset (Clopens X × Clopens Y) ↦ I.sup fun i ↦ i.1 ×ˢ i.2 := fun W ↦
+  let ⟨I, hI⟩ := W.exists_finset_eq_sup_prod; ⟨I, hI.symm⟩
+
+instance TopologicalSpace.Clopens.countable_prod [Countable (Clopens X)]
+    [Countable (Clopens Y)] : Countable (Clopens (X × Y)) :=
+  surjective_finset_sup_prod.countable
+
+instance TopologicalSpace.Clopens.finite_prod [Finite (Clopens X)] [Finite (Clopens Y)] :
+    Finite (Clopens (X × Y)) := by
+  cases nonempty_fintype (Clopens X)
+  cases nonempty_fintype (Clopens Y)
+  exact .of_surjective _ surjective_finset_sup_prod

Mathlib/Topology/CompactOpen.lean

@@ -210,6 +210,14 @@ theorem continuous_coe : Continuous ((⇑) : C(α, β) → (α → β)) :=
 #align continuous_map.continuous_coe' ContinuousMap.continuous_coe
 #align continuous_map.continuous_coe ContinuousMap.continuous_coe
 
+lemma isClosed_setOf_mapsTo {t : Set β} (ht : IsClosed t) (s : Set α) :
+    IsClosed {f : C(α, β) | MapsTo f s t} :=
+  ht.setOf_mapsTo fun _ _ ↦ continuous_eval_const _
+
+lemma isClopen_setOf_mapsTo {K : Set α} (hK : IsCompact K) {U : Set β} (hU : IsClopen U) :
+    IsClopen {f : C(α, β) | MapsTo f K U} :=
+  ⟨isOpen_setOf_mapsTo hK hU.isOpen, isClosed_setOf_mapsTo hU.isClosed K⟩
+
 instance [T0Space β] : T0Space C(α, β) :=
   t0Space_of_injective_of_continuous FunLike.coe_injective continuous_coe
 
@@ -361,8 +369,7 @@ def curry' (f : C(α × β, γ)) (a : α) : C(β, γ) :=
 
 /-- If a map `α × β → γ` is continuous, then its curried form `α → C(β, γ)` is continuous. -/
 theorem continuous_curry' (f : C(α × β, γ)) : Continuous (curry' f) :=
-  have hf : curry' f = ContinuousMap.comp f ∘ coev _ _ := by ext; rfl
-  hf ▸ Continuous.comp (continuous_comp f) continuous_coev
+  Continuous.comp (continuous_comp f) continuous_coev
 #align continuous_map.continuous_curry' ContinuousMap.continuous_curry'
 
 /-- To show continuity of a map `α → C(β, γ)`, it suffices to show that its uncurried form

Mathlib/Topology/Constructions.lean

@@ -415,6 +415,12 @@ theorem Continuous.Prod.mk_left (b : β) : Continuous fun a : α => (a, b) :=
   continuous_id.prod_mk continuous_const
 #align continuous.prod.mk_left Continuous.Prod.mk_left
 
+/-- If `f x y` is continuous in `x` for all `y ∈ s`,
+then the set of `x` such that `f x` maps `s` to `t` is closed. -/
+lemma IsClosed.setOf_mapsTo {f : α → β → γ} {s : Set β} {t : Set γ} (ht : IsClosed t)
+    (hf : ∀ y ∈ s, Continuous (f · y)) : IsClosed {x | MapsTo (f x) s t} := by
+  simpa only [MapsTo, setOf_forall] using isClosed_biInter fun y hy ↦ ht.preimage (hf y hy)
+
 theorem Continuous.comp₂ {g : α × β → γ} (hg : Continuous g) {e : δ → α} (he : Continuous e)
     {f : δ → β} (hf : Continuous f) : Continuous fun x => g (e x, f x) :=
   hg.comp <| he.prod_mk hf

Mathlib/Topology/Sets/Closeds.lean

@@ -315,6 +315,8 @@ theorem coe_mk (s : Set α) (h) : (mk s h : Set α) = s :=
   rfl
 #align topological_space.clopens.coe_mk TopologicalSpace.Clopens.coe_mk
 
+@[simp] lemma mem_mk {s : Set α} {x h} : x ∈ mk s h ↔ x ∈ s := .rfl
+
 instance : Sup (Clopens α) := ⟨fun s t => ⟨s ∪ t, s.isClopen.union t.isClopen⟩⟩
 instance : Inf (Clopens α) := ⟨fun s t => ⟨s ∩ t, s.isClopen.inter t.isClopen⟩⟩
 instance : Top (Clopens α) := ⟨⟨⊤, isClopen_univ⟩⟩
@@ -346,6 +348,15 @@ instance : BooleanAlgebra (Clopens α) :=
 
 instance : Inhabited (Clopens α) := ⟨⊥⟩
 
+variable [TopologicalSpace β]
+
+instance : SProd (Clopens α) (Clopens β) (Clopens (α × β)) where
+  sprod s t := ⟨s ×ˢ t, s.2.prod t.2⟩
+
+@[simp]
+protected lemma mem_prod {s : Clopens α} {t : Clopens β} {x : α × β} :
+    x ∈ s ×ˢ t ↔ x.1 ∈ s ∧ x.2 ∈ t := .rfl
+
 end Clopens
 
 end TopologicalSpace

docs/references.bib

@@ -504,6 +504,20 @@ @Article{         bruhnDiestelKriesselPendavinghWollan2013
   url           = {https://www.sciencedirect.com/science/article/pii/S0001870813000261}
 }
 
+@Article{         buzyakovaClopenBox,
+  author        = {Buzyakova, Raushan Z.},
+  title         = {On clopen sets in {C}artesian products},
+  journal       = {Comment. Math. Univ. Carolin.},
+  fjournal      = {Commentationes Mathematicae Universitatis Carolinae},
+  volume        = {42},
+  year          = {2001},
+  number        = {2},
+  pages         = {357--362},
+  issn          = {0010-2628,1213-7243},
+  mrclass       = {54B10 (54B15 54D20 55M10)},
+  mrnumber      = {1832154}
+}
+
 @Book{            cabreragarciarodriguezpalacios2014,
   author        = {Miguel {Cabrera Garc\'{\i}a} and \'Angel {Rodr\'{\i}guez
                   Palacios}},
@@ -933,6 +947,22 @@ @Book{            engel1997
   year          = {1997}
 }
 
+@Book{            engelking1989,
+  title         = {General topology},
+  author        = {Engelking, Ryszard},
+  series        = {Sigma Series in Pure Mathematics},
+  volume        = {6},
+  edition       = {Second},
+  note          = {Translated from the Polish by the author},
+  publisher     = {Heldermann Verlag, Berlin},
+  year          = {1989},
+  pages         = {viii+529},
+  isbn          = {3-88538-006-4},
+  mrclass       = {54-01 (54-02)},
+  mrnumber      = {1039321},
+  mrreviewer    = {Gary\ Gruenhage}
+}
+
 @Article{         erdosrenyisos,
   author        = {P. Erd\"os, A.R\'enyi, and V. S\'os},
   title         = {On a problem of graph theory},