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

Normalization commutes with restriction to an open subvariety

Statement

Assume the Axiom of Choice. Let X be a classical variety with normalization ν ⁣:Xν→X and let U⊆X be a nonempty open subvariety. Then ν−1(U) is a normalization of U: it is normal, and ν−1(U)→U is finite, surjective and birational, so it is isomorphic to Uν over U.

Facts & Assumptions

Given: AC, the algebraically closed field k, the classical variety X with normalization ν, the nonempty open U⊆X, and an affine chart V of X on an irreducible component, with coordinate ring A=k[V] and normalization B in that component’s function field. The irreducible argument below is then applied componentwise.

[F1]

In the irreducible case the normalization restricts over the affine chart V to the affine normalization A⊆B, with B the integral closure of A in k(X) and a finite A-module; over every principal open D(f)⊆V the restriction is the affine normalization (Af,Bf) (Normalization of a classical variety by gluing affine normalizations, The normalization of an irreducible affine variety, Finite normalization commutes with principal localization).

[F2]

In the irreducible case principal opens form a basis of the topology, their coordinate rings are the principal localizations, and all charts of X share the function field k(X), which is therefore also the function field of the open subvariety U (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

1.1F1F2given

First assume X is irreducible. Cover U by principal opens D(f) contained in affine charts V of X [F2]. Over each such principal open the normalization restricts to the affine normalization with ring map Af↪Bf, 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 k(X) [F2], so ν−1(U)→U is finite (finiteness is affine-local on the target), surjective (each piece is), and induces the identity on function fields, hence is birational; and ν−1(U) is normal because normality is local and each ν−1(D(f)) is normal [F1].

2.1F1F2step 1.1∎

In the irreducible case these affine restrictions are exactly the defining integral-closure charts of the normalization of U, and their canonical overlap maps give ν−1(U)≅Uν over U. For reducible X, its normalization is the disjoint union of the component normalizations by [F1]; apply step 1.1 to each nonempty U∩Xi and omit components with empty intersection. These are the irreducible components of U, so their disjoint union is its normalization. Finiteness, surjectivity and normality hold componentwise, and birationality is read on each component.

Depends on

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