A "module topology" for modules over a topological ring #
If R
is a topological ring acting on an additive abelian group A
, we define the
module topology to be the finest topology on A
making both the maps
• : R × A → A
and + : A × A → A
continuous (with all the products having the
product topology). Note that - : A → A
is also automatically continuous as it is a ↦ (-1) • a
.
This topology was suggested by Will Sawin here.
Mathematical details #
I (buzzard) don't know of any reference for this other than Sawin's mathoverflow answer, so I expand some of the details here.
First note that the definition makes sense in far more generality (for example R
just needs to
be a topological space acting on an additive monoid).
Next note that there is a finest topology with this property! Indeed, topologies on a fixed
type form a complete lattice (infinite infs and sups exist). So if τ
is the Inf of all
the topologies on A
which make +
and •
continuous, then the claim is that +
and •
are still continuous for τ
(note that topologies are ordered so that finer topologies
are smaller). To show + : A × A → A
is continuous we equivalently need to show
that the pushforward of the product topology τ × τ
along +
is ≤ τ
, and because τ
is
the greatest lower bound of the topologies making •
and +
continuous,
it suffices to show that it's ≤ σ
for any topology σ
on A
which makes +
and •
continuous.
However pushforward and products are monotone, so τ × τ ≤ σ × σ
, and the pushforward of
σ × σ
is ≤ σ
because that's precisely the statement that +
is continuous for σ
.
The proof for •
follows mutatis mutandis.
A topological module for a topological ring R
is an R
-module A
with a topology
making +
and •
continuous. The discussion so far has shown that the module topology makes
an R
-module A
into a topological module, and moreover is the finest topology with this property.
A crucial observation is that if M
is a topological R
-module, if A
is an R
-module with no
topology, and if φ : A → M
is linear, then the pullback of M
's topology to A
is a topology
making A
into a topological module. Let's for example check that •
is continuous.
If U ⊆ A
is open then by definition of the pullback topology, U = φ⁻¹(V)
for some open V ⊆ M
,
and now the pullback of U
under •
is just the pullback along the continuous map
id × φ : R × A → R × M
of the preimage of V
under the continuous map • : R × M → M
,
so it's open. The proof for +
is similar.
As a consequence of this, we see that if φ : A → M
is a linear map between topological R
-modules
modules and if A
has the module topology, then φ
is automatically continuous.
Indeed the argument above shows that if A → M
is linear then the module
topology on A
is ≤
the pullback of the module topology on M
(because it's the inf of a set
containing this topology) which is the definition of continuity.
We also deduce that the module topology is a functor from the category of R
-modules
(R
a topological ring) to the category of topological R
-modules, and it is perhaps
unsurprising that this is an adjoint to the forgetful functor. Indeed, if A
is an R
-module
and M
is a topological R
-module, then the previous paragraph shows that
the linear maps A → M
are precisely the continuous linear maps
from (A
with its module topology) to M
, so the module topology is a left adjoint
to the forgetful functor.
This file develops the theory of the module topology.
Main theorems #
IsTopologicalSemiring.toIsModuleTopology : IsModuleTopology R R
. The module topology onR
isR
's topology.IsModuleTopology.iso [IsModuleTopology R A] (e : A ≃L[R] B) : IsModuleTopology R B
. IfA
andB
areR
-modules with topologies, ife
is a topological isomorphism between them, and ifA
has the module topology, thenB
has the module topology.IsModuleTopology.instProd
: IfM
andN
areR
-modules each equipped with the module topology, then the product topology onM × N
is the module topology.IsModuleTopology.instPi
: Given a finite collection ofR
-modules each of which has the module topology, the product topology on the product module is the module topology.IsModuleTopology.isTopologicalRing
: IfD
is anR
-algebra equipped with the module topology, andD
is finite as anR
-module, thenD
is a topological ring (that is, addition, negation and multiplication are continuous).
Now say φ : A →ₗ[R] B
is an R
-linear map between R
-modules equipped with
the module topology.
IsModuleTopology.continuous_of_linearMap φ
is the proof thatφ
is automatically continuous.IsModuleTopology.isQuotientMap_of_surjective (hφ : Function.Surjective φ)
is the proof that if furthermoreφ
is surjective then it is a quotient map, that is, the module topology onB
is the pushforward of the module topology onA
.
Now say ψ : A →ₗ[R] B →ₗ[R] C
is an R
-bilinear map between R
-modules equipped with
the module topology.
IsModuleTopology.continuous_bilinear_of_finite_left
: IfA
is finite thenA × B → C
is continuous.IsModuleTopology.continuous_bilinear_of_finite_right
: IfB
is finite thenA × B → C
is continuous.
TODO #
- The module topology is a functor from the category of
R
-modules to the category of topologicalR
-modules, and it's an adjoint to the forgetful functor.
The module topology, for a module A
over a topological ring R
. It's the finest topology
making addition and the R
-action continuous, or equivalently the finest topology making A
into a topological R
-module. More precisely it's the Inf of the set of
topologies with these properties; theorems continuousSMul
and continuousAdd
show
that the module topology also has these properties.
Equations
- moduleTopology R A = sInf {t : TopologicalSpace A | ContinuousSMul R A ∧ ContinuousAdd A}
Instances For
A class asserting that the topology on a module over a topological ring R
is
the module topology. See moduleTopology
for more discussion of the module topology.
Note that this should not be used directly, and
eq_moduleTopology
, which takesR
andA
explicitly, should be used instead.
Instances
Note that the topology isn't part of the discrimination key so this gets tried on every
IsModuleTopology
goal and hence the low priority.
Scalar multiplication • : R × A → A
is continuous if R
is a topological
ring, and A
is an R
module with the module topology.
Addition + : A × A → A
is continuous if R
is a topological
ring, and A
is an R
module with the module topology.
The module topology is ≤
any topology making A
into a topological module.
If A
is a topological R
-module and the identity map from (A
with its given
topology) to (A
with the module topology) is continuous, then the topology on A
is
the module topology.
The zero module has the module topology.
If A
and B
are R
-modules, homeomorphic via an R
-linear homeomorphism, and if
A
has the module topology, then so does B
.
We now fix once and for all a topological semiring R
.
We first prove that the module topology on R
considered as a module over itself,
is R
's topology.
The topology on a topological semiring R
agrees with the module topology when considering
R
as an R
-module in the obvious way (i.e., via Semiring.toModule
).
The module topology coming from the action of the topological ring Rᵐᵒᵖ
on R
(via Semiring.toOppositeModule
, i.e. via (op r) • m = m * r
) is R
's topology.
Every R
-linear map between two topological R
-modules, where the source has the module
topology, is continuous.
A linear surjection between modules with the module topology is a quotient map. Equivalently, the pushforward of the module topology along a surjective linear map is again the module topology.
The product of the module topologies for two modules over a topological ring is the module topology.
The product of the module topologies for a finite family of modules over a topological ring is the module topology.
If n
is finite and B
,C
are R
-modules with the module topology,
then any bilinear map Rⁿ × B → C
is automatically continuous.
Note that whilst this result works for semirings, for rings this result is superseded
by IsModuleTopology.continuous_bilinear_of_finite_left
.
If A
, B
and C
have the module topology, and if furthermore A
is a finite R
-module,
then any bilinear map A × B → C
is automatically continuous
If A
, B
and C
have the module topology, and if furthermore B
is a finite R
-module,
then any bilinear map A × B → C
is automatically continuous
If D
is an R
-algebra, finite as an R
-module, and if D
has the module topology,
then multiplication on D
is automatically continuous.
If R
is a topological ring and D
is an R
-algebra, finite as an R
-module,
and if D
is given the module topology, then D
is a topological ring.