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 E→B be a numerable complex rank-n bundle over a paracompact Hausdorff CW complex, with n≥1. Let P(E), γE, and x=e((γE)R) have the conventions of Complex projective bundle and tautological complex line. For each b∈B, choose a complex-linear identification Eb≅Cn and denote the resulting fiber inclusion by jb:CPn−1→P(E).

With the complex orientation on both tautological lines, jb∗x=e(γR)=:xtaut. For n≥2 this is a generator of H2(CPn−1;Z), and 1,jb∗x,…,(jb∗x)n−1 is an integral cohomology basis. Its coefficient reductions are a basis over every prime field Fp. For n=1 the fiber is a point, jb∗x=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 Hk−1(S(ξ);Z)→Hk−2(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, d≥1 (Homology of spheres, The universal coefficient theorem for cohomology over a PID).

Proof

1.1F1F3given

Put N=n−1. 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+ib≠0 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 jb∗x=xtaut with exactly the stated orientation.

1.2F4

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.

2.1F1F2F5step 1.2

For N≥1, 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 2≤k≤2N, both flanking groups in [F2] vanish by [F5], since 1≤k−1<k<2N+1. Thus multiplication by xtaut is an isomorphism Hk−2→Hk 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.

3.1F4step 1.1step 2.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.

4.1A1F1F4step 1.1step 1.2step 3.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.

Depends on

Dependency tree · 2 levels

Sources