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 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.
• IsModuleTopology.instProd : If M and N are R-modules each equipped with the module topology, then the product topology on M × N is the module topology.
• IsModuleTopology.instPi : Given a finite collection of R-modules each of which has the module topology, the product topology on the product module is the module topology.
• IsModuleTopology.isTopologicalRing : If D is an R-algebra equipped with the module topology, and D is finite as an R-module, then D 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 on B is the pushforward of the module topology on A.

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 : If A is finite then A × B → C is continuous.
• IsModuleTopology.continuous_bilinear_of_finite_right : If B is finite then A × B → C is continuous.

TODO

• 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

@[instance 100]

instance instIsModuleTopology {R : Type u_3} [TopologicalSpace R] {A : Type u_4} [Add A] [SMul R A] : IsModuleTopology R A

Note that the topology isn't part of the discrimination key so this gets tried on every IsModuleTopology goal and hence the low priority.

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 IsTopologicalSemiring.toIsModuleTopology (R : Type u_1) [Semiring R] [τR : TopologicalSpace R] [IsTopologicalSemiring 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 IsTopologicalSemiring.toOppositeIsModuleTopology (R : Type u_1) [Semiring R] [τR : TopologicalSpace R] [IsTopologicalSemiring 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] : IsTopologicalAddGroup 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] [IsTopologicalSemiring 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 IsModuleTopology.isOpenQuotientMap_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] [TopologicalSpace B] [IsModuleTopology R B] {φ : A →ₗ[R] B} (hφ : Function.Surjective ⇑φ) : IsOpenQuotientMap ⇑φ

A linear surjection between modules with the module topology is an open quotient map.

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

A linear surjection to a module with the module topology is open.

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

instance IsModuleTopology.instQuot {R : Type u_1} [τR : TopologicalSpace R] [Ring R] {A : Type u_2} [AddCommGroup A] [Module R A] [TopologicalSpace A] [IsModuleTopology R A] (S : Submodule R A) : IsModuleTopology R (A ⧸ S)

instance IsModuleTopology.instProd {R : Type u_1} [TopologicalSpace R] [Semiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] [TopologicalSpace M] [IsModuleTopology R M] {N : Type u_3} [AddCommMonoid N] [Module R N] [TopologicalSpace N] [IsModuleTopology R N] : IsModuleTopology R (M × N)

The product of the module topologies for two modules over a topological ring is the module topology.

instance IsModuleTopology.instPi {R : Type u_1} [TopologicalSpace R] [Semiring R] {ι : Type u_2} [Finite ι] {A : ι → Type u_3} [(i : ι) → AddCommMonoid (A i)] [(i : ι) → Module R (A i)] [(i : ι) → TopologicalSpace (A i)] [∀ (i : ι), IsModuleTopology R (A i)] : IsModuleTopology R ((i : ι) → A i)

The product of the module topologies for a finite family of modules over a topological ring is the module topology.

theorem IsModuleTopology.continuous_bilinear_of_pi_fintype {R : Type u_1} [TopologicalSpace R] [CommSemiring R] {B : Type u_2} [AddCommMonoid B] [Module R B] [TopologicalSpace B] [IsModuleTopology R B] {C : Type u_3} [AddCommMonoid C] [Module R C] [TopologicalSpace C] [IsModuleTopology R C] (ι : Type u_4) [Finite ι] (bil : (ι → R) →ₗ[R] B →ₗ[R] C) : Continuous fun (ab : (ι → R) × B) => (bil ab.1) ab.2

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.

theorem IsModuleTopology.continuous_bilinear_of_finite_left {R : Type u_1} [TopologicalSpace R] [CommRing R] [IsTopologicalRing R] {A : Type u_2} [AddCommGroup A] [Module R A] [aA : TopologicalSpace A] [IsModuleTopology R A] {B : Type u_3} [AddCommGroup B] [Module R B] [aB : TopologicalSpace B] [IsModuleTopology R B] {C : Type u_4} [AddCommGroup C] [Module R C] [aC : TopologicalSpace C] [IsModuleTopology R C] [Module.Finite R A] (bil : A →ₗ[R] B →ₗ[R] C) : Continuous fun (ab : A × B) => (bil ab.1) ab.2

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

theorem IsModuleTopology.continuous_bilinear_of_finite_right {R : Type u_1} [TopologicalSpace R] [CommRing R] [IsTopologicalRing R] {A : Type u_2} [AddCommGroup A] [Module R A] [aA : TopologicalSpace A] [IsModuleTopology R A] {B : Type u_3} [AddCommGroup B] [Module R B] [aB : TopologicalSpace B] [IsModuleTopology R B] {C : Type u_4} [AddCommGroup C] [Module R C] [aC : TopologicalSpace C] [IsModuleTopology R C] [Module.Finite R B] (bil : A →ₗ[R] B →ₗ[R] C) : Continuous fun (ab : A × B) => (bil ab.1) ab.2

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

theorem IsModuleTopology.continuous_mul_of_finite (R : Type u_1) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R] (D : Type u_2) [Ring D] [Algebra R D] [Module.Finite R D] [TopologicalSpace D] [IsModuleTopology R D] : Continuous fun (ab : D × D) => ab.1 * ab.2

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.

theorem IsModuleTopology.isTopologicalRing (R : Type u_1) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R] (D : Type u_2) [Ring D] [Algebra R D] [Module.Finite R D] [TopologicalSpace D] [IsModuleTopology R D] : IsTopologicalRing D

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.