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

First Chern class of tensor, dual, and conjugate lines

Statement

Assume AC. Let L,M 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 c1(LM)=c1(L)+c1(M),c1(L)=c1(L),c1(L)=c1(L), where L is the dual line and L the conjugate line.

Facts & Assumptions

[A1]

The Axiom of Choice is assumed, exactly as inherited from the classification and metric suppliers (The Axiom of Choice).

[F1]

c1:Pictop(X)H2(X;Z) is a natural group isomorphism, tensor product corresponding to addition (The first Chern class classifies complex line bundles).

[F2]

Tensor products, duals and conjugates of complex line bundles are formed by the corresponding transition functions, and evaluation vλλ(v) 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).

[F3]

Every numerable complex bundle admits a Hermitian metric (Numerable vector bundles admit bundle metrics).

[F4]

For a complex line L the first Chern class equals the Euler class of its underlying real rank-two bundle, c1(L)=e(LR) (Chern classes from the projective-bundle relation).

Proof

technique · direct

Given: AC and numerable complex lines L,M over either of the bases in the statement.

1.1

The tensor formula is the additivity clause of the group isomorphism of [F1]: linearity of c1 under the group structure of Pictop is exactly c1(LM)=c1(L)+c1(M).

F1
2.1

The dual formula: the evaluation pairing of [F2] shows LLε1, so by step 1.1 and c1(ε1)=0 one has c1(L)=c1(L).

F2step 1.1
3.1

The conjugate formula: write a Hermitian metric from [F3] as h, conjugate-linear in its first argument and linear in its second (transpose the arguments if using the opposite convention). It provides, for each x, the conjugate-linear isomorphism LxLx, vh(v,), which is complex-linear on the conjugate line; in a local frame e, the functional sends we to zwh(e,e) for v=ze, so it is continuous with nonzero coefficient h(e,e)>0. Hence the maps define an isomorphism LL. Hence c1(L)=c1(L)=c1(L) by step 2.1.

F2F3step 2.1
3.2

Specialization to underlying real bundles: for a complex line with c1(L)=e(LR) by [F4], the dual identity reads e((L)R)=e(LR), consistent with the orientation-reversal sign.

F4step 2.1
4.1

Boundary cases. For the trivial line L=ε1 the formulas read c1(M)=0+c1(M) and 0=0; for a point base both sides vanish. The empty base is excluded by the path-connected hypothesis; the group Pictop(X) is abelian and H2(X;Z) 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.

A1F1F2step 1.1step 3.1

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 LL. 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