The pushforward of maps between smooth manifolds is defined as follows:
If $f: M \to N$ and $a \in C^\infty(N)$, then $Tf: TM \to TN$ takes $v \mapsto Tf(v)$ which operates on functions on $N$ as $Tf(v)(a) = v(f^*a) = v(a \circ f)$.
It can be shown that $T(g \circ f) = T(g) \circ T(f)$, where $f: M \to N$ and $g: N \to P$. This is one of the necessary criteria for $T$ to be a functor from the category of smooth manifolds to the category of smooth tangent bundles. The proof requires nothing more than moving some symbols around according to the definition given above. No further assumptions about $M$ or $C^\infty(M)$ are required.
But the functoriality of $T$ is just an abstract generalized statement of the chain rule of calculus, which states that the derivative of a composition of functions is the composition of the derivatives, evaluated at the appropriate points. In particular, by setting $M = N = P = \mathbf{R}$, then $f$ and $g$ become real functions of one variable, and the functoriality becomes $f(g(x))' = f'(g(x))g'(x)$. So it contains the standard chain rule of calculus as a special case.
Is this a valid proof of the chain rule? It seems to me that the proof of the chain rule requires an analytic argument resting on analytic properties of the real numbers. There should be no way around this requirement. The generalization of the chain rule should not be able to escape the requirements and give you the proof of the chain rule "for free".
Is there an assumption about the underlying spaces in the proof of functoriality that I've missed? Or does category theory really make such an important calculus trivial?
Best Answer
Let $M = N = \mathbb R$, and consider $f: M \to N$, so $f$ is a real-valued function of a real variable. Take $v = \partial_x$, based at $x_0$. Then $Tf(v)(a) = \partial_x(a\circ f)(x_0),$ for any $a:N \to \mathbb R$.
To identify this, we apply the chain rule to compute that $\partial_x(a\circ f)(x_0) = (\partial_x a)(f(x_0))\cdot f'(x_0),$ to conclude that $Tf(v)$ is equal to $f'(x_0)\partial_x$, based at $f(x_0)$.
It seems to me that you need this calculation in order to derive the classical chain rule from the the functorial version, and of course I used the classical chain rule in its derivation. Am I missing something?