map_le_comap_of_inverse — Mathlib

English

If there exists a left inverse between g and f, then map f I ≤ comap g I for any ideal I.

Русский

Если существует левый обратный элемент между g и f, то для любого идеала I выполняется map f I ≤ comap g I.

LaTeX

$$$\text{LeftInverse } (g,f) \Rightarrow \operatorname{map} f I \le \operatorname{comap} g I$$$

Lean4

/-- The `Ideal` version of `Set.image_subset_preimage_of_inverse`. -/
theorem map_le_comap_of_inverse [RingHomClass G S R] (g : G) (I : Ideal R) (h : Function.LeftInverse g f) :
    I.map f ≤ I.comap g :=
  map_le_comap_of_inv_on _ _ _ <| h.leftInvOn _

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