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.
Real and complex vector bundles are classified by stable Grassmannians
Statement
Assume AC. For every paracompact Hausdorff CGWH space and , pullback gives natural bijections
where the right sides are isomorphism classes of numerable rank- bundles. These Grassmannians are denoted and in this model. The assertion also holds for any CGWH when numerability is supplied explicitly. Nonnumerable bundles are not classified by this statement.
Facts & Assumptions
Given: AC, a CGWH space , , and .
Under AC every numerable rank- bundle has a countable embedding whose image-plane map pulls the tautological bundle back to the original bundle (A bundle embedding produces its Grassmannian classifying map).
Under AC, homotopic Grassmannian maps have isomorphic pullbacks, and isomorphic pullbacks have homotopic classifying maps (Homotopic Grassmannian maps classify isomorphic bundles and conversely).
Vector bundles and their frame bundles determine one another by the associated standard representation, compatibly with pullback and numerations (Frame bundles and associated vector bundles).
Under AC, numerable principal bundles over CGWH bases are classified by the Milnor model; its proof includes arbitrary-numeration countabilization (Numerable principal bundles are classified by maps to BG).
The stable Stiefel total space is contractible (Stable Stiefel space is contractible).
Hatcher, Appendix Proposition 1.19, proves that a weak direct limit of an increasing sequence of compact Hausdorff spaces is paracompact. Each finite real or complex Grassmannian is compact Hausdorff, so the stable Grassmannian is paracompact.
Under AC and DC a paracompact Hausdorff chart cover has a subordinate locally finite partition (Under choice and dependent choice, every open cover of a paracompact Hausdorff space admits a locally finite subordinate partition of unity).
AC has the meaning fixed in The Axiom of Choice and implies DC (AC supplies the dependent-choice instances used in vector-bundle constructions).
Proof
By [F6], the stable Grassmannian is paracompact. Apply [A1] and [F7] to the linear graph-chart cover of ; this supplies a numeration of the tautological bundle, and every pullback of that numeration is again a numeration. Thus always lands in numerable bundles.
If and is paracompact, [F2] makes the two pullbacks isomorphic. For arbitrary CGWH , pull back the numerable principal Stiefel bundle along the homotopy. The equivariant endpoint-transport argument in [F4] applies to this numerable principal - or -bundle and is a principal-bundle isomorphism; [F3] makes the associated vector bundles isomorphic. Hence is well-defined in both stated branches.
Let be numerable. By [F1] it has an embedding , and its image-plane map satisfies . Thus is surjective. The paracompact branch obtains a numeration from [F7], while the explicitly numerable branch starts with that data; [F1] uses AC to countabilize it.
If , identify the two pullbacks. The reverse construction in [F2] moves the two tautological embeddings to odd and even coordinates and interpolates their image planes through fiberwise injections; that construction uses no paracompactness. It yields , so is injective. Together with step 3.1 this proves both displayed bijections.
For , the canonical pullback comparison identifies with , so the bijections are natural. The numerable principal - or -bundle has contractible total space by [F5], so its quotient is the concrete or model. The published theorem [F4] has the same numerability boundary and likewise excludes nonnumerable bundles.
When , the Grassmannian is a point and the only rank-zero bundle is , so both sides are singletons. When , there is one map and one empty bundle in every rank. AC is used in steps 1.1–3.1 for partitions, endpoint transport, and countabilization; no claim is made for a locally trivial bundle lacking a numeration.
Depends on
A bundle embedding produces its Grassmannian classifying map
Homotopic Grassmannian maps classify isomorphic bundles and conversely
Frame bundles and associated vector bundles
Stable Stiefel space is contractible
Numerable principal bundles are classified by maps to BG
Under choice and dependent choice, every open cover of a paracompact Hausdorff space admits a locally finite subordinate partition of unity
AC supplies the dependent-choice instances used in vector-bundle constructions
The Axiom of Choice