(Geometric) Proof for the projective bundle formula in K-theory

Question

I'm trying to piece together a proof of the projective bundle formula from several incomplete sources. Here's the statement I'd like to prove:

Projective bundle formula: Let $\pi: E \to X$ be a vector bundle of rank $r$ over a compact space $X$. Let $\mathbb{P}(E)$ be the projective bundle of $E$ with distinguished line bundle $H$. Then we have the following formula: $K(\mathbb{P}(E))=K(X)[H]/( \sum^r_{k=0}(-1)^k [H]^k[\bigwedge^k E] )$.

At this point I feel like I have all the ingredients for the proof but I can't seem to piece them together. Here's what I have:

There's a canonical Kozul complex over $E$:

$$0 \to \mathbb{C} \to E \to \bigwedge^2 E \to \dots \to \bigwedge^r E \to 0$$

Over each point $e \in E$ the maps are given by wedge multiplication $(-) \wedge e$. Therefore this complex is exact outside of the zero section and gives us the thom class in $\lambda_E \in K(E,E-0)=\tilde{K}(Th(E))$. What's a neat way of proving that $K(E,E-0)$ is a free rank 1 module generated by $\lambda_E$?

Suppose wer'e past that. Observe that there's a cofiber sequence

$$\mathbb{P}(E) \to \mathbb{P}(E \oplus \mathbb{C}) \to Th(E)$$

This suggests that the pullback of $\lambda_E$ to $\mathbb{P}(E \oplus \mathbb{C})$ might tell me the relavant information. Two things are not clear to me here.

1. Why is the pullback of $\lambda_E$ to $\mathbb{P}(E \oplus \mathbb{C})$ equal to $\sum^r_{k=0}(-1)^k [H]^k[\bigwedge^k E]$? (Twisting the kozul complex by powers of $[H]$ must have some geometric interpratation... no?)
2. It seems rather implausible that for every cofiber sequence $X \to Y \to C$ one has $K(X) = K(Y)/Im(K(C)\to K(Y))$. So can we really justify and prove the formula using these ingredients? Maybe there's an inductive step here that might help simplify the statement?

I apologize if there's a well known source that discusses this in detail. The very reason I'm here is I didn't find one.

Answer 1

First, for any bundle $V$ of dimension $d$ over $Y$ put $$ \lambda(V)(t) = \sum (-1)^k[\Lambda^k(V)]t^{d-k} \in K^0(Y)[t]. $$ This is a monic polynomial of degree $d$ over $K^0(Y)$. It satisfies $\lambda(L)(t)=t-[L]$ if $L$ is a line bundle, and $\lambda(A\oplus B)(t)=\lambda(A)(t)\lambda(B)(t)$. Thus, if $L$ is isomorphic to a subbundle of $V$ then $V\simeq L\oplus W$ for some $W$ and we find that $\lambda(V)([L])=0$.

Let $p\colon \mathbb{P}(E)\to X$ be the obvious projection. For any $U\subseteq X$, put \begin{align*} A^*(U) &= K^*(U)[t]/\lambda(E|_U)(t) \\ B^*(U) &= K^*(p^{-1}(U)) \end{align*} The bundle $H$ over $\mathbb{P}(E)$ is tautologically a subbundle of $p^*E$, and using this we obtain a ring map $A^*(X)\to B^*(X)$ sending $t$ to $[H]$. Essentially the same construction gives maps $\phi_U\colon A^*(U)\to B^*(U)$ for all $U$. Recall also that $\lambda(E)(t)$ is a monic polynomial of degree $d$. It follows that the set $T=\{1,t,\dotsc,t^{d-1}\}$ is a basis for $A^*(U)$ over $K^0(U)$.

Now suppose we have open subsets $U$ and $V$. There is a Mayer-Vietoris sequence relating the $K^*$ groups of $U$, $V$, $U\cup V$ and $U\cap V$. Using the basis $T$, we obtain a long exact sequence relating the $A^*$ groups of $U$, $V$, $U\cup V$ and $U\cap V$. The Mayer-Vietoris sequence for $p^{-1}(U)$ and $p^{-1}(V)$ gives another long exact sequence relating the $B^*$ groups of $U$, $V$, $U\cup V$ and $U\cap V$. The maps $\phi$ link these two long exact sequences. They are obviously compatible with ther restriction maps $A^*(U)\to A^*(U\cap V)$ and so on, but a little work is needed to check that they are also compatible with the connecting morphisms.

Now put $\mathcal{U}=\{U\;|\;\phi_U \text{ is iso } \}$. If $U$ is contractible then $E|_U\simeq U\times\mathbb{C}^d$ and the standard calculation of $K^*(\mathbb{C}P^{d-1})$ shows that $U\in\mathcal{U}$. If $U$, $V$ and $U\cap V$ lie in $\mathcal{U}$ then the Mayer-Vietoris sequences together with the five lemma show that $U\cup V\in\mathcal{U}$. Now suppose that $X$ can be covered by open sets $U_1,\dotsc,U_n$ such that all intersections $U_{i_1}\cap\dotsb\cap U_{i_r}$ are empty or contractible. Then one can check by induction on $n$ that $\phi_X$ is iso. If $X$ is a finite simplicial complex then the open stars of vertices provide a cover of the required type, so $\phi_X$ is iso. The case of a completely general $X$ follows by homotopy invariance and a limit argument.