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.

Integral cohomology of BU(n)

Statement

Assume AC and n1. Let EU(n)BU(n) be the universal principal U(n)-bundle, and let E=EU(n)×U(n)Cn be its associated universal rank-n complex vector bundle, the tautological bundle over the Grassmannian model BU(n)=Grn(C), and let q:BTn=EU(n)/TnBU(n) be the universal flag bundle of The universal complex flag bundle is BT-n. Then restriction along q identifies H(BU(n);Z)Z[c1,,cn], the polynomial ring on the Chern classes of the universal bundle, and sends ci to the i-th elementary symmetric polynomial ei(t1,,tn) in the coordinate Chern roots of BTn.

Facts & Assumptions

[A1]

The Axiom of Choice is assumed, exactly as inherited from the splitting and classifying-space suppliers (The Axiom of Choice).

[F1]

The flag projection q splits qE=L1Ln into the tautological lines and q:H(BU(n);Z)H(BTn;Z) is injective (Complex splitting principle with integral injective pullback).

[F2]

Chern classes are natural and multiplicative over Whitney sums, with c(L)=1+c1(L) for a line (Naturality, normalization, and Whitney sum for Chern classes).

[F3]

H(BTn;Z)=Z[t1,,tn] with ti=c1(Li), the image of q is contained in the symmetric invariants; its quotient model has q as the projection to the Grassmannian (The universal complex flag bundle is BT-n).

[F4]

Over every commutative ring the symmetric polynomials in n variables are the polynomials in the elementary symmetric functions e1,,en, with R[T1,,Tn]R[x1,,xn]Σn an isomorphism (Fundamental theorem of symmetric polynomials: unique expression as a polynomial in e1,,en).

[F5]

The Grassmannian Grn(C) is the chosen model of BU(n) and classifies numerable rank-n complex bundles (Real and complex vector bundles are classified by stable Grassmannians).

[F6]

The tautological lines Li over the flag bundle are complex line bundles with qE=L1Ln (Complex flag bundle and Chern roots).

[F7]

Homotopic maps give equal cohomology pullbacks, hence a homotopy equivalence gives a ring isomorphism (Homotopic maps induce equal maps in singular cohomology).

[F8]

First Chern classes of lines are their complex-oriented Euler classes on the allowed CW-type bases (Chern classes from the projective-bundle relation); those Euler classes are natural for oriented pullbacks (Naturality, orientation sign, and Whitney product for Euler classes).

[F9]

The Stiefel frame projection has the tautological bundle as its associated standard vector bundle (Stiefel spaces, Grassmannians, and tautological bundles).

Proof

technique · direct

Given: AC, the universal bundle EBU(n) and its flag bundle q:BTnBU(n).

1.1

Put Q=BTn in its flag-quotient model. By [F3] and its explicit product comparison there is a homotopy equivalence g:P=(CP)nQ, with P a path-connected CW complex. Pull the splitting of [F1] back along g. Naturality and Whitney multiplication in [F2] apply on the actual CW base P and give (qg)c(E)=i(1+c1(gLi)). By [F8], c1(gLi)=gc1(Li)=gti, with the fixed complex orientation. Since g is an isomorphism by [F7], the equality descends to qc(E)=i(1+ti) on Q, hence qci(E)=ei(t1,,tn). This does not apply the CW-base Whitney interface directly on a space known only to have CW type.

F1F2F3F6F7F8
1.2

By [F3] the image of q is contained in the symmetric invariants of Z[t1,,tn], and by [F4] those invariants are exactly Z[e1,,en].

F3F4
2.1

By step 1.1 the image of q contains Z[e1,,en], since it contains the images of the classes ci; with step 1.2 this forces the image of q to be exactly the invariant subring Z[e1,,en].

F4step 1.1step 1.2
3.1

Let φ:Z[C1,,Cn]H(BU(n);Z) be the ring map Cici and let s:Z[C1,,Cn]Z[t1,,tn]Σn be the substitution Ciei of [F4]. Then qφ=s, which is an isomorphism by [F4]; injectivity of q from [F1] makes φ injective, and step 2.1 makes φ surjective. Hence φ is an isomorphism, which is the assertion.

F1F4step 2.1
4.1

Boundary cases. For n=1 the statement reads H(BU(1);Z)=Z[c1] with c1=e1=t1, which is the ring Z[u] of CP; the flag bundle is q=id and [F1] is trivial. The rank-zero case is excluded by n1; the coefficient ring Z is a PID and the polynomial rings considered are free, so the fundamental theorem applies verbatim. The vector bundle is the associated tautological bundle by [F9] and is universal by [F5], and AC is used only through [A1] in the splitting, classifying-space, Euler and metric suppliers.

A1F1F4F5F9step 3.1

Source notes

Miller's Lecture 35 and Hatcher's section 3.1 prove H(BU(n);Z)=Z[c1,,cn] exactly by the symmetric-polynomial argument used here: the flag pullback is injective, the image lies in the invariants because the Weyl group permutes the roots, and the elementary symmetric functions generate the invariant ring. The proof above avoids any finite-index or Gysin shortcut.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

54 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