map_eq_iff_sup_ker_eq_of_surjective

English

Let f: R → S be a surjective ring hom. Then map f I = map f J iff I ⊔ ker f = J ⊔ ker f.

Русский

Пусть f: R → S — сюръективное кольцевое отображение. Тогда map f I = map f J тогда и только тогда, когда I ⊔ ker f = J ⊔ ker f.

LaTeX

$$$$ \\operatorname{map} f I = \\operatorname{map} f J \\quad\\Longleftrightarrow\\quad I \\sqcup \\ker f = J \\sqcup \\ker f.$$$$

Lean4

theorem map_eq_iff_sup_ker_eq_of_surjective {I J : Ideal R} (f : R →+* S) (hf : Function.Surjective f) :
    map f I = map f J ↔ I ⊔ RingHom.ker f = J ⊔ RingHom.ker f := by
  rw [← (comap_injective_of_surjective f hf).eq_iff, comap_map_of_surjective f hf, comap_map_of_surjective f hf,
    RingHom.ker_eq_comap_bot]

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