continuousSMul_quotient — Mathlib

English

If R carries a topology and M is a topological R-module with continuous scalar action, then the quotient M/S carries a natural continuous scalar action of R.

Русский

Пусть R — топологическое кольцо, а M — топологический модуль над R с непрерывным действием скаляров. Тогда фактор-множество M/S наследует непрерывное действие скаляров R.

LaTeX

$$$M/S\\text{ is a topological }R\\text{-module}.$$$

Lean4

instance continuousSMul_quotient [TopologicalSpace R] [IsTopologicalAddGroup M] [ContinuousSMul R M] :
    ContinuousSMul R (M ⧸ S) where
  continuous_smul :=
    by
    rw [← (IsOpenQuotientMap.id.prodMap S.isOpenQuotientMap_mkQ).continuous_comp_iff]
    exact continuous_quot_mk.comp continuous_smul

Похожие утверждения