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.
The standard incidence locus is closed
Statement
The point--plane and plane-containment loci in the definition are closed in their constructed projective products.
Facts & Assumptions
Given: A basis of and Plucker coordinates for its subspaces.
Proof
A point belongs to an -plane with decomposable wedge exactly when . Expanding this wedge gives homogeneous bilinear equations in the point and Plucker coordinates.
These equations vanish precisely on by the annihilator characterization used for the Plucker map. The ambient product is closedly modeled by Segre and Plucker coordinates, so their common zero locus there is closed.
For the containment locus, cover both Grassmannians by their finitely many standard affine charts. On a product of two such charts, the planes and have canonical row-frame matrices. The condition is equivalent to the stacked matrix having rank at most , which is cut out by all of its minors. Thus the containment locus is closed on every member of this finite open cover. Closedness is local on an open cover, so it is closed globally. Together with steps 1.1--2.1 this proves both assertions without choosing global basis vectors of the varying plane .
Depends on
Used by
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
- MIT 18.725 Algebraic Geometry, Lecture 7, Lemma 16 (standard reference, not scraped)