Transcendental Extension of N-subrings

Adjoining a transcendental element to an N-subring R of a complete local domain T and localising at the intersection with the maximal ideal yields a new N-subring.

Loepp, "Constructing local generic formal fibers", 1997, Lemma 11.

Localization Carrier

The subring R[x]_{R[x] ∩ M} inside T, consisting of fractions p(x)/q(x) where q(x) is a unit in T (equivalently, q(x) ∉ M).

def adjoinLocSet {T : Type u_1} [CommRing T] [IsLocalRing T] [IsNoetherianRing T] [IsDomain T] (R : NSubring T) (x : T) : Set T

The carrier set of R[x] localized at R[x] ∩ M, viewed inside T. An element t ∈ T is in this set iff t = p(x)/q(x) for some p,q ∈ R[X] with q(x) a unit in T (i.e., q(x) ∉ M).

Equations

• One or more equations did not get rendered due to their size.

theorem adjoinLocSet_subring {T : Type u_1} [CommRing T] [IsLocalRing T] [IsNoetherianRing T] [IsDomain T] (R : NSubring T) (x : T) : ∃ (S : Subring T), ↑S = adjoinLocSet R x

The carrier set forms a subring of T.

theorem adjoinLocSet_le {T : Type u_1} [CommRing T] [IsLocalRing T] [IsNoetherianRing T] [IsDomain T] (R : NSubring T) (x t : T) (ht : t ∈ ↑R.carrier) : t ∈ adjoinLocSet R x

R.carrier ≤ adjoinLocSet carrier

theorem adjoinLocSet_mem_x {T : Type u_1} [CommRing T] [IsLocalRing T] [IsNoetherianRing T] [IsDomain T] (R : NSubring T) (x : T) : x ∈ adjoinLocSet R x

x ∈ adjoinLocSet carrier

Transcendental Extension (Loepp Lemma 11)

If x ∈ T is transcendental over Frac(R) and avoids a suitable set of primes, then R[x] localized at M is again an N-subring.

theorem adjoin_height_case_bot {T : Type u_1} [CommRing T] [IsLocalRing T] [IsNoetherianRing T] [IsDomain T] (R : NSubring T) (x : T) (hx_trans : Transcendental (↥R.carrier) x) (S_sub : Subring T) (hS_eq : ↑S_sub = adjoinLocSet R x) (hinv : ∀ (s : ↥S_sub), ↑s ∉ IsLocalRing.maximalIdeal T → IsUnit s) (P : Ideal T) (hP_prime : P.IsPrime) (hPR : Ideal.comap R.carrier.subtype P = ⊥) : (Ideal.comap S_sub.subtype P).height ≤ ↑1

theorem adjoin_height_case_ne_bot {T : Type u_1} [CommRing T] [IsLocalRing T] [IsNoetherianRing T] [IsDomain T] (R : NSubring T) (x : T) (hx_ker : ∀ (P : Ideal T), P.IsPrime → P.height ≤ 1 → Ideal.comap R.carrier.subtype P ≠ ⊥ → ∀ (f : Polynomial ↥R.carrier), (Polynomial.aeval x) f ∈ ↑P → ∀ (i : ℕ), f.coeff i ∈ Ideal.comap R.carrier.subtype P) (S_sub : Subring T) (hS_eq : ↑S_sub = adjoinLocSet R x) (P : Ideal T) (hP_prime : P.IsPrime) (hP_ht : P.height ≤ 1) (hR_bound : (Ideal.comap R.carrier.subtype P).height ≤ 1) (hPR : Ideal.comap R.carrier.subtype P ≠ ⊥) : (Ideal.comap S_sub.subtype P).height ≤ ↑1

theorem adjoin_transcendental_isNSubring {T : Type u_1} [CommRing T] [IsLocalRing T] [IsNoetherianRing T] [IsDomain T] (R : NSubring T) (x : T) (hx_trans : Transcendental (↥R.carrier) x) (hAss_ht : ∀ (r : T), r ≠ 0 → ∀ P ∈ associatedPrimes T (T ⧸ Ideal.span {r}), P.height ≤ 1) (hx_ker : ∀ (P : Ideal T), P.IsPrime → P.height ≤ 1 → Ideal.comap R.carrier.subtype P ≠ ⊥ → ∀ (f : Polynomial ↥R.carrier), (Polynomial.aeval x) f ∈ ↑P → ∀ (i : ℕ), f.coeff i ∈ Ideal.comap R.carrier.subtype P) : ∃ (S : NSubring T), IsAExtension R S ∧ x ∈ ↑S.carrier

Loepp Lemma 11 (simplified for P = (0)): Adjoining a transcendental element to an N-subring yields an N-subring.

If x ∈ T satisfies:

• x ∉ P for all P in a suitable set C ⊇ Ass(T) ∪ {P ∈ Ass(T/rT) | r ∈ R, r ≠ 0}
• x + P is transcendental over R/(R ∩ P) for all P ∈ C Then S = R[x]_{R[x] ∩ M} is an N-subring with |S| = sup(ℵ₀, |R|).