chore: move Topology.Support to Topology.Algebra.Support (#19651)

to make it clear it's not pure topology. Indeed, the support is the preimage of `0`, which is an algebraic object. Sounds quite trivial like that, but the file actually imports `Module`!

Mathlib.lean

@@ -4994,6 +4994,7 @@ import Mathlib.Topology.Algebra.SeparationQuotient.Basic
 import Mathlib.Topology.Algebra.SeparationQuotient.Section
 import Mathlib.Topology.Algebra.Star
 import Mathlib.Topology.Algebra.StarSubalgebra
+import Mathlib.Topology.Algebra.Support
 import Mathlib.Topology.Algebra.UniformConvergence
 import Mathlib.Topology.Algebra.UniformField
 import Mathlib.Topology.Algebra.UniformFilterBasis
@@ -5326,7 +5327,6 @@ import Mathlib.Topology.Sober
 import Mathlib.Topology.Specialization
 import Mathlib.Topology.Spectral.Hom
 import Mathlib.Topology.StoneCech
-import Mathlib.Topology.Support
 import Mathlib.Topology.TietzeExtension
 import Mathlib.Topology.Ultrafilter
 import Mathlib.Topology.UniformSpace.AbsoluteValue

Mathlib/Topology/Algebra/ConstMulAction.lean

@@ -8,9 +8,9 @@ import Mathlib.Algebra.Order.Group.Synonym
 import Mathlib.Data.Set.Pointwise.SMul
 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.Support
 
 /-!
 # Monoid actions continuous in the second variable

Mathlib/Topology/ContinuousMap/CompactlySupported.lean

@@ -3,9 +3,9 @@ Copyright (c) 2024 Yoh Tanimoto. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yoh Tanimoto
 -/
+import Mathlib.Topology.Algebra.Support
 import Mathlib.Topology.ContinuousMap.CocompactMap
 import Mathlib.Topology.ContinuousMap.ZeroAtInfty
-import Mathlib.Topology.Support
 
 /-!
 # Compactly supported continuous functions

Mathlib/Topology/Homeomorph.lean

@@ -4,9 +4,9 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johannes Hölzl, Patrick Massot, Sébastien Gouëzel, Zhouhang Zhou, Reid Barton
 -/
 import Mathlib.Logic.Equiv.Fin
-import Mathlib.Topology.DenseEmbedding
-import Mathlib.Topology.Support
+import Mathlib.Topology.Algebra.Support
 import Mathlib.Topology.Connected.LocallyConnected
+import Mathlib.Topology.DenseEmbedding
 
 /-!
 # Homeomorphisms

Mathlib/Topology/MetricSpace/ProperSpace.lean

@@ -4,11 +4,11 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Sébastien Gouëzel
 -/
 
-import Mathlib.Topology.Order.IsLUB
-import Mathlib.Topology.Support
+import Mathlib.Topology.Algebra.Support
 import Mathlib.Topology.MetricSpace.Pseudo.Basic
 import Mathlib.Topology.MetricSpace.Pseudo.Lemmas
 import Mathlib.Topology.MetricSpace.Pseudo.Pi
+import Mathlib.Topology.Order.IsLUB
 
 /-! ## Proper spaces
 

Mathlib/Topology/Order/Compact.lean

@@ -3,10 +3,10 @@ Copyright (c) 2021 Patrick Massot. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Patrick Massot, Yury Kudryashov
 -/
-import Mathlib.Topology.Order.LocalExtr
+import Mathlib.Topology.Algebra.Support
 import Mathlib.Topology.Order.IntermediateValue
-import Mathlib.Topology.Support
 import Mathlib.Topology.Order.IsLUB
+import Mathlib.Topology.Order.LocalExtr
 
 /-!
 # Compactness of a closed interval

Mathlib/Topology/UniformSpace/HeineCantor.lean

@@ -3,9 +3,9 @@ Copyright (c) 2020 Patrick Massot. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Patrick Massot, Yury Kudryashov
 -/
-import Mathlib.Topology.UniformSpace.Equicontinuity
+import Mathlib.Topology.Algebra.Support
 import Mathlib.Topology.UniformSpace.Compact
-import Mathlib.Topology.Support
+import Mathlib.Topology.UniformSpace.Equicontinuity
 
 /-!
 # Compact separated uniform spaces