Alphabeta Math
LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedjudge pass (gpt-5.6-terra)audited 2026-09-07
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 dominant affine map factors finitely over relative affine space after shrinking the base

Statement

Let f:XY be dominant between irreducible affine varieties, put A=k[Y]B=k[X], and let r=trdegk(Y)k(X). There are 0aA and elements t1,,trBa, algebraically independent over Aa, such that Ba is module-finite over Aa[t1,,tr].

Work over a fixed algebraically closed field k, with the Axiom of Choice. Classical varieties are separated and admit finite affine covers; they may be reducible or empty unless irreducibility is specified. Irreducible means nonempty. All fibres and points below are classical closed-point fibres and points.

Facts & Assumptions

Given: The objects and hypotheses in the statement.

[F1]

For irreducible classical X, the fraction fields of all nonempty affine charts identify canonically; denote the resulting field by k(X). A dominant morphism f:XY between irreducible classical varieties induces an injection f:k(Y)k(X). Dominant means that the image is dense. Work over a fixed algebraically closed field k, with the Axiom of Choice. Classical varieties are separated and admit finite affine covers; they may be reducible or empty unless irreducibility is specified. Irreducible means nonempty. All fibres and points below are classical closed-point fibres and points. (Function fields and dominant pullbacks on general varieties).

[F2]

Let k be a field and let A be a nonzero finite-type k-algebra. Then there exist algebraically independent elements z1,,zdA such that A is a module-finite algebra over the polynomial ring k[z1,,zd]. (Noether normalisation yields module finiteness over a polynomial subring).

[F3]

Assume the Axiom of Choice. Let X be a classical affine variety over an algebraically closed field k, and let fk[X]. Put U=DX(f). A function φ:Uk is called regular on U if there exist finitely many pairs (gi,hi) in k[X]×k[X] such that U=i=1rDX(hi) and φ(x)=gi(x)hi(x)for every xDX(hi). Write OX(U) for the ring of regular functions on U. Then evaluation induces a ring isomorphism k[X]fOX(U). If U=, both sides are the zero ring. (Regular functions on a principal open are the principal localization of the coordinate ring).

Proof

1.1

Dominance makes AB injective and identifies their fraction fields with k(Y)k(X). Put K=FracA. The localization BK=BAK is a nonzero finite-type K-domain inside FracB, with that same fraction field.

F1
2.1

Apply normalization over the field K to obtain algebraically independent t1,,trBK over which BK is module-finite. Their number is r because the fraction field is algebraic over the fraction field of the normalization polynomial ring. Choose finite A-algebra generators b1,,bs of B. Each satisfies a monic equation over K[t1,,tr].

F2step 1.1
3.1

Every ti is a fraction with numerator in B and nonzero denominator in A. Invert the product a of these denominators and all denominators in the finitely many monic-equation coefficients. The product is nonzero because A is a domain, and an empty product is 1. Now tiBa, and the same equations are monic over Aa[t1,,tr]. Independence descends from K. If the equation degrees are dj, the finitely many monomials jbjej with 0ej<dj span Ba over this polynomial subring by repeated monic reduction. The principal-open supplier identifies the localized rings with the corresponding open-chart rings. This works also for r=0.

F3step 2.1

Depends on

Used by

Dependency tree · two levels

5 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