map_le_iff_le_comap — Mathlib

English

Let I be an ideal of R, K an ideal of S, and f: F be a map with RingHomClass F R S. Then the image of I under f is contained in K if and only if I is contained in the comap of K along f.

Русский

Пусть I — идеал кольца R, K — идеал кольца S, и f: F — отображение с гомоморфизмом колец. Тогда образ I под действием f содержится в K тогда и только тогда I содержится в обратном образе K по f.

LaTeX

$$$ \operatorname{map} f I \le K \iff I \le \operatorname{comap} f K $$$

Lean4

theorem map_le_iff_le_comap [RingHomClass F R S] : map f I ≤ K ↔ I ≤ comap f K :=
  span_le.trans Set.image_subset_iff

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