TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-generated

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.

A normal variety is regular in codimension one

Statement

Assume the Axiom of Choice. Let $X$ be a normal classical variety over an algebraically closed field. For every affine chart $U$ with coordinate ring $A$ and every height-one prime $p \subset A$ , the ring $A_{p}$ is a discrete valuation ring and hence regular. This is regularity in codimension one; it allows reducible and empty varieties. In particular, a classical point $x$ whose local ring has dimension one has a discrete valuation ring as its local ring and is regular. No characteristic hypothesis is needed.

Facts & Assumptions

Given: AC, $X$ , an affine chart $U$ , and a height-one prime $p$ of $A = k [U]$ .

[F1]

Normality of $X$ makes $A$ a normal Noetherian ring, without requiring it to be a domain. Thus $A_{p}$ is an integrally closed domain (Normality is checked on affine open charts, normal noetherian ring, Normal points and normal varieties).

[F2]

The dimension of $A_{p}$ is the height of $p$ : prime chains in this localization are exactly prime chains in $A$ below $p$ . A one-dimensional Noetherian local integrally closed domain is a DVR, and a one-dimensional Noetherian local ring is regular if it is a DVR (Krull dimension of a nonzero ring, Equivalent characterizations of a DVR, one dimensional regular local rings are dvrs).

[F3]

At a classical point $x$ , its local ring is the maximal localization on a chart. On a reducible chart this follows by taking germs of principal-open localized sections, as explained in Normality is checked on affine open charts; the irreducible case is The local ring at a point of an affine variety is the localization at its maximal ideal.

Proof

1.1F1F2given

By [F1], $A_{p}$ is a Noetherian local integrally closed domain. Its dimension is $ht p = 1$ by [F2], so it is not a field. The DVR characterization in [F2] therefore makes it a discrete valuation ring, and the regularity characterization makes it regular.

2.1F1F2F3step 1.1∎

If a classical point $x$ has a one-dimensional local ring, normality makes that ring a Noetherian local integrally closed domain, so the same argument applies. Equivalently its maximal ideal on an affine chart has height one by [F2] and [F3]. All height-one prime localizations on all charts satisfy step 1.1, which is the asserted codimension-one conclusion. Empty charts have no such primes. No assumption on the characteristic or on irreducibility was used.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

50 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: normality and the height-one localisations of a normal Noetherian domain (standard reference, not scraped)