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.
All complex vector bundles over the circle are trivial
Example
Every finite-rank complex vector bundle over is trivial, including the rank-zero bundle. This contrasts with the nontrivial Möbius real line bundle.
Facts & Assumptions
Given: a rank- complex vector bundle , where .
Clutching over represents by a map , and homotopic clutching maps give isomorphic bundles (Clutching classifies vector bundles over spheres in the stable range).
Verification
Suppose first that . Every has polar form with unitary and positive definite. The path joins to through invertible matrices. By the finite-dimensional spectral theorem, for real angles , and joins to . Hence is path connected.
The two values of can therefore be joined independently to , producing a homotopy from to the constant identity map. By [F1], is isomorphic to the identity-clutched bundle, which is .
If , then is a point and the same conclusion is forced. The real argument fails at step 1.1 because has two components; the clutching values in different components give the Möbius line. No choice principle is used.
Depends on
Used by
Nothing in the library uses this result yet.
Dependency tree · two levels
3 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.11 discussion (standard reference, not scraped)