instQuot — Mathlib

English

There is an instance giving the module topology on the quotient A/S, induced by the quotient map.

Русский

Существует экземпляр, задающий модульную топологию на фактор-модуле A/S, индуцированную через фактор-мэп.

LaTeX

$$$IsModuleTopology R (A/S)$$$

Lean4

instance instQuot (S : Submodule R A) : IsModuleTopology R (A ⧸ S) :=
  by
  constructor
  have := toContinuousAdd R A
  have quot := (Submodule.isOpenQuotientMap_mkQ S).isQuotientMap.eq_coinduced
  have module := ModuleTopology.eq_coinduced_of_surjective <| Submodule.mkQ_surjective S
  rw [quot, module]

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