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.
Thom isomorphism for the tautological complex line over CP infinity
Example
Assume AC. Let be the tautological complex line. Its underlying real rank-two bundle has the complex orientation, is numerable, and has a unique normalized class
For every integer , multiplication by this class gives an isomorphism
Facts & Assumptions
Given: AC, the standard weak-CW model of , and its tautological complex line .
Stiefel spaces, Grassmannians, and tautological bundles defines as the space of complex lines and its tautological bundle as the pairs with .
Milnor's join model is a contractible free G-space identifies the selected with this standard weak CW colimit and makes its unit-vector principal -bundle numerable.
R-oriented vector bundle and orientation local system defines an integral orientation as a compatible family of generators of the real fiber disk-pair groups.
Thom isomorphism for oriented vector bundles gives the unique normalized class and degree- cup-product isomorphism for an oriented numerable real rank- bundle over a CW complex under AC.
The Axiom of Choice is assumed exactly to invoke [F4].
Verification
By definition, is the weak colimit of complex lines in , so [F1] identifies it with and with the pairs , . Its unit vectors therefore form the standard principal -bundle. A principal chart with local unit section gives the linear chart of ; hence the support-subordinate numeration in [F2] is also a numeration of . The base is the stated weak CW complex.
A nonzero vector in a complex fiber orders its underlying real plane by . Replacing by for changes this ordered basis by the real matrix of multiplication by , whose determinant is . Thus all complex-linear transition functions preserve the corresponding generator in [F3], and these generators define the complex orientation of the underlying real rank-two bundle.
Apply [F4] with , , the numeration from step 1.1, and the orientation from step 1.2. It gives the unique normalized and exactly the displayed isomorphism for every ; no Euler or characteristic-class identification is used.
The base is nonempty and the coefficients are the nonzero ring , so empty-base and zero-ring cases are outside this example. The single complex line, its zero vector and a coordinate-line point are included in steps 1.1–1.2. At the input-degree endpoint , the unit maps to ; negative-degree and zero inputs map between zero groups or to zero as covered by [F4]. AC is used only through [A1] in [F4]; the explicit orientation and the supplied numeration require no additional choice.
Depends on
Used by
Nothing in the library uses this result yet.
Dependency tree · two levels
20 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 and K-Theory, canonical line bundle and Thom discussion (standard reference, not scraped)