map_injective — Mathlib

English

Alternative formulation of the injectivity of coordinate ring map when ring hom is injective.

Русский

Альтернативная формулировка инъективности отображения координатного кольца при инъективном кольцевом гомоморфизме.

LaTeX

$$map_injective {f : R →+* S} (hf : Function.Injective f) : Function.Injective (map W' f)$$

Lean4

theorem map_injective {f : R →+* S} (hf : Function.Injective f) : Function.Injective <| map W' f :=
  (injective_iff_map_eq_zero _).mpr fun y hy =>
    by
    obtain ⟨p, q, rfl⟩ := exists_smul_basis_eq y
    simp_rw [map_add, CoordinateRing.map_smul, map_one, map_mk, map_X] at hy
    obtain ⟨hp, hq⟩ := smul_basis_eq_zero hy
    rw [Polynomial.map_eq_zero_iff hf] at hp hq
    simp_rw [hp, hq, zero_smul, add_zero]

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