The Main Transfinite Construction

An ordinal-indexed chain of A-extensions whose union satisfies Heitmann's Proposition 1 (surjectivity onto T/M² and ideal contraction), yielding a Noetherian local domain with prescribed completion (Jensen, 2006, Corollary 2.4).

theorem jensen_construction_p0_uncountable {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) (hT_aleph0 : Cardinal.aleph0 < Cardinal.mk T) (hht : ∀ (P : Ideal T), P.IsPrime → P ≠ IsLocalRing.maximalIdeal T → P.height ≤ 1) : ∃ (A : Type u) (x : CommRing A) (x_1 : IsLocalRing A) (_ : IsDomain A) (_ : UniqueFactorizationMonoid A) (_ : IsNoetherianRing A), Nonempty (AdicCompletion (IsLocalRing.maximalIdeal A) A ≃+* T) ∧ HasTrivialGenericFormalFiber A