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.
Hopf-line calculation of K⁰(S²)
Statement
Assume AC. Let be the tautological Hopf line on , clutched by in the fixed convention, and put . Then
Restriction to a point is projection onto the integer summand. The sign of is tied to the stated clutching convention.
Facts & Assumptions
Given: AC and the two-hemisphere decomposition of .
Complex bundles on are classified by clutching loops, with defining the tautological Hopf line in the fixed convention (Clutching construction for bundles over a suspension, Clutching classifies vector bundles over spheres in the stable range, Stiefel spaces, Grassmannians, and tautological bundles).
Determinant classifies loops in every and sends winding to (Determinant classifies loops in complex general linear groups).
Under AC, equality in is equivalent to a common trivial stabilization (Equality in K⁰ is stable isomorphism over compact bases).
Tensor product is the multiplication and agrees with the bundle external-product convention (External product in complex K-theory).
AC is used only through [F3] and the already propagated AC clause of [F4].
Proof
Let have rank . By [F1] it is clutched by a loop . If is the winding number of , [F2] deforms to , so [F1] gives . The rank-zero bundle is . Consequently every virtual class is an integral combination of and powers of .
The loops and have the same determinant. By [F2] they are homotopic, and [F1] gives . Hence , or . It follows algebraically that for every , since .
If , restriction to a point gives . Then implies by step 1.2. By [F3], after adding the same trivial bundle, and the trivial line are isomorphic. Their stabilized clutching determinants have winding numbers and , so [F2] forces . Thus and are additively independent. Together with steps 1.1–2.1 this proves the displayed ring presentation.
Basepoint restriction sends to and to , so its kernel is exactly . Reversing the hemisphere convention replaces by and hence by ; step 1.2 gives .
Depends on
- External product in complex K-theory
- Determinant classifies loops in complex general linear groups
- Clutching classifies vector bundles over spheres in the stable range
- Stiefel spaces, Grassmannians, and tautological bundles
- Clutching construction for bundles over a suspension
- Equality in K⁰ is stable isomorphism over compact bases
- The Axiom of Choice
Used by
Dependency tree · two levels
22 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, Corollary 2.3 and Example 1.13 (standard reference, not scraped)
- May, A Concise Course in Algebraic Topology, Chapter 24 §2 (standard reference, not scraped)