Prove2Me

Product rule for dimensions: dim⁡((Y⊗CB)∩(CA⊗W))=dim⁡Y⋅dim⁡W\dim\big((Y \otimes \mathbb{C}^B) \cap (\mathbb{C}^A \otimes W)\big) = \dim Y \cdot \dim W

Proved
QLLL.QSAT.finrank_inf_liftL_liftR

by sattath · Oct 6, 2026 · Mathlib 0df444a (Lean v4.33.1)

k-qsatlinear-algebraquantum-lll

Let AA and BB be finite sets, and identify CA⊗CB\mathbb{C}^A \otimes \mathbb{C}^B with CA×B\mathbb{C}^{A \times B}. For a subspace Y⊆CAY \subseteq \mathbb{C}^A let liftL(Y)\mathrm{lift}_L(Y) be the functions f:A×B→Cf : A \times B \to \mathbb{C} all of whose column slices f(⋅,b)f(\cdot, b) lie in YY, and for W⊆CBW \subseteq \mathbb{C}^B let liftR(W)\mathrm{lift}_R(W) be the functions all of whose row slices f(a,⋅)f(a, \cdot) lie in WW. Then

dim⁡(liftL(Y)∩liftR(W)) = dim⁡Y⋅dim⁡W.\dim\big(\mathrm{lift}_L(Y) \cap \mathrm{lift}_R(W)\big) \ =\ \dim Y \cdot \dim W.

This is the dimension count in the proof of Lemma 11 of Ambainis, Kempe and Sattath, dim⁡(π⊗⋂iπi)=dim⁡π⋅dim⁡⋂iπi\dim(\pi \otimes \bigcap_i \pi_i) = \dim \pi \cdot \dim \bigcap_i \pi_i, in the function model of the qubit space. It yields the mutual R-independence of constraints acting on disjoint qubits.

Preamble
import Definitions.Def_QLLL_LocalLemma_Basic
import Definitions.Def_QLLL_Quantum_KQSAT_Basic
import Mathlib

open QLLL
open QLLL.QSAT
open Finset Module
variable {n : ℕ}
open scoped Kronecker
variable {A B : Type*} [Fintype A] [Fintype B] [DecidableEq A] [DecidableEq B]
omit [Fintype A] [Fintype B] [DecidableEq A] [DecidableEq B]
Formal statement
theorem QLLL.QSAT.finrank_inf_liftL_liftR [Finite A] [Finite B]
    (Y : Submodule ℂ (A → ℂ)) (W : Submodule ℂ (B → ℂ)) :
    Module.finrank ℂ ((liftL Y ⊓ liftR W : Submodule ℂ ((A × B) → ℂ)))
      = Module.finrank ℂ Y * Module.finrank ℂ W := by sorry
Source
A. Ambainis, J. Kempe, O. Sattath, A Quantum Lovász Local Lemma, J. ACM 59(5):24 (2012), arXiv:0911.1696 (numbering of the arXiv version), proof of Lemma 11 (dimension of a tensor product of subspaces)

View graph