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 is detected by avoiding linear subspaces

Statement

For a closed subset $Z \subseteq P_{k}^{N}$ and integer $0 \leq r \leq N$ , $\dim Z < r$ if and only if some projective linear subspace of dimension $N - r$ is disjoint from $Z$ .

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]

Let $X \subseteq P_{k}^{N}$ be irreducible of dimension $d \geq 1$ . If $f$ is homogeneous of positive degree and does not vanish identically on $X$ , then $X \cap V_{+} (f)$ is nonempty and every irreducible component has dimension $d - 1$ . 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. (Nontrivial projective hypersurface sections).

[F2]

Let $X, Y \subseteq P_{k}^{n}$ be irreducible closed subvarieties. Every nonempty irreducible component $Z$ of $X \cap Y$ satisfies $\dim Z \geq \dim X + \dim Y - n$ . If $\dim X + \dim Y \geq n$ , then $X \cap Y \neq \emptyset$ . 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. (Projective intersection dimension and nonemptiness).

[F3]

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

[F4]

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

Proof

1.1

For $r = 0$ , the inequality means $Z = \emptyset$ , and the only $N$ -plane is the whole $P^{N}$ , which is disjoint from $Z$ exactly in that case. For $r > 0$ and $Z = \emptyset$ , any coordinate $(N - r)$ -plane works.

1.2

Suppose $Z \neq \emptyset$ and $\dim Z < r$ . In any current linear ambient space, choose a hyperplane containing none of the finitely many irreducible components of its intersection with $Z$ . Such a hyperplane exists: the coefficient vectors of hyperplanes containing a fixed nonempty component form a proper vector subspace of the dual; finitely many such subspaces cannot cover the dual over infinite $k$ . Indeed enclose them in hyperplanes with nonzero linear equations; their product is a nonzero polynomial and cannot vanish on all of $k^{s}$ , as follows by induction on $s$ from the one-variable root bound.

2.1

Each positive-dimensional component drops dimension by one on cutting by the chosen hyperplane, and a zero-dimensional component is a point avoided by it. Repeat inside the successive linear spaces. After at most $\dim Z + 1 \leq r$ cuts the intersection is empty; continue taking arbitrary hyperplanes if necessary until precisely $r$ cuts have been made. Each cut is a hyperplane of the previous linear space, so the final linear space has dimension $N - r$ and avoids $Z$ .

F1F3step 1.2

3.1

Conversely suppose an $(N - r)$ -plane $L$ avoids $Z$ . If $\dim Z \geq r$ , some irreducible component $Z_{j}$ has dimension at least $r$ . Then $\dim Z_{j} + \dim L \geq N$ , so the projective intersection theorem forces $Z_{j} \cap L \neq \emptyset$ , a contradiction. Thus $\dim Z < r$ .

F2F3F4step 1.1∎

Depends on

Used by

Projective fibre dimension is upper semicontinuous Theorem

Dependency tree · two levels

12 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 6.48 and Lemma 6.49 (standard reference, not scraped)