Chain Helpers for the Transfinite Construction

Cardinal arithmetic wrappers and cardinality bounds on chain unions needed for the ordinal-indexed iteration in Jensen's construction of UFDs with prescribed completions.

Jensen, "Completions of UFDs with semi-local formal fibers", 2006, Theorem 2.2.

Main Construction: Jensen's Corollary 2.4 for P = (0)

For T a complete local domain with depth ≥ 2, |T/M| = |T|, char 0, construct a local UFD A with  ≅ T and HasTrivialGenericFormalFiber A.

Construction:

1. Start with R₀ = initial N-subring (≅ ℚ).
2. Well-order V = {nonzero primes of T} × T/M² with |V| = |T/M|.
3. At successor α: use combined_step with q_α and ℓ_α.
4. At limit α: take transfinite union.
5. A = ⋃ R_α satisfies Prop 1 conditions ⟹ A is Noetherian, Â ≅ T.
6. A is a UFD (transfinite union preserves UFD).
7. For every nonzero prime q: q ∩ A ≠ (0) (handled at step for q).
8. Therefore HasTrivialGenericFormalFiber A.

Cardinal-parameter versions of the combined step

Versions of the combined step that use cardinal bounds #R < #T and ℵ₀ < #T instead of countability of R. These are the forms needed by the transfinite iteration, where intermediate subrings grow beyond countable but remain strictly smaller than T.

theorem combined_step_card {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_aleph0 : Cardinal.aleph0 < Cardinal.mk T) (hT_card : Cardinal.mk T = Cardinal.mk (IsLocalRing.ResidueField 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) ∧ Cardinal.mk ↥S.carrier < Cardinal.mk T

Cardinal-param version of combined_step: given #R < #T and ℵ₀ < #T, produce an A-extension S with coverage for ℓ, catching for q, closedness, and #S < #T.

theorem combined_step_surj_card {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_aleph0 : Cardinal.aleph0 < Cardinal.mk T) (hT_card : Cardinal.mk T = Cardinal.mk (IsLocalRing.ResidueField 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) ∧ Cardinal.mk ↥S.carrier < Cardinal.mk T

Cardinal-param version of combined_step_surj: surjectivity-only step.

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

Cardinality bound at limit steps of ordinal recursion: the union of a chain of NSubrings indexed by ι' with #ι' < #T and each #R(α) bounded by #ι' has #(⋃R) < #T. The hypothesis h_card_bound (each #R_α ≤ #ι') is satisfied in the recursion because finitely generated operations preserve cardinality of infinite rings, so #R(β) ≤ #R(0) · #β ≤ #λ for β < λ.