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))
: