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.

Uniqueness of Chern classes from the splitting principle

Statement

Assume AC. Suppose that to every isomorphism class of numerable complex bundles VC over a nonempty path-connected CW complex one assigns classes di(V)H2i(C;Z) for i0 with the following properties:

  1. Naturality: di(fV)=fdi(V) for continuous maps between these bases;
  2. Normalization: d0(V)=1, di(V)=0 for i>rankV, and d1(L)=e(LR) for a complex line L;
  3. Whitney multiplicativity: d(VW)=d(V)d(W) for the total classes d=idi.

Then d(V)=c(V) for every numerable complex bundle over a nonempty path-connected CW complex, where c is the total Chern class of Chern classes from the projective-bundle relation. In particular the assignments ci are the unique ones satisfying 1-3.

Facts & Assumptions

Given: AC, the assignment d satisfying properties 1–3, and a numerable complex rank-n bundle EB over a nonempty path-connected CW complex. Bundle assignments are on isomorphism classes, as is usual for characteristic classes.

[A1]

AC is assumed for the splitting, Chern-class and numerable-fibration suppliers and the stated CW paracompactness fact. (The Axiom of Choice).

[F1]

On path-connected CW bases, total Chern classes are natural, normalized on lines by c1(L)=e(LR), Whitney multiplicative, and have c0=1, ci=0 above the rank and c(0)=1. They depend only on the bundle isomorphism class. (Naturality, normalization, and Whitney sum for Chern classes, Chern classes from the projective-bundle relation).

[F2]

For positive rank on a path-connected paracompact Hausdorff CW base, the flag projection q splits qE into complex lines and gives an injective integral cohomology pullback. (Complex splitting principle with integral injective pullback).

[F3]

The flag construction is a finite tower of numerable projective bundles with fibers CPm1; its intermediate bases have CW type and its tautological lines are numerable. For rank one it is the identity tower. (Complex flag bundle and Chern roots, Compact-fibre bundle totals preserve paracompactness, and CW type under CW-type hypotheses).

[F4]

Numerable fiber bundles are Hurewicz fibrations under AC. The homotopy lifting property applies in particular to a homotopy on a one-point space, hence lifts any given path from a supplied initial point. (Numerable fiber bundles are hurewicz fibrations, Hurewicz and serre fibrations).

[F5]

Homotopic continuous maps induce equal pullbacks in singular cohomology for every abelian coefficient group. (Homotopic maps induce equal maps in singular cohomology).

[F6]

CW complexes are paracompact (and Hausdorff in the library convention). The paracompactness statement and complete proof are Hatcher, Vector Bundles & K-Theory, Proposition 1.20, printed pp.36–37, https://pi.math.cornell.edu/~hatcher/VBKT/VB.pdf . Thus the CW bases below satisfy the extra paracompactness hypothesis in [F2].

Proof

technique · direct, comparing on an actual CW model of the flag space
1.1

Lines and rank zero. On every complex line over an allowed base, properties 2 and [F1] give d(L)=1+e(LR)=c(L); all terms of index at least two vanish. If n=0, both totals are 1 by their degree-zero and rank conventions, so the conclusion already holds. Henceforth take n1.

F1given
1.2

The flag space is path-connected. The base B is admissible for [F2] by [F6]. In the tower of [F3], each fiber CPm1 is nonempty and path-connected: two distinct lines have linearly independent representatives v,w, and [(1t)v+tw] joins them, since that vector never vanishes; equal lines use the constant path. For a stage with path-connected base, join the images of two total-space points by a path. Lift it from the first point by [F4] and join its endpoint to the second point inside the terminal fiber. This proves that the stage total is path-connected. Finite induction proves that F=Fl(E) is nonempty and path-connected; rank one has F=B. By [F3], F has CW type. No assertion that F itself is a CW complex is made.

F2F3F4F6given
2.1

Replace the base before evaluating the assignment. Choose a homotopy equivalence h:CF from a CW complex and a homotopy inverse k:FC, as supplied by CW type in step 1.2. The complex C is nonempty and path-connected. Indeed, for x,yC, join h(x) to h(y) in F and apply k; the homotopy khidC joins its endpoints to x,y. By [F5], h is an isomorphism in integral cohomology, inverse to k. Set p=qh:CB and Mj=hLj. Pulling back the actual splitting of [F2] gives pEj=1nMj. These bundles are numerable: pull back the locally finite partition on each original bundle chart cover; local finiteness and the identity sum are preserved by composition with h. Thus d and [F1] both apply to the pulled-back bundles on the nonempty path-connected CW complex C. Also p=hq is injective.

F1F2F3F5step 1.2algebra
3.1

Compare on the CW model. By property 3, isomorphism invariance, and step 1.1 applied to the lines Mj over C, d(pE)=j=1nd(Mj)=j=1nc(Mj)=c(pE). The last equality is [F1]'s Whitney identity, applied on C, where its hypotheses hold. This proof never evaluates d on a bundle over the merely CW-type space F.

F1givenstep 1.1step 2.1algebra
4.1

Descend. The map p:CB has both source and target in the stated assignment domain. Naturality of d and [F1] gives p(d(E)c(E))=d(pE)c(pE)=0. The injectivity established in step 2.1 implies d(E)=c(E), degree by degree. Conversely [F1] provides the Chern assignment satisfying all three properties, so this is uniqueness together with the already supplied existence.

F1givenstep 2.1step 3.1algebra
5.1

Boundaries and conventions. Rank zero was settled before making a flag bundle. In rank one, normalization in step 1.1 suffices, and the tower is the identity. The empty base is explicitly excluded; no domain extension to disconnected or non-CW bases is claimed for d. Terms above the rank vanish, so each total and each product is finite even when the CW complexes are infinite-dimensional. The line normalization uses the complex orientation of LR, not an independent sign for a projective generator. AC is inherited through [A1]; the chosen single CW equivalence and the finite tower introduce no unrecorded family of choices.

A1F1F3F6step 1.1step 2.1step 4.1algebra

Source notes

May, https://www.math.uchicago.edu/~may/CONCISE/ConciseRevised.pdf , Chapter 23 section 2, printed pp.189–190, treats characteristic classes as natural assignments on bundle equivalence classes. Chapter 23 section 7, printed pp.198–199, states Chern-class uniqueness and describes the detection by elementary symmetric polynomials. The proof here supplies the required CW-model domain argument directly from the local splitting theorem. Its line sign is fixed by the library's Euler normalization; no independent choice of May's projective generator is imported. Hatcher Proposition 1.20, printed pp.36–37, supplies CW paracompactness.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

36 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