injective_lift_iff — Mathlib

English

For an ideal I and a homomorphism f with a compatible hypothesis H, the lifting map is injective if and only if ker f = I.

Русский

Для идеала I и гомоморфизма f с условием совместимости H, поднятое отображение инъективно тогда и только тогда, когда ker f = I.

LaTeX

$$$\operatorname{Injective}(\operatorname{Quotient.lift} I f H) \;\Longleftrightarrow\; \ker f = I$$$

Lean4

theorem injective_lift_iff {I : Ideal R} [I.IsTwoSided] {f : R →+* S} (H : ∀ (a : R), a ∈ I → f a = 0) :
    Injective (Quotient.lift I f H) ↔ ker f = I :=
  by
  rw [injective_iff_ker_eq_bot, ker_quotient_lift, map_eq_bot_iff_le_ker, mk_ker]
  constructor
  · exact fun h ↦ le_antisymm h H
  · rintro rfl; rfl

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