TheoremStatement: 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.

For finite-dimensional $V$ , the canonical map $V^{*} \otimes_{F} W \to {Hom}_{F} (V, W)$ is an isomorphism

Statement

Let $V$ be a finite-dimensional vector space over a field $F$ , and let $W$ be any $F$ -vector space. The bilinear map

$(ϕ, w) ⟼ [v \mapsto ϕ (v) w]$

induces a natural isomorphism

$Φ : V^{*} \otimes_{F} W ⟶ {Hom}_{F} (V, W) .$

For a basis $(v_{1}, \dots, v_{n})$ of $V$ with dual basis $(v_{1}^{*}, \dots, v_{n}^{*})$ , its inverse is

$Ψ (T) = \sum_{i = 1}^{n} v_{i}^{*} \otimes T (v_{i}) .$

The empty sum gives the assertion when $V = 0$ .

Facts & Assumptions

Given: A finite-dimensional $F$ -vector space $V$ , an $F$ -vector space $W$ , and a basis $(v_{i})_{1 \leq i \leq n}$ of $V$ with dual family $(v_{i}^{*})$ .

[L1]

Bilinear maps from $V^{*} \times W$ induce unique homomorphisms from $V^{*} \otimes_{F} W$ (Universal property of the tensor product for balanced maps into abelian groups).

[L2]

Tensor products of bases have product basis (The elementary tensors of two bases form the product basis of the tensor product).

[L3]

Over the commutative field $F$ , ${Hom}_{F} (V, W)$ is an $F$ -module under pointwise scalar multiplication (The $R$ -module ${Hom}_{R} (M, N)$ over a commutative ring).

[L4]

The algebraic dual is $V^{*} = L (V, F)$ (Linear functionals and the algebraic dual $V^{*} = L (V, F)$ ).

[L5]

The dual family of a finite basis is a basis of $V^{*}$ (The dual family of a finite basis is a basis of the dual space, with the same dimension).

Proof

technique · direct

1.1

The map $(ϕ, w) \mapsto [v \mapsto ϕ (v) w]$ is bilinear, so [L1] gives an $F$ -linear map $Φ : V^{*} \otimes_{F} W \to {Hom}_{F} (V, W)$ .

givenL1L3L4

1.2

Define $Ψ (T) = \sum_{i} v_{i}^{*} \otimes T (v_{i})$ . This is an $F$ -linear map because evaluation and the finite sum are linear in $T$ .

givenL3L5construct

2.1

For $T \in {Hom}_{F} (V, W)$ and $v = \sum_{i} v_{i}^{*} (v) v_{i}$ , one has $(Φ Ψ (T)) (v) = \sum_{i} v_{i}^{*} (v) T (v_{i}) = T (v)$ , so $Φ Ψ$ is the identity.

step 1.1step 1.2L5algebra

2.2

For an elementary tensor $ϕ \otimes w$ , one has $Ψ Φ (ϕ \otimes w) = \sum_{i} v_{i}^{*} \otimes ϕ (v_{i}) w = (\sum_{i} ϕ (v_{i}) v_{i}^{*}) \otimes w = ϕ \otimes w$ , because $(v_{i}^{*})$ is the dual basis; elementary tensors generate, so $Ψ Φ$ is the identity.

step 1.1step 1.2L2L5algebra

2.3

The map $Φ$ is natural in $W$ : for $h : W \to W^{'}$ , both routes send $ϕ \otimes w$ to the map $v \mapsto ϕ (v) h (w)$ . It is contravariantly natural in $V$ : for $a : V^{'} \to V$ , both routes send $ϕ \otimes w$ to $[v^{'} \mapsto ϕ (a (v^{'})) w]$ . Equality on elementary tensors gives both naturality squares.

step 1.1L1algebra

3.1

Thus $Φ$ is a natural isomorphism with inverse $Ψ$ . If $V = 0$ , its basis and dual basis are empty, both $V^{*} \otimes_{F} W$ and ${Hom}_{F} (V, W)$ are zero, and the same formulas are the unique inverse maps.

step 2.1step 2.2step 2.3L2L5∎

Depends on

Used by

Under End_F(V)≅ V^*⊗_FV, tensor contraction is the trace Corollary

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 57 results over 14 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)

For finite-dimensional VV, the canonical map V∗⊗FW→Hom⁡F(V,W)V∗⊗F​W→HomF​(V,W) is an isomorphism