From 2aefce62d6d933585e9c688b080ebeadc5c8e7ee Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ya=C3=ABl=20Dillies?= Date: Sun, 1 Dec 2024 16:15:39 +0000 Subject: [PATCH] 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 | 2 +- Mathlib/Topology/Algebra/ConstMulAction.lean | 2 +- Mathlib/Topology/{ => Algebra}/Support.lean | 0 Mathlib/Topology/ContinuousMap/CompactlySupported.lean | 2 +- Mathlib/Topology/Homeomorph.lean | 4 ++-- Mathlib/Topology/MetricSpace/ProperSpace.lean | 4 ++-- Mathlib/Topology/Order/Compact.lean | 4 ++-- Mathlib/Topology/UniformSpace/HeineCantor.lean | 4 ++-- 8 files changed, 11 insertions(+), 11 deletions(-) rename Mathlib/Topology/{ => Algebra}/Support.lean (100%) diff --git a/Mathlib.lean b/Mathlib.lean index f120c15dfeb9e..99e0381f97d9a 100644 --- a/Mathlib.lean +++ b/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 diff --git a/Mathlib/Topology/Algebra/ConstMulAction.lean b/Mathlib/Topology/Algebra/ConstMulAction.lean index 10007257a47c5..cd4bdb42717b6 100644 --- a/Mathlib/Topology/Algebra/ConstMulAction.lean +++ b/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 diff --git a/Mathlib/Topology/Support.lean b/Mathlib/Topology/Algebra/Support.lean similarity index 100% rename from Mathlib/Topology/Support.lean rename to Mathlib/Topology/Algebra/Support.lean diff --git a/Mathlib/Topology/ContinuousMap/CompactlySupported.lean b/Mathlib/Topology/ContinuousMap/CompactlySupported.lean index cb59956edbce0..eb5348c9f448c 100644 --- a/Mathlib/Topology/ContinuousMap/CompactlySupported.lean +++ b/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 diff --git a/Mathlib/Topology/Homeomorph.lean b/Mathlib/Topology/Homeomorph.lean index f536c0c7e30dc..f98a10c4d8b6b 100644 --- a/Mathlib/Topology/Homeomorph.lean +++ b/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 diff --git a/Mathlib/Topology/MetricSpace/ProperSpace.lean b/Mathlib/Topology/MetricSpace/ProperSpace.lean index 3868c4d9c6a97..69d91fcc8b806 100644 --- a/Mathlib/Topology/MetricSpace/ProperSpace.lean +++ b/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 diff --git a/Mathlib/Topology/Order/Compact.lean b/Mathlib/Topology/Order/Compact.lean index bf30e3961311d..c8c4297800a48 100644 --- a/Mathlib/Topology/Order/Compact.lean +++ b/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 diff --git a/Mathlib/Topology/UniformSpace/HeineCantor.lean b/Mathlib/Topology/UniformSpace/HeineCantor.lean index d97593eba0566..166e33321e049 100644 --- a/Mathlib/Topology/UniformSpace/HeineCantor.lean +++ b/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