Height bounds and detection of units

In a local ring of finite Krull dimension n + 1, the maximal ideal is the only prime of height greater than n. This complements Mathlib's Ideal.height_eq_ringKrullDim_iff.

In a Noetherian ring, an element is a unit if it belongs to no prime of height at most one. Indeed, a nonunit generates a proper principal ideal, and a minimal prime over that ideal has height at most one by Krull's principal ideal theorem. Applied to a discriminant, this detects étaleness of a finite free algebra using only primes of height at most one. By the same theorem, every nonzero prime of a Noetherian domain contains a prime of height one, namely a prime minimal over a nonzero element; in particular a Noetherian domain which is not a field has a prime of height one.

In a unique factorization domain, a prime ideal of height one is generated by a prime element. Hence a prime containing two relatively prime elements has height at least two, and in a Noetherian unique factorization domain two relatively prime elements generating a proper ideal cut out a closed subset of codimension exactly two.

Main results

• Ideal.lt_height_iff_eq_maximalIdeal: in a local ring of Krull dimension n + 1, a prime has height greater than n iff it is the maximal ideal.
• Ideal.exists_le_isPrime_height_eq_one: a nonzero prime of a Noetherian domain contains a prime of height one.
• Ideal.exists_isPrime_height_eq_one_of_not_isField: a Noetherian domain which is not a field has a prime of height one.
• TauCeti.isUnit_iff_forall_notMem_of_height_le_one: units in a Noetherian ring are detected by primes of height at most one.
• Ideal.two_le_height_of_isRelPrime: in a unique factorization domain, a prime containing two relatively prime elements has height at least two.
• Ideal.height_span_pair_eq_two_of_isRelPrime: in a Noetherian unique factorization domain, two relatively prime elements generating a proper ideal generate an ideal of height two.

theorem Ideal.lt_height_iff_eq_maximalIdeal {R : Type u_1} [CommRing R] [IsLocalRing R] {n : ℕ} (hdim : ringKrullDim R = ↑n + 1) {I : Ideal R} [I.IsPrime] : ↑n < I.height ↔ I = IsLocalRing.maximalIdeal R

In a local ring of Krull dimension n + 1, a prime has height greater than n iff it is the maximal ideal.

theorem Ideal.exists_le_isPrime_height_eq_one {R : Type u_1} [CommRing R] [IsDomain R] [IsNoetherianRing R] (p : Ideal R) [p.IsPrime] (hp : p ≠ ⊥) : ∃ P ≤ p, P.IsPrime ∧ P.height = 1

A nonzero prime p of a Noetherian domain contains a prime of height one.

theorem Ideal.exists_isPrime_height_eq_one_of_not_isField {R : Type u_1} [CommRing R] [IsDomain R] [IsNoetherianRing R] (hR : ¬IsField R) : ∃ (p : Ideal R), p.IsPrime ∧ p.height = 1

A Noetherian domain which is not a field has a prime of height one.

theorem Ideal.two_le_height_of_isRelPrime {R : Type u_1} [CommRing R] [IsDomain R] [UniqueFactorizationMonoid R] {x y : R} (h : IsRelPrime x y) {p : Ideal R} [p.IsPrime] (hx : x ∈ p) (hy : y ∈ p) : 2 ≤ p.height

In a unique factorization domain, a prime ideal containing two relatively prime elements has height at least two.

theorem Ideal.height_span_pair_eq_two_of_isRelPrime {R : Type u_1} [CommRing R] [IsDomain R] [UniqueFactorizationMonoid R] {x y : R} [IsNoetherianRing R] (h : IsRelPrime x y) (hxy : span {x, y} ≠ ⊤) : (span {x, y}).height = 2

In a Noetherian unique factorization domain, two relatively prime elements generating a proper ideal generate an ideal of height two.

theorem TauCeti.isUnit_iff_forall_notMem_of_height_le_one {R : Type u_1} [CommRing R] [IsNoetherianRing R] (x : R) : IsUnit x ↔ ∀ (p : Ideal R) [p.IsPrime], p.height ≤ 1 → x ∉ p

An element of a Noetherian ring is a unit if and only if it belongs to no prime of height at most one.