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.

Normalization resolves the singularities of a projective curve

Statement

Assume the Axiom of Choice. Let C be an integral projective curve over a perfect field k. Then its normalization Cν is a nonsingular projective curve, and ν ⁣:Cν→C is a finite birational morphism. Consequently every integral projective curve over a perfect field admits a nonsingular projective model.

Facts & Assumptions

Given: AC, the perfect field k, the integral projective curve C over k, and its normalization ν ⁣:Cν→C.

[F1]

A finite-type domain over any field has finite integral closure in its fraction field, and that closure commutes with localization at a nonzero element (A finite-type domain over a field has finite normalization, Finite normalization commutes with principal localization).

[F2]

Compatible affine schemes glue along their open overlaps. Integral schemes have affine domains and a common function field; lying over gives surjectivity for integral extensions, and the dimension of a finite-type domain is the transcendence degree of its fraction field (Gluing affine schemes along compatible open isomorphisms, Integral schemes, Lying over for integral ring maps, Affine-domain dimension equals transcendence degree).

[F3]

A normal integral finite-type curve over a perfect field is nonsingular (A normal curve over a perfect field is nonsingular).

[F4]

A finite morphism over a projective finite-type k-scheme has projective source, for any field k (Finite morphisms over a projective variety over any field).

[F5]

The Axiom of Choice is assumed and is inherited by the normal-curve and projectivity suppliers (The Axiom of Choice).

Proof

1.1F1F2F5givenconstruct

Regard the projective curve C as an integral closed subscheme of Pkr. Its nonempty standard affine charts are Ci=Spec⁡Ai, where the Ai are finite-type domains with common function field K=k(C). Put Bi equal to the integral closure of Ai in K. By [F1], Bi is finite over Ai. On Ci∩Cj=D(xj/xi) these closures localize to the same subring of K. Thus their affine spectra glue by [F2] to a scheme Cν with a finite morphism ν:Cν→C. Each Bi is a finite algebra over the finite-type k-algebra Ai, hence finite type over k; the finite chart cover makes Cν a finite-type k-scheme. This is the normalization: its affine rings and their localizations are exactly the integral closures in K.

2.1F1F2F3F4step 1.1algebra

Each Bi is a normal domain with fraction field K. Lying over makes ν surjective. Clearing the denominators in K of a finite set of Ai-module generators of Bi gives a nonzero ai∈Ai with (Bi)ai=(Ai)ai, so ν is birational. Moreover dim⁡Bi=trdeg⁡kK=1 by [F2]; hence Cν is an integral normal curve. By [F4] it is projective, and by [F3] the perfectness of k makes it nonsingular.

3.1step 1.1step 2.1∎

The scheme Cν therefore supplies the required nonsingular projective model with its finite birational normalization map. The construction uses affine integral closure over the actual field k, so it applies to every perfect field, not only the algebraically closed classical case.

Depends on

Used by

Dependency tree · two levels

73 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