Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-5.6-terra)audited 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.

Oriented real vector bundles are classified by BSO

Statement

Assume AC. For a paracompact Hausdorff CGWH base X and n≥0, pullback of γn+ gives a natural bijection

[X,Gr⁡n+(R∞)]=[X,BSO⁡(n)]≅Vect⁡nR,+(X),

where the right side consists of orientation-preserving isomorphism classes of numerable oriented rank-n real bundles. For n=0 both sets are singletons.

Facts & Assumptions

Given: AC, a paracompact Hausdorff CGWH space X, and n≥0.

[F1]

Under AC, numerable real rank-n bundles over X have countable Grassmannian embeddings and are classified by their stable Gauss maps (Real and complex vector bundles are classified by stable Grassmannians).

[F2]

With a metric, an orientation is equivalent to an SO⁡(n) reduction (Orientation is equivalent to an SO(n)-reduction).

[F3]

The oriented Grassmannian carries the tautological oriented bundle and is the chosen BSO⁡(n) model (Oriented Grassmannians and the tautological oriented bundle).

[A1]

AC has the meaning fixed in The Axiom of Choice.

Proof

technique · direct
1.1F1F3A1choose

Let (E,o) be a numerable oriented bundle. Use [F1] to choose a countable embedding j:E→X×R∞. Give the image plane j(Ex) the orientation transported by jx from ox. In oriented local frames this varies continuously, so it defines cj+:X→Gr⁡n+(R∞). The tautological pullback map e↦(p(e),j(e)) is orientation-preserving by construction. Thus every oriented bundle is in the image.

2.1F1F3step 1.1

If two maps to the oriented Grassmannian are homotopic, pull back γn+ over X×I and repeat the graph-transport proof used in [F1] with oriented charts. Every transition matrix has positive determinant, so the endpoint isomorphism is orientation-preserving. Hence pullback depends only on the homotopy class.

2.2F1F3step 1.1

Conversely, an orientation-preserving isomorphism between two pullbacks identifies them as one oriented bundle. Move their embeddings to odd and even coordinates and interpolate as in the injectivity proof of [F1], transporting the fixed domain orientation to every intermediate image plane. This is a homotopy through oriented Grassmannian maps, so the pullback assignment is injective.

3.1F1F2F3A1step 2.1step 2.2∎

Pullback of the transported image orientation commutes with base change, proving naturality. By [F2], the same classification can be read as classification of the corresponding SO⁡(n) reductions, which agrees with the notation in [F3]. When n=0, the oriented Grassmannian, structure group, and bundle fiber are points, so both sets are singletons. AC is inherited exactly from [F1]'s numeration and countabilization.

Depends on

Used by

Dependency tree · two levels

14 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