CorollaryStatement: Literature-sourcedProof: Literature-sourcedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-01

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.

Maximal chains in an affine domain all have the same length

Statement

Let $k$ be a field and let $A$ be a finite-type $k$ -domain. Every saturated prime chain from $(0)$ to a maximal ideal of $A$ has length $\dim A$ .

Facts & Assumptions

Given: A field $k$ , a finite-type $k$ -domain $A$ , and a saturated prime chain $(0) = p_{0} ⊊ p_{1} ⊊ \dots ⊊ p_{r} = m .$

[L1]

In a domain, the minimal prime $(0)$ has height zero (Minimal primes are exactly the primes of height zero).

[L2]

Every maximal ideal of an affine domain has height equal to the full dimension (Maximal ideals of an affine domain have full height).

[L3]

For primes $p \subseteq q$ in an affine domain, $ht (q / p) + {trdeg}_{k} Frac (A / q) = {trdeg}_{k} Frac (A / p)$ (Transcendence degrees along affine prime quotients add correctly).

[L4]

For every prime $p$ of an affine domain, $ht (p) + {trdeg}_{k} Frac (A / p) = {trdeg}_{k} Frac (A)$ (The dimension formula for affine domains).

Proof

technique · direct

1.1

By [L1], $ht (p_{0}) = 0$ .

L1given

2.1

For each $0 \leq i < r$ , the quotient $A / p_{i}$ is a domain and the chain is saturated, so there is no prime strictly between $0$ and $p_{i + 1} / p_{i}$ in $A / p_{i}$ . Hence $ht (p_{i + 1} / p_{i}) = 1$ . Applying [L3] to $p_{i} \subseteq p_{i + 1}$ and comparing [L4] at $p_{i}$ and $p_{i + 1}$ gives $ht (p_{i + 1}) = ht (p_{i}) + 1$ .

L3L4step 1.1given

3.1

Starting from step 1.1 and iterating step 2.1, we obtain $ht (m) = r$ . By [L2], $ht (m) = \dim A$ . Therefore the saturated chain has length $\dim A$ , and every such chain has the same length.

L2step 2.1∎

Depends on

Used by

Why the equal-chain statement stops at affine domains Remark

Dependency tree · two levels

9 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

J. S. Milne, A Primer of Commutative Algebra, v4.03, §§18, 21 (standard reference, not scraped)
Melvin Hochster, Dimension theory and systems of parameters (standard reference, not scraped)