Today I've been trying to nail down a bug that some of
lambdacalculus's twelf code is eliciting in my type-checker.I've also been reading a book called "Singular Homology Theory" and understanding a surprising amount of it. It's very satisfying, because now the whole story — at least a whole story — from calculus up to category theory makes sense to me. Indeed the introduction of the book is a very good exercise in this kind of "storytelling". It starts with people wondering when a vector field arises as the gradient of some function, a very natural calculus-y sort of question — in particular, very natural for someone interested in applying calculus to physics: that function is a potential function. If the vector field looks like P(x,y)ihat + Q(x,y)jhat, then a necessary condition is dP/dy = dQ/dx, but this isn't sufficient. It might be that you have a hole at the origin, and taking a path integral around the hole back to your starting point gives you a nonzero result, a violation of potential-conservation. This is a jumping-off point for homology theory: there is a discrepancy in this setup between the cycles (i.e. closed oriented paths) you can integrate along, and the paths that arise as boundaries of regions that lie entirely in the vector field's domain of definition. The question is, how can we compute that discrepancy? The answer --- generalized over all dimensions n --- takes the form of the definition of the (abelian) singular homology groups Hn.
So the "story" takes us from calculus on to topology (or at least the study of metric spaces) and basic algebra of abelian groups --- not necessarily the historical order of things. The category theory comes in because Hn is a fantastic example of a functor. Not only does it take a topological space X to an abelian group Hn(X), it takes any continuous map f : X → Y to a homomorphism Hn(f) : Hn(X) → Hn(Y). What's more, there's something tantalizingly 2-categorical going on as well. If f, g : X → Y are homotopic to one another, then Hn(f) = Hn(g). So if we put a homotopy 2-categorical structure on Top to get HTop, and put only trivial 2-cells into Ab, then Hn is a 2-functor, HTop → Ab. In particular it maps homotopy equivalences to equivalences, which in the trivial 2-category are just isomorphisms. If we can compute the homology groups of two spaces and they come out different, we get that they are not only nonhomeomorphic, but of different homotopy classes!
Just today I almost barely got to understand one of the prerequisites for the excision theorem: the idea of the exact homology sequence of a pair of spaces. If A is a subspace of X, it's easy to hack up maps i and j so that
Hn(A) →i Hn(X) →j Hn(X,A)
is exact (i.e. the kernel of j is the image of i) but you have to be a little more sneaky to cook up the "boundary operator of the pair (X,A)" ∂ that goes Hn(X,A) → Hn-1(A). One amazing thing is that the is, js, and ∂s make one huge exact sequence that zips around the absolute and relative homology groups at each dimension. The other, though, for which the book resorted to mere suggestive italics on the word "natural", is that there's an honest-to-goodness natural transformation,
∂ : (λ(X,A).Hn(X,A)) → (λ(X,A).Hn-1(A)) : RTop → Ab
where RTop is the category of dependent pairs consisting of a toplogical space X and a subspace A of X, where the maps are continuous maps taking the designated subspace of the domain into a subset of the designated subspace of the codomain.
About the only thing I'm still waiting and hoping to see is some adjunction fireworks.
Doing some miscellaneous reading about religions and mythologies still. Fascinating stuff.
Had a good time on the piano in the OSC, since the had the heat cranked up really high and my hands weren't freezing as I tried to play.