English
Let I be a two‑sided ideal and f: R → S a ring homomorphism. For any H with I ≤ ker f, the kernel of the lifted map is the image of ker f under the quotient map.
Русский
Пусть I — двусторонний идеал и f: R → S — кольцевой однород. При любом H с I ⊆ ker f, ядро поднятого отображения равно образу ker f под факторизацией по I.
LaTeX
$$$\ker(\operatorname{Ideal.Quotient.lift} I f H) = (\ker f).map(\operatorname{Quotient.mk} I)$$$
Lean4
theorem ker_quotient_lift {I : Ideal R} [I.IsTwoSided] (f : R →+* S) (H : I ≤ ker f) :
ker (Ideal.Quotient.lift I f H) = (RingHom.ker f).map (Quotient.mk I) :=
by
apply Ideal.ext
intro x
constructor
· intro hx
obtain ⟨y, hy⟩ := Quotient.mk_surjective x
rw [mem_ker, ← hy, Ideal.Quotient.lift_mk, ← mem_ker] at hx
rw [← hy, mem_map_iff_of_surjective (Quotient.mk I) Quotient.mk_surjective]
exact ⟨y, hx, rfl⟩
· intro hx
rw [mem_map_iff_of_surjective (Quotient.mk I) Quotient.mk_surjective] at hx
obtain ⟨y, hy⟩ := hx
rw [mem_ker, ← hy.right, Ideal.Quotient.lift_mk]
exact hy.left
