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.
Oriented clutching classifies oriented bundles over spheres
Statement
For and , orientation-preserving isomorphism classes of oriented rank- real bundles over are classified by
Reversing the chosen fiber orientation acts on a clutching map by conjugation with an orientation-reversing matrix.
Facts & Assumptions
Given: , , and an oriented rank- bundle over .
Unoriented clutching is controlled by hemisphere trivializations, homotopies, and disk-extending gauge maps (Clutching classifies vector bundles over spheres in the stable range).
Positive frames and orientation-preserving maps have transition matrices in (Oriented real bundles and oriented frame bundles).
With a metric, positive orthonormal frames are the corresponding reduction (Orientation is equivalent to an SO(n)-reduction).
Proof
Each hemisphere disk is connected and the restriction of the oriented bundle is trivial by the finite argument in [F1]. If a chosen trivialization reverses orientation, compose it with one fixed reflection; hence both hemisphere trivializations may be chosen orientation-preserving. Their equatorial transition then lies in by [F2].
Repeat the equivalence calculation of [F1] using only orientation-preserving hemisphere gauges. Such gauges take values in , which is path connected, and their disk restrictions are nullhomotopic. Thus two positive clutching maps give orientation-preservingly isomorphic bundles exactly when they are homotopic, proving the first classification. This includes : every map from to the path-connected group has the single unbased homotopy class.
Polar normalization preserves determinant sign and deformation retracts onto . Equivalently, it orthonormalizes the positive frames in [F3]. It therefore induces the second displayed bijection on homotopy classes.
Fix a reflection . After reversing the chosen orientation of every fiber, the old oriented hemisphere trivializations become orientation-reversing; postcomposing both with makes them oriented again. If their old transition was , the new one is . A different reflection differs from by positive matrices and gives the same action on the classified homotopy classes. The argument is finite and uses no choice principle.
Depends on
Used by
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
- Hatcher, Vector Bundles & K-Theory, Proposition 1.14 (standard reference, not scraped)