comap_map_of_surjective' — Mathlib

English

Let f be surjective. Then for any ideal I of R, the comap of the image map satisfies (I.map f).comap f = I ⊔ ker f.

Русский

Пусть f сюръективно. Тогда для любого идеала I кольца R верно, что comap от образа через f равен I ∪ ker f (объединение в решетке).

LaTeX

$$$$(I.map\ f).comap\ f = I \\sqcup \\ker f.$$$$

Lean4

theorem comap_map_of_surjective' (f : F) (hf : Function.Surjective f) (I : Ideal R) :
    (I.map f).comap f = I ⊔ RingHom.ker f :=
  comap_map_of_surjective f hf I

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