Adjoining Elements to N-Subrings

Three adjunction lemmas for the Jensen--Heitmann construction: transcendental adjunction preserving N-subring axioms (Loepp), adjunction from a prime ideal (Jensen), and the surjectivity step ensuring R → T/M² stays surjective (Heitmann Lemma 5).

Surjectivity Step (Heitmann Lemma 5)

Given N-subring R and u ∈ T, find an A-extension S containing some c with u - c ∈ M².

theorem adjoin_surjectivity {T : Type u_1} [CommRing T] [IsLocalRing T] [IsNoetherianRing T] [IsDomain T] [IsAdicComplete (IsLocalRing.maximalIdeal T) T] (R : NSubring T) (u : T) (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)) (hM_ne_bot : IsLocalRing.maximalIdeal T ≠ ⊥) : ∃ (S : NSubring T), IsAExtension R S ∧ ∃ (c : ↥S.carrier), u - ↑c ∈ IsLocalRing.maximalIdeal T ^ 2