ExampleConstruction: Literature-sourcedVerification: 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.

Complex line bundles over the two-sphere by clutching degree

Example

Assume AC. For $d \in Z$ let $E_{d} \to S^{2}$ be the complex line clutched by $g_{d} (z) = z^{d}$ in the upper-to-lower convention of Clutching construction for bundles over a suspension, and let $u : = c_{1} (E_{1}) \in H^{2} (S^{2}; Z) ≅ Z,$ the class of the tautological Hopf line. Then $u$ is a generator, the orientation of $S^{2}$ is fixed by requiring $⟨ u, [S^{2}] ⟩ = + 1$ in this normalization, and for every $d$ $c_{1} (E_{d}) = d u .$ In particular the clutching degree $d$ and the first Chern number $⟨ c_{1} (E_{d}), [S^{2}] ⟩ = d$ give the same $Z$ -classification of complex line bundles over $S^{2}$ .

Facts & Assumptions

Given: AC, the clutching construction over $S^{2} = Σ S^{1}$ , and the maps $g_{d} (z) = z^{d}$ .

[A1]

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

[F1]

The clutching construction turns a map $g : S^{1} \to {GL}_{1} (C)$ into a complex line over $S^{2}$ , and two clutching maps give isomorphic bundles exactly when they are homotopic in the stable range; for $C$ , $q = 2$ , the classification is $π_{1} ({GL}_{1} (C)) ≅ Z$ (Clutching classifies vector bundles over spheres in the stable range, Clutching construction for bundles over a suspension).

[F2]

$c_{1} : {Pic}_{t o p} (S^{2}) \to H^{2} (S^{2}; Z)$ is a natural group isomorphism, tensor product corresponding to addition (The first Chern class classifies complex line bundles).

[F3]

Under the fixed upper-to-lower convention, the map $g (z) = z$ clutches the tautological Hopf line over $S^{2} = {C P}^{1}$ (Clutching construction for bundles over a suspension).

[F4]

$π_{1} (S^{1}, (1, 0)) ≅ Z$ , and under this isomorphism the loop $t \mapsto (\cos 2 π n t, \sin 2 π n t)$ , i.e. $z \mapsto z^{n}$ , corresponds to $n$ for every $n \in Z$ (The trigonometric loops give $π_{1} ({(x, y) : x^{2} + y^{2} = 1}, (1, 0)) ≅ Z$ ).

[F5]

For complex lines $c_{1} (L \otimes M) = c_{1} (L) + c_{1} (M)$ and $c_{1} (L^{*}) = - c_{1} (L)$ (First Chern class of tensor, dual, and conjugate lines).

Verification

technique · direct

1.1

Multiplication of clutching functions corresponds to tensor product: $E_{g} \otimes E_{h} ≅ E_{g h}$ , because the transition functions multiply in the clutching convention; in particular $E_{d} \otimes E_{d^{'}} ≅ E_{d + d^{'}}$ and $E_{- d} ≅ E_{d}^{*}$ , since $z^{- d} = (z^{d})^{- 1}$ and dualizing inverts transition functions.

F1F5given

2.1

The class $u = c_{1} (E_{1})$ is a generator of $H^{2} (S^{2}; Z) ≅ Z$ . By [F1] and [F4], clutching identifies the isomorphism classes of complex lines with $Z$ , with $E_{1}$ corresponding to $1$ . Step 1.1 shows that this bijection carries addition of degrees to tensor product, so $E_{1}$ generates the Picard group. The group isomorphism $c_{1}$ of [F2] therefore carries $E_{1}$ to a generator $u$ of cohomology. By [F3] this is the tautological Hopf line in the fixed convention.

F1F2F3F4step 1.1

3.1

For $d \geq 0$ , iterating step 1.1 and additivity [F2] gives $c_{1} (E_{d}) = d c_{1} (E_{1}) = d u$ ; for $d < 0$ , $E_{d} ≅ E_{∣ d ∣}^{*}$ by step 1.1 and the dual formula of [F5] gives $c_{1} (E_{d}) = - ∣ d ∣ u = d u$ .

F2F5step 1.1step 2.1

4.1

The pairing with the fundamental class: by step 2.1 the class $u$ generates $H^{2} (S^{2}; Z)$ , so there is a unique orientation $[S^{2}]$ with $⟨ u, [S^{2}] ⟩ = + 1$ ; this is the Hopf normalization of the statement, and then $⟨ c_{1} (E_{d}), [S^{2}] ⟩ = d$ by step 3.1.

step 3.1

5.1

Boundary cases. For $d = 0$ the clutching map is constant, $E_{0}$ is trivial and $c_{1} = 0 = 0 \cdot u$ . For $d = 1$ we have $c_{1} (E_{1}) = u$ by definition; for $d = - 1$ the bundle is the dual of the Hopf line and $c_{1} = - u$ . Negative exponents are covered by the dual computation in step 3.1 and by [F4], which includes $d < 0$ . The coefficient ring $Z$ is nonzero, so a nonzero multiple $d \cdot u$ of a generator is nonzero exactly when $d \neq 0$ , giving the claimed classification. AC is used only through [A1].

A1F1F4step 3.1∎

Source notes

Hatcher, Example 1.10 and section 3.1 (printed pp. 22-24 and 86-88), computes the clutching classification of line bundles over $S^{2}$ and the first Chern class of the clutching construction. The explicit reversal of the upper-to-lower convention for $d < 0$ is the inversion of transition functions used in The Hopf line bundle over S² by clutching.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

29 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

Hatcher, Vector Bundles & K-Theory, Example 1.10 and section 3.1 (standard reference, not scraped)