LemmaStatement: AI-adaptedProof: 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.

Coefficient separation for an independent family of vectors, with explicit Choice assumptions

Statement

Assume the Axiom of Choice (The Axiom of Choice). Let $v_{1}, \dots, v_{n} \in V$ be linearly independent vectors in a $k$ -vector space $V$ and let $w_{1}, \dots, w_{n} \in W$ satisfy $\sum_{i = 1}^{n} v_{i} \otimes w_{i} = 0$ in $V \otimes W$ . Then $w_{i} = 0$ for every $i$ ; equivalently, the linear map $W^{n} \to V \otimes W$ , $(w_{i}) \mapsto \sum_{i} v_{i} \otimes w_{i}$ , is injective.

If $V$ is finite-dimensional the same conclusion is proved without the Axiom of Choice.

Facts & Assumptions

Given: A field $k$ , a $k$ -vector space $V$ with linearly independent vectors $v_{1}, \dots, v_{n}$ , a $k$ -vector space $W$ , and elements $w_{1}, \dots, w_{n} \in W$ with $\sum_{i} v_{i} \otimes w_{i} = 0$ in $V \otimes W$ .

[A1]

The Axiom of Choice holds (The Axiom of Choice).

[F1]

The tensor product conventions: $V \otimes W$ has the universal property, every element is a finite sum of elementary tensors, and the empty tensor $k$ is identified with the tensor unit through the unit isomorphisms, so $k \otimes W \to W$ , $c \otimes w \mapsto c w$ , is an isomorphism (Scalars, tensor powers, the empty tensor, opposite algebras and finite sums).

[F2]

Under [A1], for every injective linear map $f : V \to V^{'}$ and every $k$ -vector space $W$ the map $f \otimes {i d}_{W}$ is injective (Tensoring injections and the kernel of a tensor product of quotient maps over a field).

[F3]

The span of a set is the smallest linear subspace containing it (Linear combination of a finite list, and the span $span (S)$ as the smallest linear subspace containing $S$ ); in particular $span (v_{1}, \dots, v_{n})$ is a linear subspace containing each $v_{i}$ , and since it is a subspace it contains every finite linear combination of the $v_{i}$ .

[F4]

The span of a finite list consists of its linear combinations. A finite list is an ordered basis exactly when every vector has a unique expansion in it; addition and scaling of the unique coordinate lists show that its coordinate functionals are linear (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).

[F5]

In a finite-dimensional space every linearly independent subset is contained in a basis, with no choice principle used (If $\dim_{F} V = n$ and $U$ is a linear subspace of $V$ , then $U$ is finite-dimensional, $\dim_{F} U \leq n$ , and $\dim_{F} U = n$ if and only if $U = V$ ).

[F6]

Functoriality supplies an additive map $f \otimes g$ with $(f \otimes g) (v \otimes w) = f (v) \otimes g (w)$ and respects composition (Module homomorphisms induce tensor-product homomorphisms functorially). For linear $f, g$ over $k$ , this map is $k$ -linear: the scalar action of [F1] gives $(f \otimes g) (c (v \otimes w)) = f (c v) \otimes g (w) = c (f (v) \otimes g (w))$ , and additivity extends this identity to every finite tensor sum.

Proof

technique · direct

1.1givenA1F1F2F3F4F6algebra

Arbitrary dimension, under [A1]. Put $V_{0} : = span (v_{1}, \dots, v_{n})$ , a linear subspace of $V$ containing every $v_{i}$ by [F3]; the inclusion $ι : V_{0} ↪ V$ is injective and linear, so $ι \otimes {i d}_{W} : V_{0} \otimes W \to V \otimes W$ is injective by [F2]. Since $(ι \otimes {i d}_{W}) (\sum_{i} v_{i} \otimes w_{i}) = \sum_{i} v_{i} \otimes w_{i} = 0$ by [F6], injectivity gives $\sum_{i} v_{i} \otimes w_{i} = 0$ in $V_{0} \otimes W$ . Every element of $V_{0}$ is a linear combination of the finite list $(v_{i})$ by the span clause of [F4], so the list $(v_{1}, \dots, v_{n})$ spans $V_{0}$ , and it is linearly independent by hypothesis, so it is an ordered basis of $V_{0}$ with linear coordinate functionals $φ_{i} : V_{0} \to k$ satisfying $φ_{i} (v_{j}) = δ_{i j}$ by [F4]. For each $i$ , functoriality [F6] gives the linear map $φ_{i} \otimes {i d}_{W} : V_{0} \otimes W \to k \otimes W$ , and applying it to the relation yields $0 = \sum_{j} (φ_{i} \otimes {i d}_{W}) (v_{j} \otimes w_{j}) = \sum_{j} φ_{i} (v_{j}) \otimes w_{j} = 1 \otimes w_{i}$ ; the unit isomorphism of [F1] sends $1 \otimes w_{i}$ to $w_{i}$ , so $w_{i} = 0$ .

1.2givenF1F4F5F6algebra

Finite dimension, without Choice. If $V$ is finite-dimensional, the vectors $v_{1}, \dots, v_{n}$ are distinct and form a linearly independent finite subset of $V$ , so by [F5] this subset is contained in a basis $B$ of $V$ ; listing the finite set $B$ with $v_{1}, \dots, v_{n}$ in the first $n$ positions gives an ordered basis $(b_{1}, \dots, b_{m})$ with $b_{j} = v_{j}$ for $j \leq n$ whose coordinate functionals $ψ_{1}, \dots, ψ_{m}$ are linear by [F4] and satisfy $ψ_{j} (v_{k}) = δ_{j k}$ for $j, k \leq n$ . Applying $ψ_{i} \otimes {i d}_{W}$ to the relation in $V \otimes W$ by [F6] gives $0 = 1 \otimes w_{i}$ , hence $w_{i} = 0$ by the unit isomorphism of [F1]; no complement or Zorn extension is used, only the finite-dimensional extension of [F5].

2.1step 1.1step 1.2givenF1∎

Both cases give $w_{i} = 0$ for all $i$ : step 1.1 under the Axiom of Choice in arbitrary dimension and step 1.2 in finite dimension without it; the map $W^{n} \to V \otimes W$ with $(w_{i}) \mapsto \sum_{i} v_{i} \otimes w_{i}$ is linear by bilinearity of elementary tensors [F1] and has trivial kernel, so subtracting two tuples with the same image proves injectivity, which is the equivalent form of the claim.

Remarks

The proof uses AC through the tensor-injection lemma in arbitrary ambient dimension and avoids it when $V$ is finite-dimensional. It establishes sufficiency of these assumptions, not necessity of AC or a sharp boundary between choice principles.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

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