map_quotient_self — Mathlib

English

Let I be a two‑sided ideal in a ring R. The canonical projection π: R → R/I sends I to the zero ideal in R/I; equivalently, the image of I under the quotient map is the bottom ideal.

Русский

Пусть I — двусторонний идеал кольца R. Каноническое отображение π: R → R/I отправляет I в нулевой идеал в R/I; эквивалентно изображение I при факторизации равно нижнему идеалу.

LaTeX

$$$\operatorname{map}(\operatorname{Quotient.mk} I) I = \bot$$$

Lean4

@[simp]
theorem map_quotient_self (I : Ideal R) [I.IsTwoSided] : map (Quotient.mk I) I = ⊥ :=
  eq_bot_iff.2 <|
    Ideal.map_le_iff_le_comap.2 fun _ hx => (Submodule.mem_bot (R ⧸ I)).2 <| Ideal.Quotient.eq_zero_iff_mem.2 hx

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