DefinitionDefinition: AI-adaptedProof: AI-generatedPipeline-generated

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.

Tensor products of finitely many linear maps

Definition

For a finite ordered family of finite-dimensional complex vector spaces $H_{k}, K_{k}$ and complex-linear maps $T_{k} : H_{k} \to K_{k}$ , the tensor map $⨂_{k < n} T_{k} : H_{0} \otimes \dots \otimes H_{n - 1} \to K_{0} \otimes \dots \otimes K_{n - 1}$ is the unique linear map satisfying

$(⨂_{k < n} T_{k}) (x_{0} \otimes \dots \otimes x_{n - 1}) = T_{0} x_{0} \otimes \dots \otimes T_{n - 1} x_{n - 1} .$

For $n = 0$ , the tensor map is the identity map $z \mapsto z$ on the empty tensor product $C$ .

Facts & Assumptions

Given: A finite ordered family of complex vector spaces and linear maps $T_{k} : H_{k} \to K_{k}$ .

[F1]

A binary algebraic tensor product is generated by elementary tensors, and a tensor with a zero factor vector is zero (The tensor product $M \otimes_{R} N$ from the additive group underlying the free $Z$ -module on $M \times N$ , elementary tensors, and finite tensor sums). Over $C$ , tensoring is complex-linear in each factor (Over a commutative ring, $M \otimes_{R} N$ is an $R$ -module with $r (m \otimes n) = (r m) \otimes n = m \otimes (r n)$ ).

[F2]

A finite iterated tensor product represents multilinear maps, including the empty and one-factor cases (Finite iterated tensor products represent multilinear maps independently of parenthesization).

[F3]

Each $T_{k}$ is linear on its factor (Linear map between vector spaces over the same field).

Proof

1.1givenF1F3algebra

For $n = 0$ , the prescribed map is the identity on $C$ . For $n > 0$ , the function $(x_{0}, \dots, x_{n - 1}) \mapsto T_{0} x_{0} \otimes \dots \otimes T_{n - 1} x_{n - 1}$ is linear in each argument: replacing any $x_{k}$ by $a x_{k} + b y_{k}$ replaces its image by $a T_{k} x_{k} + b T_{k} y_{k}$ by [F3], and tensoring is linear in that factor.

2.1step 1.1F1F2algebra∎

For $n > 0$ , [F2] gives a unique linear extension of the multilinear function in step 1.1, hence the map in the Definition. Repeated use of [F1] shows that elementary tensors span any nonempty iterated tensor product. If some $H_{k} = 0$ , every source elementary tensor is zero by [F1], so the domain is zero and the unique linear map from it is zero. If some $K_{k} = 0$ , the same argument makes the codomain zero, and the unique linear map to it is zero. In either case the displayed rule holds. For $n = 0$ , the empty elementary tensor is $1 \in C$ by [F2]; its prescribed image is $1$ , which uniquely determines the identity linear map.

Depends on

Used by

Hypercube continuous-time state transfer Algorithm
One-query Bernstein–Vazirani algorithm Algorithm
One-query Deutsch algorithm Algorithm
One-query Deutsch–Jozsa algorithm Algorithm
Quantum phase estimation Algorithm
Reversible embedding of a Boolean circuit Algorithm
Distance corrects unlocated errors and known erasures Corollary
Choi matrix with input factor first Definition
Clean-ancilla zero-branch postselection Definition
Coherent XOR function oracle Definition
Finite open-graph adaptive measurement pattern Definition
Multi-Control Activation Pattern Definition
Oblivious ancilla reflection Definition
Partial trace over the first tensor factor Definition
Phase aware n qubit pauli group Definition
Support and weight of an operator on a finite register Definition
Toric star and plaquette checks Definition
A reversible AND oracle with clean work Example
Quantum repetition subspace projector and a distance-one boundary error Example
Small hypercube transfer Example
A finite instrument has an isometric coherent record Lemma
A local gate has a unique global wire embedding Lemma
Circuit Resource Composition Lemma
Clean and dirty ancilla identities extend to references and mixed states Lemma
CNOT Pauli action Lemma
Complete positivity implies Choi positivity Lemma
Computational-basis instruments and conditional states on two registers Lemma
Hadamard character sum on F₂ⁿ Lemma
Hadamard pauli action Lemma
Hadamard preparation of a uniform binary state Lemma
One-bit J-gate teleportation branch identity Lemma
Operator Norm Is Unchanged by Spectator Registers Lemma
Operator support weight is invariant under wire permutation Lemma
Optimal Cloner Attains Bound Lemma
Partial trace contracts the trace norm on Hermitian operators Lemma
Partial trace contracts trace distance Lemma
Phase gate pauli action Lemma
Phase-estimation finite outcome law Lemma
Positive Marginals Imply Joint Support Lemma
Preserving the logical marginal forces a gauge-only channel Lemma

…and 50 more results.

Dependency tree · two levels

25 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

John Watrous, The Theory of Quantum Information (standard reference, not scraped)
Ronald de Wolf, Quantum Computing: Lecture Notes, Appendix A.6 (standard reference, not scraped)