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.
Normalization commutes with restriction to an open subvariety
Statement
Assume the Axiom of Choice. Let be a classical variety with normalization and let be a nonempty open subvariety. Then is a normalization of : it is normal, and is finite, surjective and birational, so it is isomorphic to over .
Facts & Assumptions
Given: AC, the algebraically closed field , the classical variety with normalization , the nonempty open , and an affine chart of on an irreducible component, with coordinate ring and normalization in that component’s function field. The irreducible argument below is then applied componentwise.
In the irreducible case the normalization restricts over the affine chart to the affine normalization , with the integral closure of in and a finite -module; over every principal open the restriction is the affine normalization (Normalization of a classical variety by gluing affine normalizations, The normalization of an irreducible affine variety, Finite normalization commutes with principal localization).
In the irreducible case principal opens form a basis of the topology, their coordinate rings are the principal localizations, and all charts of share the function field , which is therefore also the function field of the open subvariety (Principal opens form a basis for the Zariski topology on an affine variety, Regular functions on a principal open are the principal localization, Compatible affine charts of an integral classical variety have one function field, Integral classical varieties in the compatible affine-atlas register).
Proof
First assume is irreducible. Cover by principal opens contained in affine charts of [F2]. Over each such principal open the normalization restricts to the affine normalization with ring map , which is finite, surjective and birational and has normal source, because these properties hold for the affine normalization and are preserved by principal localization [F1]. The pieces agree on overlaps as subrings of the common function field [F2], so is finite (finiteness is affine-local on the target), surjective (each piece is), and induces the identity on function fields, hence is birational; and is normal because normality is local and each is normal [F1].
In the irreducible case these affine restrictions are exactly the defining integral-closure charts of the normalization of , and their canonical overlap maps give over . For reducible , its normalization is the disjoint union of the component normalizations by [F1]; apply step 1.1 to each nonempty and omit components with empty intersection. These are the irreducible components of , so their disjoint union is its normalization. Finiteness, surjectivity and normality hold componentwise, and birationality is read on each component.
Depends on
- Normalization of a classical variety by gluing affine normalizations
- Finite normalization commutes with principal localization
- Regular functions on a principal open are the principal localization
- Principal opens form a basis for the Zariski topology on an affine variety
- Integral classical varieties in the compatible affine-atlas register
- Compatible affine charts of an integral classical variety have one function field
- The normalization of an irreducible affine variety
- The Axiom of Choice
Used by
Nothing in the library uses this result yet.
Dependency tree · two levels
52 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 §b: normalization is compatible with open restriction (standard reference, not scraped)
- Ravi Vakil, The Rising Sea: Foundations of Algebraic Geometry (November 18, 2017 public draft), §9.7 and §29.6 (standard reference, not scraped)