Krull heights of contracted primes and of two-equation intersections

Main results

• Ideal.height_under_eq_one_of_height_le_one: a nonzero prime of height at most one in an integral extension of a normal Noetherian domain contracts to a prime of height one.
• Ideal.isPrincipal_under_of_height_le_one: over a unique factorization domain, that contraction is principal.
• Ideal.height_eq_two_of_mem_minimalPrimes_span_pair: if f is prime and does not divide g, every minimal prime of (f, g) has height two.

theorem Ideal.height_under_eq_one_of_height_le_one (R : Type u_1) (A : Type u_2) [CommRing R] [IsDomain R] [IsNoetherianRing R] [IsIntegrallyClosed R] [CommRing A] [IsDomain A] [IsNoetherianRing A] [Algebra R A] [FaithfulSMul R A] [Algebra.IsIntegral R A] (Q : Ideal A) [Q.IsPrime] (hQ : Q ≠ ⊥) (hheight : Q.height ≤ 1) : (under R Q).height = 1

A nonzero prime of height at most one in an integral extension of a normal Noetherian domain contracts to a prime of height one.

theorem Ideal.isPrincipal_under_of_height_le_one (R : Type u_1) (A : Type u_2) [CommRing R] [IsDomain R] [IsNoetherianRing R] [IsIntegrallyClosed R] [UniqueFactorizationMonoid R] [CommRing A] [IsDomain A] [IsNoetherianRing A] [Algebra R A] [FaithfulSMul R A] [Algebra.IsIntegral R A] (Q : Ideal A) [Q.IsPrime] (hQ : Q ≠ ⊥) (hheight : Q.height ≤ 1) : Submodule.IsPrincipal (under R Q)

A nonzero prime of height at most one in an integral extension of a normal Noetherian unique factorization domain contracts to a principal prime.

theorem Ideal.height_eq_two_of_mem_minimalPrimes_span_pair {R : Type u_1} [CommRing R] [IsDomain R] [IsNoetherianRing R] {f g : R} (hf : Prime f) (hfg : ¬f ∣ g) {p : Ideal R} (hp : p ∈ (span {f, g}).minimalPrimes) : p.height = 2

A nontrivial two-equation intersection with prime first equation is purely of codimension two: all its minimal primes have height two.