isOpenQuotientMap_of_surjective — Mathlib

English

If φ: A →ₗ[R] B is surjective and B has the module topology, then φ is an open quotient map.

Русский

Если φ: A →ₗ[R] B сюръективно отображает A на B и B имеет модульную топологию, то φ является открытым фактор-мапом.

LaTeX

$$$IsOpenQuotientMap(φ)$ for surjective φ$$

Lean4

/-- A linear surjection between modules with the module topology is an open quotient map. -/
theorem isOpenQuotientMap_of_surjective [TopologicalSpace B] [IsModuleTopology R B] {φ : A →ₗ[R] B}
    (hφ : Function.Surjective φ) : IsOpenQuotientMap φ :=
  have := toContinuousAdd R A
  AddMonoidHom.isOpenQuotientMap_of_isQuotientMap <| isQuotientMap_of_surjective hφ

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