surjective_localizationPreserves — Mathlib

English

Localization preserves surjectivity: the localized map is surjective if the original map is.

Русский

Локализация сохраняет суръективность: локализованная карта суръективна если исходная суръективна.

LaTeX

$$$$ \operatorname{LocalizationPreserves}( \text{surjective} ). $$$$

Lean4

/-- `M⁻¹R →+* M⁻¹S` is surjective if `R →+* S` is surjective. -/
theorem surjective_localizationPreserves : LocalizationPreserves surjective :=
  by
  introv R H x
  obtain ⟨x, ⟨_, s, hs, rfl⟩, rfl⟩ := IsLocalization.mk'_surjective (M.map f) x
  obtain ⟨y, rfl⟩ := H x
  use IsLocalization.mk' R' y ⟨s, hs⟩
  rw [IsLocalization.map_mk']

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