Coefficient supports factor every finite-dimensional subalgebra

Open

QAlgorithms.Papers.Independent.Intakethird100.P96.support_factorization

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

prove2quantum

Let $B_1,B_2$ be finite-dimensional complex C*-algebras and $A\subseteq B_1\otimes B_2$ a star subalgebra, not required to contain the ambient identity. Let $s_i$ be the linear span of all contractions of elements of $A$ by complex-linear functionals on the other factor. Let $S_i$ be the star algebra generated by $s_i$ , and interpret each tensor product of subspaces as its canonical embedded image. Then

A\subseteq s_1\otimes s_2\subseteq S_1\otimes S_2\subseteq B_1\otimes B_2.

Thus the coefficient supports and their generated algebras retain every element of the original subalgebra.

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)

section SupportAlgebras

variable {B1 B2 B3 : Type*} [CStarAlgebra B1] [CStarAlgebra B2] [CStarAlgebra B3]

/-- §IV.C, equations (21)--(22), PDF p.10: coefficient and generated-support factorization. -/
theorem support_factorization
    [FiniteDimensional ℂ B1] [FiniteDimensional ℂ B2]
    (A : NonUnitalStarSubalgebra ℂ (B1 ⊗[ℂ] B2)) :
    A.toSubmodule ≤ tensorSpan (coefficientLeft (A : Set (B1 ⊗[ℂ] B2)))
      (coefficientRight (A : Set (B1 ⊗[ℂ] B2))) ∧
    tensorSpan (coefficientLeft (A : Set (B1 ⊗[ℂ] B2))) (coefficientRight (A : Set (B1 ⊗[ℂ] B2))) ≤
      tensorSpan (supportLeft (A : Set (B1 ⊗[ℂ] B2))).toSubmodule
        (supportRight (A : Set (B1 ⊗[ℂ] B2))).toSubmodule := by sorry

end SupportAlgebras

end QAlgorithms.Papers.Independent.Intakethird100.P96

end

Source

Reversible quantum cellular automata, arXiv:quant-ph/0405174v1, PDF p. 10, §IV.C, (21)–(22): factorization through coefficient supports

Read-back

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

Suppose the ambient complex algebras $B_1,B_2$ , with their given involutions, are finite dimensional over $\mathbb C$ , and let $A$ be any nonunital complex star subalgebra of $B_1\otimes_{\mathbb C}B_2$ . Let $L\subseteq B_1$ be the complex span of all $\sum_r f(y_r)x_r$ obtained from $a=\sum_r x_r\otimes y_r\in A$ and complex linear $f:B_2\to\mathbb C$ , and let $R\subseteq B_2$ be the complex span of all $\sum_r g(x_r)y_r$ obtained from $a\in A$ and complex linear $g:B_1\to\mathbb C$ . Let $S_L,S_R$ be the smallest nonunital complex star subalgebras containing $L,R$ , respectively. Then both inclusions hold:

A\subseteq \operatorname{span}_{\mathbb C}\{x\otimes y:x\in L,\ y\in R\} \subseteq \operatorname{span}_{\mathbb C}\{x\otimes y:x\in S_L,\ y\in S_R\}.

Here each inclusion concerns the underlying complex linear subspaces, and each span uses finite linear combinations.

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