chore(Topology/Homeomorph): split out the basic definitions (#22681)

Move `Homeomorph.lean` to `Homeomorph/Lemmas.lean`, and split out a new file `Homeomorph/Defs.lean` which contains just the basic definitions and properties. The definitions file intentionally has very minimal imports.

All declarations which require heavier imports are kept in `Lemmas.lean`: this can be split in future commits.

Future PRs will build on this split to dissolve `Homeomorph/Lemmas.lean` further, such as by moving the homeomorphism about direct sums next to their construction. This is also necessary to break an import cycle in #22137.

This PR gives a modest import reduction - but is a pre-requisite to more far-reaching reductions by dissolving `Homeomorph/Lemmas.lean`.



Co-authored-by: Aaron Liu <aaronliu2008@outlook.com>

Author: grunweg

Mathlib.lean

@@ -5767,7 +5767,8 @@ import Mathlib.Topology.Gluing
 import Mathlib.Topology.Hom.ContinuousEval
 import Mathlib.Topology.Hom.ContinuousEvalConst
 import Mathlib.Topology.Hom.Open
-import Mathlib.Topology.Homeomorph
+import Mathlib.Topology.Homeomorph.Defs
+import Mathlib.Topology.Homeomorph.Lemmas
 import Mathlib.Topology.Homotopy.Basic
 import Mathlib.Topology.Homotopy.Contractible
 import Mathlib.Topology.Homotopy.Equiv

Mathlib/Topology/Algebra/ConstMulAction.lean

@@ -10,7 +10,7 @@ import Mathlib.GroupTheory.GroupAction.Defs
 import Mathlib.Topology.Algebra.Constructions
 import Mathlib.Topology.Algebra.Support
 import Mathlib.Topology.Bases
-import Mathlib.Topology.Homeomorph
+import Mathlib.Topology.Homeomorph.Lemmas
 
 /-!
 # Monoid actions continuous in the second variable

Mathlib/Topology/Algebra/Constructions.lean

@@ -3,7 +3,7 @@ Copyright (c) 2021 Nicolò Cavalleri. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Nicolò Cavalleri
 -/
-import Mathlib.Topology.Homeomorph
+import Mathlib.Topology.Homeomorph.Lemmas
 
 /-!
 # Topological space structure on the opposite monoid and on the units group

Mathlib/Topology/Algebra/Constructions/DomMulAct.lean

@@ -3,7 +3,7 @@ Copyright (c) 2024 Yury Kudryashov. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yury Kudryashov
 -/
-import Mathlib.Topology.Homeomorph
+import Mathlib.Topology.Homeomorph.Lemmas
 import Mathlib.GroupTheory.GroupAction.DomAct.Basic
 
 /-!

Mathlib/Topology/Algebra/GroupWithZero.lean

@@ -6,7 +6,7 @@ Authors: Yury Kudryashov
 import Mathlib.Algebra.Group.Pi.Lemmas
 import Mathlib.Algebra.GroupWithZero.Units.Equiv
 import Mathlib.Topology.Algebra.Monoid
-import Mathlib.Topology.Homeomorph
+import Mathlib.Topology.Homeomorph.Lemmas
 
 /-!
 # Topological group with zero

Mathlib/Topology/Algebra/Support.lean

@@ -6,7 +6,7 @@ Authors: Floris van Doorn, Patrick Massot
 import Mathlib.Algebra.GroupWithZero.Indicator
 import Mathlib.Algebra.Module.Basic
 import Mathlib.Algebra.Order.Group.Unbundled.Abs
-import Mathlib.Topology.Homeomorph
+import Mathlib.Topology.Homeomorph.Defs
 import Mathlib.Topology.Separation.Hausdorff
 
 /-!

Mathlib/Topology/Category/TopCat/Limits/Products.lean

@@ -9,6 +9,7 @@ import Mathlib.CategoryTheory.Limits.Shapes.Products
 import Mathlib.CategoryTheory.Limits.ConcreteCategory.Basic
 import Mathlib.Data.Set.Subsingleton
 import Mathlib.Tactic.CategoryTheory.Elementwise
+import Mathlib.Topology.Homeomorph.Lemmas
 
 /-!
 # Products and coproducts in the category of topological spaces

Mathlib/Topology/Category/TopCat/ULift.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joël Riou
 -/
 import Mathlib.Topology.Category.TopCat.Basic
+import Mathlib.Topology.Homeomorph.Lemmas
 
 /-!
 # Lifting topological spaces to a higher universe

Mathlib/Topology/CompactOpen.lean

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

Mathlib/Topology/Compactification/OnePoint.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yourong Zang, Yury Kudryashov
 -/
 import Mathlib.Data.Fintype.Option
+import Mathlib.Topology.Homeomorph.Lemmas
 import Mathlib.Topology.Sets.Opens
 
 /-!