LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedjudge pass (gpt-5.6-terra)audited 2026-09-07

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.

Dimension can be computed on an open cover

Statement

For every open cover $T = ⋃_{i \in I} U_{i}$ of a Noetherian space, $\dim T = \sup_{i} \dim U_{i}$ , with empty supremum $- \infty$ .

Facts & Assumptions

Given: The objects and hypotheses in the statement.

[F1]

For a Noetherian topological space $T$ , define $\dim T$ as the supremum of the lengths $s$ of strict chains $Z_{0} ⊊ \dots ⊊ Z_{s}$ of nonempty irreducible closed subsets of $T$ . Thus a one-member chain has length zero. Set $\dim \emptyset = - \infty$ , and allow $\dim T = + \infty$ . The supremum of an empty family of dimensions is $- \infty$ . (Chain dimension and the empty-space convention).

Proof

1.1F1

If $T$ is empty all terms have dimension $- \infty$ . Otherwise, for a chain of irreducible closed subsets $C_{0} ⊊ \dots ⊊ C_{s}$ in an open $U$ , their closures in $T$ are irreducible and closed, and $\overline{C_{j}} \cap U = C_{j}$ . Hence their closures remain strictly nested and $\dim U \leq \dim T$ .

2.1F1step 1.1∎

For a chain $Z_{0} ⊊ \dots ⊊ Z_{s}$ in $T$ , choose $x \in Z_{0}$ and a covering open $U_{i}$ containing $x$ . Each $Z_{j} \cap U_{i}$ is nonempty, irreducible and closed in $U_{i}$ . A nonempty open of an irreducible space is dense: two disjoint nonempty opens would give a cover by two proper closed subsets. Thus $\overline{Z_{j} \cap U_{i}} = Z_{j}$ . The intersections form a strict chain of the same length. Taking suprema proves the claim.

Depends on

Chain dimension and the empty-space convention

Used by

Affine and projective n-space have dimension n Corollary
The dimension of a complete linear system Corollary
The genus of a smooth plane curve in terms of its degree Corollary
A genus-zero curve need not be the projective line Counterexample
The Riemann inequality is not an equality for special divisors Counterexample
Under AC, proper integral finite-type schemes over fields with multiple points are not affine Counterexample
A smooth conic is a projective line once it has a rational point Example
Cuspidal cubic: delta invariant and normalization Example
Nodal cubic: arithmetic genus one, delta one, geometric genus zero Example
The twists on the projective line have degree n Example
Divisors on the projective line are classified by degree Lemma
Projective-line curve and divisor basics Lemma
Regular hyperplane step for coherent support induction Lemma
The Picard group of a point blowup of the projective plane Lemma
The product of two projective lines is an integral smooth projective surface Lemma
Degree of the coherent Hilbert polynomial Theorem
Dimension equals transcendence degree Theorem
Dimensions add under products Theorem
Euler characteristic is a Hilbert polynomial Theorem
Fibres have pure expected dimension over a dense open Theorem
Normalization of a reduced curve is finite Theorem
Regularization of a one-dimensional integral curve with finite normalization by point blowups Theorem

Dependency tree · two levels

3 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

Milne §3l chain interpretation; §5j p.115 (standard reference, not scraped)