Splitting a qubit register into a Hilbert tensor product

Category: 1-Mathlib (CSD-free; staged as a Mathlib-upstream candidate).

A register of a + b qubits factors as the Hilbert tensor product of its first a and its last b qubits:

QReg (a + b) ≃ₗᵢ[ℂ] QReg a ⊗[ℂ] QReg b (regTensorEquiv).

This is the identification recorded as missing in MATHLIB-GAPS.md (specs/mathlib-gaps-plan.md MG-5). Mathlib carries the inner-product structure on E ⊗[𝕜] F (Analysis/InnerProductSpace/TensorProduct.lean), but nothing connected it to the concrete EuclideanSpace/PiLp model that QReg uses — so "apply this operator to those wires and the identity elsewhere" could not even be stated.

The construction is two reindexings and an orthonormal basis:

• regSplitEquiv — the index bijection (Fin (a+b) → Fin 2) ≃ (Fin a → Fin 2) × (Fin b → Fin 2), currying Fin (a+b) ≃ Fin a ⊕ Fin b;
• splitReg — the induced isometry onto the product-indexed Euclidean space;
• prodTensorEquiv — EuclideanSpace ℂ (ι × κ) ≃ₗᵢ[ℂ] EuclideanSpace ℂ ι ⊗[ℂ] EuclideanSpace ℂ κ from OrthonormalBasis.tensorProduct: both sides carry orthonormal bases indexed by ι × κ, so the isometry is the change of basis;
• ★★ regTensorEquiv — the composite, with regTensorEquiv_basisState confirming it is the expected map on computational basis states.

The payoff for consumers is tensorFirst: an operator on the first a qubits extended by the identity on the remaining b, as an operator on QReg (a + b), with tensorFirst_basisState computing its action.

Scope

Finite-dimensional and concrete throughout; no completion or topological tensor product is involved (in finite dimensions the algebraic tensor product already carries the Hilbert structure). The split is at a prefix of the wires; an arbitrary wire subset would compose this with a permutation reindexing, which is not done here.

References

QuantumInfo/Register.lean (QReg, basisState); MATHLIB-GAPS.md (the register tensor-factorisation row this closes); specs/mathlib-gaps-plan.md (MG-5).

The product-index model is a tensor product

noncomputable def QuantumInfo.prodTensorEquiv (ι : Type u_1) (κ : Type u_2) [Fintype ι] [Fintype κ] : EuclideanSpace ℂ (ι × κ) ≃ₗᵢ[ℂ] TensorProduct ℂ (EuclideanSpace ℂ ι) (EuclideanSpace ℂ κ)

The concrete model of a Hilbert tensor product: a Euclidean space on a product index is the tensor product of the Euclidean spaces on the factors. Both sides carry orthonormal bases indexed by ι × κ — the standard basis on the left, the tensor of the standard bases on the right — so the isometry is the change of basis.

Equations

• QuantumInfo.prodTensorEquiv ι κ = ((EuclideanSpace.basisFun ι ℂ).tensorProduct (EuclideanSpace.basisFun κ ℂ)).repr.symm

theorem QuantumInfo.prodTensorEquiv_single {ι : Type u_1} {κ : Type u_2} [Fintype ι] [Fintype κ] [DecidableEq ι] [DecidableEq κ] (i : ι) (k : κ) : (prodTensorEquiv ι κ) (EuclideanSpace.single (i, k) 1) = EuclideanSpace.single i 1 ⊗ₜ[ℂ] EuclideanSpace.single k 1

On standard basis vectors the identification is the expected one.

Splitting the wire index

def QuantumInfo.regSplitEquiv (a b : ℕ) : (Fin (a + b) → Fin 2) ≃ (Fin a → Fin 2) × (Fin b → Fin 2)

The index bijection behind the register split: a bitstring on a + b wires is a pair of bitstrings, on the first a and the last b.

Equations

• QuantumInfo.regSplitEquiv a b = (finSumFinEquiv.symm.arrowCongr (Equiv.refl (Fin 2))).trans (Equiv.sumArrowEquivProdArrow (Fin a) (Fin b) (Fin 2))

@[simp]

theorem QuantumInfo.regSplitEquiv_apply (a b : ℕ) (z : Fin (a + b) → Fin 2) : (regSplitEquiv a b) z = (fun (i : Fin a) => z (Fin.castAdd b i), fun (j : Fin b) => z (Fin.natAdd a j))

noncomputable def QuantumInfo.splitReg (a b : ℕ) : QReg (a + b) ≃ₗᵢ[ℂ] EuclideanSpace ℂ ((Fin a → Fin 2) × (Fin b → Fin 2))

The register split, as an isometry onto the product-indexed Euclidean space.

Equations

• QuantumInfo.splitReg a b = LinearIsometryEquiv.piLpCongrLeft 2 ℂ ℂ (QuantumInfo.regSplitEquiv a b)

@[simp]

theorem QuantumInfo.splitReg_basisState (a b : ℕ) (z : Fin (a + b) → Fin 2) : (splitReg a b) (basisState z) = EuclideanSpace.single ((regSplitEquiv a b) z) 1

★★ The register tensor factorisation

noncomputable def QuantumInfo.regTensorEquiv (a b : ℕ) : QReg (a + b) ≃ₗᵢ[ℂ] TensorProduct ℂ (QReg a) (QReg b)

★★ A register splits as a Hilbert tensor product of its wire blocks.

Equations

• QuantumInfo.regTensorEquiv a b = (QuantumInfo.splitReg a b).trans (QuantumInfo.prodTensorEquiv (Fin a → Fin 2) (Fin b → Fin 2))

@[simp]

theorem QuantumInfo.regTensorEquiv_basisState (a b : ℕ) (z : Fin (a + b) → Fin 2) : (regTensorEquiv a b) (basisState z) = (basisState fun (i : Fin a) => z (Fin.castAdd b i)) ⊗ₜ[ℂ] basisState fun (j : Fin b) => z (Fin.natAdd a j)

The factorisation acts as expected on computational basis states: a bitstring goes to the tensor of its two blocks.

Operators on a wire block, extended by the identity

noncomputable def QuantumInfo.tensorFirst {a b : ℕ} (A : QReg a →L[ℂ] QReg a) : QReg (a + b) →L[ℂ] QReg (a + b)

An operator on the first a wires, extended by the identity on the last b — the "local tensor factor" a register-level statement needs.

Equations

• One or more equations did not get rendered due to their size.

theorem QuantumInfo.tensorFirst_apply {a b : ℕ} (A : QReg a →L[ℂ] QReg a) (v : QReg (a + b)) : (tensorFirst A) v = (regTensorEquiv a b).symm ((LinearMap.rTensor (QReg b) ↑A) ((regTensorEquiv a b) v))

theorem QuantumInfo.tensorFirst_basisState {a b : ℕ} (A : QReg a →L[ℂ] QReg a) (z : Fin (a + b) → Fin 2) : (tensorFirst A) (basisState z) = (regTensorEquiv a b).symm (A (basisState fun (i : Fin a) => z (Fin.castAdd b i)) ⊗ₜ[ℂ] basisState fun (j : Fin b) => z (Fin.natAdd a j))

The action on computational basis states: the operator hits the first block, the second block rides along. This is the computation rule a hybrid-circuit argument consumes.

@[simp]

theorem QuantumInfo.tensorFirst_one {a b : ℕ} : tensorFirst (ContinuousLinearMap.id ℂ (QReg a)) = ContinuousLinearMap.id ℂ (QReg (a + b))

The identity extends to the identity.