Jensen's Theorem on Completions of UFDs

Under suitable hypotheses on a complete local domain T, one constructs a local UFD A whose adic completion is T and whose generic formal fiber is trivial (Jensen, 2006, Corollary 2.4).

instance T_charZero : CharZero T

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

No nonzero integer maps to zero in T (char 0 domain).

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

|T| = |T/M|: both have cardinality |ℂ|.

theorem conjI_le_ker_ccf : conjI ≤ RingHom.ker MvPowerSeries.constantCoeff

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

theorem coeff_gen_zero_of_le_single (s : Fin 3) (b : Fin 3 →₀ ℕ) (hb : ∀ (i : Fin 3), b i ≤ (Finsupp.single s 1) i) : (MvPowerSeries.coeff b) (MvPowerSeries.X 0 ^ 2 - MvPowerSeries.X 1 * MvPowerSeries.X 2) = 0

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

theorem mk_X2_ne_zero' : (Ideal.Quotient.mk conjI) (MvPowerSeries.X 2) ≠ 0

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

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

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

Equations

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

noncomputable def divR' (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, and 0 otherwise.

Equations

• divR' 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' f) = if d 1 = 0 then (MvPowerSeries.coeff d) f else 0

theorem coeff_rhs' (f : MvPowerSeries (Fin 3) ℂ) (d : Fin 3 →₀ ℕ) : (MvPowerSeries.coeff d) (MvPowerSeries.X 0 ^ 2 * divR' f) = if 2 ≤ d 0 ∧ d 1 = 0 then (MvPowerSeries.coeff d) f 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

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

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

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

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

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

theorem maximal_not_assoc_local (hdepth : ∃ (a : T) (b : T), a ∈ IsLocalRing.maximalIdeal T ∧ b ∈ IsLocalRing.maximalIdeal T ∧ RingTheory.Sequence.IsRegular T [a, b]) (r : T) (hr : r ≠ 0) : IsLocalRing.maximalIdeal T ∉ associatedPrimes T (T ⧸ Ideal.span {r})

In a local domain with depth ≥ 2, M is not an associated prime of T/rT for any nonzero r. (Local copy of Construction.maximal_not_assoc_of_depth_ge_two.)

theorem heitmann_prop1_noetherian [IsAdicComplete (IsLocalRing.maximalIdeal T) T] (R : Subring T) [IsLocalRing ↥R] (h_closed : ∀ (I : Ideal ↥R), I.FG → ∀ (c : ↥R), ↑c ∈ Ideal.map R.subtype I → c ∈ I) : IsNoetherianRing ↥R

Heitmann's Proposition 1, Noetherian part: if R → T/M² is surjective and IT ∩ R = I for all f.g. ideals, then R is Noetherian. (Local copy of the first conjunct of Construction.heitmann_prop1.)

theorem jensen_map_maxIdeal_le_of_closed [IsAdicComplete (IsLocalRing.maximalIdeal T) T] (R : Subring T) [IsLocalRing ↥R] (h_closed : ∀ (I : Ideal ↥R), I.FG → ∀ (c : ↥R), ↑c ∈ Ideal.map R.subtype I → c ∈ I) : Ideal.map R.subtype (IsLocalRing.maximalIdeal ↥R) ≤ IsLocalRing.maximalIdeal T

theorem jensen_comap_maxIdeal_le_of_local (R : Subring T) [IsLocalRing ↥R] : Ideal.comap R.subtype (IsLocalRing.maximalIdeal T) ≤ IsLocalRing.maximalIdeal ↥R

theorem jensen_map_maxIdeal_eq_of_surj_closed [IsAdicComplete (IsLocalRing.maximalIdeal T) T] (R : Subring T) [IsLocalRing ↥R] (h_surj : Function.Surjective fun (r : ↥R) => (Ideal.Quotient.mk (IsLocalRing.maximalIdeal T ^ 2)) ↑r) (h_closed : ∀ (I : Ideal ↥R), I.FG → ∀ (c : ↥R), ↑c ∈ Ideal.map R.subtype I → c ∈ I) : Ideal.map R.subtype (IsLocalRing.maximalIdeal ↥R) = IsLocalRing.maximalIdeal T

theorem jensen_construction (hdepth : ∃ (a : T) (b : T), a ∈ IsLocalRing.maximalIdeal T ∧ b ∈ IsLocalRing.maximalIdeal T ∧ RingTheory.Sequence.IsRegular T [a, b]) (hcard : Cardinal.mk T = Cardinal.mk (IsLocalRing.ResidueField T)) (hchar : ∀ (n : ℤ), n ≠ 0 → (algebraMap ℤ T) n ≠ 0) (hT_aleph0 : Cardinal.aleph0 < Cardinal.mk T) : ∃ (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 for P = (0): the deep transfinite construction. Given verification conditions on T, produces a local UFD A with  ≅ T and trivial generic formal fiber. The full proof is in Construction.lean and Application.lean this local version avoids circular imports since HasTrivialGenericFormalFiber is defined here and used in Construction.lean.

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

There exists a 2-dimensional Noetherian local UFD A whose completion is isomorphic to T and whose generic formal fiber is trivial.

This is Jensen's Corollary 2.4 applied to T with P = (0).