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. We prove that the module topology on R as a module over itself is R's original topology, and that the module topology is isomorphism-invariant.

Main theorems

• TopologicalSemiring.toIsModuleTopology : IsModuleTopology R R. The module topology on R is R's topology.
• IsModuleTopology.iso [IsModuleTopology R A] (e : A ≃L[R] B) : IsModuleTopology R B. If A and B are R-modules with topologies, if e is a topological isomorphism between them, and if A has the module topology, then B has the module topology.

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 on B is the pushforward of the module topology on A.

TODO

A forthcoming PR from the FLT repo will show that the module topology on a (binary or finite) product of modules is the product of the module topologies.

We will also show the slightly more subtle result that if M, N and P are R-modules equipped with the module topology and if furthermore M is finite as an R-module, then any bilinear map M × N → P is continuous.

As a consequence of this, we deduce that if R is a commutative topological ring and A is an R-algebra of finite type as R-module, then A with its module topology becomes a topological ring (i.e., multiplication is continuous).

Other TODOs (not done in the FLT repo):

• The module topology is a functor from the category of R-modules to the category of topological R-modules, and it's an adjoint to the forgetful functor.

@[reducible, inline]

abbrev moduleTopology (R : Type u_1) [TopologicalSpace R] (A : Type u_2) [Add A] [SMul R A] : TopologicalSpace A

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}

class IsModuleTopology (R : Type u_1) [TopologicalSpace R] (A : Type u_2) [Add A] [SMul R A] [τA : TopologicalSpace A] : Prop

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.

• eq_moduleTopology' : τA = moduleTopology R A

  Note that this should not be used directly, and eq_moduleTopology, which takes R and A explicitly, should be used instead.

theorem eq_moduleTopology (R : Type u_1) [TopologicalSpace R] (A : Type u_2) [Add A] [SMul R A] [τA : TopologicalSpace A] [IsModuleTopology R A] : τA = moduleTopology R A

theorem ModuleTopology.continuousSMul (R : Type u_1) [TopologicalSpace R] (A : Type u_2) [Add A] [SMul R A] : ContinuousSMul R A

Scalar multiplication • : R × A → A is continuous if R is a topological ring, and A is an R module with the module topology.

theorem ModuleTopology.continuousAdd (R : Type u_1) [TopologicalSpace R] (A : Type u_2) [Add A] [SMul R A] : ContinuousAdd A

Addition + : A × A → A is continuous if R is a topological ring, and A is an R module with the module topology.

instance IsModuleTopology.toContinuousSMul (R : Type u_1) [TopologicalSpace R] (A : Type u_2) [Add A] [SMul R A] [TopologicalSpace A] [IsModuleTopology R A] : ContinuousSMul R A

theorem IsModuleTopology.toContinuousAdd (R : Type u_1) [TopologicalSpace R] (A : Type u_2) [Add A] [SMul R A] [TopologicalSpace A] [IsModuleTopology R A] : ContinuousAdd A

theorem moduleTopology_le (R : Type u_1) [TopologicalSpace R] (A : Type u_2) [Add A] [SMul R A] [τA : TopologicalSpace A] [ContinuousSMul R A] [ContinuousAdd A] : moduleTopology R A ≤ τA

The module topology is ≤ any topology making A into a topological module.

theorem IsModuleTopology.of_continuous_id {R : Type u_1} [TopologicalSpace R] {A : Type u_2} [Add A] [SMul R A] [τA : TopologicalSpace A] [ContinuousAdd A] [ContinuousSMul R A] (h : Continuous id) : IsModuleTopology R A

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.

instance IsModuleTopology.instSubsingleton {R : Type u_1} [TopologicalSpace R] {A : Type u_2} [Add A] [SMul R A] [τA : TopologicalSpace A] [Subsingleton A] : IsModuleTopology R A

The zero module has the module topology.

theorem IsModuleTopology.iso {R : Type u_1} [τR : TopologicalSpace R] [Semiring R] {A : Type u_2} [AddCommMonoid A] [Module R A] [τA : TopologicalSpace A] [IsModuleTopology R A] {B : Type u_3} [AddCommMonoid B] [Module R B] [τB : TopologicalSpace B] (e : A ≃L[R] B) : IsModuleTopology R B

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.

instance TopologicalSemiring.toIsModuleTopology (R : Type u_1) [Semiring R] [τR : TopologicalSpace R] [TopologicalSemiring R] : IsModuleTopology R R

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).

instance TopologicalSemiring.toOppositeIsModuleTopology (R : Type u_1) [Semiring R] [τR : TopologicalSpace R] [TopologicalSemiring R] : IsModuleTopology Rᵐᵒᵖ R

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.

theorem IsModuleTopology.continuous_of_distribMulActionHom {R : Type u_1} [τR : TopologicalSpace R] [Semiring R] {A : Type u_2} [AddCommMonoid A] [Module R A] [aA : TopologicalSpace A] [IsModuleTopology R A] {B : Type u_3} [AddCommMonoid B] [Module R B] [aB : TopologicalSpace B] [ContinuousAdd B] [ContinuousSMul R B] (φ : A →+[R] B) : Continuous ⇑φ

Every R-linear map between two topological R-modules, where the source has the module topology, is continuous.

theorem IsModuleTopology.continuous_of_linearMap {R : Type u_1} [τR : TopologicalSpace R] [Semiring R] {A : Type u_2} [AddCommMonoid A] [Module R A] [aA : TopologicalSpace A] [IsModuleTopology R A] {B : Type u_3} [AddCommMonoid B] [Module R B] [aB : TopologicalSpace B] [ContinuousAdd B] [ContinuousSMul R B] (φ : A →ₗ[R] B) : Continuous ⇑φ

theorem IsModuleTopology.continuous_neg (R : Type u_1) [τR : TopologicalSpace R] [Semiring R] (C : Type u_4) [AddCommGroup C] [Module R C] [TopologicalSpace C] [IsModuleTopology R C] : Continuous fun (a : C) => -a

theorem IsModuleTopology.continuousNeg (R : Type u_1) [τR : TopologicalSpace R] [Semiring R] (C : Type u_4) [AddCommGroup C] [Module R C] [TopologicalSpace C] [IsModuleTopology R C] : ContinuousNeg C

theorem IsModuleTopology.topologicalAddGroup (R : Type u_1) [τR : TopologicalSpace R] [Semiring R] (C : Type u_4) [AddCommGroup C] [Module R C] [TopologicalSpace C] [IsModuleTopology R C] : TopologicalAddGroup C

theorem IsModuleTopology.continuous_of_ringHom {R : Type u_4} {A : Type u_5} {B : Type u_6} [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [TopologicalSpace R] [TopologicalSpace A] [IsModuleTopology R A] [TopologicalSpace B] [TopologicalSemiring B] (φ : A →+* B) (hφ : Continuous ⇑(φ.comp (algebraMap R A))) : Continuous ⇑φ

theorem IsModuleTopology.isQuotientMap_of_surjective {R : Type u_1} [τR : TopologicalSpace R] [Ring R] {A : Type u_2} [AddCommGroup A] [Module R A] [TopologicalSpace A] [IsModuleTopology R A] {B : Type u_3} [AddCommGroup B] [Module R B] [τB : TopologicalSpace B] [IsModuleTopology R B] {φ : A →ₗ[R] B} (hφ : Function.Surjective ⇑φ) : Topology.IsQuotientMap ⇑φ

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.

theorem ModuleTopology.eq_coinduced_of_surjective {R : Type u_1} [τR : TopologicalSpace R] [Ring R] {A : Type u_2} [AddCommGroup A] [Module R A] [TopologicalSpace A] [IsModuleTopology R A] {B : Type u_3} [AddCommGroup B] [Module R B] {φ : A →ₗ[R] B} (hφ : Function.Surjective ⇑φ) : moduleTopology R B = TopologicalSpace.coinduced (⇑φ) inferInstance