Alphabeta Math
LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedverified 2026-09-24 (gpt-6-sol)
How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

  • Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
  • AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
  • AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

normal domain implies s two

Statement

Assume the Axiom of Choice (The Axiom of Choice). Every commutative Noetherian integrally closed domain satisfies (S2).

Facts & Assumptions

Given: The objects and hypotheses in the statement. The Axiom of Choice is assumed; cited dependent-choice and resolution-existence hypotheses are retained.

[F1]

serre r k and s k conditions: For a commutative Noetherian ring R and an integer j≥0, condition (Rj) means that Rp is regular whenever ht⁡p≤j. Condition (Sj) means that depth⁡Rp≥min⁡{j,dim⁡Rp} for every prime p. A finite module M satisfies (Sj) if depth⁡RpMp≥min⁡{j,dim⁡Supp⁡RpMp} for every prime in its support. Outside the support the condition is vacuous, consistent with depth of the zero module being +∞ and the empty support having no nonnegative dimension. Thus the zero module satisfies all (Sj) conditions, and the zero ring satisfies both families vacuously.

[F2]

A domain is integrally closed if and only if its prime localisations are, equivalently if and only if its maximal localisations are: Assume the Axiom of Choice. Let A be a domain. Then the following are equivalent: 1. A is integrally closed. 2. For every prime ideal p of A, the localisation Ap is integrally closed. 3. For every maximal ideal m of A, the localisation Am is integrally closed.

[F3]

The local depth-zero associated-prime criterion: Let (R,m) be a Noetherian local ring and let M≠0 be a finite R-module. Then depth⁡(M)=0⟺m∈Ass⁡R(M).

[F4]

Depth drops by one after quotienting by a regular element: Let R be Noetherian, let M be finite, let I lie in the Jacobson radical, and let x∈I be M-regular. Then depth⁡I(M/xM)=depth⁡I(M)−1.

[F5]

Krull's height theorem: Let R be a Noetherian commutative ring, let I=(x1,…,xn) be an ideal generated by n≥1 elements, and let p be a prime ideal minimal over I. Then ht⁡(p)≤n.

Proof

1.1F2F1

Localize at any prime. The resulting ring A is again an integrally closed domain. In dimension zero it is a field and the required bound is zero; in positive dimension a nonzero element of the maximal ideal is a nonzerodivisor, so its depth is at least one. It remains to consider dim⁡A≥2.

2.1F4F3step 1.1

If such an A had depth one, choose 0≠a∈mA. The regular-element depth formula and the depth-zero criterion supply b∉(a) with Ann⁡A/(a)(bˉ)=mA. Put u=b/a∈Frac⁡A∖A. Then umA⊆A.

3.1step 2.1algebra

If umA⊆mA, take finite generators z1,…,zs of the nonzero ideal mA and write uzi=∑jcijzj with cij∈A. The adjugate identity for uI−C gives det⁡(uI−C)zi=0 for all i. Some zi≠0 in a domain, hence det⁡(uI−C)=0. This is a monic equation for u, contradicting integral closedness.

4.1F5F1step 1.1step 3.1∎

Otherwise there exists t∈mA with ut a unit. For every s∈mA, s=t(us)/(ut) belongs to (t), so mA=(t). The height theorem with one generator gives dim⁡A≤1, again impossible. Therefore depth is at least two at every prime of height at least two; with the low-dimensional cases this is (S2).

Depends on

Used by

Dependency tree · two levels

25 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources