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

Normality is checked on affine open charts

Statement

Assume the Axiom of Choice. Let $X$ be a classical variety over an algebraically closed field $k$ , with a finite affine open cover $X = ⋃_{i} U_{i}$ and coordinate rings $A_{i}$ . Then $X$ is normal if and only if every $A_{i}$ is a normal Noetherian ring. If $U_{i}$ is irreducible, this says precisely that $A_{i}$ is an integrally closed domain. A point can be checked in any one affine chart containing it. Empty charts have the zero ring, which is normal vacuously.

Facts & Assumptions

Given: AC, $k$ , $X$ and its affine cover.

[F1]

Affine chart rings are finite-type $k$ -algebras and hence Noetherian (Every algebra of finite type over a Noetherian ring is a Noetherian ring). The local ring at a classical point $x \in U_{i}$ is $(A_{i})_{m_{x}}$ . This is The local ring at a point of an affine variety is the localization at its maximal ideal for irreducible charts; for a reduced affine algebraic set the same identification follows from Regular functions on a principal open are the principal localization: a germ is represented on a principal neighbourhood and hence by a localized fraction. The maximal ideals are exactly the point ideals (Points of an affine algebraic set correspond to maximal ideals of its coordinate ring).

[F2]

A classical variety is normal when its point local rings are integrally closed domains. A Noetherian ring is normal when all prime localizations are integrally closed domains, including the vacuous zero-ring case (Normal points and normal varieties, normal noetherian ring).

[F3]

Localizations of an integrally closed domain are integrally closed, and a domain is integrally closed if all its maximal localizations are (A domain is integrally closed if and only if its prime localisations are, equivalently if and only if its maximal localisations are). An irreducible affine chart has a domain as coordinate ring (A classical affine variety has a domain coordinate ring, and conversely).

Proof

1.1F1F2given

If every $A_{i}$ is normal, each maximal localization $(A_{i})_{m_{x}}$ is an integrally closed domain by [F2]. These are the local rings of $X$ by [F1], so $X$ is normal.

1.2F1F2F3givenchoose

Conversely suppose $X$ is normal. For a prime $p$ of $A_{i}$ , choose a maximal ideal $m$ containing it, using AC. By [F1] and [F2], $(A_{i})_{m}$ is an integrally closed domain. Its further localization at $p (A_{i})_{m}$ is $(A_{i})_{p}$ and is integrally closed by [F3]. Thus $A_{i}$ is normal. For an irreducible chart, [F3] identifies this with integral closedness of its coordinate domain.

2.1F1F2step 1.1step 1.2∎

For $x \in U_{i}$ , [F1] identifies its germ ring with $(A_{i})_{m_{x}}$ , so this one ring decides normality of $x$ independently of the chart. The empty variety and empty charts have no points or primes, and all conditions are vacuous. This proves the chartwise and pointwise assertions.

Depends on

Used by

Cited to discharge well-definedness by Normal points and normal varieties.

Dependency tree · two levels

53 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: Definition 8.1 and the preceding localisation reductions (cross-references 1.42, 1.49) (standard reference, not scraped)
Michael Artin, MIT 18.721 Algebraic Geometry notes (January 26, 2022), Ch. 4 §§4.2-4.3 (standard reference, not scraped)