ker_quotLeftToQuotSup — Mathlib

English

The kernel of quotLeftToQuotSup equals the image of J under the quotient mk I.

Русский

Ядро quotLeftToQuotSup равно образ J под тождественным отображением mk I.

LaTeX

$$$\\ker(\\!\\mathrm{quotLeftToQuotSup}\\! I\\; J) = J.map(\\mathrm{Ideal.Quotient.mk} I)$$$

Lean4

/-- The kernel of `quotLeftToQuotSup` -/
theorem ker_quotLeftToQuotSup : RingHom.ker (quotLeftToQuotSup I J) = J.map (Ideal.Quotient.mk I) := by
  simp only [mk_ker, sup_idem, sup_comm, quotLeftToQuotSup, Quotient.factor, ker_quotient_lift,
    map_eq_iff_sup_ker_eq_of_surjective (Ideal.Quotient.mk I) Quotient.mk_surjective, ← sup_assoc]

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