Close-up: two-generator ideals

The crux case of Heitmann's Lemma 4: given an A-extension R of a Noetherian local domain T and an ideal I = (a, b) with a nonzero element c in the span, produce a new A-extension in which the close-up condition holds for I. The coprime case is handled directly the general case reduces to it by extracting common factors.

Crux case: two generators (n = 2)

If I = (y₁, y₂)R and c ∈ IT ∩ R, write c = t₁y₁ + t₂y₂. Parameterize: c = (t₁ + ty₂)y₁ + (t₂ - ty₁)y₂. Choose t via avoidance, set x₁ = t₁ + ty₂, x₂ = t₂ - ty₁. The ring Rbar = R[x₁, y₂⁻¹] ∩ R[x₂, y₁⁻¹] localized at M is an A-extension with c = x₁y₁ + x₂y₂ ∈ IRbar.

Proof strategy (single adjoin + generalized close_up)

1. Decompose c = t₁·y₁ + t₂·y₂ in T (from Submodule.mem_span_pair)
2. Choose t via countable_avoidance so x₁ = t₁ + t·y₂ is transcendental over R and avoids associated primes of T/rT for all nonzero r ∈ R
3. Adjoin x₁ to R via adjoin_transcendental_isNSubring → get S with x₁ ∈ S
4. In S: c - x₁·y₁ = (t₂ - t·y₁)·y₂ ∈ y₂·T, and c - x₁·y₁ ∈ S
5. By close_up_dvd on S: c - x₁·y₁ ∈ y₂·S, i.e., ∃ x₂' ∈ S, c - x₁·y₁ = x₂'·y₂
6. Then c = x₁·y₁ + x₂'·y₂ ∈ span{y₁, y₂} in S

theorem close_up_two_gen_coprime {T : Type u_1} [CommRing T] [IsLocalRing T] [IsNoetherianRing T] [IsDomain T] [IsAdicComplete (IsLocalRing.maximalIdeal T) T] (R : NSubring T) (y₁ y₂ c : ↥R.carrier) (hc : ↑c ∈ Ideal.span {↑y₁, ↑y₂}) (hcoprime : ∀ (p : ↥R.carrier), Prime p → ¬(p ∣ y₁ ∧ p ∣ y₂)) (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)) : ∃ (S : NSubring T), IsAExtension R S ∧ ∃ (hle : R.carrier ≤ S.carrier) (x₁ : ↥S.carrier), ⟨↑c, ⋯⟩ - x₁ * ⟨↑y₁, ⋯⟩ ∈ Ideal.span {⟨↑y₂, ⋯⟩}

Coprime case of two-generator close-up: when y₁, y₂ have no common prime factor in R, find A-extension S with c - x₁·y₁ ∈ span{y₂} in S. This is the hard case requiring Krull domain intersection machinery.

theorem close_up_two_gen_key {T : Type u_1} [CommRing T] [IsLocalRing T] [IsNoetherianRing T] [IsDomain T] [IsAdicComplete (IsLocalRing.maximalIdeal T) T] (R : NSubring T) (y₁ y₂ c : ↥R.carrier) (hc : ↑c ∈ Ideal.span {↑y₁, ↑y₂}) (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)) : ∃ (S : NSubring T), IsAExtension R S ∧ ∃ (hle : R.carrier ≤ S.carrier) (x₁ : ↥S.carrier), ⟨↑c, ⋯⟩ - x₁ * ⟨↑y₁, ⋯⟩ ∈ Ideal.span {⟨↑y₂, ⋯⟩}

Key construction for the common factor case of close_up_two_gen: Given y₁ = pa, y₂ = pb with p prime and c ∈ span{y₁,y₂}T, factor out p using close_up_dvd, cancel it, and reduce to (a,b). Uses WF induction on y₁ via DvdNotUnit to handle the recursive case.

theorem close_up_two_gen {T : Type u_1} [CommRing T] [IsLocalRing T] [IsNoetherianRing T] [IsDomain T] [IsAdicComplete (IsLocalRing.maximalIdeal T) T] (R : NSubring T) (y₁ y₂ c : ↥R.carrier) (hc : ↑c ∈ Ideal.span {↑y₁, ↑y₂}) (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)) : ∃ (S : NSubring T), IsAExtension R S ∧ ∃ (hle : R.carrier ≤ S.carrier), ⟨↑c, ⋯⟩ ∈ Ideal.span {⟨↑y₁, ⋯⟩, ⟨↑y₂, ⋯⟩}

Close-up for two-generator ideals: if I = (y₁, y₂) and c ∈ IT ∩ R, there exists an A-extension S with c ∈ IS. This is the crux of Lemma 4.

General case: n generators (induction)

For n > 2, reduce to the n-1 case by factoring out common prime factors and applying the two-generator case.

theorem isAExtension_trans' {T : Type u_1} [CommRing T] [IsLocalRing T] [IsNoetherianRing T] [IsDomain T] {R S U : NSubring T} (h₁ : IsAExtension R S) (h₂ : IsAExtension S U) : IsAExtension R U

Local copy of isAExtension_trans (CombinedStep.lean has circular import).

theorem exists_prime_mem_of_ne_bot_closeup {S : Type u_2} [CommRing S] [IsDomain S] [UniqueFactorizationMonoid S] (Q : Ideal S) [hQ : Q.IsPrime] (hQ_ne_bot : Q ≠ ⊥) : ∃ (q : S), Prime q ∧ q ∈ Q