Finite-dimensional complex C*-algebras have unique matrix block sizes

Open

QAlgorithms.Papers.Independent.Intakethird100.P96.finite_cstar_classification

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

prove2quantum

Let $A$ be a finite-dimensional complex C*-algebra. There is a unique finite nonincreasing list of positive integers $n_1\ge\cdots\ge n_k\ge1$ for which

A\cong\bigoplus_{\mu=1}^k M_{n_\mu}(\mathbb C)

as complex star algebras. The empty list is allowed and represents the zero algebra. The isomorphism itself need not be unique.

The ordered list completely determines the algebra up to star isomorphism. A finite direct sum is represented by the componentwise finite product.

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 11, PDF p.18: unique ordered positive matrix sizes.
The empty list represents the zero algebra. Finite products are finite direct sums. -/
theorem finite_cstar_classification (A : Type*) [CStarAlgebra A] [FiniteDimensional ℂ A] :
    ∃! sizes : List ℕ,
      (∀ n ∈ sizes, 0 < n) ∧ sizes.Pairwise (fun a b => b ≤ a) ∧
      Nonempty (A ≃⋆ₐ[ℂ] ((i : Fin sizes.length) → Mat (sizes.get i))) := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P96

end

Source

Reversible quantum cellular automata, arXiv:quant-ph/0405174v1, PDF p. 18, Proposition 11: finite-dimensional C*-algebra classification

Read-back

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

For every complex $C^{*}$ -algebra $A$ that is finite dimensional over $\mathbb C$ , there exists exactly one finite list of natural numbers $(s_0,\ldots,s_{\ell-1})$ such that every entry is strictly positive, the entries are weakly decreasing ( $s_j\le s_i$ whenever $i<j$ ), and there exists a complex linear, multiplicative, involution-preserving algebra equivalence

A\cong \prod_{i=0}^{\ell-1}M_{s_i}(\mathbb C).

The uniqueness concerns the list of sizes; the equivalence is only asserted to exist. The list may be empty, in which case the product is the algebra with one element.

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