Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passaudited 2026-09-14
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 X and n≥0, pullback gives natural bijections

[X,Gr⁡n(R∞)]≅Vect⁡nR(X),[X,Gr⁡n(C∞)]≅Vect⁡nC(X),

where the right sides are isomorphism classes of numerable rank-n bundles. These Grassmannians are denoted BO⁡(n) and BU⁡(n) in this model. The assertion also holds for any CGWH X when numerability is supplied explicitly. Nonnumerable bundles are not classified by this statement.

Facts & Assumptions

Given: AC, a CGWH space X, n≥0, and F∈{R,C}.

[F1]

Under AC every numerable rank-n bundle has a countable F∞ embedding whose image-plane map pulls the tautological bundle back to the original bundle (A bundle embedding produces its Grassmannian classifying map).

[F2]

Under AC, homotopic Grassmannian maps have isomorphic pullbacks, and isomorphic pullbacks have homotopic classifying maps (Homotopic Grassmannian maps classify isomorphic bundles and conversely).

[F3]

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).

[F4]

Under AC, numerable principal bundles over CGWH bases are classified by the Milnor BG model; its proof includes arbitrary-numeration countabilization (Numerable principal bundles are classified by maps to BG).

[F5]

The stable Stiefel total space is contractible (Stable Stiefel space is contractible).

[F6]

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.

[F7]

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).

Proof

technique · direct
1.1F3F6F7A1

By [F6], the stable Grassmannian is paracompact. Apply [A1] and [F7] to the linear graph-chart cover of γn; this supplies a numeration of the tautological bundle, and every pullback of that numeration is again a numeration. Thus Φ([f])=[f∗γn] always lands in numerable bundles.

2.1F2F3F4step 1.1

If f0≃f1 and X is paracompact, [F2] makes the two pullbacks isomorphic. For arbitrary CGWH X, pull back the numerable principal Stiefel bundle along the homotopy. The equivariant endpoint-transport argument in [F4] applies to this numerable principal O⁡(n)- or U⁡(n)-bundle and is a principal-bundle isomorphism; [F3] makes the associated vector bundles isomorphic. Hence Φ is well-defined in both stated branches.

3.1F1F7A1step 2.1choose

Let E→X be numerable. By [F1] it has an embedding j:E→X×F∞, and its image-plane map cj satisfies cj∗γn≅E. 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.

4.1F2step 3.1

If Φ([f0])=Φ([f1]), 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 f0≃f1, so Φ is injective. Together with step 3.1 this proves both displayed bijections.

5.1F4F5step 1.1step 4.1

For a:X′→X, the canonical pullback comparison identifies a∗(f∗γn) with (fa)∗γn, so the bijections are natural. The numerable principal O⁡(n)- or U⁡(n)-bundle Vn(F∞)→Gr⁡n(F∞) has contractible total space by [F5], so its quotient is the concrete BO⁡(n) or BU⁡(n) model. The published theorem [F4] has the same numerability boundary and likewise excludes nonnumerable bundles.

6.1F1F2F4F7A1step 3.1step 4.1step 5.1∎

When n=0, the Grassmannian is a point and the only rank-zero bundle is X→X, so both sides are singletons. When X=∅, 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

Dependency tree · 2 levels

Sources