Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-14
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 S2=CP1, clutched by g(z)=z in the fixed convention, and put β=[γ]1. Then

K0(S2)Z[β]/(β2),K~0(S2)=Zβ.

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

[F1]

Complex bundles on S2 are classified by clutching loops, with g(z)=z 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).

[F2]

Determinant classifies loops in every GLn(C) and sends winding k to diag(zk,1,,1) (Determinant classifies loops in complex general linear groups).

[F3]

Under AC, equality in K0 is equivalent to a common trivial stabilization (Equality in K⁰ is stable isomorphism over compact bases).

[F4]

Tensor product is the K0 multiplication and agrees with the bundle external-product convention (External product in complex K-theory).

[A1]

AC is used only through [F3] and the already propagated AC clause of [F4].

Proof

technique · direct
1.1

Let E have rank n>0. By [F1] it is clutched by a loop g:S1GLn(C). If k is the winding number of detg, [F2] deforms g to diag(zk,1,,1), so [F1] gives Eγkεn1. The rank-zero bundle is 0S2. Consequently every virtual class is an integral combination of 1 and powers of [γ].

F1F2
1.2

The loops diag(z2,1) and diag(z,z) have the same determinant. By [F2] they are homotopic, and [F1] gives γ2ε1γγ. Hence [γ]22[γ]+1=0, or β2=0. It follows algebraically that [γ]k=(1+β)k=1+kβ for every kZ, since (1+β)1=1β.

F1F2F4algebra
2.1

If a+kβ=0, restriction to a point gives a=0. Then kβ=0 implies [γk]=1 by step 1.2. By [F3], after adding the same trivial bundle, γk and the trivial line are isomorphic. Their stabilized clutching determinants have winding numbers k and 0, so [F2] forces k=0. Thus 1 and β are additively independent. Together with steps 1.1–2.1 this proves the displayed ring presentation.

F2F3A1step 1.1step 1.2
3.1

Basepoint restriction sends 1 to 1Z and β=[γ]1 to 0, so its kernel is exactly Zβ. Reversing the hemisphere convention replaces z by z1 and hence γ by γ; step 1.2 gives [γ]1=(1β)1=β.

F1step 1.2step 2.1

Depends on

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