TheoremStatement: Literature-sourcedProof: AI-adaptedverified 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.

The dimension formula for affine domains

Statement

Assume the Axiom of Choice. Let $k$ be a field, let $A$ be a finite-type $k$ -domain, and let $p \in Spec (A)$ . Then $ht (p) + {trdeg}_{k} Frac (A / p) = {trdeg}_{k} Frac (A) .$

Facts & Assumptions

Given: The Axiom of Choice (The Axiom of Choice), a field $k$ , a finite-type $k$ -domain $A$ , and a prime ideal $p \subset A$ .

[L1]

Under Choice, if $C$ is Noetherian and $Q \subset C [x]$ lies over $q \subset C$ of finite height, then $ht Q = ht q$ when $Q = q C [x]$ , and $ht Q = ht q + 1$ otherwise (A prime chain in R[x] has length at most one more than its contraction chain). Finite polynomial rings over fields are Noetherian (If $R$ is Noetherian then $R [x_{1}, \dots, x_{n}]$ is Noetherian for every $n \in N$ ).

[L2]

Noether normalization embeds a polynomial ring $B = k [z_{1}, \dots, z_{d}]$ in $A$ so that $A$ is module-finite over $B$ (Noether normalisation yields module finiteness over a polynomial subring). Such an extension is integral. Under Choice, if the base is integrally closed, the height of a prime of $A$ equals that of its contraction to $B$ (Under going down and incomparability, lying-over primes have the same finite height).

[L3]

Gauss's lemma says primitive polynomials remain primitive under products and detect irreducibility over the fraction field (Gauss lemma over a UFD). If $R$ is a UFD, factor the content of a polynomial in $R [x]$ and factor its primitive part over $Frac (R) [x]$ ; clearing denominators and taking primitive parts lifts those factors to $R [x]$ , while Gauss's lemma makes factorization unique. Thus $R [x]$ is again a UFD, and induction makes every finite-variable polynomial ring over a field a UFD. A UFD is integrally closed: if a reduced fraction $a / b$ is integral, its monic equation multiplied by $b^{n}$ makes $b ∣ a^{n}$ ; coprimality forces $b$ to be a unit.

[L4]

A prime quotient is a domain ( $R / P$ is an integral domain if and only if $P$ is a prime ideal); a one-variable polynomial ring over a field is a PID (For every field $F$ , $F [x]$ is a principal ideal domain); transcendence degree is additive in finite field towers (Transcendence degree is additive in finite towers).

Proof

technique · direct

1.1basealgebra

First prove the formula for $B_{d} = k [x_{1}, \dots, x_{d}]$ and every prime $Q \subset B_{d}$ , by induction on $d$ . When $d = 0$ , $B_{0} = k$ , its only prime is $(0)$ , and both sides are zero.

1.2L1L4ih

Write $B_{d} = C [x_{d}]$ where $C = B_{d - 1}$ , put $q = Q \cap C$ , and let $K = Frac (C / q)$ . By the induction hypothesis, $ht q + {trdeg}_{k} K = d - 1$ , so $q$ has finite height. The relative-height formula [L1] applies to the Noetherian ring $C$ .

1.3L2L4givenchoose

Independently, [L2] supplies algebraically independent $z_{1}, \dots, z_{e} \in A$ such that $B = k [z_{1}, \dots, z_{e}] \subset A$ is module-finite. Fix such a normalization. The fraction field $Frac (A)$ is algebraic over $Frac (B) = k (z_{1}, \dots, z_{e})$ , so its transcendence degree over $k$ is $e$ . Put $p_{B} = p \cap B$ . This fixed normalization will be used after the polynomial induction.

2.1L1L4step 1.2algebra

If $Q = q C [x_{d}]$ , then $B_{d} / Q = (C / q) [x_{d}]$ and its fraction field is $K (x_{d})$ . By [L1] the height remains $ht q$ , while the transcendence degree grows by one. If $Q \neq q C [x_{d}]$ , its image in $K [x_{d}]$ is a nonzero prime. The PID $K [x_{d}]$ makes this image generated by an irreducible polynomial, so the image of $x_{d}$ in $Frac (B_{d} / Q)$ is algebraic over $K$ . Thus the quotient fraction field has the same transcendence degree as $K$ , while [L1] raises the height by one. In either case the sum is $d$ .

3.1step 1.1step 2.1discharge-induction

The base and induction step prove $ht Q + {trdeg}_{k} Frac (B_{d} / Q) = d$ for every $d \geq 0$ and prime $Q \subset B_{d}$ .

4.1L2L3L4step 3.1step 1.3

By [L3] the polynomial ring $B$ is integrally closed, and by step 3.1 its prime $p_{B}$ has finite height. Hence the Choice-qualified height-preservation result [L2] gives $ht (p) = ht (p_{B})$ . The quotient $A / p$ is a domain by [L4] and remains integral over $B / p_{B}$ , so its fraction field is algebraic over $Frac (B / p_{B})$ . Therefore their transcendence degrees over $k$ agree.

5.1step 3.1step 1.3step 4.1∎

Apply step 3.1 to $p_{B} \subset B$ and substitute the two equalities from step 4.1 and $e = {trdeg}_{k} Frac (A)$ from step 1.3. This gives $ht (p) + {trdeg}_{k} Frac (A / p) = {trdeg}_{k} Frac (A)$ .

Depends on

Used by

Dependency tree · two levels

38 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)
The Stacks Project, Section 10.116: Dimension of finite type algebras over fields, reprise (standard reference, not scraped)
Melvin Hochster, Dimension theory and systems of parameters (standard reference, not scraped)