Well now we know how to translate -forms by pulling back, and thus we can define another Lie derivative:
What happens if is a -form — a function ? We check
That is, the Lie derivative by acts on exactly the same as the vector field does itself.
I also say that the Lie derivative by is a degree-zero derivation of the algebra . That is, it’s a real-linear transformation, and it satisfies the Leibniz rule:
for any -form and -form . Linearity is straightforward, and given linearity the Leibniz rule follows if we can show
for -forms . Indeed, we can write and as linear combinations of such - and -fold wedges, and then the Leibniz rule is obvious.
So, let us calculate:
So we see how we can peel off one of the -forms. A simple induction gives us the general case.
We’ve just seen that smooth real-valued functions are differential forms with grade zero. We also know that functions pull back along smooth maps; if is a smooth function on an open subset and if is a smooth map, then is a smooth function — .
It turns out that all -forms pull back in a similar way. But the “value” of a -form doesn’t only depend on a point, but on vectors at that point. Functions pull back because smooth maps push points forward. It turns out that vectors push forward as well, by the derivative. And so we can define the pullback of a -form :
Here is a -form on a region , is a point in , and the are vectors in . Since the differential is a linear function and is a multilinear function on , is a multilinear function on , as asserted.
This pullback is a homomorphism of graded algebras. Since it sends -forms to -forms, it has degree zero. To show that it’s a homomorphism, we must verify that it preserves addition, scalar multiplication by functions, and exterior multiplication. If and are -forms in , we can check
so . Also if we can check
As for exterior multiplication, we will use the fact that we can write any -form as a linear combination of -fold products of -forms. Thus we only have to check that
Thus preserves the wedge product as well, and thus gives us a degree-zero homomorphism of the exterior algebras.