isOpenMap_of_surjective — Mathlib

English

If φ: A →ₗ[R] B is surjective and the module topology is given, then φ is an open map: it sends open sets to open sets.

Русский

Если линейное отображение сюръективно и задана модульная топология, то оно открывает открытые множества.

LaTeX

$$$IsOpenMap(φ)$$$

Lean4

/-- A linear surjection to a module with the module topology is open. -/
theorem isOpenMap_of_surjective [TopologicalSpace B] [IsModuleTopology R B] [ContinuousAdd A] [ContinuousSMul R A]
    {φ : A →ₗ[R] B} (hφ : Function.Surjective φ) : IsOpenMap φ :=
  by
  have hOpenMap :=
    letI : TopologicalSpace A := moduleTopology R A
    have : IsModuleTopology R A := ⟨rfl⟩
    isOpenQuotientMap_of_surjective hφ |>.isOpenMap
  intro U hU
  exact hOpenMap U <| moduleTopology_le R A U hU

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