injective_of_map_algebraMap_zero — Mathlib

English

If a ring homomorphism f from localized S to T respects the vanishing of images of algebraMap from R, then f is injective.

Русский

Если гомоморфизм кольца f из локализации S в T учитывает нули изображения algebraMap из R, то f инъективен.

LaTeX

$$$\\forall x,\\ f(\\mathrm{algebraMap}\\ R S x) = 0 \\Rightarrow \\mathrm{algebraMap}\\ R S x = 0 \\quad\\Rightarrow\\quad \\mathrm{Injective}(f)$$$

Lean4

theorem injective_of_map_algebraMap_zero {T} [CommRing T] (f : S →+* T)
    (h : ∀ x, f (algebraMap R S x) = 0 → algebraMap R S x = 0) : Function.Injective f :=
  by
  rw [IsLocalization.injective_iff_map_algebraMap_eq M]
  refine fun x y ↦ ⟨fun hz ↦ hz ▸ rfl, fun hz ↦ ?_⟩
  rw [← sub_eq_zero, ← map_sub, ← map_sub] at hz
  apply h at hz
  rwa [map_sub, sub_eq_zero] at hz

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