Heitmann's Proposition 1

If a subring R of a complete local domain T surjects onto T/M^2 and satisfies IT cap R = I for all finitely generated ideals I, then R is Noetherian with completion isomorphic to T. Also: when depth T >= 2, associated primes of T have height at most 1.

Heitmann, "Characterization of completions of UFDs", 1993, Prop. 1.

Helper lemmas for the completion isomorphism

theorem map_maxIdeal_eq_of_surj_closed {T : Type u} [CommRing T] [IsLocalRing T] [IsNoetherianRing T] [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

Under the hypotheses of Proposition 1, M = M_R · T. This is a Nakayama argument: R + M² = T implies M ≤ Ideal.map R.subtype M_R + M², and since M is f.g. and M ≤ jacobson ⊥, Nakayama gives M ≤ Ideal.map R.subtype M_R.

Proposition 1: Criterion for Noetherian completion

If (R, M ∩ R) ⊆ (T, M) with R → T/M² surjective and IT ∩ R = I for all finitely generated ideals I, then R is Noetherian and R̂ ≅ T.

theorem heitmann_prop1 {T : Type u} [CommRing T] [IsLocalRing T] [IsNoetherianRing T] [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) : IsNoetherianRing ↥R ∧ ∃ (e : AdicCompletion (IsLocalRing.maximalIdeal ↥R) ↥R ≃+* T), ∀ (a : ↥R), e ((AdicCompletion.of (IsLocalRing.maximalIdeal ↥R) ↥R) a) = R.subtype a

Heitmann's Proposition 1: A subring R of a complete local ring T satisfying

• R → T/M² surjective
• IT ∩ R = I for all finitely generated ideals I of R is Noetherian with completion isomorphic to T.

Auxiliary: Depth ≥ 2 implies associated prime conditions

From depth T ≥ 2, we derive:

1. M is not an associated prime of T/rT for any nonzero r (since ht(M) ≥ 2 > 1)
2. All associated primes of T/rT have height ≤ 1 (Krull PIT for principal ideals)

theorem maximal_not_assoc_of_depth_ge_two {T : Type u} [CommRing T] [IsLocalRing T] [IsNoetherianRing T] [IsDomain T] (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, the maximal ideal M is not an associated prime of T/rT for any nonzero r. This follows because if M ∈ Ass(T/rT) then depth(M, T/rT) = 0, but depth(M, T) ≥ 2 and r is regular (domain) so depth(M, T/rT) ≥ 1 by the depth lemma.

theorem assoc_height_le_one_of_domain {T : Type u} [CommRing T] [IsLocalRing T] [IsNoetherianRing T] [IsDomain T] (hdepth : ∃ (a : T) (b : T), a ∈ IsLocalRing.maximalIdeal T ∧ b ∈ IsLocalRing.maximalIdeal T ∧ RingTheory.Sequence.IsRegular T [a, b]) (hht : ∀ (P : Ideal T), P.IsPrime → P ≠ IsLocalRing.maximalIdeal T → P.height ≤ 1) (r : T) (hr : r ≠ 0) (P : Ideal T) (hP : P ∈ associatedPrimes T (T ⧸ Ideal.span {r})) : P.height ≤ 1

In a Noetherian local domain with depth ≥ 2, if all primes P ≠ M have height ≤ 1, then associated primes of T/rT for nonzero r have height ≤ 1. The height hypothesis holds for our concrete T (dim = 2).