Alphabeta Math
LemmaStatement: 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.

The complex tautological Euler class restricts to the projective-fiber generator

Statement

Assume AC. Let EB be a numerable complex rank-n bundle over a paracompact Hausdorff CW complex, with n1. Let P(E), γE, and x=e((γE)R) have the conventions of Complex projective bundle and tautological complex line. For each bB, choose a complex-linear identification EbCn and denote the resulting fiber inclusion by jb:CPn1P(E).

With the complex orientation on both tautological lines, jbx=e(γR)=:xtaut. For n2 this is a generator of H2(CPn1;Z), and 1,jbx,,(jbx)n1 is an integral cohomology basis. Its coefficient reductions are a basis over every prime field Fp. For n=1 the fiber is a point, jbx=0, and the basis is 1. A comparison with a generator given the opposite normalization introduces one fixed sign; with the tautological Euler normalization above the sign is +1, independently of b and the chosen complex-linear identification.

Facts & Assumptions

Given: AC and the bundle, orientations and fiber inclusion of the statement.

[A1]

AC is assumed through the bundle and cohomology suppliers (The Axiom of Choice).

[F1]

The projective bundle and its tautological complex line have the displayed fiberwise descriptions, the line has the orientation (v,iv), and its real rank-two Euler class is defined on its paracompact Hausdorff CW-type base (Complex projective bundle and tautological complex line).

[F2]

For an oriented rank-two bundle in general Thom scope, the Gysin sequence contains Hk1(S(ξ);Z)Hk2(B;Z)e(ξ)Hk(B;Z)Hk(S(ξ);Z) (Gysin long exact sequence of an oriented sphere bundle).

[F3]

Euler classes are natural under oriented pullback, with both bases in general Thom scope (Naturality, orientation sign, and Whitney product for Euler classes).

[F4]

Complex projective N-space has a finite Schubert CW structure with one cell in each dimension 0,2,,2N (Schubert cells in real and complex Grassmannians, Schubert cells give the stable Grassmannian CW structure). Its cellular cochains compute singular cohomology naturally for coefficient maps (Cellular cochains compute cohomology with local coefficients).

[F5]

Integral sphere homology, together with the cohomological universal coefficient sequence for a free complex over Z, gives Hk(Sd;Z)=0 for 0<k<d, d1 (Homology of spheres, The universal coefficient theorem for cohomology over a PID).

Proof

1.1

Put N=n1. The pullback jbγE has fiber precisely the line represented by each point of P(Eb). The chosen complex-linear identification therefore identifies it with the usual tautological line over CPN. The identification preserves the frames (v,iv); changing a complex line frame by a+ib0 has positive real determinant a2+b2. Both bases are in Thom scope by [F1], also applied to the trivial rank-n bundle over a point. Thus [F3] gives jbx=xtaut with exactly the stated orientation.

F1F3given
1.2

The integral cellular cochain complex of CPN has one copy of Z in each even degree 0,2,,2N and zero in every other degree. Every differential is zero. Hence its integral cohomology is Z in those degrees and zero elsewhere, including all degrees above 2N. Its degree-zero unit is a generator.

F4
2.1

For N1, the sphere bundle of its tautological complex line is S2N+1: the homeomorphism sends (,v) with v of unit length to v, and its inverse sends v to (Cv,v). Both maps are continuous in the quotient and bundle charts of [F1]. For 2k2N, both flanking groups in [F2] vanish by [F5], since 1k1<k<2N+1. Thus multiplication by xtaut is an isomorphism Hk2Hk in this range. Starting at the unit, its powers generate all the even groups in step 1.2. This proves the integral basis assertion and degree-two generation; vanishing above the top degree comes from step 1.2, not from an induction through the exceptional top sphere group.

F1F2F5step 1.2
3.1

With Fp coefficients the same cellular cochain complex has one copy of Fp in each even degree and zero differentials. The natural coefficient map reduces each integral cell coordinate modulo p. Each power in step 2.1 is an integral generator, hence has coordinate +1 or 1 and reduces to a basis vector over Fp. Together with step 1.1 this proves the reduction assertion.

F4step 1.1step 2.1
4.1

When n=1, step 1.2 with N=0 gives H2=0 and the single basis element 1, integrally and after reduction. No use of step 2.1 is needed. An empty base contributes no fibers. Rank zero is excluded; the separate convention in [F1] gives empty projectivization with no x. The determinant argument in step 1.1 proves independence of each complex-linear identification, so no varying sign is introduced across components. AC is inherited from the stated suppliers; choosing a frame for one fixed fiber introduces no further choice assumption.

A1F1F4step 1.1step 1.2step 3.1

Depends on

Used by

Dependency tree · two levels

45 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