lift_injective_of_ker_le_ideal — Mathlib

English

If ker f ≤ I and H(a) = 0 for a ∈ I, then the induced map from R/I to S is injective.

Русский

Если ker f ≤ I и H(a) = 0 для a ∈ I, то индуцированное отображение R/I → S инъективно.

LaTeX

$$$$\text{Injective}(\text{Ideal.Quotient.lift } I\ f\ H).$$$$

Lean4

theorem lift_injective_of_ker_le_ideal (I : Ideal R) [I.IsTwoSided] {f : R →+* S} (H : ∀ a : R, a ∈ I → f a = 0)
    (hI : ker f ≤ I) : Function.Injective (Ideal.Quotient.lift I f H) :=
  by
  rw [RingHom.injective_iff_ker_eq_bot, RingHom.ker_eq_bot_iff_eq_zero]
  intro u hu
  obtain ⟨v, rfl⟩ := Ideal.Quotient.mk_surjective u
  rw [Ideal.Quotient.lift_mk] at hu
  rw [Ideal.Quotient.eq_zero_iff_mem]
  exact hI (RingHom.mem_ker.mpr hu)

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