map_le_comap_of_inv_on — Mathlib

English

If g has the left inverse on f over I, then I.map f ≤ I.comap g.

Русский

Если g имеет левый обратный член на f над I, то I.map f ≤ I.comap g.

LaTeX

$$$ \text{LeftInvOn } g f I \Rightarrow I.map f \le I.comap g $$$

Lean4

theorem map_le_comap_of_inv_on [RingHomClass G S R] (g : G) (I : Ideal R) (hf : Set.LeftInvOn g f I) :
    I.map f ≤ I.comap g := by
  refine Ideal.span_le.2 ?_
  rintro x ⟨x, hx, rfl⟩
  rw [SetLike.mem_coe, mem_comap, hf hx]
  exact hx

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