Combined Construction Step

Given an N-subring R, produce an A-extension S lifting a given element of T/M² and meeting a given nonzero prime, while closing all finitely generated ideals (Heitmann, 1993, Lemma 7).

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

theorem card_lt_of_aext' {T : Type u} [CommRing T] [IsLocalRing T] [IsNoetherianRing T] [IsDomain T] (hT_aleph0 : Cardinal.aleph0 < Cardinal.mk T) {A B : NSubring T} (hAB : IsAExtension A B) (hA : Cardinal.mk ↥A.carrier < Cardinal.mk T) : Cardinal.mk ↥B.carrier < Cardinal.mk T

theorem build_union_isNSubring {T : Type u} [CommRing T] [IsLocalRing T] [IsNoetherianRing T] [IsDomain T] {ι' : Type u} [LinearOrder ι'] [Nonempty ι'] (chain : NSubringChain T ι') (h_card : ∀ (α : ι'), Cardinal.mk ↥(chain.ring α).carrier ≤ max Cardinal.aleph0 (Cardinal.mk (IsLocalRing.ResidueField T))) (h_ι_card : Cardinal.mk ι' ≤ max Cardinal.aleph0 (Cardinal.mk (IsLocalRing.ResidueField T))) : ∃ (S : NSubring T), S.carrier = chain.unionSubring ∧ ∀ (α : ι'), (chain.ring α).carrier ≤ S.carrier

theorem close_up_all_one_pass {T : Type u} [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) (R' : NSubring T) (hR' : Cardinal.mk ↥R'.carrier < Cardinal.mk T) : ∃ (S : NSubring T), IsAExtension R' S ∧ Cardinal.mk ↥S.carrier < Cardinal.mk T ∧ ∀ (I : Ideal ↥R'.carrier), I.FG → ∀ (c : ↥R'.carrier), ↑c ∈ Ideal.map R'.carrier.subtype I → ∃ (hle : R'.carrier ≤ S.carrier), ⟨↑c, ⋯⟩ ∈ Ideal.map (Subring.inclusion hle) I

theorem build_union_isNSubring_nat {T : Type u} [CommRing T] [IsLocalRing T] [IsNoetherianRing T] [IsDomain T] (chain : NSubringChain T ℕ) (h_card : ∀ (n : ℕ), Cardinal.mk ↥(chain.ring n).carrier ≤ max Cardinal.aleph0 (Cardinal.mk (IsLocalRing.ResidueField T))) : ∃ (S : NSubring T), S.carrier = chain.unionSubring ∧ ∀ (n : ℕ), (chain.ring n).carrier ≤ S.carrier

theorem close_up_all_omega {T : Type u} [CommRing T] [IsLocalRing T] [IsNoetherianRing T] [IsDomain T] (R : NSubring T) (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) (one_pass : ∀ (R' : NSubring T), Cardinal.mk ↥R'.carrier < Cardinal.mk T → ∃ (S : NSubring T), IsAExtension R' S ∧ Cardinal.mk ↥S.carrier < Cardinal.mk T ∧ ∀ (I : Ideal ↥R'.carrier), I.FG → ∀ (c : ↥R'.carrier), ↑c ∈ Ideal.map R'.carrier.subtype I → ∃ (hle : R'.carrier ≤ S.carrier), ⟨↑c, ⋯⟩ ∈ Ideal.map (Subring.inclusion hle) I) : ∃ (S : NSubring T), IsAExtension R S ∧ ∀ (I : Ideal ↥S.carrier), I.FG → ∀ (c : ↥S.carrier), ↑c ∈ Ideal.map S.carrier.subtype I → c ∈ I

theorem close_up_all {T : Type u} [CommRing T] [IsLocalRing T] [IsNoetherianRing T] [IsDomain T] [IsAdicComplete (IsLocalRing.maximalIdeal T) T] (R : NSubring 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) (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) : ∃ (S : NSubring T), IsAExtension R S ∧ ∀ (I : Ideal ↥S.carrier), I.FG → ∀ (c : ↥S.carrier), ↑c ∈ Ideal.map S.carrier.subtype I → c ∈ I

theorem combined_step {T : Type u} [CommRing T] [IsLocalRing T] [IsNoetherianRing T] [IsDomain T] [IsAdicComplete (IsLocalRing.maximalIdeal T) T] (R : NSubring T) (ℓ : T ⧸ IsLocalRing.maximalIdeal T ^ 2) (q : Ideal T) (hq_prime : q.IsPrime) (hq_ne_bot : q ≠ ⊥) (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) : ∃ (S : NSubring T), IsAExtension R S ∧ (∃ (c : ↥S.carrier), (Ideal.Quotient.mk (IsLocalRing.maximalIdeal T ^ 2)) ↑c = ℓ) ∧ (∃ (t : ↥S.carrier), ↑t ∈ q ∧ ↑t ≠ 0) ∧ ∀ (I : Ideal ↥S.carrier), I.FG → ∀ (c : ↥S.carrier), ↑c ∈ Ideal.map S.carrier.subtype I → c ∈ I

theorem combined_step_surj {T : Type u} [CommRing T] [IsLocalRing T] [IsNoetherianRing T] [IsDomain T] [IsAdicComplete (IsLocalRing.maximalIdeal T) T] (R : NSubring T) (ℓ : T ⧸ IsLocalRing.maximalIdeal T ^ 2) (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) (hM_ne_bot : IsLocalRing.maximalIdeal T ≠ ⊥) : ∃ (S : NSubring T), IsAExtension R S ∧ (∃ (c : ↥S.carrier), (Ideal.Quotient.mk (IsLocalRing.maximalIdeal T ^ 2)) ↑c = ℓ) ∧ ∀ (I : Ideal ↥S.carrier), I.FG → ∀ (c : ↥S.carrier), ↑c ∈ Ideal.map S.carrier.subtype I → c ∈ I