Theorems · Theorem · commutative algebra

Ideal.exists_notMem_dvd_algebraMap_of_primesOver_eq_singleton

∀ {R : Type u_1} [inst : CommRing R] {S : Type u_2} [inst_1 : CommRing S] [inst_2 : Algebra R S] {p : Ideal R}
  [p.IsPrime] {q : Ideal S} [q.IsPrime],
  p.primesOver S = {q} → ∀ [Algebra.IsIntegral R S], ∀ x ∉ q, ∃ r ∉ p, x ∣ (algebraMap R S) r

If S is an integral R-algebra such that q is the unique prime of S lying over a prime p of R, then any x ∉ q divides some r ∉ p.

Defined in

Mathlib.RingTheory.Ideal.GoingUp

Cited by

3 results in Mathlib

Foundations

Depth 118 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommRingCommRingAlgebraIdeal.IsPrimeIdeal.IsPrimeAlgebra.IsIntegral