To further make our case that the exterior derivative deserves its name, I say it’s a derivation of the algebra . But since it takes -forms and sends them to -forms, it has degree one instead of zero like the Lie derivative. As a consequence, the Leibniz rule looks a little different. If is a -form and is an -form, I say that:
This is because of a general rule of thumb that when we move objects of degree and past each other we pick up a sign of .
Anyway, the linearity property of a derivation is again straightforward, and it’s the Leibniz rule that we need to verify. And again it suffices to show that
If we plug this into both sides of the Leibniz identity, it’s obviously true. And then it suffices to show that we can peel off a single -form from the front of the list. That is, we can just show that the Leibniz identity holds in the case where is a -form and bootstrap it from there.
So here’s the thing: this is a huge, tedious calculation. I had this thing worked out most of the way; it was already five times as long as this post you see here, and the last steps would make it even more complicated. So I’m just going to assert that if you let be a -form and be an -form, and if you expand out both sides of the Leibniz rule all the way, you’ll see that they’re the same. To make it up to you, I promise that we can come back to this later once we have a simpler expression for the exterior derivative and show that it works then.