LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-6.1-sol)audited 2026-10-08

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.

Finite tensor duality and basis-independent coevaluation

Statement

Let $V, W$ be finite-dimensional $k$ -vector spaces.

The bilinear map $V^{*} \times W^{*} \to (V \otimes W)^{*}$ , $(f, g) \mapsto [v \otimes w \mapsto f (v) g (w)]$ , induces an isomorphism $V^{*} \otimes W^{*} \to (V \otimes W)^{*}$ . For ordered bases $(v_{1}, \dots, v_{m})$ of $V$ , $(w_{1}, \dots, w_{n})$ of $W$ with dual bases $(v_{i}^{*})$ , $(w_{j}^{*})$ , the image of $v_{i}^{*} \otimes w_{j}^{*}$ is the dual basis vector of $v_{i} \otimes w_{j}$ in the product basis of $V \otimes W$ .
For every ordered basis $(v_{1}, \dots, v_{n})$ of $V$ the element $\sum_{i = 1}^{n} v_{i}^{*} \otimes v_{i} \in V^{*} \otimes V$ is independent of the basis and corresponds to ${i d}_{V}$ under the isomorphism $V^{*} \otimes V \to Hom (V, V)$ , $f \otimes v \mapsto [x \mapsto f (x) v]$ (For finite-dimensional $V$ , the canonical map $V^{*} \otimes_{F} W \to {Hom}_{F} (V, W)$ is an isomorphism). Its image under $σ_{V^{*}, V}$ is the corresponding element $\sum_{i} v_{i} \otimes v_{i}^{*}$ of $V \otimes V^{*}$ .
The evaluation $e v : V^{*} \otimes V \to k$ , $f \otimes v \mapsto f (v)$ , and the coevaluation $c o e v : k \to V \otimes V^{*}$ , $1 \mapsto \sum_{i} v_{i} \otimes v_{i}^{*}$ , are independent of the basis and satisfy $({i d}_{V} \otimes e v) \circ α_{V, V^{*}, V} \circ (c o e v \otimes {i d}_{V}) = {i d}_{V}$ and $(e v \otimes {i d}_{V^{*}}) \circ α_{V^{*}, V, V^{*}}^{- 1} \circ ({i d}_{V^{*}} \otimes c o e v) = {i d}_{V^{*}}$ , the unit isomorphisms $k \otimes V ≅ V$ , $V \otimes k ≅ V$ being understood.

Facts & Assumptions

Given: A field $k$ , finite-dimensional $k$ -vector spaces $V, W$ , ordered bases $(v_{1}, \dots, v_{m})$ of $V$ and $(w_{1}, \dots, w_{n})$ of $W$ with their dual bases, and ordered bases of $V$ written $(v_{1}, \dots, v_{n})$ .

[F1]

The tensor product conventions: $M \otimes N$ is the tensor product over $k$ with its universal property, every element is a finite sum of elementary tensors, the unit isomorphisms $λ_{N} : k \otimes N \to N$ and $ρ_{M} : M \otimes k \to M$ are given by $r \otimes n \mapsto r n$ and $m \otimes r \mapsto m r$ , and tensor powers are left-associated with $V^{\otimes 0} = k$ (Scalars, tensor powers, the empty tensor, opposite algebras and finite sums).

[F2]

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

[F3]

The dual family $(b^{*})_{b \in B}$ of a basis is defined by $b^{*} (c) = δ_{b c}$ and linear extension (The dual family $(b^{*})_{b \in B}$ associated to a Hamel basis $B$ , defined by $b^{*} (c) = δ_{b c}$ ).

[F4]

If $B = (b_{1}, \dots, b_{n})$ is a basis of a finite-dimensional space, its dual family $B^{*}$ is a basis, so it is linearly independent and spans the dual space (The dual family of a finite basis is a basis of the dual space, with the same dimension).

[F5]

The elementary tensors of two bases form a basis of the tensor product (The elementary tensors of two bases form the product basis of the tensor product).

[F6]

Coordinates with respect to an ordered basis are unique, so $x = \sum_{i} λ_{i} b_{i}$ with $λ$ the coordinate list of $x$ ; for the dual basis of a basis this gives $f = \sum_{i} f (b_{i}) b_{i}^{*}$ and $x = \sum_{i} b_{i}^{*} (x) b_{i}$ (A finite list $v : n \to V$ is an ordered basis if and only if every $x \in V$ equals $\sum_{i < n} λ_{i} v_{i}$ for exactly one $λ : n \to F$ ; those scalars are the coordinates of $x$ in that ordered basis).

[F7]

For finite-dimensional $V$ the map $Φ : V^{*} \otimes W \to Hom (V, W)$ , $ϕ \otimes w \mapsto [y \mapsto ϕ (y) w]$ , is an isomorphism with inverse $Ψ (T) = \sum_{i} v_{i}^{*} \otimes T (v_{i})$ (For finite-dimensional $V$ , the canonical map $V^{*} \otimes_{F} W \to {Hom}_{F} (V, W)$ is an isomorphism).

[F8]

The symmetry and associativity isomorphisms act on elementary tensors by $σ_{M, N} (m \otimes n) = n \otimes m$ and $α_{L, M, N} ((l \otimes m) \otimes n) = l \otimes (m \otimes n)$ (Symmetry and associativity isomorphisms for tensor products over a commutative ring).

[F9]

The unit isomorphisms $λ_{N} : k \otimes N \to N$ and $ρ_{M} : M \otimes k \to M$ are isomorphisms with the stated formulas (The regular module is a tensor unit: $R \otimes_{R} N ≅ N$ and $M \otimes_{R} R ≅ M$ ).

Proof

technique · direct

1.1givenF1F2F3F4F5algebra

Claim 1. For fixed $(f, g) \in V^{*} \times W^{*}$ the pairing $V \times W \to k$ , $(v, w) \mapsto f (v) g (w)$ , is $k$ -bilinear, so it defines a functional $θ (f, g) \in (V \otimes W)^{*}$ with $θ (f, g) (v \otimes w) = f (v) g (w)$ by the universal property in [F1], the star denoting the space of linear functionals [F2]; the assignment $(f, g) \mapsto θ (f, g)$ is itself $k$ -bilinear, so it induces a $k$ -linear map $θ : V^{*} \otimes W^{*} \to (V \otimes W)^{*}$ by [F1]. On the one hand $(v_{i}^{*} \otimes w_{j}^{*})$ is a basis of $V^{*} \otimes W^{*}$ by [F4] and [F5], on the other hand the dual vectors $(v_{i} \otimes w_{j})^{*}$ in $(V \otimes W)^{*}$ of the product basis $(v_{i} \otimes w_{j})$ (a basis by [F5]) form a basis of $(V \otimes W)^{*}$ by [F4]; and $θ (v_{i}^{*} \otimes w_{j}^{*}) (v_{k} \otimes w_{l}) = v_{i}^{*} (v_{k}) w_{j}^{*} (w_{l}) = δ_{i k} δ_{j l} = (v_{i} \otimes w_{j})^{*} (v_{k} \otimes w_{l})$ by [F3], so $θ (v_{i}^{*} \otimes w_{j}^{*}) = (v_{i} \otimes w_{j})^{*}$ because linear functionals agreeing on the spanning product basis agree. If $z = \sum_{i, j} c_{i j} v_{i}^{*} \otimes w_{j}^{*}$ satisfies $θ (z) = 0$ , then $\sum_{i, j} c_{i j} (v_{i} \otimes w_{j})^{*} = 0$ and linear independence of the dual product basis [F4] gives all $c_{i j} = 0$ , so $θ$ is injective; and every $L \in (V \otimes W)^{*}$ is $L = \sum_{i, j} d_{i j} (v_{i} \otimes w_{j})^{*} = θ (\sum_{i, j} d_{i j} v_{i}^{*} \otimes w_{j}^{*})$ by spanning [F4], so $θ$ is surjective. Hence $θ$ is an isomorphism with the stated values on the dual product basis.

1.2givenF6F7F8algebra

Claim 2. By [F7] the map $Φ : V^{*} \otimes V \to Hom (V, V)$ is an isomorphism, so the preimage of ${i d}_{V}$ is unique and any two bases $(v_{1}, \dots, v_{n})$ give the same element as soon as both give ${i d}_{V}$ . For $y \in V$ the coordinate expansion of [F6] gives $y = \sum_{i} v_{i}^{*} (y) v_{i}$ , hence $Φ (\sum_{i} v_{i}^{*} \otimes v_{i}) (y) = \sum_{i} v_{i}^{*} (y) v_{i} = y$ on a spanning set of $V$ , so $Φ (\sum_{i} v_{i}^{*} \otimes v_{i}) = {i d}_{V}$ and the element $\sum_{i} v_{i}^{*} \otimes v_{i}$ is the unique preimage of ${i d}_{V}$ , independent of the basis. Its image under $σ_{V^{*}, V}$ is $\sum_{i} v_{i} \otimes v_{i}^{*}$ by the elementary-tensor formula of [F8].

2.1step 1.2F1F6F8F9algebra

Claim 3. The pairing $V^{*} \times V \to k$ , $(f, v) \mapsto f (v)$ , is $k$ -bilinear, so it induces $e v : V^{*} \otimes V \to k$ , $f \otimes v \mapsto f (v)$ , by [F1]; evaluation is basis-free. The coevaluation $c o e v : k \to V \otimes V^{*}$ is defined by $1 \mapsto \sum_{i} v_{i} \otimes v_{i}^{*}$ , which by step 1.2 is independent of the basis and equals $σ_{V^{*}, V}$ applied to the unique preimage of ${i d}_{V}$ ; it is $k$ -linear because $k$ is spanned by $1$ . For the first zigzag, use the conventions of [F1] and the formulas of [F8] and [F9]: for $x \in V$ , $(c o e v \otimes {i d}_{V}) (1 \otimes x) = \sum_{i} (v_{i} \otimes v_{i}^{*}) \otimes x$ , the associator sends this to $\sum_{i} v_{i} \otimes (v_{i}^{*} \otimes x)$ , and $({i d}_{V} \otimes e v)$ sends it to $\sum_{i} v_{i} \otimes v_{i}^{*} (x) = x \otimes 1$ by [F6], which the unit isomorphism $ρ_{V}$ identifies with $x$ ; both composites are linear in $x$ , so they agree everywhere. For the second zigzag, $f \otimes 1$ maps under $({i d}_{V^{*}} \otimes c o e v)$ to $\sum_{i} f \otimes (v_{i} \otimes v_{i}^{*})$ , the inverse associator sends this to $\sum_{i} (f \otimes v_{i}) \otimes v_{i}^{*}$ , and $(e v \otimes {i d}_{V^{*}})$ sends it to $\sum_{i} f (v_{i}) (1 \otimes v_{i}^{*}) = 1 \otimes f$ by the dual expansion of [F6], which the unit isomorphism $λ_{V^{*}}$ identifies with $f$ ; again both composites are linear, so equality on the spanning elements $f \otimes 1$ proves the identity.

3.1step 1.1step 1.2step 2.1∎

Steps 1.1, 1.2 and 2.1 prove claims 1, 2 and 3 respectively, with the dual product basis values, the basis independence of the preimage of ${i d}_{V}$ , and both zigzag identities established.

Remarks

Infinite dimension is deliberately outside the claim. No surjectivity of $V^{*} \otimes W^{*} \to (V \otimes W)^{*}$ is claimed in infinite dimension, and the companion page's An infinite-dimensional tensor-dual functional outside the image ↗ exhibits a functional outside the image when $V$ has an infinite basis, so the finite-dimensional hypothesis of part 1 cannot simply be dropped.

Depends on

Used by

An infinite-dimensional tensor-dual functional outside the image Counterexample
Finite coevaluation computed in two bases Example

Dependency tree · two levels

40 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

Keith Conrad, Tensor products (University of Connecticut expository notes, 60 pp.) (standard reference, not scraped)