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.

Closed families with irreducible equal-dimensional fibres

Statement

Let $f : X \to Y$ be a closed surjective morphism of classical varieties with $Y$ irreducible. If every fibre is irreducible of one fixed dimension $r$ , then $X$ is irreducible and $\dim X = \dim Y + r$ .

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]

For a dominant morphism $f : X \to Y$ between irreducible classical varieties and every closed point $y \in Y$ , each nonempty irreducible component $Z$ of $X_{y}$ satisfies $\dim Z \geq \dim X - \dim Y$ . No bound is asserted for an empty fibre. 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. (Every fibre component has the expected lower bound).

[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).

[F4]

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).

Proof

1.1

Write $X = ⋃_{i} X_{i}$ as its finite irreducible-component cover. Since $f$ is closed, each image $f (X_{i})$ is closed. Those which do not equal $Y$ are proper closed subsets. At least one component has image $Y$ , since their finite union is the irreducible space $Y$ . Remove all the proper component images to obtain a nonempty open $V$ .

2.1

For each component mapping onto $Y$ , the generic fibre theorem gives a nonempty open on which its fibre dimension is $d_{i} = \dim X_{i} - \dim Y$ . Each such fibre is a closed subset of the full fibre, so $d_{i} \leq r$ . Intersect these finitely many generic opens with $V$ and choose a point there. The full fibre is a finite union of the component fibres, so its dimension $r$ equals the maximum of the corresponding $d_{i}$ . Thus some surjective component $X_{j}$ has $\dim X_{j} = \dim Y + r$ .

F1F4step 1.1

3.1

For every $y \in Y$ , surjectivity of $X_{j} \to Y$ makes $(X_{j})_{y}$ nonempty. The lower-bound theorem gives every component of it dimension at least $r$ . Since the full fibre $X_{y}$ is irreducible of dimension $r$ , no proper closed subset can have dimension at least $r$ : any chain in a proper closed subset extends by $X_{y}$ , so has length at most $r - 1$ . Therefore $(X_{j})_{y} = X_{y}$ for all $y$ . Every point of $X$ lies in $X_{j}$ , proving $X = X_{j}$ and the asserted dimension. The reasoning applies when $r = 0$ as well.

F2step 2.1∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

19 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 Proposition 9.11 (standard reference, not scraped)