eq_coinduced_of_surjective — Mathlib

English

If φ: A →ₗ[R] B is surjective, then the module topology on B equals the coinduced topology along φ.

Русский

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

LaTeX

$$$\text{moduleTopology}(R,B) = \text{TopologicalSpace.coinduced}(φ, -)$$$

Lean4

theorem _root_.ModuleTopology.eq_coinduced_of_surjective {φ : A →ₗ[R] B} (hφ : Function.Surjective φ) :
    moduleTopology R B = TopologicalSpace.coinduced φ inferInstance :=
  by
  letI : TopologicalSpace B := moduleTopology R B
  haveI : IsModuleTopology R B := ⟨rfl⟩
  exact (isQuotientMap_of_surjective hφ).eq_coinduced

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