ExampleConstruction: Literature-sourcedVerification: AI-adaptedPipeline-generatedaudited 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.

Fibre dimensions of a family of homogeneous linear systems

Example

Let $A (y)$ be an $m \times n$ matrix of regular functions on a classical variety $Y$ , with $m, n \geq 0$ , and $W = {(y, x) \in Y \times A^{n} : A (y) x = 0}$ . Then $\dim W_{y} = n - rank A (y)$ . For every integer $r$ , the locus ${y : \dim W_{y} \geq r}$ is closed: it is all of $Y$ for $r \leq 0$ , empty for $r > n$ , and otherwise is cut out by the minors of size $n - r + 1$ , with an absent family of minors imposing no conditions. No irreducibility or global dimension formula for $W$ is asserted.

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 morphism $f : X \to Y$ of classical varieties and a closed point $y \in Y$ , let $X_{y} = f^{- 1} (y)$ have its reduced closed-subvariety structure. Its dimension is the chain dimension, with $\dim X_{y} = - \infty$ if the fibre is empty. On affine charts $V \subseteq Y$ containing $y$ and $U \subseteq f^{- 1} (V)$ , writing $A = k [V]$ and $B = k [U]$ , the fibre chart has coordinate ring $B / \sqrt{m_{y} B}$ . Here general morphisms have the locally ringed-space meaning; the earlier affine morphism definition applies to the restrictions $U \to V$ . 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. (Reduced closed-point fibres and their dimension).

[F2]

For every integer $n \geq 0$ , $\dim A_{k}^{n} = \dim P_{k}^{n} = n$ . 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. (Affine and projective n-space have dimension n).

[F3]

Products of nonempty classical varieties exist in the category of classical varieties, and $\dim (X \times_{k} Y) = \dim X + \dim Y$ . If both factors are irreducible, their product is irreducible. 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. (Dimensions add under products).

Verification

1.1

The product exists, and on its affine base charts the entries of $A (y) x$ are regular polynomial expressions. Their common zeros give a reduced closed subvariety $W$ . Fix $y$ . Elementary row and column changes over $k$ reduce $A (y)$ to a block matrix with an identity block of size $q = rank A (y)$ and zeros elsewhere. The inverse linear coordinate changes identify its kernel, as an affine algebraic set, with $A^{n - q}$ . Thus the fibre has dimension $n - q$ and always contains zero.

F1F2F3

2.1

For $1 \leq s \leq \min (m, n)$ , rank is at least $s$ exactly when some $s \times s$ minor is nonzero. One implication follows from the independence of its columns. For the other, choose $s$ independent columns; the resulting injective map $k^{s} \to k^{m}$ has $s$ independent coordinate row functionals, giving such a minor. Therefore rank at most $s - 1$ is equivalent to vanishing of all size- $s$ minors. For $1 \leq r \leq n$ , take $s = n - r + 1$ : these minors are regular functions, hence define a closed locus. If $s > m$ all such minors are absent and the rank bound holds automatically.

step 1.1

3.1

Every fibre is nonempty and has dimension between zero and $n$ , so $r \leq 0$ gives all of $Y$ and $r > n$ gives the empty locus. If $n = 0$ , every fibre is a point; if $m = 0$ , there are no equations and every fibre is $A^{n}$ . The zero matrix gives that latter fibre too. These verify all boundary conventions without assuming the total space is irreducible.

F2step 1.1step 2.1∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

13 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 Example 9.10, pp.201–202 (standard reference, not scraped)