§ Chain rule functorially
Let's think through the functoriality. It says that if we have two arrows which can be composed,
and -- note that it has to be because only compatible basepoint
functions can be composed.
I feel like we shouldn't use natural numbers for , but we should rather use real vector spaces.
And as for , we should replace this with where we use based
"charted" opens of a differentiable manifold. This makes the diffgeo clear!
- The first category is , whose objects are pointed subsets of Euclidean space. So, the objects are of the form . Morphisms are based smooth functions between these opens: smooth functions such that .
- The second category is whose objects are natural numbers and morphisms are matrices of dimension .
- Define a functor which sends subsets to the dimension of the space they live in: , and sends smooth functions to their Jacobian evaluated at the basepoint, .
- Functoriality asserts that the jacobian of the composition of the two functions is a matrix multiplication of the jacobians.