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.
Schubert cells in real and complex Grassmannians
Definition
Fix the coordinate flag . A Schubert symbol for is a strictly increasing sequence with . Its Schubert cell is
Every has a unique pivot-normalized basis
after using earlier pivot rows to clear their columns. The free coordinates number
so . Its real dimension is for and for . Equivalently, the integers , read in reverse order, form a partition fitting the by rectangle. These spaces use the Grassmannian topology fixed in Stiefel spaces, Grassmannians, and tautological bundles. For , the unique symbol is the empty sequence, the displayed sum is the empty sum , and its Schubert cell is the one-point Grassmannian.
Depends on
Used by
- The Euler characteristic does not determine the signature Counterexample
- Chern character of a complex vector bundle Definition
- A point and projective-line check of source-first convolution and opposite composition Example
- Chern classes of a sum of universal complex lines Example
- Complex K-AHSS for complex projective space Example
- The complex projective plane has nonzero w2 and no Spin structure Example
- Unequal-dimensional proper pushforwards carry the summed-dimension Ext/Borel–Moore degree Example
- Cohomology ring of infinite complex projective space Lemma
- Finite type and odd-primary acyclicity of K(F₂,q) Lemma
- First Chern form agrees with the topological line class Lemma
- Integral cohomology ring of complex projective space Lemma
- Oriented real two-plane splitting with real-cohomology injection Lemma
- The complex tautological Euler class restricts to the projective-fiber generator Lemma
- Integral finite generation of universal real and oriented Thom homology Theorem
- Schubert cells give the stable Grassmannian CW structure Theorem
Dependency tree · two levels
4 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
- Hatcher, Vector Bundles & K-Theory, Proposition 1.17 (standard reference, not scraped)
- Milnor and Stasheff, Characteristic Classes, §6 (standard reference, not scraped)