I’ve been taking the year-long algebraic topology sequence, which has been really great — I’ve started dipping my toes into areas that I had no prior familarity with, like the theory of model categories and simplicial sets. Michael Hopkins, who is teaching the course this year, is making the second half much more algebraic than a typical course (covering, say, characteristic classes) than usual; the goal, it seems, is to prove a Quillen equivalence of the rational homotopy category with an algebraic model category (I think the category of differential graded algebras).
One of the things you’ll notice that was reflected in the notes is that Hopkins’s style is to sketch big ideas without necessarily delving into details. Part of this is the nature of the subject. The rudiments of homotopical algebra have a similar feel to the basic proofs in homological algebra — diagram-chasing left and right, lots of abstract nonsense, proofs that may be hard digest but which are equally hard to forget. In short, the details of the foundations seem to be one of those things that one checks in the privacy of one’s room rather than in public. Just as people don’t write out full proofs of the five-lemma in class, we didn’t formally verify the construction of the homotopy category of a model category, or even prove formally the details of the model structure on simplicial sets — had we, there wouldn’t have been enough time for the fun stuff.
But, as a student, getting the details of the foundations straight in one’s mind is important. And, especially if we want to make these notes more suitable for public consumption, including full Bourbaki-esque proofs for each result would be helpful — not least because the modern, post-Whitehead style of homotopy theory where “space” means “simplicial set” seems to have rather few textbooks. There is no EGA for algebraic topology!
So, we are planning eventually to turn these notes into an open-source and collaborative project, currently named the PATH project. The pressures of the academic semester makes it unlikely that this will really get off the ground before the summer, but when it does, it should be a useful experience for anyone interested in working through the nuts and bolts of the foundations. (The plan is to have a significant amount of overlap with the CRing project. After all, you need a certain amount of algebra to do algebraic topology, and homotopical methods figure in commutative algebra in, for instance, the theory of the cotangent complex.)