It starts with the observation that for a function and a vector field , the Lie derivative is and the exterior derivative evaluated at is . That is, on functions.
Next we consider the differential of a function. If we apply to it, the nilpotency of the exterior derivative tells us that we automatically get zero. On the other hand, if we apply , we get , which it turns out is . To see this, we calculate
just as if we took and applied it to .
So on exact -forms, gives zero while gives . And on functions gives , while gives zero. In both cases we find that
and in fact this holds for all differential forms, which follows from these two base cases by a straightforward induction. This is Cartan’s formula, and it’s the natural extension to all differential forms of the basic identity on functions.
We have yet another operation on the algebra of differential forms: the “interior product”. Given a vector field and a -form , the interior product is the -form defined by
That is, we just take the vector field and stick it into the first “slot” of a -form. We extend this to functions by just defining .
Two interior products anticommute: , which follows easily from the antisymmetry of differential forms. Each one is also clearly linear, and in fact is also a graded derivation of with degree -1:
where is the degree of . This can be shown by reducing to the case where and are wedge products of -forms, but rather than go through all that tedious calculation we can think about it like this: sticking into a slot of means either sticking it into a slot of or into one of . In the first case we just get , while in the second we have to “move the slot” through all of , which incurs a sign of , as asserted.