PropositionStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passaudited 2026-09-06

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

The coordinate formula for the Lie derivative of a contravariant tensor

Statement

Let $M$ be a smooth manifold, $(U, x^{1}, \dots, x^{n})$ a smooth chart, $X$ a smooth vector field on $M$ , and $k \geq 0$ . For a smooth contravariant $k$ -tensor field $T = T^{i_{1} \dots i_{k}} \partial_{i_{1}} \otimes \dots \otimes \partial_{i_{k}}$ on $U$ , $(L_{X} T)^{i_{1} \dots i_{k}} = X^{j} \partial_{j} T^{i_{1} \dots i_{k}} - \sum_{a = 1}^{k} (\partial_{j} X^{i_{a}}) T^{i_{1} \dots j \dots i_{k}} .$

Repeated coordinate indices are summed from $1$ to $n$ ; the $j$ in the $a$ th correction term replaces the $a$ th index. For $k = 0$ the correction sum is empty and the formula reads $L_{X} T = X (T)$ .

Facts & Assumptions

Given: The smooth manifold, chart, smooth vector field $X$ , and smooth tensor field $T$ in the statement.

[F1]

The preceding result states that The Lie derivative obeys $L_{X} (S \otimes T) = (L_{X} S) \otimes T + S \otimes (L_{X} T)$ and commutes with every natural contraction. (The Lie derivative is a derivation of the tensor algebra).

[F2]

On smooth functions, $L_{X} f = X f$ , and on vector fields, $L_{X} Y = [X, Y]$ (Tensor Lie derivative agrees with $X$ on functions and bracket on vector fields).

[F3]

The coordinate formula for $[X, Y]$ differentiates the coordinate coefficients of $X$ and $Y$ (Coordinate formula for the Lie bracket).

Proof

technique · direct

1.1

Apply the tensor derivation law to the coordinate tensor expansion of $T$ .

F1given

2.1

The coordinate bracket formula and $L_{X} \partial_{i} = [X, \partial_{i}]$ give $L_{X} \partial_{i} = - (\partial_{i} X^{j}) \partial_{j}$ . The coefficient derivative is $X^{j} \partial_{j} T^{i_{1} \dots i_{k}}$ , and applying the preceding identity in each tensor slot supplies the displayed minus terms.

F2F3step 1.1given∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

15 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

John M. Lee, Introduction to Smooth Manifolds, 2nd ed. (standard reference, not scraped)