Theorems · Theorem · commutative algebra

Ideal.height_le_height_add_of_liesOver

∀ {R : Type u_1} [inst : CommRing R] [IsNoetherianRing R] {S : Type u_2} [inst_2 : CommRing S] [inst_3 : Algebra R S]
  [IsNoetherianRing S] (p : Ideal R) [p.IsPrime] (P : Ideal S) [P.IsPrime] [P.LiesOver p],
  P.height ≤ p.height + (Ideal.map (Ideal.Quotient.mk (Ideal.map (algebraMap R S) p)) P).height

If P lies over p, the height of P is bounded by the height of p plus the height of the image of P in S ⧸ p S. Equality holds if S satisfies going-down as an R-algebra (see Ideal.height_eq_height_add_of_liesOver_of_hasGoingDown).

Defined in

Mathlib.RingTheory.Ideal.KrullsHeightTheorem

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommRingIsNoetherianRingCommRingAlgebraIsNoetherianRingIdeal.IsPrimeIdeal.IsPrimeIdeal.LiesOver