Primality in R[x, y^{-1}] and coprime height bound

If x is transcendental over R and r is prime in R with r not dividing y, then r remains prime in R[x, y^{-1}]. As a consequence, if y_1 and y_2 are coprime in R, no height-one prime of T contracting to a nonzero ideal of R can contain both y_1 and y_2.

theorem not_mem_associatedPrime_of_ndvd {T : Type u_1} [CommRing T] [IsLocalRing T] [IsNoetherianRing T] [IsDomain T] (R : NSubring T) (r y : ↥R.carrier) (hr : Prime r) (hry : ¬r ∣ y) (P : Ideal T) (hP : P ∈ associatedPrimes T (T ⧸ Ideal.span {↑r})) : ↑y ∉ P

If r is prime in NSubring R and r ∤ y, then y ∉ P for any P ∈ Ass(T/(r·T)). Uses the NSubring height bound: ht(P∩R) ≤ 1 forces P∩R = (r), so y ∈ P → r | y.

theorem isSMulRegular_of_ndvd {T : Type u_1} [CommRing T] [IsLocalRing T] [IsNoetherianRing T] [IsDomain T] (R : NSubring T) (r y : ↥R.carrier) (hr : Prime r) (hry : ¬r ∣ y) : IsSMulRegular (T ⧸ Ideal.span {↑r}) ↑y

y is a non-zero-divisor on T/(r·T) when r is prime in NSubring R and r ∤ y.

theorem prime_in_adjoinLocSet {T : Type u_1} [CommRing T] [IsLocalRing T] [IsNoetherianRing T] [IsDomain T] (R : NSubring T) (x : T) (y r : ↥R.carrier) (hx_trans : Transcendental (↥R.carrier) x) (hr : Prime r) (hry : ¬r ∣ y) (a₁ b₁ c : T) (ha₁ : a₁ ∈ adjoinLocSetY R x y) (hb₁ : b₁ ∈ adjoinLocSetY R x y) (hc : c ∈ adjoinLocSetY R x y) (heq : a₁ * b₁ = ↑r * c) : (∃ d ∈ adjoinLocSetY R x y, a₁ = ↑r * d) ∨ ∃ d ∈ adjoinLocSetY R x y, b₁ = ↑r * d

A prime element r of R that doesn't divide y is "prime" in adjoinLocSetY R x y when x is transcendental over R: if a₁ * b₁ = (r:T) * c in T with a₁, b₁, c ∈ adjoinLocSetY, then r divides a₁ or b₁ within adjoinLocSetY.

The proof has three key ingredients:

1. Polynomial factorization: from a₁b₁ = rc and transcendence, derive C(r)|f₁ or C(r)|f₂ in R[X] (using C(r) prime and C(r) ∤ C(y)^n).
2. NSubring height bound: y is a non-zero-divisor in T/(r·T) because y ∉ P for every P ∈ Ass(T/rT). This uses: P∩R has height ≤ 1, r ∈ P∩R with ht((r))=1, so P∩R = (r), and y ∉ (r) since r ∤ y.
3. Divisibility transfer: from a₁y^m = re and y regular mod r, conclude r|a₁ in T. Then d := a₁/r ∈ adjoinLocSetY with witness (h₁, m₁).

Coprime height bound

Key lemma: if y₁, y₂ ∈ R are coprime (no prime divides both), then no height-1 prime P of T (that contracts to a nonzero ideal of R) can contain both y₁ and y₂. This is what makes the intersection approach work.

theorem exists_prime_mem_of_ne_bot {S : Type u_2} [CommRing S] [UniqueFactorizationMonoid S] (Q : Ideal S) [hQ : Q.IsPrime] (hQ_ne_bot : Q ≠ ⊥) : ∃ (q : S), Prime q ∧ q ∈ Q

In a UFD, every nonzero prime ideal contains a prime element.

theorem coprime_not_both_in_prime {T : Type u_1} [CommRing T] [IsLocalRing T] [IsNoetherianRing T] [IsDomain T] (R : NSubring T) (y₁ y₂ : ↥R.carrier) (hcoprime : ∀ (p : ↥R.carrier), Prime p → ¬(p ∣ y₁ ∧ p ∣ y₂)) (P : Ideal T) [hP : P.IsPrime] (hPR_ht : (Ideal.comap R.carrier.subtype P).height ≤ 1) (hPR_ne : Ideal.comap R.carrier.subtype P ≠ ⊥) : ↑y₁ ∉ P ∨ ↑y₂ ∉ P

If y₁, y₂ are coprime in R and P∩R has height ≤ 1 and is nonzero, then y₁ ∉ P or y₂ ∉ P.