The tensor product over blocks

Category: 1-Mathlib (CSD-free; staged for upstream). BACKLOG #86, step (a) of its route: the layer a concatenated code needs, where a register is a family of blocks and an operator is one operator per block.

blockKron M is the matrix on the label space β → L whose entry at (k, l) is the product ∏_b (M b) (k b) (l b). It is the β-fold tensor product written on function labels instead of through Matrix.kron, which keeps the label space of a k-fold concatenation literally recursive (Fin 7 → Fin 7 → ⋯ → Fin 2) instead of a tower of reindexings.

• blockKron_one, ★ blockKron_mul, blockKron_conjTranspose, blockKron_smul — the algebra. Multiplicativity and the expansion below are both Fintype.prod_sum: a product of sums over the blocks is a sum over the functions choosing one summand per block;
• ★ blockKron_sum — multilinearity: expanding each block over a finite family expands the tensor over the function space of choices. This is what lets an arbitrary operator per block be written in a fixed finite family (Matrix.matrix_eq_sum_single at the leaves);
• ★★ blockKron_replace_eq_gateOf_mul — error propagation: a fault at one block is a single-block error after the ideal tensor;
• ★ blockKron_single_eq_gateOf — the family with one slot filled and the identity elsewhere is #83's single-qubit gate gateOf b₀ G on a qubit register, which ties the layer back to the controlled-gate vocabulary.

Honest scope

⚠️ No Matrix.kron bridge: blockKron is not identified with an iterated Kronecker product here. Nothing in the concatenation needs that identification, and stating it would need the reindexing (β → L) ≃ β × L-style equivalences this layer exists to avoid. ⚠️ Unitarity of blockKron M for unitary blocks is not proved here (it follows from blockKron_mul and blockKron_conjTranspose where it is wanted).

Source

M. Nielsen, I. Chuang, Quantum Computation and Quantum Information §10.6.1 (concatenated codes); QuantumInfo/ControlledSingle.lean (#84), QuantumInfo/ControlledGate.lean (#83); specs/BACKLOG.md #86; specs/steane-plan.md; specs/future-work.md.

def QuantumInfo.blockKron {β : Type u_1} {L : Type u_2} {L' : Type u_3} [Fintype β] (M : β → Matrix L L' ℂ) : Matrix (β → L) (β → L') ℂ

The tensor product over blocks: one matrix per block, acting on the labels β → L.

Equations

• QuantumInfo.blockKron M k l = ∏ b : β, M b (k b) (l b)

theorem QuantumInfo.blockKron_apply {β : Type u_1} {L : Type u_2} {L' : Type u_3} [Fintype β] (M : β → Matrix L L' ℂ) (k : β → L) (l : β → L') : blockKron M k l = ∏ b : β, M b (k b) (l b)

theorem QuantumInfo.blockKron_one {β : Type u_1} {L : Type u_2} [Fintype β] [DecidableEq L] : (blockKron fun (x : β) => 1) = 1

theorem QuantumInfo.blockKron_mul {β : Type u_1} {L : Type u_2} {L' : Type u_3} {L'' : Type u_4} [Fintype β] [DecidableEq β] [Fintype L'] (M : β → Matrix L L' ℂ) (N : β → Matrix L' L'' ℂ) : blockKron M * blockKron N = blockKron fun (b : β) => M b * N b

★ The tensor over blocks is multiplicative: a product of sums over the blocks is a sum over the functions choosing one summand per block (Fintype.prod_sum).

theorem QuantumInfo.blockKron_conjTranspose {β : Type u_1} {L : Type u_2} {L' : Type u_3} [Fintype β] (M : β → Matrix L L' ℂ) : (blockKron M).conjTranspose = blockKron fun (b : β) => (M b).conjTranspose

theorem QuantumInfo.blockKron_eq_zero {β : Type u_1} {L : Type u_2} {L' : Type u_3} [Fintype β] {M : β → Matrix L L' ℂ} {b : β} (hb : M b = 0) : blockKron M = 0

A zero block kills the tensor.

theorem QuantumInfo.blockKron_smul {β : Type u_1} {L : Type u_2} {L' : Type u_3} [Fintype β] (c : β → ℂ) (M : β → Matrix L L' ℂ) : (blockKron fun (b : β) => c b • M b) = (∏ b : β, c b) • blockKron M

Scalars pull out of every block at once.

theorem QuantumInfo.blockKron_sum {β : Type u_1} {L : Type u_2} {L' : Type u_3} {ι : Type u_4} [Fintype β] [DecidableEq β] [Fintype ι] (f : β → ι → Matrix L L' ℂ) : (blockKron fun (b : β) => ∑ i : ι, f b i) = ∑ g : β → ι, blockKron fun (b : β) => f b (g b)

★ Multilinearity: expanding every block over a finite family expands the tensor over the functions choosing one index per block.

theorem QuantumInfo.blockKron_sum_smul {β : Type u_1} {L : Type u_2} {L' : Type u_3} {ι : Type u_4} [Fintype β] [DecidableEq β] [Fintype ι] (a : β → ι → ℂ) (f : β → ι → Matrix L L' ℂ) : (blockKron fun (b : β) => ∑ i : ι, a b i • f b i) = ∑ g : β → ι, (∏ b : β, a b (g b)) • blockKron fun (b : β) => f b (g b)

The same expansion with coefficients, the form the concatenation uses: an arbitrary operator per block is a combination of a fixed finite family.

theorem QuantumInfo.blockKron_single_eq_gateOf {m : ℕ} (b₀ : Fin m) (G : Matrix (Fin 2) (Fin 2) ℂ) : (blockKron fun (b : Fin m) => if b = b₀ then G else 1) = Controlled.gateOf b₀ G

★ One slot filled, the identity elsewhere, is a single-qubit gate: the tensor over blocks with G at b₀ is #83's gateOf b₀ G on the qubit register.

theorem QuantumInfo.blockKron_replace_eq_gateOf_mul {m : ℕ} (A : Fin m → Matrix (Fin 2) (Fin 2) ℂ) (b₀ : Fin m) (E : Matrix (Fin 2) (Fin 2) ℂ) : (blockKron fun (b : Fin m) => if b = b₀ then E * A b₀ else A b) = Controlled.gateOf b₀ E * blockKron A

★★ Error propagation through a transversal gadget: replacing the factor at one block by E * A b₀ — a fault at that location, acting after the ideal single-qubit gate — is the ideal gadget followed by the single-block error E. One faulty location of a transversal gadget is a weight-one error, which is the reason transversal gadgets are fault-tolerant at all.