mapₐ_injective_of_injective — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem mapₐ_injective_of_injective (f : A →ₐ[R] B) (hf : Function.Injective f) :
    Function.Injective (mapₐ M Rₚ Aₚ Bₚ f) :=
  IsLocalization.map_injective_of_injective _ _ _ hf

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