Searching for an unabridged proof of “The Basic Theorem of Morse Theory”

Steven Smale labels the following statement "The Basic Theorem of Morse Theory" in A Survey of some Recent Developments in Differential Topology:

Let f be a $C^\infty$ function on a closed manifold with no critical points on $f^{-1}[-\epsilon,\epsilon]$ except k nondegenerate ones on $f^{-1}(0)$, all of index $s$. Then $f^{-1}[-\infty,\epsilon]$ is diffeomorphic to $X(f^{-1}[-\infty,-\epsilon];f_1,\ldots,f_k;s)$ (for suitable fi.

Here $X(M;f;s)$ for $f\colon\,(\partial D^s)\times D^{n-s}\to M$ is M with an s-handle attached by f.
Where can I find a complete proof of this theorem, with all the t's crossed and i's dotted? Textbooks (Milnor, Matsumoto) only seem to prove homology/homotopy versions of the above statement, usually with substantial steps to be filled in by the reader. I nosed around some old papers for a few hours, (surely Smale himself proved it somewhere!) but to no avail. If I were to continue to search, no doubt I could eventually turn it up (there are a finite number of differential topology papers written 1958-1962, which is when I assume it was proven), but because I think that this question might be of wider interest, and to save me a lot of time, I'd like to ask:

Where can I find a complete unabridged proof of "The Basic Theorem of Morse Theory"? (in fact I care only about low dimensions) What is the original paper, and is there a textbook exposition of it anywhere?
-
I'm leaving this as a comment since I don't have the text available to confirm. "From Calculus to Cohomology" by Madsen and Tornehave has a very detailed treatment of basic Morse theory in the chapter on the Poincare-Hopf theorem, and I seem to recall that the book has an appendix which is specifically dedicated to hammering out all the details of what you want. It might be worth a look, anyway. – Paul Siegel Jul 14 '11 at 13:07
The original paper was: Generalized Poincaré conjecture in dimensions greater than 4, Annals of Mathematics, 74 (1961), pp. 391--406. The Kosinski book Johannes mentions and Milnor's h-cobordism theorem lectures are the best textbook references that I'm aware of. Smale's papers tend to have a lot of typos, and he also runs into several "smoothing the corner" problems that Kosinski avoids. – Ryan Budney Jul 14 '11 at 13:56
@Ryan I wasn't able to figure out where to look in Smale... I mean, definitely the core ideas are there, but Page 403 only gives a "proof sketch" of the result, without any details at all. – Daniel Moskovich Jul 14 '11 at 19:10
@Ryan isn't Milnor's h-cobordism treatment a "homotopy proof" again? Anyway, Kosinski + Palais are beautiful and simple, so now I'm happy... but I wish I understood the history better! There's also Wallace "Modifications and cobounding manifolds" Canad. J. Math. 12 (1960) 503-528, who proves a related-looking statement in Section 4. – Daniel Moskovich Jul 15 '11 at 18:23
@Paul Siegel: Madsen-Tornehave turns out to be the homotopy version also (but a nice and slightly different version). Goresky-MacPherson prove the statement in the stratified setting. The proof is a 100 page tour-de-force. The original proof appears to be Palais. – Daniel Moskovich Jun 1 '12 at 5:24

R.Palais, Morse theory on Hilbert manifolds (main Theorem of §12). As you will see, in the infinite dimensional setting the construction looses nothing in clearness.

-

Kosinski, ''Differential manifolds'', Chapter VII, section 2. He gives a detailed proof in the case of just one critical point.

-
BANG!! This is exactly what I was looking for! Do you know the history of the argument? The construction of an explicit diffeomorphism can't be due to Kosinski; it must be from the late 50's or early 60's surely! – Daniel Moskovich Jul 13 '11 at 21:05
I think the proof in my paper "Morse Theory on Hilbert Manifolds" (referenced and linked to in Pietro Majer's answer) was probably the first place that the smooth handle attaching theorem was proved---it was certainly the first place that it was proved for Hilbert manifolds. Until then people settled for a homotopy version. – Dick Palais Jul 14 '11 at 15:53
I wish I could accept 2 answers- then I would also have accepted this one. Kosinski's treatment was really clear and helpful- thanks! – Daniel Moskovich Jul 14 '11 at 17:57
Incidentally, Kosinski's book is available in electronic form: gen.lib.rus.ec/… – Dmitri Pavlov Jan 25 '12 at 15:43

My recollection is that Milnor's proof gives exactly what you are asking. In fact, see the remark on the bottom of page 17 of his book.

-
This is what I was looking at, but it looks like a homotopy proof (although it can surely be upgraded). Theorem 3.2 Page 14 claims only homotopy equivalence, and Assertion 4 Page 18 pushes along horizontal lines... does this preserve smoothness? I don't follow the details of his argument (maybe I'm just not reading carefully). Also, Remark 3.3 on page 19 confuses me... what's the argument which "unmixes" the various handles? – Daniel Moskovich Jul 13 '11 at 20:10
No it really is a diffeomorphism proof. Assume for simplcity that there is a single critical point $p$ with $f(p)=c$. The idea is that $M^a \cup H$ is a deformation retract of $M^b$ where $a<c<b$ are regular values and $c$ is the only critical value in the interval $[a,b]$ (where $M^b := f^{-1}((-\infty,b])$) . Then theorem 3.1 implies that $M^a \cup H$ is diffeomorphic to $M^b$ (since the gradient field on $M^b$ had no zeros on the complement of $M^a \cup H$). – John Klein Jul 13 '11 at 21:04
As for as "unmixing the handles" goes, you can change the function slightly near the critical points so that all the critical points have distinct critical values. That will do it. – John Klein Jul 13 '11 at 21:05
I believe you, but I still don't get it... H is <i>defined</i> to be $F^{-1}(-\infty,a]-M^{a}$. Why is this diffeomorphic to an s-handle? Don't you need a smooth version of Assertion 4? (which it turns out is in Kosinski, as Johannes Ebert points out, but I can't see how to upgrade the argument in Milnor, if indeed it needs upgrading...) I'm sure I'm just missing something very simple and obvious... – Daniel Moskovich Jul 13 '11 at 21:26

Dear Daniel Moskovich, I am answering just the last part of your question. As you said this could be useful to many others beyond the original poster, so I report my experience hoping to be useful.

The only textbook on differentiable manifolds including a proof of the basic theorem in Morse Theory, that until now I have met, is "Differentiable manifolds, Second Edition" by Lawrence Conlon.

His presentation of Morse Theory is distributed on sections 2.9.B, 3.10, and 4.2, and is closely inspired by Milnor's book.
In a certain way it requires the active cooperation of the reader by completing just some minor details, but at the end this work is doubly rewarding, it renforces your previous knowledge and assures that you grasp the content of basic morse theory.

Edit: I have found that Conlon leaves apart just to recognize that a certain manifold is a $\lambda$-handle, and for this result he refers to S.Smale "Generalized Poincarè's conjecture in dimensions greater than four"

-
Do you know where in Smale? (I was unsuccessful finding it) On page 403, there seems only to be a "proof sketch"... also, I didn't understand how corners were being treated. I mean, somehow the "idea" is in Smale, but where is the proof? – Daniel Moskovich Jul 14 '11 at 19:07
Dear Daniel Moskovich, it seems to me that Smale says that the proof of theorem 5.1 is only sketched because its proof closely follows that of the Handlebody Theorem 1.2. Sections 2,3, and 4 are devoted to prove theorem 1.2. About straightening the angle along the corners, on page 396 in the first paragraph of §1, Smale says that he refers for such a procedure to Milnor[10] "Differentiable manifolds which are homotopy sheres". – Giuseppe Tortorella Jul 14 '11 at 19:31
Thanks! But I'm still having difficulty understanding. The corners I am concerned about are when you attach the cell, especially if there are many handles (one is "easy"). So what I'm looking for is where he shows that "what you contract the saddle to" is diffeomorphic to a handle $D^s\times D^{n-s}$ (smoothed somehow), and that this diffeomorphism extends over the rest of the manifold. Could you give a page reference for this step? – Daniel Moskovich Jul 14 '11 at 19:56
@Daniel Moskovich: For your first point of interest look at the sketched proof of theorem 6.2(that is your original statement), so $f^{-1}([-\infty,\varepsilon])$ is the union of $f^{-1}([-\infty,-\varepsilon])$ and of $f^{-1}([-\varepsilon,\varepsilon])$ along their common boundary $f^{-1}(\varepsilon)$, and $f^{-1}([-\varepsilon,\varepsilon])$ is diffeomorfic to $D^\lambda\times D^{n-\lambda}$, So $f^{-1}([-\infty,\varepsilon])$ is already an handlebody. For your second point of interest, starting §1, Smale says: the smooth structure obtained straightening the angles is unique up to diffeo. – Giuseppe Tortorella Jul 14 '11 at 21:18
Thanks you for your answer. I'm probably just missing something, but I can't find the relevant details written down there at these critical steps. So (although I might be wrong) it looks to me like Smale's proof is a "sketch proof", which is all it claims to be. – Daniel Moskovich Jul 15 '11 at 18:19