English
The product of the module topologies on M and N is the module topology on M × N.
Русский
Произведение модульных топологий на M и N равно модульной топологии на произведении M × N.
LaTeX
$$$IsModuleTopology(R, M \times N)$$$
Lean4
/-- The product of the module topologies for two modules over a topological ring
is the module topology. -/
instance instProd : IsModuleTopology R (M × N) := by
constructor
have : ContinuousAdd M := toContinuousAdd R M
have : ContinuousAdd N := toContinuousAdd R N
refine
le_antisymm ?_ <|
sInf_le
⟨Prod.continuousSMul, Prod.continuousAdd⟩
-- Or equivalently, if `P` denotes `M × N` with the module topology,
let P := M × N
let τP : TopologicalSpace P := moduleTopology R P
have : IsModuleTopology R P := ⟨rfl⟩
have : ContinuousAdd P := ModuleTopology.continuousAdd R P
let i : M × N → P := id
rw [← continuous_id_iff_le]
change @Continuous (M × N) P instTopologicalSpaceProd τP i
let i₁ : M →ₗ[R] P := LinearMap.inl R M N
let i₂ : N →ₗ[R] P := LinearMap.inr R M N
rw [show (i : M × N → P) = (fun abcd ↦ abcd.1 + abcd.2 : P × P → P) ∘ (fun ab ↦ (i₁ ab.1, i₂ ab.2)) by
ext ⟨a, b⟩ <;> aesop]
-- and these maps are all continuous, hence `i` is too
fun_prop
