comap_map_mk — Mathlib

English

Let I ≤ J be ideals in R. Then the comap of the quotient map equals J, i.e., the preimage of the image is exactly J.

Русский

Пусть I ≤ J — идеалы в R. Тогда комапа факторной карты равна J, то есть предобраз образа равен ровно J.

LaTeX

$$$\\text{Ideal.comap}\\left(\\text{Ideal.Quotient.mk } I\\right)\\left(\\text{Ideal.map}(\\text{Ideal.Quotient.mk } I) J\\right) = J$$$

Lean4

theorem comap_map_mk {I J : Ideal R} [I.IsTwoSided] (h : I ≤ J) :
    Ideal.comap (Ideal.Quotient.mk I) (Ideal.map (Ideal.Quotient.mk I) J) = J := by ext;
  rw [← Ideal.mem_quotient_iff_mem h, Ideal.mem_comap]

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