comap_le_map_of_inverse — Mathlib

English

Let P be prime in R and I an ideal in S with I.comap f ≤ P; there exists Q ≥ I, with Q prime and Q.comap f ≤ P.

Русский

Пусть P простый в R и I — идеал в S такой, что I.comap f ≤ P; существует Q ≥ I, причём Q простый и Q.comap f ≤ P.

LaTeX

$$$\exists Q \ge I,\ Q.IsPrime \wedge Q.\comap f \le P$$$

Lean4

/-- The `Ideal` version of `Set.preimage_subset_image_of_inverse`. -/
theorem comap_le_map_of_inverse (g : G) (I : Ideal S) (h : Function.LeftInverse g f) : I.comap f ≤ I.map g :=
  comap_le_map_of_inv_on _ _ _ <| h.leftInvOn _

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