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 projective bundle and tautological complex line
Definition
Assume AC. Let be a numerable complex vector bundle of rank over a paracompact Hausdorff CW complex , with zero section and total space . Its projective bundle is the quotient where acts fiberwise by ; write for the class of a nonzero vector. The projection , , is well defined because scaling preserves the base point.
is a fiber bundle over with fiber : over a complex linear chart of the quotient is . On an overlap, the transition matrix induces ; this is a homeomorphism with inverse induced by , depends continuously on , and the cocycle identities descend unchanged to projective classes. These quotient charts therefore form a fiber-bundle atlas with fiber . Under the identification supplied by Stiefel spaces, Grassmannians, and tautological bundles, a point of the fiber over is a complex line .
The tautological complex line is the subbundle whose fiber over is itself, with the complex structure induced from ; its transition functions are the projectivized linear maps restricted to the selected line, so it is a complex line bundle over .
Here is the base and orientation justification needed to define its Euler class. The numeration for also numerates the displayed projective charts. The CW complex is CGWH. The fiber is compact Hausdorff and a finite CW complex (with one cell in dimensions ). Thus Compact-fibre bundle totals preserve paracompactness, and CW type under CW-type hypotheses applies and makes paracompact Hausdorff, CGWH, and of CW type. The tautological line is locally trivial: in a projective coordinate chart , choose the unique representative with and write each vector on the line as its scalar multiple. These charts, combined with the charts of , give linear trivializations. Under AC (hence DC), Under choice and dependent choice, every open cover of a paracompact Hausdorff space admits a locally finite subordinate partition of unity numerates their open cover.
Orient the underlying real line bundle by the frame in each such complex trivialization. Changing to has real matrix , of determinant . Hence these orientations agree on overlaps by Oriented real bundles and oriented frame bundles. This direct rank-one construction uses no CW structure on itself. The resulting numerable oriented real rank-two bundle is in the general Thom scope, so Euler class by zero-section pullback of the Thom class defines Defining by the Euler class of the tautological line avoids any circular use of Chern classes, which are introduced only afterwards on this page. For the zero bundle of rank we set , and is not defined there; for a line bundle the map is a homeomorphism over and corresponds to under it.
Depends on
Real and complex topological vector bundles
Euler class by zero-section pullback of the Thom class
Stiefel spaces, Grassmannians, and tautological bundles
The Axiom of Choice
Compact-fibre bundle totals preserve paracompactness, and CW type under CW-type hypotheses
Under choice and dependent choice, every open cover of a paracompact Hausdorff space admits a locally finite subordinate partition of unity
Oriented real bundles and oriented frame bundles