CounterexampleConstruction: Literature-sourcedVerification: AI-adaptedPipeline-generatedprecheck passaudited 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.

An infinite-dimensional tensor-dual functional outside the image

Statement refuted

The finitely proved identification of Finite tensor duality and basis-independent coevaluation, read without its finite-dimensional hypothesis, would say that the canonical map $V^{*} \otimes V^{*} \to (V \otimes V)^{*}$ , $f \otimes g \mapsto [v \otimes w \mapsto f (v) g (w)]$ , is surjective for every $k$ -vector space $V$ .

Facts & Assumptions

Given: An infinite set $I$ , a field $k$ , the free module $V = k^{(I)} = ⨁_{i \in I} k$ with standard basis $(e_{i})_{i \in I}$ , and the functional $L \in (V \otimes V)^{*}$ with $L (e_{i} \otimes e_{j}) = δ_{i j}$ .

[F1]

The free module on $I$ has standard basis $(e_{i})$ with unique finite expansions, and a set map from a basis into a module extends uniquely to a linear map (The free module on a set and its standard basis, Universal property of the free module on a set).

[F2]

The elementary tensors $e_{i} \otimes e_{j}$ of two bases form a basis of $V \otimes V$ (The elementary tensors of two bases form the product basis of the tensor product).

[F3]

The algebraic dual $V^{*}$ is the space of linear functionals $V \to k$ ; the coordinate functionals $e_{j}^{*}$ with $e_{j}^{*} (e_{i}) = δ_{i j}$ exist by [F1] (Linear functionals and the algebraic dual $V^{*} = L (V, F)$ ).

[F4]

A set $S \subseteq V$ is linearly independent when every injective finite list into $S$ is independent, and a basis is an independent spanning set (Linear independence: a finite list $v : n \to V$ is independent when $\sum_{i < n} λ_{i} v_{i} = 0_{V}$ forces every $λ_{i} = 0_{F}$ , and a subset $S \subseteq V$ is independent when every injective finite list into $S$ is independent, Basis of a vector space: a linearly independent spanning subset; and ordered basis: an injective finite list whose image is a basis).

[F5]

If a vector space has a spanning set with $n$ elements, then every linearly independent subset of it is finite with at most $n$ elements (If $V$ has a spanning set with $n$ elements, then every linearly independent subset of $V$ is finite with at most $n$ elements; in particular $V$ has no linearly independent subset equinumerous with $N$ ).

[F6]

Every element of a tensor product is a finite sum of elementary tensors, and bilinear pairings induce linear maps by its universal property (Scalars, tensor powers, the empty tensor, opposite algebras and finite sums).

Counterexample

technique · direct

Let $I$ be an infinite set, let $V = k^{(I)}$ have basis $(e_{i})_{i \in I}$ , and let $L \in (V \otimes V)^{*}$ be the linear functional determined on the product basis by $L (e_{i} \otimes e_{j}) = δ_{i j}$ . Then $L$ is not in the image of the canonical map $V^{*} \otimes V^{*} \to (V \otimes V)^{*}$ , $f \otimes g \mapsto [v \otimes w \mapsto f (v) g (w)]$ : the tensor-dual identification is a finite-dimensional phenomenon, and for $I = N$ the outside functional is the coefficient pairing $(\sum_{n} a_{n} e_{n}) \otimes (\sum_{m} b_{m} e_{m}) \mapsto \sum_{n} a_{n} b_{n}$ , which is not a finite sum of products of functionals.

1.1givenF1F2F3F4F6algebra

For $f, g \in V^{*}$ , the bilinear pairing $(v, w) \mapsto f (v) g (w)$ defines a functional $θ (f, g) \in (V \otimes V)^{*}$ by [F6]; the assignment $(f, g) \mapsto θ (f, g)$ is itself bilinear, so [F6] gives a linear map $θ : V^{*} \otimes V^{*} \to (V \otimes V)^{*}$ with $θ (f \otimes g) (v \otimes w) = f (v) g (w)$ , without a finite-dimensional hypothesis. The product basis $(e_{i} \otimes e_{j})_{(i, j) \in I \times I}$ of [F2] is a basis of $V \otimes V$ , so prescribing the values $L (e_{i} \otimes e_{j}) = δ_{i j}$ on it defines a unique linear functional $L \in (V \otimes V)^{*}$ by [F1]; in particular $L$ is well defined and $I \times I$ , hence $I$ , is infinite. Likewise the coordinate functionals $e_{j}^{*}$ of [F3] are well defined, and the set $S : = {e_{j}^{*} : j \in I} \subseteq V^{*}$ is infinite because $j \mapsto e_{j}^{*}$ is injective (they take different values at the single vector $e_{j}$ ), and it is linearly independent: if $\sum_{l = 1}^{r} λ_{l} e_{j_{l}}^{*} = 0$ is a finite relation with distinct indices $j_{1}, \dots, j_{r}$ , evaluating at $e_{j_{l}}$ gives $λ_{l} = 0$ .

2.1step 1.1F5F6algebra

Suppose $L$ is the image of an element of $V^{*} \otimes V^{*}$ , written as a finite sum $\sum_{s = 1}^{m} f_{s} \otimes g_{s}$ of elementary tensors by [F6]. For fixed $j \in I$ the functional $v \mapsto L (v \otimes e_{j})$ is the coordinate functional $e_{j}^{*}$ , because $L (e_{i} \otimes e_{j}) = δ_{i j}$ , and by the canonical-map formula in step 1.1 it is also $\sum_{s = 1}^{m} f_{s} (\cdot) g_{s} (e_{j}) = \sum_{s = 1}^{m} g_{s} (e_{j}) f_{s}$ ; hence every $e_{j}^{*}$ lies in the finite-dimensional span of $f_{1}, \dots, f_{m}$ . Thus the infinite linearly independent set $S$ of step 1.1 lies in a space spanned by $m$ elements, contradicting [F5], which forbids an infinite linearly independent subset in such a space.

3.1step 2.1F6algebra∎

No finite sum $\sum_{s} f_{s} \otimes g_{s}$ can have image $L$ , so $L$ lies outside the image of the canonical map and the map is not surjective for this infinite-dimensional $V$ : surjectivity of $V^{*} \otimes V^{*} \to (V \otimes V)^{*}$ is a finite-dimensional phenomenon, as claimed. For $I = N$ and $v = \sum_{n} a_{n} e_{n}$ , $w = \sum_{m} b_{m} e_{m}$ (finite sums) one computes $L (v \otimes w) = \sum_{n, m} a_{n} b_{m} L (e_{n} \otimes e_{m}) = \sum_{n} a_{n} b_{n}$ , so the outside functional is exactly the coefficient pairing, which is not a finite sum of products of functionals by step 2.1.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

43 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)
The CRing Project, open-source commutative algebra text (2016 PDF; Chapter 13) (standard reference, not scraped)