Alphabeta Math
TheoremStatement: 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.

Equal dimension is equivalent to generic quasi-finiteness

Statement

For a dominant morphism f:XY of irreducible classical varieties, the following are equivalent: dimX=dimY; the extension k(Y)k(X) is finite; and f1(U)U is quasi-finite for some nonempty target open U. Inseparable extensions are allowed.

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 a dominant morphism f:XY between irreducible classical varieties, there is a nonempty open UY, contained in f(X), such that every Xy with yU is nonempty and has pure dimension r=dimXdimY. 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. (Fibres have pure expected dimension over a dense open).

[F2]

A classical variety X has dimX0 if and only if its underlying set is finite. The empty set is included. A nonempty irreducible variety of dimension zero is one point. 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. (Zero-dimensional varieties are finite sets).

[F3]

A morphism f:XY of classical varieties is quasi-finite if every closed-point fibre Xy is a finite set; empty fibres are allowed. Classical morphisms here are of finite type: for an affine target chart and an affine source chart above it, any finite set of k-algebra generators of the source ring also generates it over the target ring. The inverse image has a finite affine cover because it is an open of a Noetherian variety. 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. (Quasi-finite classical morphisms).

[F4]

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).

[F5]

Let kKL be a tower of field extensions. Assume that trdegkK and trdegKL are finite. Then trdegkL=trdegkK+trdegKL. (Transcendence degree is additive in finite towers).

[F6]

If X is an irreducible classical variety, then dimX=trdegkk(X)<. 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. (Dimension equals transcendence degree).

Proof

1.1

Let K=k(Y)L=k(X) be the field injection. Both fields are finitely generated over k, and L is finitely generated over K. The dimension/transcendence-degree formula and tower additivity show that equal dimensions mean trdegKL=0. A finitely generated algebraic field extension is finite: adjoining its generators one at a time gives finite degrees whose product bounds the total degree. Conversely a finite extension is algebraic, so tower additivity gives equal dimensions.

F4F5F6
1.2

If the dimensions are equal, generic fibres on a nonempty target open are nonempty and zero-dimensional. They are finite by the zero-dimensional finiteness result, so the restriction is quasi-finite.

F1F2F3
2.1

Conversely suppose the restriction over a nonempty open U is quasi-finite. Intersect U with the nonempty open given by the generic fibre theorem. Irreducibility makes the intersection nonempty. A fibre there is nonempty and finite, hence has dimension zero, while the generic theorem gives its dimension as dimXdimY. Thus the dimensions are equal. The argument never equates fibre cardinality with field degree.

F1F2F3step 1.1

Depends on

Used by

Dependency tree · two levels

18 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