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 be a classical variety over an algebraically closed field and let , , be normalizations. There is a unique isomorphism over .
Facts & Assumptions
Given: AC, the algebraically closed field , the variety , and the two normalizations and .
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).
Universal property: if is a normalization and is a dominant birational morphism from a normal variety , there is a unique morphism with (Universal property of the normalization). AC is used there.
Proof
First suppose is irreducible. Each is a dominant birational morphism from the normal variety [F1]. Apply the universal property [F2] to the normalization and the morphism : there is a unique morphism over , i.e. with . Symmetrically there is a unique morphism with .
The composite satisfies . Apply [F2] to the normalization and the morphism : both and lift that morphism, so uniqueness gives . Symmetrically , so is an isomorphism with inverse .
Any isomorphism over satisfies , so is a morphism over lifting the identity of between the two normalizations; by the uniqueness clause of [F2] applied to the normalization and the dominant birational morphism , such a equals constructed above. Thus the isomorphism is unique in the irreducible case. For reducible , [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 sends a source component into the target normalization component with the same dense image in , since the target components are disjoint; uniqueness therefore holds componentwise. If is empty both normalizations are empty.
Depends on
- Universal property of the normalization
- The normalization of an irreducible affine variety
- Normalization of a classical variety by gluing affine normalizations
- Irreducible affine varieties are birational exactly when their function fields are isomorphic
- Birational maps and birational equivalence of classical affine varieties
- The Axiom of Choice
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
- J. S. Milne, Algebraic Geometry (2025 version), Ch. 8 §a-b: uniqueness of the normalization from its universal property (standard reference, not scraped)