ac.commutative algebra - What is the insight of Quillen's proof that all projective modules over a polynomial ring are free?

Here is a summary of what I learned from a nice expository account by Eisenbud (written in French), can be found as number 27 here.

First, one studies a more general problem: Let $A$ be a Noetherian ring, $M$ a finite presented projective $A[T]$-module. When is $M$ extended from $A$, meaning there is $A$-module $N$ such that $M = A[T]otimes_AN$?

The proof can be broken down to 2 punches:

Theorem 1 (Horrocks) If $A$ is local and there is a monic $f in A[T]$ such that $M_f$ is free over $A_f$, then $M$ is $A$-free

(this statement is much more elementary than what was stated in Quillen's paper).

Theorem 2 (Quillen) If for each maximal ideal $m subset A$, $M_m$ is extended from $A_m[T]$, then $M$ is extended from $A$

(on $A$, locally extended implies globally extended).

So the proof of Serre's conjecture goes as follows: Let $A=k[x_1,cdots,x_{n-1}]$, $T=x_n$, $M$ projective over $A[T]$. Induction (invert all monic polynomials in $k[T]$ to reduce the dimension) + further localizing at maximal ideals of $A$ + Theorem 1 show that $M$ is locally extended. Theorem 2 shows that $M$ is actually extended from $A$, so by induction must be free.

Eisenbud note also provides a very elementary proof of Horrocks's Theorem, basically using linear algebra, due to Swan and Lindel (Horrocks's original proof was quite a bit more geometric).

As Lieven wrote, the key contribution by Quillen was Theorem 2: patching. Actually the proof is fairly natural, there is only one candidate for $N$, namely $N=M/TM$, so let $M'=A[T]otimes_AN$ and build an isomorphism $M to M'$ from the known isomorphism locally.

It is hard to answer your question: what did Serre miss (-:? I don't know what he tried? Anyone knows?