The interior product is defined to be the contraction of a differential form with a vector field. Thus if is a vector field on the manifold then is the map which sends a -form to the -form defined by the property that for any vector fields
When is a scalar field (0-form), by convention.
The interior product is the unique antiderivation of degree −1 on the exterior algebra such that on one-forms where is the duality pairing between and the vector Explicitly, if is a -form and is a -form, then The above relation says that the interior product obeys a graded Leibniz rule. An operation satisfying linearity and a Leibniz rule is called a derivation.
If in local coordinates the vector field is given by
then the interior product is given by where is the form obtained by omitting from .
By antisymmetry of forms, and so This may be compared to the exterior derivative which has the property
The interior product with respect to the commutator of two vector fields satisfies the identity Proof. For any k-form , and similarly for the other result.
The interior product relates the exterior derivative and Lie derivative of differential forms by the Cartan formula (also known as the Cartan identity, Cartan homotopy formula[2] or Cartan magic formula):
Since vector fields are locally integrable, we can always find a local coordinate system such that the vector field corresponds to the partial derivative with respect to the first coordinate, i.e., .
By linearity of the interior product, exterior derivative, and Lie derivative, it suffices to prove the Cartan's magic formula for monomial -forms. There are only two cases:
The exterior derivative is an anti-derivation on the exterior algebra. Similarly, the interior product with a vector field is also an anti-derivation. On the other hand, the Lie derivative is a derivation.
The anti-commutator of two anti-derivations is a derivation.
To show that two derivations on the exterior algebra are equal, it suffices to show that they agree on a set of generators. Locally, the exterior algebra is generated by 0-forms (smooth functions ) and their differentials, exact 1-forms (). Verify Cartan's magic formula on these two cases.