Application to T = C[[x,y,z]]/(x^2 - yz)

The quotient T = C[[x,y,z]]/(x^2 - yz) is a complete local domain of depth 2 with uncountable residue field C. We verify Jensen's hypotheses (Corollary 2.4 with P = (0)) and apply the construction to produce a local UFD whose completion is T.

Helper lemmas for T conditions

theorem conjI_ccf_zero (f : MvPowerSeries (Fin 3) ℂ) (hf : f ∈ conjI) : MvPowerSeries.constantCoeff f = 0

theorem mk_mem_maxIdeal (f : MvPowerSeries (Fin 3) ℂ) (hf : MvPowerSeries.constantCoeff f = 0) : (Ideal.Quotient.mk conjI) f ∈ IsLocalRing.maximalIdeal T

theorem coeff_conjI_zero_of_deg_le_one (m : Fin 3 →₀ ℕ) (hm : ∀ (i : Fin 3), m i ≤ (Finsupp.single 1 1) i) (f : MvPowerSeries (Fin 3) ℂ) (hf : f ∈ conjI) : (MvPowerSeries.coeff m) f = 0

theorem mk_X1_ne_zero : (Ideal.Quotient.mk conjI) (MvPowerSeries.X 1) ≠ 0

theorem T_smulRegular_of_ne_zero (a : T) (ha : a ≠ 0) : IsSMulRegular T a

Verify T conditions

Helper: z is a non-zerodivisor in T/(y)

We show that mk(X 2) is smul-regular on the quotient module T/(mk(X 1)·T).

Proof idea: Lift to MvPowerSeries (Fin 3) ℂ. If X₂f − X₁g ∈ conjI, then f(a,0,c) = 0 for a < 2 (coefficient argument at the generator's degree). Define shiftX1(f)(m) = f(m + single 1 1) (removes the X₁≥1 part) and divR(f)(m) = f(m₀+2, 0, m₂) when m₁=0 (the X₀² quotient of the X₁=0 slice). Then f − X₁·shiftX1(f) = X₀²·divR(f) (coefficient identity using the vanishing), so f = X₁·(shiftX1(f) + X₂·divR(f)) + (X₀²−X₁X₂)·divR(f), giving f ∈ (X₁) + conjI and hence mk(f) ∈ mk(X₁)·⊤.

noncomputable def shiftX1'App (f : MvPowerSeries (Fin 3) ℂ) : MvPowerSeries (Fin 3) ℂ

Shift X₁-exponent by 1: (shiftX1 f)(m) = f(m + single 1 1).

Equations

• shiftX1'App f m = f (m + Finsupp.single 1 1)

noncomputable def divR'App (f : MvPowerSeries (Fin 3) ℂ) : MvPowerSeries (Fin 3) ℂ

The "X₁=0 restriction divided by X₀²": (divR f)(m) = f(m₀+2, 0, m₂) when m₁=0, else 0.

Equations

• divR'App f m = if m 1 = 0 then f (m.update 0 (m 0 + 2)) else 0

theorem coeff_lhs (f : MvPowerSeries (Fin 3) ℂ) (d : Fin 3 →₀ ℕ) : (MvPowerSeries.coeff d) (f - MvPowerSeries.X 1 * shiftX1'App f) = if d 1 = 0 then (MvPowerSeries.coeff d) f else 0

LHS coefficient: (f - X₁ · shiftX1'App f)(d) = f(d) when d₁=0, else 0.

theorem coeff_rhs (f : MvPowerSeries (Fin 3) ℂ) (d : Fin 3 →₀ ℕ) : (MvPowerSeries.coeff d) (MvPowerSeries.X 0 ^ 2 * divR'App f) = if 2 ≤ d 0 ∧ d 1 = 0 then (MvPowerSeries.coeff d) f else 0

RHS coefficient: (X₀² · divR'App f)(d) = f(d) when d₀≥2 and d₁=0, else 0.

theorem coeff_gen_zero (a : Fin 3 →₀ ℕ) (ha0 : a 0 < 2) (ha1 : a 1 = 0) : (MvPowerSeries.coeff a) (MvPowerSeries.X 0 ^ 2 - MvPowerSeries.X 1 * MvPowerSeries.X 2) = 0

Coefficient of the generator at a monomial with a₀ < 2 and a₁ = 0.

theorem coeff_gen_mul_zero (k : MvPowerSeries (Fin 3) ℂ) (d : Fin 3 →₀ ℕ) (hd0 : d 0 < 2) (hd1 : d 1 = 0) : (MvPowerSeries.coeff d) ((MvPowerSeries.X 0 ^ 2 - MvPowerSeries.X 1 * MvPowerSeries.X 2) * k) = 0

gen * k vanishes at d when d₀ < 2 and d₁ = 0.

theorem coeff_f_vanish (f g : MvPowerSeries (Fin 3) ℂ) (hmem : MvPowerSeries.X 2 * f - MvPowerSeries.X 1 * g ∈ conjI) (d : Fin 3 →₀ ℕ) (hd1 : d 1 = 0) (hd0 : d 0 < 2) : (MvPowerSeries.coeff d) f = 0

Vanishing of f at low X₀-degree when X₁-index is 0, derived from hmem.

theorem rest_eq_X0sq_divR (f g : MvPowerSeries (Fin 3) ℂ) (hmem : MvPowerSeries.X 2 * f - MvPowerSeries.X 1 * g ∈ conjI) : f - MvPowerSeries.X 1 * shiftX1'App f = MvPowerSeries.X 0 ^ 2 * divR'App f

The coefficient identity: when X₂f − X₁g ∈ conjI, the "X₁=0 restriction" of f is divisible by X₀², yielding f − X₁·(shift) = X₀²·(quotient). The proof uses three facts:

1. (f − X₁·shiftX1'App f)(d) = f(d) when d₁=0, 0 when d₁≥1
2. (X₀²·divR'App f)(d) = f(d) when d₀≥2 and d₁=0, 0 otherwise
3. f(d₀, 0, d₂) = 0 for d₀ < 2 (from the hypothesis, using coeff at d + single 2 1)

theorem key_decomp'_app (f g : MvPowerSeries (Fin 3) ℂ) (hmem : MvPowerSeries.X 2 * f - MvPowerSeries.X 1 * g ∈ conjI) : f - MvPowerSeries.X 1 * (shiftX1'App f + MvPowerSeries.X 2 * divR'App f) ∈ conjI

theorem T_depth_ge_two : ∃ (a : T) (b : T), a ∈ IsLocalRing.maximalIdeal T ∧ b ∈ IsLocalRing.maximalIdeal T ∧ RingTheory.Sequence.IsRegular T [a, b]

T has depth ≥ 2: there exists a regular sequence of length 2 in M. Since T = ℂ[[x,y,z]]/(x²-yz) is Cohen-Macaulay of dimension 2, the images of y and z form a regular sequence.

theorem T_card_eq_residue_card : Cardinal.mk T = Cardinal.mk (IsLocalRing.ResidueField T)

|T| = |T/M|: both have cardinality |ℂ|. T/M ≅ ℂ and |T| = |ℂ[[x,y,z]]/(x²-yz)| = |ℂ|.

theorem T_no_integer_zerodivisor (n : ℤ) (hn : n ≠ 0) : (algebraMap ℤ T) n ≠ 0

No integer is a zero divisor in T. Since T is a domain of characteristic 0, and ℤ embeds into ℂ ⊆ T, every nonzero integer maps to a nonzero (hence non-zerodivisor) element. The key: algebraMap ℤ (MvPowerSeries (Fin 3) ℂ) n is a unit (constantCoeff = (n : ℂ) ≠ 0), and units map to units under the quotient map.

theorem T_prime_height_le_one (P : Ideal T) [hP : P.IsPrime] (hne : P ≠ IsLocalRing.maximalIdeal T) : P.height ≤ 1

All primes P ≠ M in T have height ≤ 1. Since ringKrullDim T = 2 and T is a local ring, height(M) = 2. By strict monotonicity of height on primes, any P < M has height < 2.

The main result

Apply jensen_construction_p0_uncountable to T to get A.

theorem jensen_special_case_proof : ∃ (A : Type) (x : CommRing A) (x_1 : IsLocalRing A) (_ : IsDomain A) (_ : UniqueFactorizationMonoid A) (_ : IsNoetherianRing A), Nonempty (AdicCompletion (IsLocalRing.maximalIdeal A) A ≃+* T) ∧ HasTrivialGenericFormalFiber A

Jensen's Corollary 2.4 applied to T = ℂ[[x,y,z]]/(x²-yz): There exists a 2-dimensional Noetherian local UFD A with  ≅ T and trivial generic formal fiber.

This directly proves jensen_special_case from Jensen.lean.