English
If M is linearly topologized over R and over Rᵐᵒᵖ, then the zero-neighborhood basis can be taken from two-sided ideals.
Русский
Если M линейно топологизирован по R и по Rᵐᵒᵖ, база окрестностей нуля может быть взята из двусторонних идеалов.
LaTeX
$$$ (\\mathcal{N}(0)).HasBasis (fun I : TwoSidedIdeal R \\Rightarrow (I:Set R) \\in 𝓝 0) (fun I => I:Set R) $$$
Lean4
/-- 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 _root_.IsCentralScalar.isLinearTopology_iff [Module Rᵐᵒᵖ M] [IsCentralScalar R M] :
IsLinearTopology Rᵐᵒᵖ M ↔ IsLinearTopology R M :=
by
constructor <;> intro H
·
exact
mk_of_hasBasis' R (IsLinearTopology.hasBasis_submodule Rᵐᵒᵖ) fun S r m hm ↦ op_smul_eq_smul r m ▸ S.smul_mem _ hm
·
exact
mk_of_hasBasis' Rᵐᵒᵖ (IsLinearTopology.hasBasis_submodule R) fun S r m hm ↦
unop_smul_eq_smul r m ▸ S.smul_mem _ hm
