Alphabeta Math
LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generated
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.

A numerated real bundle embeds in a finite trivial bundle

Statement

Let X be compact Hausdorff and let E→X be a rank-r real vector bundle with a finite linear trivializing cover (Ui,τi) and a subordinate finite partition of unity (ρi). Then some N and a bundle F→X satisfy E⊕F≅X×RN. The embedding and orthogonal complement construction uses only the supplied finite numeration.

Facts & Assumptions

Given: A compact Hausdorff space X, a rank-r real vector bundle E→X, finitely many linear charts τi:E∣Ui→Ui×Rr, and a finite subordinate partition ρ1,…,ρs.

[F1]

Each bundle chart restricts on every fiber to a linear isomorphism Ex≅Rr (Real and complex topological vector bundles).

[F2]

Subordination means supp⁡(ρi)⊆Ui (Locally finite partitions of unity and subordination to an open cover).

Proof

technique · explicit weighted chart embedding
1.1givenF1F2construct

If X=∅, the conclusion is vacuous; assume X is nonempty. For each i define the ith component of Φ:E→X×Rrs over x by ρi(x)τi(v) when x∈Ui, and by zero when x∉Ui. The real square-root function is continuous on [0,∞) (away from zero, ∣a−b∣=∣a−b∣/(a+b); at zero, 0≤a<ε whenever 0≤a<ε2). Because supp⁡(ρi)⊆Ui, every point outside Ui has a neighborhood on which ρi=0; hence extending the chart component by zero is continuous there, and within Ui it is a product of continuous coordinate functions. Hence each component, and therefore Φ, is continuous. It is fiberwise linear.

2.1givenF1step 1.1algebra

If v∈Ex is nonzero, the partition identity gives some i with ρi(x)>0. Then x∈Ui and [F1] makes τi(v)≠0, so the ith component of Φx(v) is nonzero. Thus each Φx is injective and has rank r.

3.1step 2.1algebra

In local bundle coordinates, the matrix of Φ has rank r at every point. At any chosen x, some r×r minor is nonzero; continuity keeps that minor nonzero on a neighborhood. After reordering the target coordinates, the image there is the graph of a continuous matrix over Rr. Thus E′=Φ(E) is a rank-r subbundle of the trivial bundle.

4.1step 2.1step 3.1algebra∎

On a neighborhood with a continuous frame matrix Q for E′, the orthogonal projection onto E′ is P=Q(QTQ)−1QT. The Gram matrix QTQ is positive definite and invertible; its inverse varies continuously because each inverse entry is a cofactor divided by the nonzero determinant, so P is continuous. Therefore I−P has locally constant rank rs−r and its image is a subbundle F=E′⊥. Fiberwise orthogonal decomposition gives E′⊕F=X×Rrs, and Φ identifies E with E′. If r=0, take E′=0 and F=X×R0.

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