chore(topology): move 3 files to topology/algebra/module/ (#11242)

leanprover-community · Jan 5, 2022 · a1f4ac3 · a1f4ac3
1 parent 9fd7a02
commit a1f4ac3
Show file tree

Hide file tree

Showing 16 changed files with 17 additions and 17 deletions.
diff --git a/src/analysis/normed_space/banach_steinhaus.lean b/src/analysis/normed_space/banach_steinhaus.lean
@@ -5,7 +5,7 @@ Authors: Jireh Loreaux
 -/
 import analysis.normed_space.operator_norm
 import topology.metric_space.baire
-import topology.algebra.module
+import topology.algebra.module.basic
 /-!
 # The Banach-Steinhaus theorem: Uniform Boundedness Principle
 

diff --git a/src/analysis/normed_space/basic.lean b/src/analysis/normed_space/basic.lean
@@ -7,7 +7,7 @@ import algebra.algebra.restrict_scalars
 import algebra.algebra.subalgebra
 import analysis.normed.group.infinite_sum
 import data.matrix.basic
-import topology.algebra.module
+import topology.algebra.module.basic
 import topology.instances.ennreal
 import topology.sequences
 

diff --git a/src/analysis/normed_space/bounded_linear_maps.lean b/src/analysis/normed_space/bounded_linear_maps.lean
@@ -42,7 +42,7 @@ already expounds the theory of multilinear maps, but the `2`-variables case is s
 to currently deserve its own treatment.
 
 `is_bounded_linear_map` is effectively an unbundled version of `continuous_linear_map` (defined
-in `topology.algebra.module`, theory over normed spaces developed in
+in `topology.algebra.module.basic`, theory over normed spaces developed in
 `analysis.normed_space.operator_norm`), albeit the name disparity. A bundled
 `continuous_linear_map` is to be preferred over a `is_bounded_linear_map` hypothesis. Historical
 artifact, really.

diff --git a/src/analysis/normed_space/linear_isometry.lean b/src/analysis/normed_space/linear_isometry.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yury Kudryashov, Frédéric Dupuis, Heather Macbeth
 -/
 import analysis.normed.group.basic
-import topology.algebra.module
+import topology.algebra.module.basic
 
 /-!
 # (Semi-)linear isometries

diff --git a/src/analysis/normed_space/multilinear.lean b/src/analysis/normed_space/multilinear.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Sébastien Gouëzel
 -/
 import analysis.normed_space.operator_norm
-import topology.algebra.multilinear
+import topology.algebra.module.multilinear
 
 /-!
 # Operator norm on the space of continuous multilinear maps

diff --git a/src/analysis/normed_space/weak_dual.lean b/src/analysis/normed_space/weak_dual.lean
@@ -3,7 +3,7 @@ Copyright (c) 2021 Kalle Kytölä. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kalle Kytölä
 -/
-import topology.algebra.weak_dual_topology
+import topology.algebra.module.weak_dual
 import analysis.normed_space.dual
 import analysis.normed_space.operator_norm
 
@@ -42,7 +42,7 @@ TODOs:
 * Add that in finite dimensions, the weak-* topology and the dual norm topology coincide.
 * Add that in infinite dimensions, the weak-* topology is strictly coarser than the dual norm
   topology.
-* Add Banach-Alaoglu theorem (general version maybe in `topology.algebra.weak_dual_topology`).
+* Add Banach-Alaoglu theorem (general version maybe in `topology.algebra.module.weak_dual`).
 * Add metrizability of the dual unit ball (more generally bounded subsets) of `weak_dual 𝕜 E`
   under the assumption of separability of `E`. Sequential Banach-Alaoglu theorem would then follow
   from the general one.
@@ -53,7 +53,7 @@ No new notation is introduced.
 
 ## Implementation notes
 
-Weak-* topology is defined generally in the file `topology.algebra.weak_dual_topology`.
+Weak-* topology is defined generally in the file `topology.algebra.module.weak_dual`.
 
 When `E` is a normed space, the duals `dual 𝕜 E` and `weak_dual 𝕜 E` are type synonyms with
 different topology instances.

diff --git a/src/measure_theory/measure/finite_measure_weak_convergence.lean b/src/measure_theory/measure/finite_measure_weak_convergence.lean
@@ -6,7 +6,7 @@ Authors: Kalle Kytölä
 import measure_theory.measure.measure_space
 import measure_theory.integral.bochner
 import topology.continuous_function.bounded
-import topology.algebra.weak_dual_topology
+import topology.algebra.module.weak_dual
 
 /-!
 # Weak convergence of (finite) measures

diff --git a/src/topology/algebra/algebra.lean b/src/topology/algebra/algebra.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Scott Morrison
 -/
 import algebra.algebra.subalgebra
-import topology.algebra.module
+import topology.algebra.module.basic
 
 /-!
 # Topological (sub)algebras

diff --git a/src/topology/algebra/continuous_affine_map.lean b/src/topology/algebra/continuous_affine_map.lean
@@ -5,7 +5,7 @@ Authors: Oliver Nash
 -/
 import linear_algebra.affine_space.affine_map
 import topology.continuous_function.basic
-import topology.algebra.module
+import topology.algebra.module.basic
 
 /-!
 # Continuous affine maps.

diff --git a/src/topology/algebra/filter_basis.lean b/src/topology/algebra/filter_basis.lean
@@ -5,7 +5,7 @@ Authors: Patrick Massot
 -/
 
 import order.filter.bases
-import topology.algebra.module
+import topology.algebra.module.basic
 /-!
 # Group and ring filter bases
 

diff --git a/src/topology/algebra/module.lean → src/topology/algebra/module/basic.lean b/src/topology/algebra/module.lean → src/topology/algebra/module/basic.lean
diff --git a/src/topology/algebra/multilinear.lean → src/topology/algebra/module/multilinear.lean b/src/topology/algebra/multilinear.lean → src/topology/algebra/module/multilinear.lean
@@ -3,7 +3,7 @@ Copyright (c) 2020 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 topology.algebra.module
+import topology.algebra.module.basic
 import linear_algebra.multilinear.basic
 
 /-!

diff --git a/src/topology/algebra/weak_dual_topology.lean → src/topology/algebra/module/weak_dual.lean b/src/topology/algebra/weak_dual_topology.lean → src/topology/algebra/module/weak_dual.lean
@@ -3,7 +3,7 @@ Copyright (c) 2021 Kalle Kytölä. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kalle Kytölä
 -/
-import topology.algebra.module
+import topology.algebra.module.basic
 
 /-!
 # Weak dual topology

diff --git a/src/topology/continuous_function/algebra.lean b/src/topology/continuous_function/algebra.lean
@@ -3,7 +3,7 @@ Copyright (c) 2019 Scott Morrison. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Scott Morrison, Nicolò Cavalleri
 -/
-import topology.algebra.module
+import topology.algebra.module.basic
 import topology.continuous_function.basic
 import algebra.algebra.subalgebra
 import tactic.field_simp

diff --git a/src/topology/instances/real_vector_space.lean b/src/topology/instances/real_vector_space.lean
@@ -3,7 +3,7 @@ Copyright (c) 2020 Yury Kudryashov. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yury Kudryashov
 -/
-import topology.algebra.module
+import topology.algebra.module.basic
 import topology.instances.real
 
 /-!

diff --git a/src/topology/vector_bundle.lean b/src/topology/vector_bundle.lean
@@ -5,7 +5,7 @@ Authors: Nicolò Cavalleri, Sebastien Gouezel
 -/
 
 import topology.fiber_bundle
-import topology.algebra.module
+import topology.algebra.module.basic
 
 /-!
 # Topological vector bundles