NB: This entry involves hand-wavey maths-abuse.
I've been reading a book on differential geometry. It's the first maths book I've read (other than an introduction to category theory, which is kinda cheating) that actually has commutivity diagrams. I didn't really see why category theory might have come out of geometry, but it does seem far more understandable, having seen all these maps between different spaces, and mathematical equivalents of 'if you do this in over there, it's just like doing that over here'.
So, geometry's given category theory to computer science. I'd love it if computer science could give really clear types and anonymous functions to geometry. For example, what actually is a differential form? To keep it simple, let's look at a differential 1-form... these are standalone things like 'dx'. A-level maths said that a 'dx' isn't an actual thing, it's just a bit of notational convention in an integral, be careful, etc. At this level, it's made into a thing...
So, what is it? Let's say we have a manifold U. At each point of U we have a tangent space, which is a vector space of all the tangents at a particular point. How do we tie this tangent space to the underlying manifold? We can make it the space of functions which take derivatives in particular directions - i.e. the things normally written 'd/dx', for some direction x. That is, it's a vector space of functions from points to real values to points to real values. In Haskell type terms, this is a space of (Point -> Real) -> (Point -> Real). Given each point in U has its own tangent space, the overall type is Point -> (Point -> Real) -> (Point -> Real). Of course, in the text the parameters and abstractions and all the rest of it are done in implicit mathsy form, which I think makes things a little more obscure for no good reason.
What's a differential 1-form? It's a member of the cotangent spaces - the dual of the tangent spaces. Does this mean it's of type (Point -> (Point -> Real) -> (Point -> Real)) -> Whatever? No, it's actually a function from point to member of the vector space that is the dual of the tangent space at that particular point. In other words, this whole dual business is being done in a lifted world, if you were writing Haskell. The type is Point -> (Point -> (Point -> Real) -> (Point -> Real)) -> Whatever. What is 'Whatever'? Well, it's the scalar type of the vector space we're looking at, so for a fairly dull manifold, it'll be Real: Point -> (Point -> (Point -> Real) -> (Point -> Real)) -> Real. Still pretty impenetrable, but perhaps the start of an explanation.
What is 'dx' supposed to be? It's supposed to be the thing that when given a member of the tangent space projects out the d/dx component of it. How can we do that? Well, I guess we can just make a function which is linearly increasing in the direction of interest, but is otherwise flat, feed it into our derivative-taking function, and then evaluate it at an arbitrary point (the resulting function should be the constant function, for a given tangent space):
diff_1_form point tangent_space =
tangent_space_elt my_fn zero
where
tangent_space_elt = tangent_space point
my_fn = -- Function linearly increasing in our preferred direction
zero = -- Zero element of vector space
Other function could be substituted in, I guess. Is this correct and accurate, or have I missed something? I'm not sure. For all the formal notation, I'm still not sure if I've extracted the true meaning correctly!
Update! More re-reading reveals further details. The smoothly varying tangent space thing is called a vector field, and the point used to select the derivative-taking functor from the tangent space is the same point used to evaluate it. That is, the overall type is, depending on how you look at it, (Point -> Real) -> (Point -> Real), or Point -> (Point -> Real) -> Real - that is, you can look at it as a thing that transforms functions of the form (Point -> Real), or as, for each point in the manifold, a thing that maps functions to real numbers (specifically, the derivative of that function in a particular direction at that point).
Interestingly, the second type means that the tangent space is effectively over certain functions of the type '(Point -> Real) -> Real', which already looks like the dual of some vector space of functions of type 'Point -> Real'. Sticking together the element of the tangent space with the cotangent space is then basically the idea of passing this function to the tangent space functor. Indeed, the definition of the differential operator 'd' is exactly that:
Given a function f : Point -> Real, and a vector field X : (Point -> Real) -> (Point -> Real), d : (Point -> Real) -> ((Point -> Real) -> (Point -> Real)) -> (Point -> Real) is the surprisingly obvious ((d f) . X) x = X(f). (No, I'm still not sure I've got it exactly right!) For things beyond 1-forms it's more complicated.
Posted 2011-04-22.