Adjoining from a Prime Ideal

Given an N-subring R and a nonzero prime q of the ambient complete local domain, construct an N-subring S containing R such that q meets S nontrivially.

Jensen, "Completions of UFDs with semi-local formal fibers", 2006, Lemma 2.1 (case P = (0)).

Jensen's Lemma 2.1 for P = (0)

Given N-subring R and nonzero prime q of T, find an N-subring S ⊇ R with q ∩ S ≠ (0). This uses avoidance to find a transcendental element in q.

theorem adjoin_from_prime {T : Type u_1} [CommRing T] [IsLocalRing T] [IsNoetherianRing T] [IsDomain T] [IsAdicComplete (IsLocalRing.maximalIdeal T) T] (R : NSubring T) (q : Ideal T) (hq_prime : q.IsPrime) (hq_ne_bot : q ≠ ⊥) (hM_not_assoc : ∀ (r : T), r ≠ 0 → IsLocalRing.maximalIdeal T ∉ associatedPrimes T (T ⧸ Ideal.span {r})) (hAss_ht : ∀ (r : T), r ≠ 0 → ∀ P ∈ associatedPrimes T (T ⧸ Ideal.span {r}), P.height ≤ 1) (hR_card : Cardinal.mk ↥R.carrier < Cardinal.mk T) (hT_card : Cardinal.mk T = Cardinal.mk (IsLocalRing.ResidueField T)) : ∃ (S : NSubring T), IsAExtension R S ∧ ∃ (t : ↥S.carrier), ↑t ∈ q ∧ ↑t ≠ 0

Jensen Lemma 2.1 (P = (0) case): Given an N-subring R and a nonzero prime ideal q of T, there exists an N-subring S ⊇ R with q ∩ S ≠ {0}, |S| = sup(ℵ₀, |R|), and primes of R remain prime in S.

Proof idea: Use avoidance (Lemma 3) to find t ∈ q that is transcendental over R modulo all relevant primes. Then S = R[t]_{R[t] ∩ M}.