English
If M is a bimodule with linear topologies for R and R' and SMulCommClass holds, then the zero-neighborhood basis consists of sub-(R,R')-bimodules.
Русский
Если M является би-модулем с линейными топологиями по R и R' и выполнен SMulCommClass, тогда вокруг нуля имеется база подмодулей, сохраняющих обе скалярные действия.
LaTeX
$$$ (\\mathcal{N}(0_M)).HasBasis \\big( I : AddSubgroup M \\mapsto (I:Set M) \\in 𝓝 0 \\land (\\forall r\\in R, \\forall x\\in I, r \\cdot x \\in I) \\land (\\forall r'\\in R', \\forall x\\in I, r' \\cdot x \\in I) \\big)\\,(\\text{I:Set}) $$$
Lean4
/-- 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 `AddSubgroup`s with
extra conditions. -/
theorem hasBasis_subbimodule [IsLinearTopology R M] [IsLinearTopology R' M] :
(𝓝 (0 : M)).HasBasis
(fun I : AddSubgroup M ↦ (I : Set M) ∈ 𝓝 0 ∧ (∀ r : R, ∀ x ∈ I, r • x ∈ I) ∧ (∀ r' : R', ∀ x ∈ I, r' • x ∈ I))
(fun I : AddSubgroup M ↦ (I : Set M)) :=
by
-- Start from a neighborhood `V`. It contains some open sub-`R`-module `I`.
refine
IsLinearTopology.hasBasis_submodule R |>.to_hasBasis (fun I hI ↦ ?_)
(fun I hI ↦ ⟨{ I with smul_mem' := fun r x hx ↦ hI.2.1 r x hx }, hI.1, subset_rfl⟩)
-- `I` itself is a neighborhood of zero, so it contains some open sub-`R'`-module `J`.
rcases (hasBasis_submodule R').mem_iff.mp hI with ⟨J, hJ, J_sub_I⟩
set uR : Set R := univ
set uR' : Set R' := univ
have hRR : uR * uR ⊆ uR := subset_univ _
have hRI : uR • (I : Set M) ⊆ I := smul_subset_iff.mpr fun x _ i hi ↦ I.smul_mem x hi
have hR'J : uR' • (J : Set M) ⊆ J := smul_subset_iff.mpr fun x _ j hj ↦ J.smul_mem x hj
have hRJ : uR • (J : Set M) ⊆ I := subset_trans (smul_subset_smul_left J_sub_I) hRI
set S : Set M := J ∪ uR • J
have S_sub_I : S ⊆ I := union_subset J_sub_I hRJ
have hRS : uR • S ⊆ S :=
calc
uR • S = uR • (J : Set M) ∪ (uR * uR) • (J : Set M) := by simp_rw [S, smul_union, mul_smul]
_ ⊆ uR • (J : Set M) ∪ uR • (J : Set M) := by gcongr
_ = uR • (J : Set M) := (union_self _)
_ ⊆ S := subset_union_right
have hR'S : uR' • S ⊆ S :=
calc
uR' • S = uR' • (J : Set M) ∪ uR • uR' • (J : Set M) := by simp_rw [S, smul_union, smul_comm]
_ ⊆ J ∪ uR • J := by gcongr
_ = S := rfl
set A : AddSubgroup M := .closure S
have hRA : ∀ r : R, ∀ i ∈ A, r • i ∈ A := fun r i hi ↦
by
refine AddSubgroup.closure_induction (fun x hx => ?base) ?zero (fun x y _ _ hx hy ↦ ?add) (fun x _ hx ↦ ?neg) hi
case base => exact AddSubgroup.subset_closure <| hRS <| Set.smul_mem_smul trivial hx
case zero => simp_rw [smul_zero]; exact zero_mem _
case add => simp_rw [smul_add]; exact add_mem hx hy
case neg => simp_rw [smul_neg]; exact neg_mem hx
have hR'A : ∀ r' : R', ∀ i ∈ A, r' • i ∈ A := fun r' i hi ↦
by
refine AddSubgroup.closure_induction (fun x hx => ?base) ?zero (fun x y _ _ hx hy ↦ ?add) (fun x _ hx ↦ ?neg) hi
case base => exact AddSubgroup.subset_closure <| hR'S <| Set.smul_mem_smul trivial hx
case zero => simp_rw [smul_zero]; exact zero_mem _
case add => simp_rw [smul_add]; exact add_mem hx hy
case neg => simp_rw [smul_neg]; exact neg_mem hx
have A_sub_I : (A : Set M) ⊆ I := I.toAddSubgroup.closure_le.mpr S_sub_I
have J_sub_A : (J : Set M) ⊆ A := subset_trans subset_union_left AddSubgroup.subset_closure
exact ⟨A, ⟨mem_of_superset hJ J_sub_A, hRA, hR'A⟩, A_sub_I⟩
