Theorems · Theorem · commutative algebra

IsLinearTopology.hasBasis_subbimodule

∀ (R : Type u_1) (R' : Type u_2) {M : Type u_3} [inst : Ring R] [inst_1 : Ring R'] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] [inst_4 : Module R' M] [SMulCommClass R R' M] [inst_6 : TopologicalSpace M]
  [IsLinearTopology R M] [IsLinearTopology R' M],
  (nhds 0).HasBasis (fun I => ↑I ∈ nhds 0 ∧ (∀ (r : R), ∀ x ∈ I, r • x ∈ I) ∧ ∀ (r' : R'), ∀ x ∈ I, r' • x ∈ I) fun I =>
    ↑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](kaplansky_topological_1947). 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.

Defined in

Mathlib.Topology.Algebra.LinearTopology

Cited by

2 results in Mathlib

Foundations

Depth 71 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

RingRingAddCommGroupModuleModuleSMulCommClassTopologicalSpaceIsLinearTopologyIsLinearTopology