N-subrings and A-extensions

An N-subring of a complete local domain (T, M) is a quasi-local UFD subring satisfying a height condition on associated primes. An A-extension preserves primality and cardinality bounds.

• Heitmann, "Characterization of completions of UFDs", 1993.
• Jensen, "Completions of UFDs with semi-local formal fibers", 2006.

N-subring definition

For T a complete local domain, the N-subring conditions simplify:

• Condition (2) (Q ∩ R = (0) for Q ∈ Ass(T)) is automatic since Ass(T) = {(0)} and R ⊆ T domain.
• Condition (3): for every regular t ∈ T and P ∈ Ass(T/tT), ht(P ∩ R) ≤ 1.

structure NSubring (T : Type u_2) [CommRing T] [IsLocalRing T] [IsNoetherianRing T] [IsDomain T] : Type u_2

An N-subring of a complete local domain (T, M). This is a quasi-local UFD R ⊆ T with bounded cardinality and a height condition on associated primes of principal ideals.

• carrier : Subring T

  The underlying subring of T

• isUFD : UniqueFactorizationMonoid ↥self.carrier

  R is a UFD

• isLocalRing : IsLocalRing ↥self.carrier

  R is a local ring (quasi-local with M ∩ R as maximal ideal)

• card_le : Cardinal.mk ↥self.carrier ≤ max Cardinal.aleph0 (Cardinal.mk (IsLocalRing.ResidueField T))

  |R| ≤ max(ℵ₀, |T/M|)

• maximal_ideal_eq : IsLocalRing.maximalIdeal ↥self.carrier = Ideal.comap self.carrier.subtype (IsLocalRing.maximalIdeal T)

  The maximal ideal of R equals the contraction of M to R. This ensures R is "centered on M" — prime elements of R land in M.

• height_bound (t : T) : t ≠ 0 → ∀ P ∈ associatedPrimes T (T ⧸ Ideal.span {t}), (Ideal.comap self.carrier.subtype P).height ≤ 1

  For every nonzero t ∈ T and P ∈ Ass(T/tT), ht(P ∩ R) ≤ 1. This is the key condition ensuring that primes of T interact well with R.

instance NSubring.instUniqueFactorizationMonoidSubtypeMemSubringCarrier {T : Type u_1} [CommRing T] [IsLocalRing T] [IsNoetherianRing T] [IsDomain T] (N : NSubring T) : UniqueFactorizationMonoid ↥N.carrier

instance NSubring.instIsLocalRingSubtypeMemSubringCarrier {T : Type u_1} [CommRing T] [IsLocalRing T] [IsNoetherianRing T] [IsDomain T] (N : NSubring T) : IsLocalRing ↥N.carrier

@[implicit_reducible]

instance NSubring.instCoeOutSubring {T : Type u_1} [CommRing T] [IsLocalRing T] [IsNoetherianRing T] [IsDomain T] : CoeOut (NSubring T) (Subring T)

Coercion: an N-subring is a subring of T.

Equations

• NSubring.instCoeOutSubring = { coe := NSubring.carrier }

instance NSubring.isDomain {T : Type u_1} [CommRing T] [IsLocalRing T] [IsNoetherianRing T] [IsDomain T] (N : NSubring T) : IsDomain ↥N.carrier

An N-subring of a domain is itself a domain (as a subring of a domain).

A-extension

An A-extension S of an N-subring R is a larger N-subring where prime elements of R remain prime in S, and |S| ≤ max(ℵ₀, |R|).

structure IsAExtension {T : Type u_1} [CommRing T] [IsLocalRing T] [IsNoetherianRing T] [IsDomain T] (R S : NSubring T) : Prop

S is an A-extension of R if R ≤ S, primes of R remain prime in S, and the cardinality of S is bounded by max(ℵ₀, |R|).

• le : R.carrier ≤ S.carrier

  R is contained in S

• primes_preserved (r : ↥R.carrier) : Prime r → Prime ⟨↑r, ⋯⟩

  Prime elements of R remain prime in S. Expressed via the canonical embedding: if r ∈ R is prime, then its image in S is prime.

• card_le : Cardinal.mk ↥S.carrier ≤ max Cardinal.aleph0 (Cardinal.mk ↥R.carrier)

  |S| ≤ max(ℵ₀, |R|)

Initial N-subring

For T a complete local domain with depth ≥ 2, char 0, and no integer zero divisor, the prime subring (image of ℤ) localized at M ∩ (prime subring) gives an N-subring. In characteristic 0 over ℂ, this is essentially ℚ embedded in T.

theorem initial_NSubring {T : Type u_1} [CommRing T] [IsLocalRing T] [IsNoetherianRing T] [IsDomain T] [IsAdicComplete (IsLocalRing.maximalIdeal T) T] (hchar : ∀ (n : ℤ), n ≠ 0 → (algebraMap ℤ T) n ≠ 0) : ∃ (N : NSubring T), Cardinal.mk ↥N.carrier ≤ Cardinal.aleph0

The prime subring of T (image of ℤ → T), localized at its intersection with M, is an N-subring when T has depth ≥ 2 and no integer is a zero divisor.

Basic API

def NSubring.subtype {T : Type u_1} [CommRing T] [IsLocalRing T] [IsNoetherianRing T] [IsDomain T] (N : NSubring T) : ↥N.carrier →+* T

The inclusion map from an N-subring into T.

Equations

• N.subtype = N.carrier.subtype

theorem NSubring.ext {T : Type u_1} [CommRing T] [IsLocalRing T] [IsNoetherianRing T] [IsDomain T] {N₁ N₂ : NSubring T} (h : N₁.carrier = N₂.carrier) : N₁ = N₂

Two N-subrings are equal if their carriers are equal.