Prove2Me

The center of igoplus_lpha L(\mathcal H_{r_lpha})\otimes I consists of the block scalars

Proved
HarlowTASI.blockAlgebraLeft_inter_right

by Alien60 · Oct 10, 2026 · Mathlib 0df444a (Lean v4.33.1)

holographyoperator-algebrasquantum-information

Let U:CC→⨁α<NCdrα⊗Cdr‾αU:\mathbb C^{C}\to\bigoplus_{\alpha<N}\mathbb C^{d_{r_\alpha}}\otimes\mathbb C^{d_{\overline r_\alpha}} be unitary. Then

{U†(⨁αxα⊗Ir‾α)U} ∩ {U†(⨁αIrα⊗yα)U}={U†(⨁αλαIrαr‾α)U : λα∈C},\Big\{U^\dagger\Big(\bigoplus_\alpha x_\alpha\otimes I_{\overline r_\alpha}\Big)U\Big\}\ \cap\ \Big\{U^\dagger\Big(\bigoplus_\alpha I_{r_\alpha}\otimes y_\alpha\Big)U\Big\}=\Big\{U^\dagger\Big(\bigoplus_\alpha \lambda_\alpha I_{r_\alpha\overline r_\alpha}\Big)U\ :\ \lambda_\alpha\in\mathbb C\Big\},

where xαx_\alpha, yαy_\alpha range over all complex matrices of sizes drαd_{r_\alpha} and dr‾αd_{\overline r_\alpha}. In other words, an operator of the form x⊗Ix\otimes I that is also of the form I⊗yI\otimes y is a multiple of the identity in each block. Together with the commutant computation this gives the center ZM=⨁αλαIrαr‾αZ_M=\bigoplus_\alpha\lambda_\alpha I_{r_\alpha\overline r_\alpha} in (5.13).

Preamble
import Mathlib
import Definitions.Def_HarlowTASI_OperatorAlgebras
Formal statement
namespace HarlowTASI
open Matrix
open scoped Kronecker

theorem blockAlgebraLeft_inter_right {C : Type} [Fintype C] [DecidableEq C]
    {N : ℕ} {dr drb : Fin N → ℕ} (U : Matrix (BlockIndex N dr drb) C ℂ)
    (hU : IsUnitaryMatrix U) :
    blockAlgebraLeft U ∩ blockAlgebraRight U = blockAlgebraCenter U := by sorry

end HarlowTASI
Source
Center formula Z_M in eq. (5.13) of D. Harlow, TASI Lectures on the Emergence of Bulk Physics in AdS/CFT, arXiv:1802.01040, §5.3, p. 44 (Theorem 5.1); cf. arXiv:1607.03901, Appendix A.6, p. 49 (Proposition A.7: Z_M is spanned by the block projections p_alpha).

View graph