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

Complex splitting principle with integral injective pullback

Statement

Assume AC. Let EB be a numerable complex rank-n bundle with n1 over a path-connected paracompact Hausdorff CW complex, and let q:Fl(E)B be its flag bundle, constructed from a Hermitian metric as in Complex flag bundle and Chern roots. Then qE=L1L2Ln with the tautological complex lines Li, and the pullback q:H(B;R)H(Fl(E);R) is injective for R=Z and for every field Fp.

Moreover, for finitely many numerable complex bundles E(1),,E(m) over B there is a single CW-type base FB over which every qE(j) splits as a sum of complex lines and for which the pullback H(B;R)H(F;R) is injective for R=Z and every Fp.

Facts & Assumptions

[A1]

The Axiom of Choice is assumed, exactly as inherited from the numerable-bundle and projective-bundle suppliers (The Axiom of Choice).

[F1]

The flag bundle is built as an iterated projective bundle with tautological lines Li and qE=L1Ln; its intermediate bases are compact-fiber numerable bundles over CW-type bases (Complex flag bundle and Chern roots).

[F2]

For a numerable complex bundle of rank m over a paracompact Hausdorff CGWH base of CW type the projective bundle P(E) has H(P(E);R) free over H(B;R) on 1,x,,xm1, and the same theorem covers the iterated CW-type bases (Integral complex projective bundle theorem).

[F3]

Totals of numerable bundles with compact Hausdorff fiber over paracompact Hausdorff bases are paracompact Hausdorff; over CGWH bases the totals are CGWH, and under CW-type hypotheses they retain CW type (Compact-fibre bundle totals preserve paracompactness, and CW type under CW-type hypotheses).

[F4]

The projective bundle of a numerable complex bundle is a fiber bundle with compact fiber CPm1 over a CW base by Complex projective bundle and tautological complex line, and over a paracompact Hausdorff CGWH base of CW type by the explicit extension in Integral complex projective bundle theorem.

Proof

technique · direct

Given: AC, a numerable complex rank-n bundle EB with n1 over a path-connected paracompact Hausdorff CW complex, a Hermitian metric on E, and a coefficient ring R equal to Z or a field Fp.

1.1

Splitting. By [F1] the flag bundle is the iterated projective-bundle tower of E and its metric complements, and the tautological lines satisfy qE=L1Ln. At each stage [F3] applies to the compact complex-projective fiber and the preceding paracompact Hausdorff CGWH CW-type base, so the next base again has all four properties required by [F2].

F1F3given
2.1

Each stage has injective structure map. Consider one stage BiBi1 of the tower, the projective bundle of a numerable complex bundle of rank m1 over a CW-type base. By [F2] the cohomology H(Bi;R) is free over H(Bi1;R) on the basis 1,x,,xm1; the structure homomorphism H(Bi1;R)H(Bi;R) is the map apa, whose basis coordinates are (a,0,,0), so it is injective.

F2F4step 1.1
2.2

Splitting over the flag bundle is step 1.1, so the first two assertions hold.

step 1.1
3.1

Injectivity of q. The map q:H(B;R)H(Fl(E);R) is the composite of the injective structure maps of the finitely many stages of step 2.1, hence injective.

step 2.1
3.2

Finitely many bundles. Ignore the rank-zero bundles, whose pullbacks are already empty sums of lines. For each remaining bundle construct its flag tower over the original CW base B, where [F1] applies, and choose its metric once there. Now suppose Fj1B has been built, starting with F0=B. Pull the entire original flag tower for E(j) back over Fj1, and let Fj be its top. Pullback of a projective stage is the projective bundle of the pulled-back vector bundle: the local identification is (b,[v])[b,v] and respects the linear transition maps. Its numeration pulls back with the original chart cover. Thus every stage is licensed by the CW-type extension [F2], without applying the CW-base definition [F1] anew on Fj1. Inductively [F3] makes every base paracompact Hausdorff, CGWH, and of CW type. Each such stage has injective cohomology pullback by the module-basis argument of step 2.1. The original splitting is pulled back as an actual bundle isomorphism, so E(j) splits over Fj; earlier splittings persist under further pullback. Set F to the final stage. Finite composition gives the required injection simultaneously for all the stated coefficients. If every rank is zero or the family is empty, set F=B and use the identity map.

F1F2F3F4step 2.1
4.1

Boundary cases. For n=1 the tower has no projectivization and q is the identity of B, so q is injective and qE=L1 with L1=E; the basis 1 is the trivial basis. For the empty family m=0 the assertion is vacuous with F=B. The coefficient rings Z and Fp are nonzero, and the main bundle has positive rank; if an empty base is allowed, all cohomology groups are zero and the injectivity assertion is immediate. No choice beyond the inherited numerability data of [A1] is used, and only finitely many metrics on the original bundles are used, then pulled back through their towers.

A1F1step 3.1step 3.2

Source notes

Miller's Lecture 35 and May's Chapter 24 section 3 prove the splitting principle exactly in this form: the projective-bundle theorem makes each structure map an inclusion of a direct summand, and the iterated projectivization splits the bundle into lines. The integral and coefficientwise Fp injectivity are the strengthened statements the page uses for the mod-two comparison and for the uniqueness theorem; they are proved by the same projective-bundle theorem over each coefficient ring.

Depends on

Used by

Dependency tree · two levels

31 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