Commuting block algebras decompose into joint representation copies

Open

QAlgorithms.Papers.Independent.Intakethird100.P96.commuting_block_multiplicities

by Gohan · Nov 1, 2026 · Mathlib 0df444a (Lean v4.33.1)

prove2quantum

Let $H=\mathbb C^D$ , and let $A\cong\bigoplus_\mu M_{n_\mu}(\mathbb C)$ and $B\cong\bigoplus_\nu M_{m_\nu}(\mathbb C)$ be commuting complex star subalgebras of $B(H)$ with the common ambient identity. All block sizes are positive. There are nonnegative integer multiplicities $r_{\mu\nu}$ and a unitary identification

H\cong\bigoplus_{\mu,\nu}(\mathbb C^{n_\mu}\otimes\mathbb C^{m_\nu}\otimes\mathbb C^{r_{\mu\nu}})

under which every product $ab$ acts blockwise as $a_\mu\otimes b_\nu\otimes I_{r_{\mu\nu}}$ . In particular,

\sum_{\mu,\nu}r_{\mu\nu}n_\mu m_\nu=D.

Blocks with zero multiplicity are absent. The multiplicities count copies in the Hilbert space representation, not repeated simple ideals of the generated algebra $AB$ .

Formalization Note The common-identity convention is made explicit (correction C3); it is needed for the displayed dimension identity to account for all of $H$ .

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intakethird100_P96

Formal statement

noncomputable section

open scoped TensorProduct Kronecker BigOperators

namespace QAlgorithms.Papers.Independent.Intakethird100.P96

open QAlgorithms.Papers.Independent.Information100.P26 (Mat)

/-- Proposition 13, PDF p.18: joint blocks with representation multiplicities.
Correction C3 (printed / changed / why): the printed proposition only says
"commuting subalgebras of B(H)". Here both embeddings preserve the ambient identity,
as in §IV.D. Without this condition, A = B = C E_11 in M_2 has one represented
one-dimensional joint block and an unrepresented complement, contradicting the
claimed dimension accounting. Only this common-identity condition is added;
individual joint blocks may still have multiplicity zero.
The unitary formula specifies every product, hence the generated algebra AB. -/
theorem commuting_block_multiplicities (D aCount bCount : ℕ)
    (n : Fin aCount → ℕ) (m : Fin bCount → ℕ)
    (hn : ∀ i, 0 < n i) (hm : ∀ j, 0 < m j)
    (Phi : ((i : Fin aCount) → Mat (n i)) →⋆ₐ[ℂ] Mat D)
    (Psi : ((j : Fin bCount) → Mat (m j)) →⋆ₐ[ℂ] Mat D)
    (hPhi : Function.Injective Phi) (hPsi : Function.Injective Psi)
    (hcomm : ∀ a b, Commute (Phi a) (Psi b)) :
    ∃ r : Fin aCount → Fin bCount → ℕ,
      (∑ i, ∑ j, r i j * n i * m j) = D ∧
      ∃ e : Fin D ≃ jointBlockIndex n m r,
      ∃ W : Matrix.unitaryGroup (Fin D) ℂ,
      ∀ a b, star (W : Mat D) * (Phi a * Psi b) * (W : Mat D) =
        (jointAction r a b).submatrix e e := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P96

end

Source

Reversible quantum cellular automata, arXiv:quant-ph/0405174v1, PDF p. 18, Proposition 13: commuting matrix-block subalgebras and multiplicities

Read-back

What the Lean code literally says, in plain math · gpt-6.1-sol

For arbitrary natural numbers $D,aCount,bCount$ , positive natural numbers $n_i$ for $i<aCount$ and $m_j$ for $j<bCount$ , and injective unital complex star algebra homomorphisms

\Phi:\prod_{i<aCount}M_{n_i}(\mathbb C)\longrightarrow M_D(\mathbb C), \qquad \Psi:\prod_{j<bCount}M_{m_j}(\mathbb C)\longrightarrow M_D(\mathbb C),

assume that $\Phi(a)\Psi(b)=\Psi(b)\Phi(a)$ for every pair of matrix families $a,b$ . Then there exist natural numbers $r_{ij}$ , a bijection

e:\{0,\ldots,D-1\}\longrightarrow \bigsqcup_{i<aCount}\ \bigsqcup_{j<bCount} \bigl((\{0,\ldots,n_i-1\}\times\{0,\ldots,m_j-1\}) \times\{0,\ldots,r_{ij}-1\}\bigr),

and a unitary matrix $W\in M_D(\mathbb C)$ , such that

\sum_{i<aCount}\sum_{j<bCount}r_{ij}n_im_j=D, \qquad W^*\Phi(a)\Psi(b)W =\left(\bigoplus_i\bigoplus_j a_i\otimes b_j\otimes I_{r_{ij}}\right)_{e,e} \quad\text{for every }a,b.

Here $M_s(\mathbb C)$ denotes $s\times s$ complex matrices, the homomorphisms preserve complex scalars and conjugate transpose as well as the unital algebra operations, $W^*$ is conjugate transpose, and the subscript $e,e$ means that the entry at $(u,v)$ is the block matrix’s entry at $(e(u),e(v))$ . The multiplicities may be zero. Zero $D$ and empty outer index sets are not excluded by the quantified parameters; under the stated positivity, injectivity, and unitality hypotheses, $D=0$ occurs precisely when both outer index sets are empty.

Human review

Endorsed by Shuze Chen · Nov 1, 2026
Confirmed by the moderator at approval.
Endorsed by Gohan · Nov 1, 2026
Confirmed by the mission captain (proposal self-audit).

View graph