Heitmann's Lemma 4 — Closing Up Finitely Generated Ideals #
Given an N-subring R and c ∈ IT for a finitely generated ideal I of R, construct an A-extension S with c ∈ IS. The proof uses induction on generator count with GCD complexity as a well-founded measure (Heitmann, 1993, Lemma 4).
theorem
close_up_aux_wf
{T : Type u_1}
[CommRing T]
[IsLocalRing T]
[IsNoetherianRing T]
[IsDomain T]
[IsAdicComplete (IsLocalRing.maximalIdeal T) 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)
(hT_card : Cardinal.mk T = Cardinal.mk (IsLocalRing.ResidueField T))
(hT_aleph0 : Cardinal.aleph0 < Cardinal.mk T)
(n'' : ℕ)
(ih :
∀ (R : NSubring T),
Cardinal.mk ↥R.carrier < Cardinal.mk T →
∀ (s : Finset ↥R.carrier),
s.card ≤ n'' + 1 + 1 →
∀ (c : ↥R.carrier),
↑c ∈ Ideal.map R.carrier.subtype (Ideal.span ↑s) →
∃ (S : NSubring T),
IsAExtension R S ∧ ∃ (hle : R.carrier ≤ S.carrier), ⟨↑c, ⋯⟩ ∈ Ideal.map (Subring.inclusion hle) (Ideal.span ↑s))
(m : ℕ)
(R : NSubring T)
:
Cardinal.mk ↥R.carrier < Cardinal.mk T →
∀ (a : ↥R.carrier) (s : Finset ↥R.carrier),
gcdComplexity s ≤ m →
s.card = n'' + 1 + 1 + 1 →
a ∈ s →
∀ (c : ↥R.carrier),
↑c ∈ Ideal.map R.carrier.subtype (Ideal.span ↑s) →
∃ (S : NSubring T),
IsAExtension R S ∧ ∃ (hle : R.carrier ≤ S.carrier), ⟨↑c, ⋯⟩ ∈ Ideal.map (Subring.inclusion hle) (Ideal.span ↑s)
theorem
close_up_aux
{T : Type u_1}
[CommRing T]
[IsLocalRing T]
[IsNoetherianRing T]
[IsDomain T]
[IsAdicComplete (IsLocalRing.maximalIdeal T) 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)
(hT_card : Cardinal.mk T = Cardinal.mk (IsLocalRing.ResidueField T))
(hT_aleph0 : Cardinal.aleph0 < Cardinal.mk T)
(n : ℕ)
(R : NSubring T)
:
Cardinal.mk ↥R.carrier < Cardinal.mk T →
∀ (s : Finset ↥R.carrier),
s.card ≤ n →
∀ (c : ↥R.carrier),
↑c ∈ Ideal.map R.carrier.subtype (Ideal.span ↑s) →
∃ (S : NSubring T),
IsAExtension R S ∧ ∃ (hle : R.carrier ≤ S.carrier), ⟨↑c, ⋯⟩ ∈ Ideal.map (Subring.inclusion hle) (Ideal.span ↑s)
Helper for close_up: induction on generator count, universally quantified over all NSubrings R. This allows the IH to apply to A-extensions in the n≥3 case.
theorem
close_up
{T : Type u_1}
[CommRing T]
[IsLocalRing T]
[IsNoetherianRing T]
[IsDomain T]
[IsAdicComplete (IsLocalRing.maximalIdeal T) T]
(R : NSubring T)
(I : Ideal ↥R.carrier)
(hI_fg : I.FG)
(c : ↥R.carrier)
(hc : ↑c ∈ Ideal.map R.carrier.subtype I)
(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))
(hT_aleph0 : Cardinal.aleph0 < Cardinal.mk T)
:
Heitmann Lemma 4 (main close-up theorem): Given N-subring R, finitely generated ideal I of R, and c ∈ R with c ∈ IT, there exists an A-extension S of R with c ∈ IS (in S.carrier).
Proof by induction on number of generators:
- n = 1: close_up_dvd
- n = 2: close_up_two_gen
- n > 2: Heitmann general case