Linear topologies on modules and rings

Let M be a (left) module over a ring R. Following Stacks: Definition 15.36.1, we say that a topology on M is R-linear if it is invariant by translations and admits a basis of neighborhoods of 0 consisting of (left) R-submodules.

If M is an (R, R')-bimodule, we show that a topology is both R-linear and R'-linear if and only if there exists a basis of neighborhoods of 0 consisting of (R, R')-subbimodules.

In particular, we say that a topology on the ring R is linear if it is linear if it is linear when R is viewed as an (R, Rᵐᵒᵖ)-bimodule. By the previous results, this means that there exists a basis of neighborhoods of 0 consisting of two-sided ideals, hence our definition agrees with N. Bourbaki, Algebra II, chapter 4, §2, n° 3.

Main definitions and statements

• IsLinearTopology R M: the topology on M is R-linear, meaning that there exists a basis of neighborhoods of 0 consisting of R-submodules. Note that we don't impose that the topology is invariant by translation, so you'll often want to add ContinuousConstVAdd M M to get something meaningless. To express that the topology of a ring R is linear, use [IsLinearTopology R R] [IsLinearTopology Rᵐᵒᵖ R].

• IsLinearTopology.mk_of_hasBasis: a convenient constructor for IsLinearTopology. See also IsLinearTopology.mk_of_hasBasis'.

• The discrete topology on M is R-linear (declared as an instance).

• IsLinearTopology.hasBasis_subbimodule: assume that M is an (R, R')-bimodule, and that its topology is both R-linear and R'-linear. Then there exists a basis of neighborhoods of 0 made of (R, R')-subbimodules. Note that this is not trivial, since the bases witnessing R-linearity and R'-linearity may have nothing to do with each other

• IsLinearTopology.tendsto_smul_zero: assume that the topology on M is linear. For m : ι → M such that m i tends to 0, r i • m i still tends to 0 for any r : ι → R.

• IsLinearTopology.hasBasis_twoSidedIdeal: if the ring R is linearly topologized, in the sense that we have both IsLinearTopology R R and IsLinearTopology Rᵐᵒᵖ R, then there exists a basis of neighborhoods of 0 consisting of two-sided ideals.

• Conversely, to prove IsLinearTopology R R and IsLinearTopology Rᵐᵒᵖ R from a basis of two-sided ideals, use IsLinearTopology.mk_of_hasBasis' twice.

• IsLinearTopology.tendsto_mul_zero_of_left: assume that the topology on R is (right-)linear. For f, g : ι → R such that f i tends to 0, f i * g i still tends to 0.

• IsLinearTopology.tendsto_mul_zero_of_right: assume that the topology on R is (left-)linear. For f, g : ι → R such that g i tends to 0, f i * g i still tends to 0

• If R is a commutative ring and its topology is left-linear, it is automatically right-linear (declared as a low-priority instance).

Notes on the implementation

• Some statements assume ContinuousAdd M where ContinuousConstVAdd M M (invariance by translation) would be enough. In fact, in presence of IsLinearTopology R M, invariance by translation implies that M is a topological additive group on which R acts by homeomorphisms. Similarly, IsLinearTopology R R and ContinuousConstVAdd R R imply that R is a topological ring. All of this will follow from PR#18437.

Nevertheless, we don't plan on adding those facts as instances: one should use directly results from PR#18437 to get TopologicalAddGroup and TopologicalRing instances.

• The main constructor for IsLinearTopology, IsLinearTopology.mk_of_hasBasis is formulated in terms of the subobject classes AddSubmonoidClass and SMulMemClass to allow for more complicated types than Submodule R M or Ideal R. Unfortunately, the scalar ring in SMulMemClass is an outParam, which means that Lean only considers one base ring for a given subobject type. For example, Lean will never find SMulMemClass (TwoSidedIdeal R) R R because it prioritizes the (later-defined) instance of SMulMemClass (TwoSidedIdeal R) Rᵐᵒᵖ R.

This makes IsLinearTopology.mk_of_hasBasis un-applicable to TwoSidedIdeal (and probably other types), thus we provide IsLinearTopology.mk_of_hasBasis' as an alternative not relying on typeclass inference.

class IsLinearTopology (R : Type u_1) (M : Type u_3) [Ring R] [AddCommGroup M] [Module R M] [TopologicalSpace M] : Prop

Consider a (left-)module M over a ring R. A topology on M is R-linear if the open sub-R-modules of M form a basis of neighborhoods of zero.

Typically one would also that the topology is invariant by translation (ContinuousConstVAdd M M), or equivalently that M is a topological group, but we do not assume it for the definition.

In particular, we say that a topology on the ring R is linear if it is both R-linear and Rᵐᵒᵖ-linear for the obvious module structures. To spell this in Lean, simply use [IsLinearTopology R R] [IsLinearTopology Rᵐᵒᵖ R].

• hasBasis_submodule' : (nhds 0).HasBasis (fun (N : Submodule R M) => ↑N ∈ nhds 0) fun (N : Submodule R M) => ↑N

theorem IsLinearTopology.hasBasis_submodule (R : Type u_1) {M : Type u_3} [Ring R] [AddCommGroup M] [Module R M] [TopologicalSpace M] [IsLinearTopology R M] : (nhds 0).HasBasis (fun (N : Submodule R M) => ↑N ∈ nhds 0) fun (N : Submodule R M) => ↑N

theorem IsLinearTopology.hasBasis_open_submodule (R : Type u_1) {M : Type u_3} [Ring R] [AddCommGroup M] [Module R M] [TopologicalSpace M] [ContinuousAdd M] [IsLinearTopology R M] : (nhds 0).HasBasis (fun (N : Submodule R M) => IsOpen ↑N) fun (N : Submodule R M) => ↑N

theorem IsLinearTopology.mk_of_hasBasis' (R : Type u_1) {M : Type u_3} [Ring R] [AddCommGroup M] [Module R M] [TopologicalSpace M] {ι : Sort u_4} {S : Type u_5} [SetLike S M] [AddSubmonoidClass S M] {p : ι → Prop} {s : ι → S} (h : (nhds 0).HasBasis p fun (i : ι) => ↑(s i)) (hsmul : ∀ (s : S) (r : R), ∀ m ∈ s, r • m ∈ s) : IsLinearTopology R M

A variant of IsLinearTopology.mk_of_hasBasis asking for an explicit proof that S is a class of submodules instead of relying on (fragile) typeclass inference of SMulCommClass.

theorem IsLinearTopology.mk_of_hasBasis (R : Type u_1) {M : Type u_3} [Ring R] [AddCommGroup M] [Module R M] [TopologicalSpace M] {ι : Sort u_4} {S : Type u_5} [SetLike S M] [SMulMemClass S R M] [AddSubmonoidClass S M] {p : ι → Prop} {s : ι → S} (h : (nhds 0).HasBasis p fun (i : ι) => ↑(s i)) : IsLinearTopology R M

To show that M is linearly-topologized as an R-module, it suffices to show that it has a basis of neighborhoods of zero made of R-submodules.

Note: for technical reasons detailed in the module docstring, Lean sometimes struggle to find the right SMulMemClass instance. See IsLinearTopology.mk_of_hasBasis' for a more explicit variant.

theorem isLinearTopology_iff_hasBasis_submodule {R : Type u_1} {M : Type u_3} [Ring R] [AddCommGroup M] [Module R M] [TopologicalSpace M] : IsLinearTopology R M ↔ (nhds 0).HasBasis (fun (N : Submodule R M) => ↑N ∈ nhds 0) fun (N : Submodule R M) => ↑N

theorem isLinearTopology_iff_hasBasis_open_submodule {R : Type u_1} {M : Type u_3} [Ring R] [AddCommGroup M] [Module R M] [TopologicalSpace M] [ContinuousAdd M] : IsLinearTopology R M ↔ (nhds 0).HasBasis (fun (N : Submodule R M) => IsOpen ↑N) fun (N : Submodule R M) => ↑N

instance IsLinearTopology.instOfDiscreteTopology {R : Type u_1} {M : Type u_3} [Ring R] [AddCommGroup M] [Module R M] [TopologicalSpace M] [DiscreteTopology M] : IsLinearTopology R M

The discrete topology on any R-module is R-linear.

theorem IsLinearTopology.hasBasis_subbimodule (R : Type u_1) (R' : Type u_2) {M : Type u_3} [Ring R] [Ring R'] [AddCommGroup M] [Module R M] [Module R' M] [SMulCommClass R R' M] [TopologicalSpace M] [IsLinearTopology R M] [IsLinearTopology R' M] : (nhds 0).HasBasis (fun (I : AddSubgroup M) => ↑I ∈ nhds 0 ∧ (∀ (r : R), ∀ x ∈ I, r • x ∈ I) ∧ ∀ (r' : R'), ∀ x ∈ I, r' • x ∈ I) fun (I : AddSubgroup M) => ↑I

Assume that M is a module over two rings R and R', and that its topology is linear with respect to each of these rings. Then, it has a basis of neighborhoods of zero made of sub-(R, R')-bimodules.

The proof is inspired by lemma 9 in I. Kaplansky, Topological Rings. TODO: Formalize the lemma in its full strength.

Note: due to the lack of a satisfying theory of sub-bimodules, we use AddSubgroups with extra conditions.

theorem IsLinearTopology.hasBasis_open_subbimodule (R : Type u_1) (R' : Type u_2) {M : Type u_3} [Ring R] [Ring R'] [AddCommGroup M] [Module R M] [Module R' M] [SMulCommClass R R' M] [TopologicalSpace M] [ContinuousAdd M] [IsLinearTopology R M] [IsLinearTopology R' M] : (nhds 0).HasBasis (fun (I : AddSubgroup M) => IsOpen ↑I ∧ (∀ (r : R), ∀ x ∈ I, r • x ∈ I) ∧ ∀ (r' : R'), ∀ x ∈ I, r' • x ∈ I) fun (I : AddSubgroup M) => ↑I

A variant of IsLinearTopology.hasBasis_subbimodule using IsOpen I instead of I ∈ 𝓝 0.

theorem IsLinearTopology.tendsto_smul_zero (R : Type u_1) {M : Type u_3} [Ring R] [AddCommGroup M] [Module R M] [TopologicalSpace M] [IsLinearTopology R M] {ι : Type u_4} {f : Filter ι} (a : ι → R) (m : ι → M) (ha : Filter.Tendsto m f (nhds 0)) : Filter.Tendsto (a • m) f (nhds 0)

If M is a linearly topologized R-module and i ↦ m i tends to zero, then i ↦ a i • m i still tends to zero for any family a : ι → R.

theorem IsCentralScalar.isLinearTopology_iff (R : Type u_1) {M : Type u_3} [Ring R] [AddCommGroup M] [Module R M] [TopologicalSpace M] [Module Rᵐᵒᵖ M] [IsCentralScalar R M] : IsLinearTopology Rᵐᵒᵖ M ↔ IsLinearTopology R M

If the left and right actions of R on M coincide, then a topology is Rᵐᵒᵖ-linear if and only if it is R-linear.

theorem IsLinearTopology.hasBasis_ideal {R : Type u_1} [Ring R] [TopologicalSpace R] [IsLinearTopology R R] : (nhds 0).HasBasis (fun (I : Ideal R) => ↑I ∈ nhds 0) fun (I : Ideal R) => ↑I

theorem IsLinearTopology.hasBasis_open_ideal {R : Type u_1} [Ring R] [TopologicalSpace R] [ContinuousAdd R] [IsLinearTopology R R] : (nhds 0).HasBasis (fun (I : Ideal R) => IsOpen ↑I) fun (I : Ideal R) => ↑I

theorem isLinearTopology_iff_hasBasis_ideal {R : Type u_1} [Ring R] [TopologicalSpace R] : IsLinearTopology R R ↔ (nhds 0).HasBasis (fun (I : Ideal R) => ↑I ∈ nhds 0) fun (I : Ideal R) => ↑I

theorem isLinearTopology_iff_hasBasis_open_ideal {R : Type u_1} [Ring R] [TopologicalSpace R] [TopologicalRing R] : IsLinearTopology R R ↔ (nhds 0).HasBasis (fun (I : Ideal R) => IsOpen ↑I) fun (I : Ideal R) => ↑I

theorem IsLinearTopology.hasBasis_twoSidedIdeal {R : Type u_1} [Ring R] [TopologicalSpace R] [IsLinearTopology R R] [IsLinearTopology Rᵐᵒᵖ R] : (nhds 0).HasBasis (fun (I : TwoSidedIdeal R) => ↑I ∈ nhds 0) fun (I : TwoSidedIdeal R) => ↑I

If a ring R is linearly ordered as a left and right module over itself, then it has a basis of neighborhoods of zero made of two-sided ideals.

This is usually called a linearly topologized ring, but we do not add a specific spelling: you should use [IsLinearTopology R R] [IsLinearTopology Rᵐᵒᵖ R] instead.

theorem IsLinearTopology.hasBasis_open_twoSidedIdeal {R : Type u_1} [Ring R] [TopologicalSpace R] [ContinuousAdd R] [IsLinearTopology R R] [IsLinearTopology Rᵐᵒᵖ R] : (nhds 0).HasBasis (fun (I : TwoSidedIdeal R) => IsOpen ↑I) fun (I : TwoSidedIdeal R) => ↑I

theorem isLinearTopology_iff_hasBasis_twoSidedIdeal {R : Type u_1} [Ring R] [TopologicalSpace R] : IsLinearTopology R R ∧ IsLinearTopology Rᵐᵒᵖ R ↔ (nhds 0).HasBasis (fun (I : TwoSidedIdeal R) => ↑I ∈ nhds 0) fun (I : TwoSidedIdeal R) => ↑I

theorem isLinearTopology_iff_hasBasis_open_twoSidedIdeal {R : Type u_1} [Ring R] [TopologicalSpace R] [ContinuousAdd R] : IsLinearTopology R R ∧ IsLinearTopology Rᵐᵒᵖ R ↔ (nhds 0).HasBasis (fun (I : TwoSidedIdeal R) => IsOpen ↑I) fun (I : TwoSidedIdeal R) => ↑I

theorem IsLinearTopology.tendsto_mul_zero_of_left {R : Type u_1} [Ring R] [TopologicalSpace R] [IsLinearTopology Rᵐᵒᵖ R] {ι : Type u_2} {f : Filter ι} (a b : ι → R) (ha : Filter.Tendsto a f (nhds 0)) : Filter.Tendsto (a * b) f (nhds 0)

theorem IsLinearTopology.tendsto_mul_zero_of_right {R : Type u_1} [Ring R] [TopologicalSpace R] [IsLinearTopology R R] {ι : Type u_2} {f : Filter ι} (a b : ι → R) (hb : Filter.Tendsto b f (nhds 0)) : Filter.Tendsto (a * b) f (nhds 0)

@[instance 100]

instance IsLinearTopology.instMulOpposite {R : Type u_1} [CommRing R] [TopologicalSpace R] [IsLinearTopology R R] : IsLinearTopology Rᵐᵒᵖ R

If R is commutative and left-linearly topologized, it is also right-linearly topologized.