Alphabeta Math
LemmaStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 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.

Induction produces a polynomial subalgebra over which the affine algebra is integral

Statement

Let k be a field and let A be a nonzero finite-type k-algebra. Then there exist algebraically independent elements z1,…,zd∈A such that A is integral over the polynomial subalgebra k[z1,…,zd].

Facts & Assumptions

Given: A field k and a nonzero finite-type k-algebra A.

[L1]

Finite type means generated by finitely many algebra elements (Subalgebra generated by a subset, algebras of finite type, and module-finite algebras).

[L2]

Integrality is transitive in towers of rings (Integral extensions are transitive).

[L3]

Over an infinite field, a triangular change can make a nonzero relation monic in the last variable (Over an infinite field, a triangular change makes a nonzero polynomial monic).

[L4]

Over an arbitrary field, the exponent-substitution trick isolates a unique highest xn-term (Rapidly increasing power substitutions isolate one highest x_n-term).

[L5]

A monic relation makes the last generator integral over the subalgebra generated by the earlier ones (A monic relation makes the last generator integral over the earlier ones).

Proof

technique · induction on the number of algebra generators
1.1L1givenchoose

By [L1], choose generators x1,…,xn of A as a k-algebra. We prove the theorem by induction on n.

1.2ih

Inductive hypothesis: assume the statement for every k-algebra generated by at most n−1 elements.

2.1basestep 1.1given

Base case n=0: then A is the image of k. Because A≠0 and k is a field, the structure map k→A is injective and hence identifies A with k=k[ ]. Thus A is integral over the empty polynomial algebra.

2.2step 1.1given

If x1,…,xn are algebraically independent over k, then A=k[x1,…,xn] already has the required form.

2.3L3L4L5step 1.1

Otherwise there is a nonzero polynomial relation among x1,…,xn. If k is infinite, apply [L3] to make such a relation monic in the last variable after a triangular change. If k is finite, apply [L4] to make such a relation monic in the last variable after the exponent substitution. In either case we obtain new generators y1,…,yn of A such that A is integral over B:=k[y1,…,yn−1] by [L5].

3.1L2step 1.2step 2.3

The algebra B is generated over k by n−1 elements, so the induction hypothesis yields algebraically independent elements z1,…,zd∈B such that B is integral over k[z1,…,zd]. Then [L2] and step 2.3 show that A is integral over k[z1,…,zd].

4.1step 2.1step 2.2step 3.1discharge-induction∎

Step 2.2 handles the algebraically independent case, while steps 2.3 and 3.1 handle the dependent case. Therefore the theorem holds for n generators, and hence for every finite-type k-algebra.

Depends on

Used by

Dependency tree · two levels

15 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