Transfinite Construction #
The ordinal-indexed iteration that builds an ascending chain of N-subrings, ensuring at each successor step that one more prime is caught and one more element of T/M^2 is covered.
Jensen, "Completions of UFDs with semi-local formal fibers", 2006, Theorem 2.2.
Ordinal-indexed transfinite construction #
Replace the Zorn approach (which needs hk_countable) with ordinal recursion
over V = {nonzero primes of T} × T/M². This eliminates the countability
assumption, using ℵ₀ < #T and #R < #T propagation instead.
Architecture #
- Index set: V = {q : Ideal T // q.IsPrime ∧ q ≠ ⊥} × (T ⧸ M²)
- Ordinal: κ = Cardinal.ord (#V)
- Base: R₀ = initial_NSubring (from NSubring.lean), closed up
- Successor at α: combined_step_card R(α) (q_α, ℓ_α)
- Limit at λ: transfinite union of R(β) for β < λ
- Result: A = R(κ) satisfies surjectivity, closedness, prime coverage
Helper lemma: build an NSubring from a union of predecessors #
Extracted from the main transfinite construction to stay within the default
heartbeat budget. Given a family of NSubrings indexed by predecessors of α,
builds the union as an NSubring with cardinal bounds and prime preservation.
theorem
transfinite_construction
{T : Type u}
[CommRing T]
[IsLocalRing T]
[IsNoetherianRing T]
[IsDomain T]
[IsAdicComplete (IsLocalRing.maximalIdeal T) T]
(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)
(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_aleph0 : Cardinal.aleph0 < Cardinal.mk T)
: