CorollaryStatement: Literature-sourcedProof: Literature-sourcedprecheck passaudited 2026-08-30

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.

A domain finite over a polynomial ring has dimension at least the number of variables

Statement

Assume the Axiom of Choice.

Let $k$ be a field, let $d \geq 0$ , and let $A$ be an integral domain that is module-finite over the polynomial ring $k [z_{1}, \dots, z_{d}]$ via an injective $k$ -algebra map

k [z_{1}, \dots, z_{d}] ↪ A .

Then

\dim A \geq d .

Facts & Assumptions

Given: The Axiom of Choice, a field $k$ , an integer $d \geq 0$ , an integral domain $A$ , and an injective $k$ -algebra map $k [z_{1}, \dots, z_{d}] ↪ A$ making $A$ module-finite over $k [z_{1}, \dots, z_{d}]$ .

[L1]

Krull dimension is the supremum of the lengths of chains of prime ideals (Krull dimension of a nonzero ring).

[L2]

Integral extensions lift finite prime chains from the base (Integral extensions lift finite prime chains from the base).

Proof

technique · direct

1.1

Because $A$ is finitely generated as a module over $R : = k [z_{1}, \dots, z_{d}]$ , multiplication by any $a \in A$ is an $R$ -linear endomorphism of a finite $R$ -module. Cayley-Hamilton therefore gives a monic polynomial over $R$ satisfied by $a$ , so $A$ is integral over $R$ .

givenalgebra

1.2

The polynomial ring $R$ has the prime chain $(0) \subset (z_{1}) \subset (z_{1}, z_{2}) \subset \dots \subset (z_{1}, \dots, z_{d}),$ of length $d$ : each quotient by $(z_{1}, \dots, z_{i})$ is again a polynomial ring over $k$ and hence an integral domain, so those ideals are prime.

givenalgebra

2.1

Apply [L2] to the chain from step 1.2 and the integral inclusion $R \subseteq A$ from step 1.1. This gives a chain of $d + 1$ prime ideals in $A$ , so by [L1] the dimension of $A$ is at least $d$ .

L1L2step 1.1step 1.2∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

4 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

Allen B. Altman and Steven L. Kleiman, A Term of Commutative Algebra, 13th ed., Lemma (15.9) (standard reference, not scraped)