Tensor derivation (source code)

= Tensor derivation
{title2=$D$}

A <tensor derivation> is a real-linear operation preserving every tensor type, obeying the tensor-product <Leibniz rule>, and commuting with every <tensor contraction>. A derivation $D$ of <smooth functions> and a real-linear operator on <vector fields> satisfying $D(fY)=fDY+(Df)Y$ extend uniquely to a <tensor derivation>. On a <differential one-form> it must satisfy
$$
(D\omega)(Y)=D(\omega(Y))-\omega(DY).
$$
This expression is linear over <smooth functions> in $Y$. In a local frame $De_a=A^b{}_ae_b$, the dual rule is $D\epsilon^a=-A^a{}_b\epsilon^b$. Apply the product rule to every coefficient and frame factor to define the extension; these dual signs cancel under contraction. Frame changes agree by differentiating the inverse <matrix>. Cutoffs prove locality and hence uniqueness from local expansions.