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.
First Chern class of tensor, dual, and conjugate lines
Statement
Assume AC. Let be numerable complex line bundles over a path-connected CW complex with a vertex basepoint, or over a path-connected paracompact Hausdorff CGWH space of CW homotopy type. Then where is the dual line and the conjugate line.
Facts & Assumptions
The Axiom of Choice is assumed, exactly as inherited from the classification and metric suppliers (The Axiom of Choice).
is a natural group isomorphism, tensor product corresponding to addition (The first Chern class classifies complex line bundles).
Tensor products, duals and conjugates of complex line bundles are formed by the corresponding transition functions, and evaluation is an isomorphism of line bundles (in a local line frame it is multiplication of the two scalar coordinates) (Whitney sum, tensor, dual, Hom, and exterior-power bundles).
Every numerable complex bundle admits a Hermitian metric (Numerable vector bundles admit bundle metrics).
For a complex line the first Chern class equals the Euler class of its underlying real rank-two bundle, (Chern classes from the projective-bundle relation).
Proof
Given: AC and numerable complex lines over either of the bases in the statement.
The tensor formula is the additivity clause of the group isomorphism of [F1]: linearity of under the group structure of is exactly .
The dual formula: the evaluation pairing of [F2] shows , so by step 1.1 and one has .
The conjugate formula: write a Hermitian metric from [F3] as , conjugate-linear in its first argument and linear in its second (transpose the arguments if using the opposite convention). It provides, for each , the conjugate-linear isomorphism , , which is complex-linear on the conjugate line; in a local frame , the functional sends to for , so it is continuous with nonzero coefficient . Hence the maps define an isomorphism . Hence by step 2.1.
Specialization to underlying real bundles: for a complex line with by [F4], the dual identity reads , consistent with the orientation-reversal sign.
Boundary cases. For the trivial line the formulas read and ; for a point base both sides vanish. The empty base is excluded by the path-connected hypothesis; the group is abelian and is nonzero as a group in general but may be zero, in which case all three identities still hold. AC is used only through [A1] in the classification and metric suppliers.
Source notes
May, Chapter 24 section 4, printed pp. 211-212, obtains the tensor and dual formulas from the Picard group description; the conjugate formula is the same identity composed with the metric isomorphism . The underlying real-bundle reading of the dual formula is the orientation-reversal sign for Euler classes.
Depends on
Used by
Dependency tree · two levels
26 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
- May, A Concise Course in Algebraic Topology, Chapter 24 section 4 (standard reference, not scraped)