Lying over along an integral ring homomorphism

An integral ring homomorphism g : S →+* T lifts each prime ideal of S containing its kernel to a prime ideal of T. This is Mathlib's Ideal.exists_ideal_over_prime_of_isIntegral stated directly for g, so callers need not install an algebra structure.

Main results

• Ideal.exists_comap_eq_of_isIntegral: a prime of S containing the kernel of g is the contraction along g of a prime of T.

theorem Ideal.exists_comap_eq_of_isIntegral {S : Type u_1} {T : Type u_2} [CommRing S] [CommRing T] (P : Ideal S) [P.IsPrime] (g : S →+* T) (hg : g.IsIntegral) (hP : RingHom.ker g ≤ P) : ∃ (Q : Ideal T), Q.IsPrime ∧ comap g Q = P

Lying over along an integral ring homomorphism g : S →+* T: a prime P of S containing the kernel of g is the contraction along g of a prime of T.