Alphabeta Math
DefinitionDefinition: Literature-sourcedProof: Not applicablePipeline-generatedaudited 2026-09-22
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 flag bundle and Stiefel–Whitney roots

Definition

Assume AC, and let EB be a numerable real vector bundle of rank n1 over a paracompact Hausdorff CGWH base of CW homotopy type. The real flag bundle of E is obtained by the following finite iteration.

At the first stage put X1:=P(E), let q1:X1B be the projection, let E1:=q1E, and let L1E1 be the tautological line. By Numerable vector bundles admit bundle metrics choose a bundle metric on the numerable bundle E1, and let L1E1 be the orthogonal complement of L1. Then L1L1E1 as bundles over X1, in the convention of Whitney sum, tensor, dual, Hom, and exterior-power bundles.

Suppose Xj, bundles L1,,Lj over Xj and a rank-(nj) bundle Lj over Xj with qjEL1LjLj have been constructed. If j<n, put Xj+1:=P(Lj),πj+1:Xj+1Xj,Lj+1:=γLj,qj+1:=qjπj+1, choose a metric on the numerable bundle πj+1Lj and let Lj+1 be the orthogonal complement of Lj+1 in it. Iterating until j=n gives the real flag bundle Fl(E):=Xn,q:=qn:Fl(E)B, together with line bundles L1,,Ln over Fl(E), which we keep denoting by the same symbols after pulling back along the remaining projections.

By construction, and by the pullback compatibilities of Vector-bundle pullback is canonically functorial, qEL1Lnover Fl(E). The Stiefel–Whitney roots of E are the classes tj:=w1(Lj)=xLjH1(Fl(E);F2),1jn, computed with the rank-one case of Stiefel–Whitney classes from the projective-bundle relation. For n=0 we set Fl(E):=B, q:=idB, and the sum L1Ln is empty, so no root is defined. For n=1 the construction stops at the first stage, so Fl(E)=P(E)B, L1E and t1=w1(E).

Facts & Assumptions

Given: AC, a numerable real rank-n bundle EB with n0 over a paracompact Hausdorff CGWH base of CW homotopy type, and the iteration above.

[F1]

For a numerable real bundle G of rank r1, the projective bundle P(G) base is a numerable fiber bundle with fiber RPr1 carrying the tautological line γGπG; for r=1 the projection is a homeomorphism and γGG (Real projective bundle and tautological line).

[F2]

Under AC every numerable real or complex vector bundle admits a continuous positive-definite fiber metric (Numerable vector bundles admit bundle metrics).

[F3]

In a local frame of a topological vector bundle in which a line subbundle is spanned by the first vector, fiberwise Gram--Schmidt with a continuous bundle metric produces a continuous orthonormal frame. Hence the remaining frame vectors locally trivialize the orthogonal complement, and the addition map gives a bundle isomorphism LLG. Whitney sums have the block-diagonal transition convention of Whitney sum, tensor, dual, Hom, and exterior-power bundles, and the relevant local-frame convention is that of Real and complex topological vector bundles.

[F4]

Under AC every vector bundle over a paracompact Hausdorff base is numerable: apply the subordinate-partition theorem to a linear chart cover (Under choice and dependent choice, every open cover of a paracompact Hausdorff space admits a locally finite subordinate partition of unity, Real and complex topological vector bundles).

[F5]

Pullback is canonically functorial, so the successive pullbacks compose and π of a direct sum is the direct sum of the pullbacks (Vector-bundle pullback is canonically functorial).

[F6]

The total space of a numerable compact-Hausdorff-fiber bundle over a paracompact Hausdorff CGWH base is again paracompact Hausdorff and CGWH; its total space also has CW homotopy type when both the base and the fiber do. Every fiber used here is RPr1 for some r1, hence is a compact Hausdorff finite CW complex. Therefore every intermediate Xj and Fl(E) has all four properties (Compact-fibre bundle totals preserve paracompactness, and CW type under CW-type hypotheses).

[F7]

For a rank-one bundle L the class w1(L)=xL is defined and lies in H1 of the base (Stiefel–Whitney classes from the projective-bundle relation).

[A1]

AC is the Axiom of Choice in the form fixed by The Axiom of Choice.

Verification

1.1

The first stage splits. By [F1] the tautological line L1=γE is a subbundle of E1=q1E, and E1 is numerable. Choose a metric by [F2]. On a local frame (s1,,sn) with s1 spanning L1, the Gram--Schmidt formulas divide only by the positive continuous norms of the successive nonzero orthogonalized vectors, so they produce a continuous orthonormal frame (e1,,en) with e1 spanning L1. Thus e2,,en locally frame the fiberwise orthogonal complement L1, and fiberwise addition gives E1L1L1 as in [F3]. The complement is numerable by [F4], since X1=P(E) is paracompact Hausdorff by [F6].

F1F2F3F4F6A1
2.1

The iteration is legitimate and terminates. Suppose the data of stage j are constructed with qjEL1LjLj and Lj numerable of rank nj. If j<n then Lj has positive rank, so [F1] gives the numerable projective bundle πj+1:Xj+1=P(Lj)Xj with tautological line Lj+1=γLjπj+1Lj. Choosing a metric on πj+1Lj and repeating the local Gram--Schmidt construction of step 1.1 splits πj+1LjLj+1Lj+1 with Lj+1 numerable by [F4] and of rank nj1; by [F5] the pulled-back splitting of qjE combines with this one, giving qj+1EL1LjLj+1Lj+1. At j=n no positive-rank complement remains and the iteration stops. Each Xj is paracompact Hausdorff, CGWH, and of CW type by [F6], applied to the numerable compact-fiber bundle πj.

F1F2F3F4F5F6step 1.1A1
3.1

The conclusion and the degenerate cases. Substituting the terminal identity of step 2.1 gives qEL1Ln over the paracompact Hausdorff CGWH CW-type space Fl(E). Each Lj is a line bundle, so its first Stiefel–Whitney class tj=w1(Lj)=xLj is defined by [F7] and lies in H1(Fl(E);F2); this is the content of [def-stiefel-whitney-classes-from-the-projective-bundle-relation]'s rank-one case. For n=0 the convention gives Fl(E)=B and the empty sum, and for n=1 the iteration stops after step 1.1, where X1=P(E)B and γEE, so t1=w1(E).

F1F7step 2.1
4.1

The fiber of the construction. Over a base point b, the successive projectivizations parametrize a chain of subspaces 0L1L1L2Eb with dim(L1Lj)=j, since each stage consists of the lines in the orthogonal complement of the previous sum. Sending such a chain to the flag Vj=L1Lj is a bijection onto the complete flags in Eb, with inverse obtained by taking successive orthogonal complements; the identification is compatible with the chosen metrics but its underlying set of chains does not depend on them. Hence the fiber of Fl(E)B is the complete flag manifold of Rn, a compact manifold, in agreement with the compactness invoked in [F6].

F1F3step 2.1step 3.1

Depends on

Used by

Dependency tree · two levels

27 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