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.
Global and local dimension of classical varieties
Definition
For a classical variety , let be its chain dimension. If are its irreducible components and is a closed point, define . The indexing family is nonempty. Say that has pure dimension if every irreducible component has dimension ; the condition on components is vacuous for the empty variety, whose dimension is nevertheless .
Work over a fixed algebraically closed field , 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.
Depends on
Used by
- General hypersurfaces give smooth complete intersections Corollary
- Minimal tangent dimension and homogeneous regularity Corollary
- The semistable locus depends on the linearization, not only on the sheaf Counterexample
- Codimension of an irreducible closed subvariety Definition
- Reduced closed-point fibres and their dimension Definition
- Semistable and stable points for a linearization Definition
- Stable points of an affine action Definition
- A nondegenerate projective quadric Example
- The coordinate cross has two one-dimensional components Example
- A dominant map has a surjective differential on a dense source open Lemma
- A tangent direction is realized by a local smooth curve Lemma
- A transverse hyperplane slice is smooth at the chosen point Lemma
- Algebraic open inclusions surject on fundamental groups Lemma
- Complex affine algebraic groups are smooth Lemma
- Critical loci have small images in characteristic zero Lemma
- Fibre dimension and orbit dimension add to the dimension of the group Lemma
- Nonempty opens preserve irreducible dimension Lemma
- Orbit dimension and closed orbits for complex group actions Lemma
- Semicontinuity of stabilizer and orbit dimension Lemma
- The submersion criterion between smooth varieties Lemma
- Zero-dimensional varieties are finite sets Lemma
- A normal curve over a perfect field is nonsingular Theorem
- A normal variety is regular in codimension one Theorem
- Generic smoothness over a dense target open Theorem
- Jacobian rank detects regularity at closed points Theorem
- Projective GIT quotient for a linear action Theorem
Dependency tree · two levels
8 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 §5j p.115 and §3c Note 3.13 p.63; local-dimension convention prescribed by AV-5 design (standard reference, not scraped)