Commuting subalgebras have commuting shared-factor supports

Open

QAlgorithms.Papers.Independent.Intakethird100.P96.shared_supports_commute

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

prove2quantum

Let $B_1,B_2,B_3$ be finite-dimensional complex C*-algebras, $A_1\subseteq B_1\otimes B_2$ and $A_2\subseteq B_2\otimes B_3$ star subalgebras. Suppose $A_1\otimes1$ and $1\otimes A_2$ commute elementwise in the common three-factor algebra. Define each support algebra by generating the star algebra from all coefficient slices on the indicated factor. Then

[S(A_1,B_2),S(A_2,B_2)]=0.

This transfers commutation to the common tensor factor; no containment of the ambient identity in either subalgebra is required.

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]

/-- Lemma 8, PDF p.10: supports on the common middle factor commute. -/
theorem shared_supports_commute
    [FiniteDimensional ℂ B1] [FiniteDimensional ℂ B2] [FiniteDimensional ℂ B3]
    (A1 : NonUnitalStarSubalgebra ℂ (B1 ⊗[ℂ] B2))
    (A2 : NonUnitalStarSubalgebra ℂ (B2 ⊗[ℂ] B3))
    (hcomm : ∀ a ∈ A1, ∀ b ∈ A2,
      Commute ((TensorProduct.assoc ℂ B1 B2 B3) (a ⊗ₜ[ℂ] (1 : B3)))
        ((1 : B1) ⊗ₜ[ℂ] b)) :
    ∀ x ∈ supportRight (A1 : Set (B1 ⊗[ℂ] B2)), ∀ y ∈ supportLeft (A2 : Set (B2 ⊗[ℂ] B3)), Commute x y := by sorry

end SupportAlgebras

end QAlgorithms.Papers.Independent.Intakethird100.P96

end

Source

Reversible quantum cellular automata, arXiv:quant-ph/0405174v1, PDF p. 10, Lemma 8: commutation passes to shared-factor supports

Read-back

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

Suppose the ambient unital complex algebras $B_1,B_2,B_3$ , with their given involutions, are finite dimensional over $\mathbb C$ . Let $A_1\subseteq B_1\otimes_{\mathbb C}B_2$ and $A_2\subseteq B_2\otimes_{\mathbb C}B_3$ be nonunital complex star subalgebras. Assume that for every $a\in A_1$ and $b\in A_2$ , the elements $\alpha(a\otimes1_{B_3})$ and $1_{B_1}\otimes b$ commute in $B_1\otimes_{\mathbb C}(B_2\otimes_{\mathbb C}B_3)$ , where $\alpha$ is the canonical tensor reassociation map. Let $S_1\subseteq B_2$ be the smallest nonunital complex star subalgebra containing the complex span of all right contractions $\sum_r f(x_r)y_r$ of $a=\sum_r x_r\otimes y_r\in A_1$ , for complex linear $f:B_1\to\mathbb C$ . Let $S_2\subseteq B_2$ be the smallest nonunital complex star subalgebra containing the complex span of all left contractions $\sum_r g(w_r)z_r$ of $b=\sum_r z_r\otimes w_r\in A_2$ , for complex linear $g:B_3\to\mathbb C$ . Then every $x\in S_1$ commutes with every $y\in S_2$ : $xy=yx$ .

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