CorollaryStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passaudited 2026-08-16

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.

Under ${End}_{F} (V) ≅ V^{*} \otimes_{F} V$ , tensor contraction is the trace

Statement

Let $V$ be a finite-dimensional vector space over $F$ . Under the isomorphism

$V^{*} \otimes_{F} V ⟶ {End}_{F} (V), ϕ \otimes v ⟼ [x \mapsto ϕ (x) v],$

the contraction map $c : V^{*} \otimes_{F} V \to F$ , defined by $c (ϕ \otimes v) = ϕ (v)$ , corresponds to the trace $T \mapsto tr (T)$ .

Facts & Assumptions

Given: A finite-dimensional $F$ -vector space $V$ and the canonical Hom-tensor isomorphism with $W = V$ .

[L1]

The canonical isomorphism sends $ϕ \otimes v$ to the rank-one endomorphism $x \mapsto ϕ (x) v$ (For finite-dimensional $V$ , the canonical map $V^{*} \otimes_{F} W \to {Hom}_{F} (V, W)$ is an isomorphism).

[L2]

The trace of an endomorphism is the sum of the diagonal entries of its matrix in any basis, and is zero in dimension zero (The basis-independent trace of an endomorphism of a finite-dimensional vector space).

[L3]

A bilinear pairing induces a unique linear map from a tensor product (Universal property of the tensor product for balanced maps into abelian groups).

Proof

technique · direct

1.1

Evaluation $(ϕ, v) \mapsto ϕ (v)$ is bilinear, so [L3] induces the linear contraction map $c : V^{*} \otimes_{F} V \to F$ with $c (ϕ \otimes v) = ϕ (v)$ .

givenL3

1.2

Choose a basis $(e_{1}, \dots, e_{n})$ of $V$ and write $v = \sum_{j} v_{j} e_{j}$ . For $T_{ϕ, v} (x) = ϕ (x) v$ , the coefficient of $e_{i}$ in $T_{ϕ, v} (e_{i})$ is $ϕ (e_{i}) v_{i}$ .

givenL1algebra

1.3

If $V = 0$ , the tensor product and endomorphism space are zero and both maps are the zero map by [L2].

L1L2L3

2.1

By [L2], $tr (T_{ϕ, v}) = \sum_{i} ϕ (e_{i}) v_{i} = ϕ (\sum_{i} v_{i} e_{i}) = ϕ (v) = c (ϕ \otimes v)$ .

step 1.1step 1.2L2algebra

3.1

Matrix diagonal sums are linear, so trace is linear by [L2]. Therefore trace after [L1] and contraction are linear maps inducing the same bilinear pairing by step 2.1; uniqueness in [L3] proves that they agree everywhere.

step 1.1step 2.1L1L2L3algebra

4.1

Thus tensor contraction is precisely trace under the canonical isomorphism, including the zero-dimensional case.

step 3.1step 1.3∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 57 results over 10 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.

Sources

C. Dennis, Week 1 recap on tensor products (standard reference, not scraped)

Under End⁡F(V)≅V∗⊗FVEndF​(V)≅V∗⊗F​V, tensor contraction is the trace