ExampleConstruction: Literature-sourcedVerification: 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 coevaluation computed in two bases

Example

Let $V = k^{2}$ with standard basis $e_{1}, e_{2}$ , and let $k$ have characteristic $\neq 2$ . For the second basis $b_{1} = e_{1} + e_{2}$ , $b_{2} = e_{1} - e_{2}$ with dual basis $b_{1}^{*} = \frac{1}{2} (e_{1}^{*} + e_{2}^{*})$ , $b_{2}^{*} = \frac{1}{2} (e_{1}^{*} - e_{2}^{*})$ , the elements $\sum_{i} e_{i} \otimes e_{i}^{*}$ and $\sum_{j} b_{j} \otimes b_{j}^{*}$ of $V \otimes V^{*}$ are equal. Hence the coevaluation $c o e v : k \to V \otimes V^{*}$ of Finite tensor duality and basis-independent coevaluation is computed by the same element in both bases, and the zigzag identities hold in both.

Facts & Assumptions

Given: The field $k$ of characteristic $\neq 2$ , the space $V = k^{2}$ with standard basis $e_{1}, e_{2}$ and dual basis $e_{1}^{*}, e_{2}^{*}$ , and the second ordered basis $b_{1} = e_{1} + e_{2}$ , $b_{2} = e_{1} - e_{2}$ with dual basis $b_{1}^{*}, b_{2}^{*}$ .

[F1]

The tensor product conventions: every element of $V \otimes V^{*}$ is a finite sum of elementary tensors and the defining relations give bilinearity and $c (u \otimes v) = (c u) \otimes v = u \otimes (c v)$ (Scalars, tensor powers, the empty tensor, opposite algebras and finite sums).

[F2]

The dual family of a basis is characterized by $b_{j}^{*} (b_{k}) = δ_{j k}$ (The dual family $(b^{*})_{b \in B}$ associated to a Hamel basis $B$ , defined by $b^{*} (c) = δ_{b c}$ ), and a dual family of a finite basis is again a basis, so it is determined by those values (The dual family of a finite basis is a basis of the dual space, with the same dimension).

[F3]

For finite-dimensional $V$ , the element $\sum_{i} v_{i}^{*} \otimes v_{i} \in V^{*} \otimes V$ , equivalently $\sum_{i} v_{i} \otimes v_{i}^{*} \in V \otimes V^{*}$ under the symmetry, is independent of the ordered basis and equals the coevaluation image of $1$ ; both zigzag identities hold (Finite tensor duality and basis-independent coevaluation).

Verification

technique · direct

1.1givenF1F2algebra

First, $b_{1}^{*}, b_{2}^{*}$ as displayed are the dual basis of $b_{1}, b_{2}$ : using $e_{i}^{*} (e_{j}) = δ_{i j}$ one computes $b_{1}^{*} (b_{1}) = \frac{1}{2} (1 + 1) = 1$ , $b_{1}^{*} (b_{2}) = \frac{1}{2} (1 - 1) = 0$ , $b_{2}^{*} (b_{1}) = \frac{1}{2} (1 - 1) = 0$ and $b_{2}^{*} (b_{2}) = \frac{1}{2} (1 + 1) = 1$ , so by the characterization of [F2] the displayed functionals are $b_{1}^{*}, b_{2}^{*}$ . Then [F1] gives $\sum_{j} b_{j} \otimes b_{j}^{*} = \frac{1}{2} ((e_{1} + e_{2}) \otimes (e_{1}^{*} + e_{2}^{*}) + (e_{1} - e_{2}) \otimes (e_{1}^{*} - e_{2}^{*})) = \frac{1}{2} (2 e_{1} \otimes e_{1}^{*} + 2 e_{2} \otimes e_{2}^{*}) = e_{1} \otimes e_{1}^{*} + e_{2} \otimes e_{2}^{*}$ , the two cross terms cancelling and the factor $\frac{1}{2} \cdot 2 = 1$ being legitimate because $char k \neq 2$ .

2.1step 1.1F3∎

By step 1.1 the same element of $V \otimes V^{*}$ is computed by the sum over the standard basis and by the sum over the second basis, which is exactly the basis-independence asserted in [F3]; since [F3] identifies this element with the image of $1$ under the coevaluation, the coevaluation is computed by the same element in both bases, and the zigzag identities of [F3] hold for both ordered bases.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

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