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

Image dimension and the generic fibre formula

Statement

For an irreducible classical variety $X$ and morphism $f : X \to Y$ , the reduced closure $Z = \overline{f (X)}$ is irreducible and $\dim X = \dim Z + r$ , where $r$ is the common dimension of the nonempty fibres on a nonempty open of $Z$ . For arbitrary nonempty $X$ with components $X_{i}$ , $\dim X = \max_{i} (\dim \overline{f (X_{i})} + r_{i})$ , with a separately chosen generic open and relative dimension $r_{i}$ for each $X_{i}$ . For empty $X$ use the empty maximum $- \infty$ .

Work over a fixed algebraically closed field $k$ , with the Axiom of Choice. Classical varieties are separated and admit finite affine covers; they may be reducible or empty unless irreducibility is specified. Irreducible means nonempty. All fibres and points below are classical closed-point fibres and points.

Facts & Assumptions

Given: The objects and hypotheses in the statement.

[F1]

For a dominant morphism $f : X \to Y$ between irreducible classical varieties, there is a nonempty open $U \subseteq Y$ , contained in $f (X)$ , such that every $X_{y}$ with $y \in U$ is nonempty and has pure dimension $r = \dim X - \dim Y$ . Work over a fixed algebraically closed field $k$ , with the Axiom of Choice. Classical varieties are separated and admit finite affine covers; they may be reducible or empty unless irreducibility is specified. Irreducible means nonempty. All fibres and points below are classical closed-point fibres and points. (Fibres have pure expected dimension over a dense open).

[F2]

If a Noetherian space $T$ is a finite union of closed subsets $T_{1}, \dots, T_{m}$ , then $\dim T = \max_{i} \dim T_{i}$ . For $m = 0$ both sides are $- \infty$ . (Dimension of a finite closed union).

[F3]

Every classical variety is Noetherian and has finitely many irreducible components. Every open or closed subvariety has a finite affine cover. Work over a fixed algebraically closed field $k$ , with the Axiom of Choice. Classical varieties are separated and admit finite affine covers; they may be reducible or empty unless irreducibility is specified. Irreducible means nonempty. All fibres and points below are classical closed-point fibres and points. (Classical varieties have finite irreducible decompositions).

Proof

1.1

A continuous image of an irreducible space is irreducible: a finite closed cover of its image pulls back to a closed cover of the source. Its closure $Z$ is irreducible as well. The morphism factors through the reduced closed subvariety $Z$ , since all its defining functions vanish on the image. The induced $X \to Z$ is dominant, so the generic fibre theorem gives $r = \dim X - \dim Z$ on a nonempty image open. Fibres over points of $Z$ are unchanged.

2.1

In the reducible case apply that assertion to each of the finitely many nonempty irreducible components $X_{i}$ . The finite-closed-union dimension formula then gives the displayed maximum. This does not identify different $r_{i}$ or require a common generic open in different image closures. If $X$ is empty both its dimension and the empty maximum are $- \infty$ .

F2F3step 1.1∎

Depends on

Used by

Hypotheses and conventions in dimension theory Remark

Dependency tree · two levels

16 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 §9b opening and Theorem 9.9 (standard reference, not scraped)