chore(Topology/Constructions): split out results about sums, products and distributivity (#22827)

And move all homeomorphism related to direct sums, products and distributivity into the new file.

This resolves a large file warning. It mostly reduces transitive imports (and causes mild increases in other places, and didn't import `Homeomorph.Defs` before).
This is also necessary to break an import cycle in #22137.



Co-authored-by: grunweg <rothgami@math.hu-berlin.de>

Author: grunweg

Mathlib.lean

@@ -5711,6 +5711,7 @@ import Mathlib.Topology.Connected.Separation
 import Mathlib.Topology.Connected.TotallyDisconnected
 import Mathlib.Topology.Constructible
 import Mathlib.Topology.Constructions
+import Mathlib.Topology.Constructions.SumProd
 import Mathlib.Topology.ContinuousMap.Algebra
 import Mathlib.Topology.ContinuousMap.Basic
 import Mathlib.Topology.ContinuousMap.Bounded.Basic

Mathlib/Dynamics/TopologicalEntropy/DynamicalEntourage.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Damien Thomine, Pietro Monticone
 -/
 import Mathlib.Order.Interval.Finset.Nat
-import Mathlib.Topology.Constructions
+import Mathlib.Topology.Constructions.SumProd
 import Mathlib.Topology.UniformSpace.Defs
 
 /-!

Mathlib/Topology/CompactOpen.lean

@@ -5,7 +5,7 @@ Authors: Reid Barton
 -/
 import Mathlib.Topology.Hom.ContinuousEval
 import Mathlib.Topology.ContinuousMap.Basic
-import Mathlib.Topology.Homeomorph.Lemmas
+import Mathlib.Topology.Separation.Regular
 
 /-!
 # The compact-open topology

Mathlib/Topology/Compactness/Paracompact.lean

@@ -3,8 +3,8 @@ Copyright (c) 2021 Yury Kudryashov. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Reid Barton, Yury Kudryashov
 -/
-import Mathlib.Topology.Homeomorph.Lemmas
 import Mathlib.Data.Option.Basic
+import Mathlib.Topology.Separation.Regular
 
 /-!
 # Paracompact topological spaces

Mathlib/Topology/Constructions.lean

@@ -3,7 +3,7 @@ Copyright (c) 2019 Sébastien Gouëzel. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Sébastien Gouëzel
 -/
-import Mathlib.Topology.Homeomorph.Lemmas
+import Mathlib.Topology.Constructions.SumProd
 
 /-!
 # Maps equivariantly-homeomorphic to projection in a product

Mathlib/Topology/Constructions/SumProd.lean

@@ -6,7 +6,6 @@ Authors: Johannes Hölzl, Patrick Massot, Sébastien Gouëzel, Zhouhang Zhou, Re
 import Mathlib.Logic.Equiv.Fin
 import Mathlib.Topology.Connected.LocallyConnected
 import Mathlib.Topology.DenseEmbedding
-import Mathlib.Topology.Homeomorph.Defs
 
 /-!
 # Further properties of homeomorphisms
@@ -208,169 +207,8 @@ def setCongr {s t : Set X} (h : s = t) : s ≃ₜ t where
   continuous_invFun := continuous_inclusion h.symm.subset
   toEquiv := Equiv.setCongr h
 
-/-- Sum of two homeomorphisms. -/
-def sumCongr (h₁ : X ≃ₜ X') (h₂ : Y ≃ₜ Y') : X ⊕ Y ≃ₜ X' ⊕ Y' where
-  continuous_toFun := h₁.continuous.sumMap h₂.continuous
-  continuous_invFun := h₁.symm.continuous.sumMap h₂.symm.continuous
-  toEquiv := h₁.toEquiv.sumCongr h₂.toEquiv
-
-@[simp]
-lemma sumCongr_symm (h₁ : X ≃ₜ X') (h₂ : Y ≃ₜ Y') :
-  (sumCongr h₁ h₂).symm = sumCongr h₁.symm h₂.symm := rfl
-
-@[simp]
-theorem sumCongr_refl : sumCongr (.refl X) (.refl Y) = .refl (X ⊕ Y) := by
-  ext i
-  cases i <;> rfl
-
-@[simp]
-theorem sumCongr_trans {X'' Y'' : Type*} [TopologicalSpace X''] [TopologicalSpace Y'']
-    (h₁ : X ≃ₜ X') (h₂ : Y ≃ₜ Y') (h₃ : X' ≃ₜ X'') (h₄ : Y' ≃ₜ Y'') :
-    (sumCongr h₁ h₂).trans (sumCongr h₃ h₄) = sumCongr (h₁.trans h₃) (h₂.trans h₄) := by
-  ext i
-  cases i <;> rfl
-
-/-- Product of two homeomorphisms. -/
-def prodCongr (h₁ : X ≃ₜ X') (h₂ : Y ≃ₜ Y') : X × Y ≃ₜ X' × Y' where
-  toEquiv := h₁.toEquiv.prodCongr h₂.toEquiv
-
-@[simp]
-theorem prodCongr_symm (h₁ : X ≃ₜ X') (h₂ : Y ≃ₜ Y') :
-    (h₁.prodCongr h₂).symm = h₁.symm.prodCongr h₂.symm :=
-  rfl
-
-@[simp]
-theorem coe_prodCongr (h₁ : X ≃ₜ X') (h₂ : Y ≃ₜ Y') : ⇑(h₁.prodCongr h₂) = Prod.map h₁ h₂ :=
-  rfl
-
--- Commutativity and associativity of the disjoint union of topological spaces,
--- and the sum with an empty space.
-section sum
-
-variable (X Y W Z)
-
-/-- `X ⊕ Y` is homeomorphic to `Y ⊕ X`. -/
-def sumComm : X ⊕ Y ≃ₜ Y ⊕ X where
-  toEquiv := Equiv.sumComm X Y
-  continuous_toFun := continuous_sum_swap
-  continuous_invFun := continuous_sum_swap
-
-@[simp]
-theorem sumComm_symm : (sumComm X Y).symm = sumComm Y X :=
-  rfl
-
-@[simp]
-theorem coe_sumComm : ⇑(sumComm X Y) = Sum.swap :=
-  rfl
-
-@[continuity, fun_prop]
-lemma continuous_sumAssoc : Continuous (Equiv.sumAssoc X Y Z) :=
-  Continuous.sumElim (by fun_prop) (by fun_prop)
-
-@[continuity, fun_prop]
-lemma continuous_sumAssoc_symm : Continuous (Equiv.sumAssoc X Y Z).symm :=
-  Continuous.sumElim (by fun_prop) (by fun_prop)
-
-/-- `(X ⊕ Y) ⊕ Z` is homeomorphic to `X ⊕ (Y ⊕ Z)`. -/
-def sumAssoc : (X ⊕ Y) ⊕ Z ≃ₜ X ⊕ Y ⊕ Z where
-  toEquiv := Equiv.sumAssoc X Y Z
-  continuous_toFun := continuous_sumAssoc X Y Z
-  continuous_invFun := continuous_sumAssoc_symm X Y Z
-
-@[simp]
-lemma sumAssoc_toEquiv : (sumAssoc X Y Z).toEquiv = Equiv.sumAssoc X Y Z := rfl
-
-/-- Four-way commutativity of the disjoint union. The name matches `add_add_add_comm`. -/
-def sumSumSumComm : (X ⊕ Y) ⊕ W ⊕ Z ≃ₜ (X ⊕ W) ⊕ Y ⊕ Z where
-  toEquiv := Equiv.sumSumSumComm X Y W Z
-  continuous_toFun := by
-    unfold Equiv.sumSumSumComm
-    dsimp only
-    have : Continuous (Sum.map (Sum.map (@id X) ⇑(Equiv.sumComm Y W)) (@id Z)) := by continuity
-    fun_prop
-  continuous_invFun := by
-    unfold Equiv.sumSumSumComm
-    dsimp only
-    have : Continuous (Sum.map (Sum.map (@id X) (Equiv.sumComm Y W).symm) (@id Z)) := by continuity
-    fun_prop
-
-@[simp]
-lemma sumSumSumComm_toEquiv : (sumSumSumComm X Y W Z).toEquiv = (Equiv.sumSumSumComm X Y W Z) := rfl
-
-@[simp]
-lemma sumSumSumComm_symm : (sumSumSumComm X Y W Z).symm = (sumSumSumComm X W Y Z) := rfl
-
-/-- The sum of `X` with any empty topological space is homeomorphic to `X`. -/
-@[simps! -fullyApplied apply]
-def sumEmpty [IsEmpty Y] : X ⊕ Y ≃ₜ X where
-  toEquiv := Equiv.sumEmpty X Y
-  continuous_toFun := Continuous.sumElim continuous_id (by fun_prop)
-  continuous_invFun := continuous_inl
-
-/-- The sum of `X` with any empty topological space is homeomorphic to `X`. -/
-def emptySum [IsEmpty Y] : Y ⊕ X ≃ₜ X := (sumComm Y X).trans (sumEmpty X Y)
-
-@[simp] theorem coe_emptySum [IsEmpty Y] : (emptySum X Y).toEquiv = Equiv.emptySum Y X := rfl
-
-end sum
-
--- Commutativity and associativity of the product of top. spaces, and the product with `PUnit`.
 section prod
 
-variable (X Y W Z)
-
-/-- `X × Y` is homeomorphic to `Y × X`. -/
-def prodComm : X × Y ≃ₜ Y × X where
-  continuous_toFun := continuous_snd.prod_mk continuous_fst
-  continuous_invFun := continuous_snd.prod_mk continuous_fst
-  toEquiv := Equiv.prodComm X Y
-
-@[simp]
-theorem prodComm_symm : (prodComm X Y).symm = prodComm Y X :=
-  rfl
-
-@[simp]
-theorem coe_prodComm : ⇑(prodComm X Y) = Prod.swap :=
-  rfl
-
-/-- `(X × Y) × Z` is homeomorphic to `X × (Y × Z)`. -/
-def prodAssoc : (X × Y) × Z ≃ₜ X × Y × Z where
-  continuous_toFun := continuous_fst.fst.prod_mk (continuous_fst.snd.prod_mk continuous_snd)
-  continuous_invFun := (continuous_fst.prod_mk continuous_snd.fst).prod_mk continuous_snd.snd
-  toEquiv := Equiv.prodAssoc X Y Z
-
-@[simp]
-lemma prodAssoc_toEquiv : (prodAssoc X Y Z).toEquiv = Equiv.prodAssoc X Y Z := rfl
-
-/-- Four-way commutativity of `prod`. The name matches `mul_mul_mul_comm`. -/
-def prodProdProdComm : (X × Y) × W × Z ≃ₜ (X × W) × Y × Z where
-  toEquiv := Equiv.prodProdProdComm X Y W Z
-  continuous_toFun := by
-    unfold Equiv.prodProdProdComm
-    dsimp only
-    fun_prop
-  continuous_invFun := by
-    unfold Equiv.prodProdProdComm
-    dsimp only
-    fun_prop
-
-@[simp]
-theorem prodProdProdComm_symm : (prodProdProdComm X Y W Z).symm = prodProdProdComm X W Y Z :=
-  rfl
-
-/-- `X × {*}` is homeomorphic to `X`. -/
-@[simps! -fullyApplied apply]
-def prodPUnit : X × PUnit ≃ₜ X where
-  toEquiv := Equiv.prodPUnit X
-  continuous_toFun := continuous_fst
-  continuous_invFun := continuous_id.prod_mk continuous_const
-
-/-- `{*} × X` is homeomorphic to `X`. -/
-def punitProd : PUnit × X ≃ₜ X :=
-  (prodComm _ _).trans (prodPUnit _)
-
-@[simp] theorem coe_punitProd : ⇑(punitProd X) = Prod.snd := rfl
-
 /-- The product over `S ⊕ T` of a family of topological spaces
 is homeomorphic to the product of (the product over `S`) and (the product over `T`).
 
@@ -480,19 +318,6 @@ theorem _root_.Fin.appendHomeomorph_toEquiv (m n : ℕ) :
 
 section Distrib
 
-/-- `(X ⊕ Y) × Z` is homeomorphic to `X × Z ⊕ Y × Z`. -/
-@[simps!]
-def sumProdDistrib : (X ⊕ Y) × Z ≃ₜ (X × Z) ⊕ (Y × Z) :=
-  Homeomorph.symm <|
-    homeomorphOfContinuousOpen (Equiv.sumProdDistrib X Y Z).symm
-        ((continuous_inl.prodMap continuous_id).sumElim
-          (continuous_inr.prodMap continuous_id)) <|
-      (isOpenMap_inl.prodMap IsOpenMap.id).sumElim (isOpenMap_inr.prodMap IsOpenMap.id)
-
-/-- `X × (Y ⊕ Z)` is homeomorphic to `X × Y ⊕ X × Z`. -/
-def prodSumDistrib : X × (Y ⊕ Z) ≃ₜ (X × Y) ⊕ (X × Z) :=
-  (prodComm _ _).trans <| sumProdDistrib.trans <| sumCongr (prodComm _ _) (prodComm _ _)
-
 variable {ι : Type*} {X : ι → Type*} [∀ i, TopologicalSpace (X i)]
 
 /-- `(Σ i, X i) × Y` is homeomorphic to `Σ i, (X i × Y)`. -/