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

Many finite presentations of one tensor and the invariant contraction

Example

Let $k$ be a field of characteristic $\neq 2$ . Work in $V = W = k^{2}$ with $u = (1, 0)$ , $v = (0, 1)$ , $u^{'} = (2, 0)$ and $v^{'} = (0, \frac{1}{2})$ . Then $u \otimes v = u^{'} \otimes v^{'}$ in $k^{2} \otimes k^{2}$ , although $(u, v) \neq (u^{'}, v^{'})$ . Consequently every $k$ -bilinear form $B : k^{2} \times k^{2} \to k$ with $B (u, v) = 1$ gives the value $1$ on every finite presentation of that tensor: if $\sum_{l} x_{l} \otimes y_{l} = u \otimes v$ then $\sum_{l} B (x_{l}, y_{l}) = 1$ . The contraction of a bilinear form against a tensor is therefore independent of the presentation.

Facts & Assumptions

Given: A field $k$ of characteristic $\neq 2$ , the vectors $u = (1, 0)$ , $v = (0, 1)$ , $u^{'} = (2, 0)$ and $v^{'} = (0, \frac{1}{2})$ in $k^{2}$ , and a $k$ -bilinear form $B : k^{2} \times k^{2} \to k$ with $B (u, v) = 1$ .

[F1]

The tensor product conventions: $k^{2} \otimes k^{2}$ is the tensor product over $k$ with its universal property, every element is a finite sum of elementary tensors, and the defining relations give $c (x \otimes y) = (c x) \otimes y = x \otimes (c y)$ for every $c \in k$ (Scalars, tensor powers, the empty tensor, opposite algebras and finite sums).

[F2]

Bilinear maps over a commutative ring are additive in each variable and satisfy $b (r x, y) = r b (x, y) = b (x, r y)$ (Balanced maps from a right module and a left module, and bilinear maps over a commutative ring).

[F3]

A balanced pairing on $V \times W$ induces a unique group homomorphism on $V \otimes W$ with the corresponding values on elementary tensors (Universal property of the tensor product for balanced maps into abelian groups).

[F4]

A prescription on elementary tensors descends to a homomorphism exactly when its underlying pairing is balanced, and then the extension is unique (A formula on elementary tensors defines a homomorphism exactly when its underlying pairing is balanced).

[F5]

The elementary tensors of two bases form a basis of the tensor product, so for the basis vectors $e_{1} = u$ , $e_{2} = v$ the tensor $u \otimes v = e_{1} \otimes e_{2}$ is a nonzero element of $k^{2} \otimes k^{2}$ (The elementary tensors of two bases form the product basis of the tensor product).

Verification

technique · direct

1.1givenF1F5algebra

Since $u^{'} = 2 u$ and $v^{'} = \frac{1}{2} v$ , bilinearity of the elementary tensor [F1] gives $u^{'} \otimes v^{'} = (2 u) \otimes (\frac{1}{2} v) = 2 \cdot \frac{1}{2} (u \otimes v) = u \otimes v$ because $2 \cdot \frac{1}{2} = 1$ in $k$ by the characteristic hypothesis; and $(u, v) \neq (u^{'}, v^{'})$ because $u = (1, 0) \neq (2, 0) = u^{'}$ ; moreover $u \otimes v = e_{1} \otimes e_{2} \neq 0$ by [F5], so an empty presentation, whose sum is $0$ , can never satisfy $\sum_{l} x_{l} \otimes y_{l} = u \otimes v$ .

2.1step 1.1F1F2F3F4∎

The form $B$ is $k$ -bilinear [F2], hence balanced, so it descends to the unique group homomorphism $\overline{B} : k^{2} \otimes k^{2} \to k$ with $\overline{B} (x \otimes y) = B (x, y)$ by [F3] and [F4]. It is $k$ -linear: for $c \in k$ and $t = \sum_{l} x_{l} \otimes y_{l}$ , [F1] and [F2] give $\overline{B} (c t) = \sum_{l} B (c x_{l}, y_{l}) = c \sum_{l} B (x_{l}, y_{l}) = c \overline{B} (t)$ . If $\sum_{l} x_{l} \otimes y_{l} = u \otimes v$ is any finite presentation of the tensor, linearity of $\overline{B}$ and step 1.1 give $\sum_{l} B (x_{l}, y_{l}) = \overline{B} (\sum_{l} x_{l} \otimes y_{l}) = \overline{B} (u \otimes v) = B (u, v) = 1$ , so the contraction has the same value $1$ on every presentation and is independent of the presentation.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

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