Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passaudited 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.

Fundamental product theorem for complex K-theory

Statement

Assume AC. For every compact Hausdorff space X, external product is a natural ring isomorphism

μ:K0(X)⊗ZK0(S2)→ ≅ K0(X×S2).

Writing β=[γ]−1, every class on X×S2 has a unique form

pr⁡X∗a+pr⁡X∗b pr⁡S2∗β,a,b∈K0(X).

Facts & Assumptions

Given: AC, compact Hausdorff X, the Hopf line γ clutched by z, and β=[γ]−1.

[F1]

External product is a natural ring map (External product in complex K-theory).

[F2]

Every stabilized bundle on X×S2 has normalized data [E,f], unique up to normalized clutching homotopy (Normalized clutching data for bundles over X×S²).

[F3]

A normalized clutching map and a normalized homotopy admit Laurent approximations, including a Laurent-polynomial homotopy relative to chosen endpoints (Uniform Laurent approximation through bundle automorphisms).

[F4]

Negative powers are cleared by tensoring with γm (Negative Laurent powers are cleared by Hopf-line stabilization).

[F5]

If q has degree at most n, its block linearization Lnq satisfies [E,q]⊕[nE,I]≅[(n+1)E,Lnq] (Polynomial clutching families stabilize to linear clutching), and the linear family has an additive spectral splitting into its outside and inside bundles M+ and M− (Linear clutching splits into spectral subbundles).

[F6]

K0(S2)=Z{1,β}, β2=0, and γ=1+β (Hopf-line calculation of K⁰(S²)).

[F7]

Under AC, the restrictions of a bundle over X×I to its two endpoints are isomorphic (Homotopy invariance of vector-bundle pullback).

[A1]

AC is propagated through [F1]–[F7]; in particular it licenses their stable-complement, homotopy-invariance, partition, and reduced-product uses.

Proof

technique · direct
1.1F1F6A1

By [F1] and [F6], μ is the natural ring map determined by e⊗1↦pr⁡X∗e and e⊗γ↦pr⁡X∗e pr⁡S2∗γ.

2.1F2F3F4F5A1step 1.1algebra

Let V be a bundle on X×S2. By [F2]–[F4], after harmless stabilization and homotopy it has data [E,z−mq] with m≥0 and q polynomial of degree at most n. By [F5], if M+⊕M− is the spectral splitting of (n+1)E for Lnq, then [E,q]=[M+,I]+[M−,z]−[nE,I]. Multiplying by γ−m gives [V]=M+⊠γ−m+M−⊠γ1−m−nE⊠γ−m, which lies in the image of μ. Since bundle classes generate K0(X×S2), μ is surjective.

3.1F5step 2.1algebra

The explicit block matrices in [F5] give two stabilization identities. Padding q to degree at most n+1 and clearing the first −z block yields [(n+2)E,Ln+1q]≅[(n+1)E,Lnq]⊕[E,I]. Applying the same matrix to zq and clearing the final −z block yields [(n+2)E,Ln+1(zq)]≅[(n+1)E,Lnq]⊕[E,z]; the possible sign −z is absorbed by the constant gauge −I.

4.1F5step 3.1algebra

Under the spectral procedure of [F5], [E,I] has minus bundle 0 and [E,z] has minus bundle E: for z the monic endomorphism is A=0, while the Möbius reduction of the constant I produces z+t0−1I, whose associated A=−t0−1I has all eigenvalues outside S1. Direct-sum compatibility in [F5] therefore turns the first identity of step 3.1 into M−(n+1,q)≅M−(n,q) and the second into M−(n+1,zq)≅M−(n,q)⊕E.

5.1F6step 4.1construct

Define on a bundle represented by [E,z−mq] the element ν([E,z−mq])=[M−(n,q)]⊗β+[E]⊗γ−m. The first identity in step 4.1 shows independence of the chosen degree bound n≥deg⁡q.

6.1F6step 4.1step 5.1algebra

Replacing (m,q) by (m+1,zq) changes the formula of step 5.1 to ([M−]+[E])⊗β+[E]⊗γ−m−1. Since [F6] gives γk=1+kβ, one has β=γ−m−γ−m−1; the new expression is therefore [M−]⊗β+[E]⊗γ−m. Thus ν is independent of the Laurent shift.

7.1F2F3F5F7A1step 5.1step 6.1

The remaining choices also do not change ν. Varying the Möbius parameter t0 through values sufficiently close to 1 gives the spectral endomorphism over X×I, whose inside subbundle has isomorphic endpoint restrictions by [F7]. By [F2] any two normalized presentations of the same bundle are homotopic, and [F3] joins their Laurent approximations by a Laurent homotopy. Applying the finite block formula and spectral splitting over X×I again identifies the endpoint minus bundles by [F7]. Isomorphic initial bundles transport all data along their restriction over X×{1}. Hence the formula depends only on the isomorphism class of V.

8.1F5F6step 5.1step 7.1

Block linearization and spectral splitting preserve direct sums by [F5], so the formula in step 5.1 takes Whitney sums to sums. It therefore extends uniquely from bundle classes to a homomorphism ν:K0(X×S2)→K0(X)⊗Z[β]/(β2).

9.1F1F6step 4.1step 5.1step 8.1algebra

It remains to compute νμ. The domain is additively generated by [E]⊗γ−m with m≥0: m=0,1 already give the basis 1,β because β=1−γ−1. Now μ([E]⊗γ−m)=[E,z−m], so take q=I and n=0. Step 4.1 gives M−=0, and step 5.1 yields νμ([E]⊗γ−m)=[E]⊗γ−m. Additivity proves νμ=I.

10.1F6step 1.1step 2.1step 9.1∎

Step 9.1 makes μ injective, while step 2.1 makes it surjective; by step 1.1 it is a natural ring isomorphism. Finally [F6] identifies its domain additively with K0(X)⊕K0(X)β, so bijectivity gives existence and uniqueness of the displayed normal form, including X=∅ and the zero class.

Depends on

Dependency tree · 2 levels

Sources