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.

Complex flag bundle and Chern roots

Definition

Assume AC. Let E→B be a numerable complex rank-n bundle with n≥1 over a path-connected paracompact Hausdorff CW complex, equipped with a Hermitian metric h, which exists by Numerable vector bundles admit bundle metrics.

A complete flag in a fiber Eb is a chain of complex subspaces 0=V0⊂V1⊂V2⊂⋯⊂Vn=Eb,dim⁡CVi=i. The flag bundle q:Fl⁡(E)→B is the bundle of complete flags: its points are the pairs (b,V∙), topologized by the iterated projective-bundle construction, which exhibits it as a fiber bundle with fiber the full flag manifold U(n)/Tn. Concretely, put B0:=B and E(0):=E. For r=1,…,n−1, let Br:=P(E(r−1)) with projection πr:Br→Br−1, let Lr⊆πr∗E(r−1) be its tautological line, and let E(r):=Lr⊥ inside πr∗E(r−1). Pulling the earlier Lj through the later projections and taking Ln:=E(n−1) gives the n ordered orthogonal lines. The composite q:Bn−1→B is Fl⁡(E). All intermediate bases are paracompact Hausdorff CGWH spaces of CW type by Compact-fibre bundle totals preserve paracompactness, and CW type under CW-type hypotheses. At every stage use the CW-type construction established in Integral complex projective bundle theorem, not an assertion that Br itself is a CW complex. The projective charts are numerated by the partition for E(r−1). At every compact projective-fiber stage, the same lemma supplies the CGWH conclusion directly from the preceding CGWH base; no inheritance by arbitrary open subspaces is used. The complement E(r) is a vector subbundle: in a local frame for the ambient bundle the Hermitian orthogonal projection onto Lr varies continuously, and projecting a basis of its kernel at a fixed point gives independent local sections on a neighborhood, by the nonvanishing of a minor. They span the kernel of this constant-rank projection there. Every such bundle is numerable, since the intermediate base is paracompact Hausdorff and Under choice and dependent choice, every open cover of a paracompact Hausdorff space admits a locally finite subordinate partition of unity supplies a partition on its linear chart cover (AC implies DC). This proves the hypotheses required at the next stage, by finite induction.

The i-th tautological line Li→Fl⁡(E) is the sub-line bundle of q∗E whose fiber over a flag V∙ is Vi∩Vi−1⊥, the orthogonal complement of Vi−1 in Vi; it is a complex line bundle. Orthogonal decomposition of each flag gives a metric-preserving isomorphism of complex bundles q∗E=L1⊕L2⊕⋯⊕Ln, where the summands are the tautological lines. The Chern roots of E are the classes ti:=c1(Li)∈H2(Fl⁡(E);Z)(1≤i≤n), defined by Chern classes from the projective-bundle relation after the Chern classes themselves exist; the summands and their first Chern classes are the data in which the splitting principle is stated.

For n=1 there are no projectivization steps: Fl⁡(E)=B, q is the identity and L1=E. Rank zero is outside this definition.

Depends on

Dependency tree · 2 levels

Sources