Alphabeta Math
CorollaryStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedjudge pass (gpt-6.1-sol)
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.

The normalization is unique up to unique isomorphism

Statement

Assume the Axiom of Choice. Let X be a classical variety over an algebraically closed field and let νi ⁣:Xi→X, i=1,2, be normalizations. There is a unique isomorphism X1→∼X2 over X.

Facts & Assumptions

Given: AC, the algebraically closed field k, the variety X, and the two normalizations ν1 ⁣:X1→X and ν2 ⁣:X2→X.

[F1]

In the irreducible case a normalization is a finite, surjective, birational morphism from a normal variety, and it exists per component in the reduced reducible case (Normalization of a classical variety by gluing affine normalizations, The normalization of an irreducible affine variety); birational morphisms between varieties induce isomorphisms of function fields (Irreducible affine varieties are birational exactly when their function fields are isomorphic, Birational maps and birational equivalence of classical affine varieties).

[F2]

Universal property: if ν ⁣:Xν→X is a normalization and f ⁣:Y→X is a dominant birational morphism from a normal variety Y, there is a unique morphism g ⁣:Y→Xν with ν∘g=f (Universal property of the normalization). AC is used there.

Proof

1.1F1F2given

First suppose X is irreducible. Each νi is a dominant birational morphism from the normal variety Xi [F1]. Apply the universal property [F2] to the normalization ν1 and the morphism ν2 ⁣:X2→X: there is a unique morphism g ⁣:X2→X1 over X, i.e. with ν1∘g=ν2. Symmetrically there is a unique morphism h ⁣:X1→X2 with ν2∘h=ν1.

2.1F1F2step 1.1

The composite h∘g ⁣:X2→X2 satisfies ν2∘(h∘g)=ν1∘g=ν2. Apply [F2] to the normalization ν2:X2→X and the morphism ν2:X2→X: both h∘g and idX2 lift that morphism, so uniqueness gives h∘g=idX2. Symmetrically g∘h=idX1, so g is an isomorphism with inverse h.

3.1F1F2step 1.1step 2.1∎

Any isomorphism u ⁣:X1→X2 over X satisfies ν2∘u=ν1, so u is a morphism over X lifting the identity of X between the two normalizations; by the uniqueness clause of [F2] applied to the normalization ν2 and the dominant birational morphism ν1:X1→X, such a u equals h constructed above. Thus the isomorphism is unique in the irreducible case. For reducible X, [F1] describes each normalization as the disjoint union over its finitely many irreducible components. Apply the irreducible result to each component and take the disjoint union. Any map over X sends a source component into the target normalization component with the same dense image in X, since the target components are disjoint; uniqueness therefore holds componentwise. If X is empty both normalizations are empty.

Depends on

Used by

Nothing in the library uses this result yet.

Cited to discharge well-definedness by The normalization of an irreducible affine variety.

Dependency tree · two levels

34 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