mapₐ_surjective_of_surjective — Mathlib

English

If an algebra homomorphism f is surjective, then its induced localization map on algebras is also surjective.

Русский

Если отображение алгебры $f$ сюръективно, то и локализованное отображение по $f$ сюръективно.

LaTeX

$$$\\text{Surjective}(f) \\Rightarrow \\text{Surjective}(\\mathrm{mapₐ} M R_p A_p B_p f)$$$

Lean4

theorem mapₐ_surjective_of_surjective (f : A →ₐ[R] B) (hf : Function.Surjective f) :
    Function.Surjective (mapₐ M Rₚ Aₚ Bₚ f) :=
  IsLocalization.map_surjective_of_surjective _ _ _ hf

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