Transfinite Union of A-extensions

A well-ordered ascending chain of A-extensions has union that is again an N-subring: the UFD property and prime preservation pass to the colimit.

Heitmann, "Characterization of completions of UFDs", 1993, Lemma 6 Loepp, "Constructing local generic formal fibers", 1997, Lemmas 14--15.

Chain of N-subrings

A well-ordered ascending chain of N-subrings where each successor step is an A-extension and limit steps are unions.

structure NSubringChain (T : Type u_2) [CommRing T] [IsLocalRing T] [IsNoetherianRing T] [IsDomain T] (ι : Type u_3) [Preorder ι] : Type (max u_2 u_3)

A well-ordered ascending chain of N-subrings indexed by a linearly ordered type. Prime elements are preserved along the chain (A-extension property).

• ring : ι → NSubring T

  The N-subring at each index

• mono ⦃α β : ι⦄ : α ≤ β → (self.ring α).carrier ≤ (self.ring β).carrier

  The chain is ascending

• primes_preserved ⦃α β : ι⦄ (h : α ≤ β) (r : ↥(self.ring α).carrier) : Prime r → Prime ⟨↑r, ⋯⟩

  Prime elements are preserved along the chain

theorem NSubringChain.directed_carriers {T : Type u_1} [CommRing T] [IsLocalRing T] [IsNoetherianRing T] [IsDomain T] {ι : Type u_2} [LinearOrder ι] (chain : NSubringChain T ι) : Directed (fun (x1 x2 : Subring T) => x1 ≤ x2) fun (α : ι) => (chain.ring α).carrier

The family of carriers is directed (since ι is linearly ordered).

def NSubringChain.unionSubring {T : Type u_1} [CommRing T] [IsLocalRing T] [IsNoetherianRing T] [IsDomain T] {ι : Type u_2} [LinearOrder ι] (chain : NSubringChain T ι) : Subring T

The union of all subrings in the chain.

Equations

• chain.unionSubring = ⨆ (α : ι), (chain.ring α).carrier

theorem NSubringChain.le_union {T : Type u_1} [CommRing T] [IsLocalRing T] [IsNoetherianRing T] [IsDomain T] {ι : Type u_2} [LinearOrder ι] (chain : NSubringChain T ι) (α : ι) : (chain.ring α).carrier ≤ chain.unionSubring

Every chain member is contained in the union.

theorem NSubringChain.mem_union_iff {T : Type u_1} [CommRing T] [IsLocalRing T] [IsNoetherianRing T] [IsDomain T] {ι : Type u_2} [LinearOrder ι] [Nonempty ι] (chain : NSubringChain T ι) {x : T} : x ∈ chain.unionSubring ↔ ∃ (α : ι), x ∈ (chain.ring α).carrier

An element is in the union iff it's in some chain member.

theorem transfinite_union_primes_preserved {T : Type u_1} [CommRing T] [IsLocalRing T] [IsNoetherianRing T] [IsDomain T] {ι : Type u_2} [LinearOrder ι] (chain : NSubringChain T ι) (S : Subring T) (hS : ∀ (α : ι), (chain.ring α).carrier ≤ S) (hS_union : ∀ (x : ↥S), ∃ (α : ι), ↑x ∈ (chain.ring α).carrier) (α : ι) (p : ↥(chain.ring α).carrier) (hp : Prime p) : Prime ⟨↑p, ⋯⟩

Prime elements of any R_α remain prime in the union.

theorem transfinite_union_isUFD {T : Type u_1} [CommRing T] [IsLocalRing T] [IsNoetherianRing T] [IsDomain T] {ι : Type u_2} [LinearOrder ι] (chain : NSubringChain T ι) (S : Subring T) (hS : ∀ (α : ι), (chain.ring α).carrier ≤ S) (hS_union : ∀ (x : ↥S), ∃ (α : ι), ↑x ∈ (chain.ring α).carrier) : UniqueFactorizationMonoid ↥S

The union of A-extensions is a UFD. If x is irreducible in ⋃ R_α, then x ∈ R_β for some β, and x is prime in R_β (since R_β is a UFD), hence x | a or x | b in R_β ⊆ ⋃ R_α.

def NSubringChain.unionNSubring {T : Type u_1} [CommRing T] [IsLocalRing T] [IsNoetherianRing T] [IsDomain T] {ι : Type u_2} [LinearOrder ι] [Nonempty ι] (chain : NSubringChain T ι) (h_card : Cardinal.mk ↥chain.unionSubring ≤ max Cardinal.aleph0 (Cardinal.mk (IsLocalRing.ResidueField T))) : NSubring T

The union of a chain of N-subrings, when its carrier satisfies the N-subring cardinality bound.

Equations

• chain.unionNSubring h_card = { carrier := chain.unionSubring, isUFD := ⋯, isLocalRing := ⋯, card_le := ⋯, maximal_ideal_eq := ⋯, height_bound := ⋯ }

theorem transfinite_union_isNSubring {T : Type u_1} [CommRing T] [IsLocalRing T] [IsNoetherianRing T] [IsDomain T] {ι' : Type u_1} [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), ∀ (α : ι'), (chain.ring α).carrier ≤ S.carrier

Heitmann Lemma 6: The union of a well-ordered ascending chain of A-extensions is an N-subring (modulo cardinality bound).

Key properties preserved:

• UFD: factors in some R_α irreducibles are prime.
• N-subring conditions (2) and (3) pass to unions.
• Cardinality: |⋃ R_α| ≤ sup(ℵ₀, |R₀|, |α|).