PropositionStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-09-01

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.

Linear pullback respects tensor products and permutations

Statement

Let $V$ and $W$ be finite-dimensional real vector spaces, let $A : V \to W$ be linear, let $S$ and $T$ be covariant tensors on $W$ of degrees $k$ and $ℓ$ , respectively, and let $σ \in S_{ℓ}$ . Then

$A^{*} (S \otimes T) = A^{*} S \otimes A^{*} T, A^{*} (σ \cdot T) = σ \cdot (A^{*} T) .$

Facts & Assumptions

Given: Finite-dimensional real vector spaces $V, W$ , a linear map $A : V \to W$ , covariant tensors $S, T$ on $W$ of degrees $k, ℓ$ , and a permutation $σ \in S_{ℓ}$ .

[F1]

Pullback of a covariant tensor substitutes $A v_{i}$ into every slot (The pullback of a covariant tensor by a linear map).

[F2]

Tensor product multiplies the factor values on concatenated arguments, and the permutation action reorders the arguments (The tensor product of multilinear tensors, The permutation action on covariant tensors).

Proof

technique · direct

1.1

Evaluating on $v_{1}, \dots, v_{k + ℓ}$ and using [F1] and [F2], $A^{*} (S \otimes T) (v_{1}, \dots, v_{k + ℓ}) = (S \otimes T) (A v_{1}, \dots, A v_{k + ℓ}) = S (A v_{1}, \dots, A v_{k}) T (A v_{k + 1}, \dots, A v_{k + ℓ}),$ which is exactly $(A^{*} S \otimes A^{*} T) (v_{1}, \dots, v_{k + ℓ})$ .

F1F2givenalgebra

1.2

Likewise, $A^{*} (σ \cdot T) (v_{1}, \dots, v_{ℓ}) = (σ \cdot T) (A v_{1}, \dots, A v_{ℓ}) = T (A v_{σ (1)}, \dots, A v_{σ (ℓ)}),$ which equals $(σ \cdot A^{*} T) (v_{1}, \dots, v_{ℓ})$ .

F1F2givenalgebra

2.1

Therefore linear pullback respects tensor products and permutations.

step 1.1step 1.2∎

Depends on

Used by

Pullback of covariant tensors is smooth and functorial Proposition
Pullback of forms is smooth functorial and preserves wedges Proposition

Dependency tree · two levels

5 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)