map_eq_submodule_map — Mathlib

English

With a surjective RingHom f, the map of an ideal I from R to S can be equated with a corresponding submodule map: I.map f = Submodule.map f I.

Русский

При сюръективном отображении f равенство между отображением I и подмодулем: I.map f = Submodule.map f I.

LaTeX

$$$I : \mathrm{Ideal}(R),\; [h : \mathrm{RingHomSurjective} f] \Rightarrow \mathrm{Ideal.map} f I = \mathrm{Submodule.map} f^{\mathrm{toSemilinearMap}} I$$$

Lean4

theorem map_eq_submodule_map (f : R →+* S) [h : RingHomSurjective f] (I : Ideal R) :
    I.map f = Submodule.map f.toSemilinearMap I :=
  Submodule.ext fun _ => mem_map_iff_of_surjective f h.1

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