Alphabeta Math
CorollaryStatement: Literature-sourcedProof: AI-adaptedPipeline-generated
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.

Birational quasi-finite maps to normal targets are open immersions

Statement

Assume the Axiom of Choice. Let f ⁣:Y→X be a finite morphism of irreducible classical varieties over an algebraically closed field. If f is birational and X is normal, then f is an isomorphism. In particular bijectivity plus finiteness does not repair a failure of normality of the target, as the cusp example on the companion page shows.

More generally, a quasi-finite birational morphism f:Y→X of irreducible classical varieties with normal target X is an open immersion. If it is bijective, it is an isomorphism even without an additional finiteness hypothesis.

Facts & Assumptions

Given: AC, the algebraically closed field k, the irreducible varieties Y,X, the finite morphism f ⁣:Y→X, birationality of f, and normality of X.

[F1]

A finite birational morphism onto a normal classical variety is an isomorphism (A finite birational morphism onto a normal variety is an isomorphism): this is the substantive input, whose hypotheses are exactly finiteness, birationality, and normality of the target.

[F2]

Finiteness, birationality and normality are the notions of Finite morphisms of classical varieties, Birational maps and birational equivalence of classical affine varieties, Irreducible affine varieties are birational exactly when their function fields are isomorphic and Normal points and normal varieties; AC is the choice principle consumed by the localisation and Nullstellensatz interfaces behind [F1].

[F3]

A separated finite-type classical morphism with finite fibres factors as an open immersion followed by a finite morphism (Zariski's Main Theorem: open immersion followed by a finite morphism, Quasi-finite classical morphisms). Classical varieties are separated and have finite affine atlases; a morphism between them is separated, since its relative diagonal is the restriction of the closed absolute diagonal. Closed subvarieties have their reduced classical structure (Classical algebraic prevarieties, regular maps, and varieties).

[F4]

The Axiom of Choice is assumed through the cited finite and Zariski Main suppliers (The Axiom of Choice).

Proof

1.1F1F2given

The hypotheses of [F1] are satisfied: f is finite, birational, and X is normal. Hence [F1] applies and f is an isomorphism. No injectivity, bijectivity, or surjectivity hypothesis was used, and none is needed.

1.2F1F2F3F4constructalgebra

For the general quasi-finite case assume Y,X irreducible, f birational and X normal. Apply [F3] to factor f=g∘j, with j:Y↪N open and g:N→X finite. Let N0 be the reduced irreducible closure of j(Y) in N. The subset j(Y) is open and dense in N0, so j identifies Y with that open subvariety and their function fields agree. Over an affine open of X, the coordinate ring of N0 is a quotient of the finite coordinate algebra of N and is still finite. Thus g0:N0→X is finite. It is birational because its pullback of function fields agrees with that of f under the dense open identification. By [F1], g0 is an isomorphism. Consequently f=g0∘j is an open immersion.

2.1F1F2step 1.1

The stated consequence for the cusp is a matter of exhibiting a finite birational morphism onto a nonnormal target that is bijective and not an isomorphism; that witness is the cusp reprise on the companion examples page, where the normalization of the cusp is bijective with a nonsurjective pullback of coordinate rings. Normality of the target is the hypothesis used in step 1.1; the recorded nonnormal-target witness does not contradict it.

3.1step 1.1step 1.2∎

If f is also bijective, its image open subvariety is all of X, and the open immersion of step 1.2 is an isomorphism. This proves both general consequences while retaining the original finite case of step 1.1.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

36 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