The tensor intersection of subspaces: the dimension of {X : columns ⊆ U ∧ rows ⊆ W}

The whole difficulty of the dimension tensor formula $k = k_1k_2 + k_1^\top k_2^\top$ is concentrated in one fact: the space of matrices whose columns lie in $U$ and whose rows lie in $W$ has dimension exactly $\dim U\cdot\dim W$ (the dimension count of a subspace tensor intersection, that is, the dimension of $U\otimes W$).

This module proves it in one go (finrank_colsRows), by an explicit equivalence rather than a dimension argument:

• take a basis $u$ of $U$ together with the coordinate read-back linear map $L$ on Fin a → Vec p (a left inverse of an independent family, exists_leftInverse_of_linearIndependent)
• the coefficient expansion vee ($a\times s$ coefficients ↦ $p\times s$ matrices) and the coordinate extraction wedge ($p\times s$ matrices ↦ $a\times s$ coefficients) are mutually inverse
• the key step: the row condition is unaffected by wedge, which translates "the rows all lie in $W$" into "the rows all lie in $W$", so $\{columns\subseteq U,\ rows\subseteq W\}\cong \{\text{rows}\subseteq W\}$, and the latter is isomorphic to Fin a → W, of dimension $a\cdot\dim W$.

The first two auxiliary facts (the dimensions of the column- and row-constrained spaces) are finrank_colsSub / finrank_rowsSub.

Index conventions

Matrices are always written with product indexing, VMat p s = Fin p × Fin s → ZMod 2 (the same row type as hgpHX), and are never flattened into Fin; the structural theorem therefore needs no relabelling.

1. Product-indexed matrices and the two constrained subspaces

@[reducible, inline]

abbrev QECCertificates.VMat (p s : ℕ) : Type

A product-indexed matrix: rows Fin p, columns Fin s.

Equations

• QECCertificates.VMat p s = (Fin p × Fin s → ZMod 2)

def QECCertificates.colOf {p s : ℕ} (X : VMat p s) (j : Fin s) : Vec p

Column j (as a Vec p).

Equations

• QECCertificates.colOf X j i = X (i, j)

def QECCertificates.rowOf {p s : ℕ} (X : VMat p s) (i : Fin p) : Vec s

Row i (as a Vec s).

Equations

• QECCertificates.rowOf X i j = X (i, j)

@[simp]

theorem QECCertificates.colOf_apply {p s : ℕ} {X : VMat p s} {j : Fin s} {i : Fin p} : colOf X j i = X (i, j)

@[simp]

theorem QECCertificates.rowOf_apply {p s : ℕ} {X : VMat p s} {i : Fin p} {j : Fin s} : rowOf X i j = X (i, j)

@[simp]

theorem QECCertificates.colOf_add {p s : ℕ} {X Y : VMat p s} {j : Fin s} : colOf (X + Y) j = colOf X j + colOf Y j

@[simp]

theorem QECCertificates.colOf_smul {p s : ℕ} {c : ZMod 2} {X : VMat p s} {j : Fin s} : colOf (c • X) j = c • colOf X j

@[simp]

theorem QECCertificates.rowOf_add {p s : ℕ} {X Y : VMat p s} {i : Fin p} : rowOf (X + Y) i = rowOf X i + rowOf Y i

@[simp]

theorem QECCertificates.rowOf_smul {p s : ℕ} {c : ZMod 2} {X : VMat p s} {i : Fin p} : rowOf (c • X) i = c • rowOf X i

def QECCertificates.colsSub {p s : ℕ} (U : Submodule (ZMod 2) (Vec p)) : Submodule (ZMod 2) (VMat p s)

The column-constrained subspace: the matrices all of whose columns lie in U.

Equations

• QECCertificates.colsSub U = { carrier := {X : QECCertificates.VMat p s | ∀ (j : Fin s), QECCertificates.colOf X j ∈ U}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }

def QECCertificates.rowsSub {p s : ℕ} (W : Submodule (ZMod 2) (Vec s)) : Submodule (ZMod 2) (VMat p s)

The row-constrained subspace: the matrices all of whose rows lie in W.

Equations

• QECCertificates.rowsSub W = { carrier := {X : QECCertificates.VMat p s | ∀ (i : Fin p), QECCertificates.rowOf X i ∈ W}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }

@[simp]

theorem QECCertificates.mem_colsSub {p s : ℕ} {U : Submodule (ZMod 2) (Vec p)} {X : VMat p s} : X ∈ colsSub U ↔ ∀ (j : Fin s), colOf X j ∈ U

@[simp]

theorem QECCertificates.mem_rowsSub {p s : ℕ} {W : Submodule (ZMod 2) (Vec s)} {X : VMat p s} : X ∈ rowsSub W ↔ ∀ (i : Fin p), rowOf X i ∈ W

2. The dimensions of the column- and row-constrained spaces

noncomputable def QECCertificates.colsSubEquiv {p s : ℕ} (U : Submodule (ZMod 2) (Vec p)) : ↥(colsSub U) ≃ₗ[ZMod 2] Fin s → ↥U

An explicit linear equivalence between the matrices with all columns in U and Fin s → U (reading column by column).

Equations

• One or more equations did not get rendered due to their size.

noncomputable def QECCertificates.rowsSubEquiv {p s : ℕ} (W : Submodule (ZMod 2) (Vec s)) : ↥(rowsSub W) ≃ₗ[ZMod 2] Fin p → ↥W

An explicit linear equivalence between the matrices with all rows in W and Fin p → W (reading row by row).

Equations

• One or more equations did not get rendered due to their size.

theorem QECCertificates.finrank_colsSub {p s : ℕ} (U : Submodule (ZMod 2) (Vec p)) : Module.finrank (ZMod 2) ↥(colsSub U) = s * Module.finrank (ZMod 2) ↥U

The dimension of the column-constrained space: $\dim\{X : \mathrm{col}\,X\subseteq U\} = s\cdot\dim U$.

theorem QECCertificates.finrank_rowsSub {p s : ℕ} (W : Submodule (ZMod 2) (Vec s)) : Module.finrank (ZMod 2) ↥(rowsSub W) = p * Module.finrank (ZMod 2) ↥W

The dimension of the row-constrained space: $\dim\{X : \mathrm{row}\,X\subseteq W\} = p\cdot\dim W$.

3. Coordinate read-back of an independent family (left inverse)

theorem QECCertificates.linearMap_apply_eq_sum_single {p a : ℕ} (L : Vec p →ₗ[ZMod 2] Fin a → ZMod 2) (x : Vec p) : L x = fun (k : Fin a) => ∑ i : Fin p, x i * L (Pi.single i 1) k

The matrix representation of a linear map in the standard basis: L x = Σ_i x_i · L(e_i).

theorem QECCertificates.exists_leftInverse_of_linearIndependent {p a : ℕ} {u : Fin a → Vec p} (hu : LinearIndependent (ZMod 2) u) : ∃ (L : Vec p →ₗ[ZMod 2] Fin a → ZMod 2), ∀ (c : Fin a → ZMod 2), L (∑ k : Fin a, c k • u k) = c

Left inverse of an independent family: when u : Fin a → Vec p is linearly independent, there is a linear map L that reads the coefficients $c$ back from any combination $\sum_k c_k u_k$.

The construction: the combination map $\varphi(c)=\sum_k c_k u_k$ is injective by independence, and one takes a left inverse of it on the whole space (LinearMap.exists_leftInverse_of_injective: over a vector space every injective linear map has a left inverse).

4. Coefficient expansion vee and coordinate extraction wedge

noncomputable def QECCertificates.vee {p s a : ℕ} (u : Fin a → Vec p) : VMat a s →ₗ[ZMod 2] VMat p s

Coefficient expansion: expands an a×s coefficient matrix along the basis vectors of U into a p×s matrix (column j is $\sum_k C_{kj}u_k$).

Equations

• QECCertificates.vee u = { toFun := fun (C : QECCertificates.VMat a s) (ij : Fin p × Fin s) => ∑ k : Fin a, C (k, ij.2) * u k ij.1, map_add' := ⋯, map_smul' := ⋯ }

noncomputable def QECCertificates.wedge {p s a : ℕ} (L : Vec p →ₗ[ZMod 2] Fin a → ZMod 2) : VMat p s →ₗ[ZMod 2] VMat a s

Coordinate extraction: reads each column of a p×s matrix as coefficients, through the left inverse L.

Equations

• QECCertificates.wedge L = { toFun := fun (X : QECCertificates.VMat p s) (kj : Fin a × Fin s) => L (QECCertificates.colOf X kj.2) kj.1, map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem QECCertificates.vee_apply {p s a : ℕ} (u : Fin a → Vec p) (C : VMat a s) (i : Fin p) (j : Fin s) : (vee u) C (i, j) = ∑ k : Fin a, C (k, j) * u k i

@[simp]

theorem QECCertificates.wedge_apply {p s a : ℕ} (L : Vec p →ₗ[ZMod 2] Fin a → ZMod 2) (X : VMat p s) (k : Fin a) (j : Fin s) : (wedge L) X (k, j) = L (colOf X j) k

theorem QECCertificates.vee_wedge_of_coords {p s a : ℕ} {u : Fin a → Vec p} {L : Vec p →ₗ[ZMod 2] Fin a → ZMod 2} {U : Submodule (ZMod 2) (Vec p)} (hcoords : ∀ x ∈ U, ∑ k : Fin a, L x k • u k = x) {X : VMat p s} (hX : ∀ (j : Fin s), colOf X j ∈ U) : (vee u) ((wedge L) X) = X

vee after wedge is the identity (on the column-constrained space): vee is a left inverse of wedge.

theorem QECCertificates.wedge_vee {p s a : ℕ} {u : Fin a → Vec p} {L : Vec p →ₗ[ZMod 2] Fin a → ZMod 2} (hleft : ∀ (c : Fin a → ZMod 2), L (∑ k : Fin a, c k • u k) = c) (C : VMat a s) : (wedge L) ((vee u) C) = C

wedge after vee is the identity (everywhere): vee is a right inverse of wedge.

5. The row condition under wedge

theorem QECCertificates.rowOf_wedge_mem {p s a : ℕ} {L : Vec p →ₗ[ZMod 2] Fin a → ZMod 2} {W : Submodule (ZMod 2) (Vec s)} {X : VMat p s} (hX : ∀ (i : Fin p), rowOf X i ∈ W) (k : Fin a) : rowOf ((wedge L) X) k ∈ W

The row condition pushes forward: if the rows of X all lie in W, then so do the rows of wedge L X (substituting the matrix representation L x = Σ_i x_i · L(e_i) into the row sums of wedge).

theorem QECCertificates.rowOf_mem_of_wedge_rowOf_mem {p s a : ℕ} {u : Fin a → Vec p} {L : Vec p →ₗ[ZMod 2] Fin a → ZMod 2} {U : Submodule (ZMod 2) (Vec p)} {W : Submodule (ZMod 2) (Vec s)} (hcoords : ∀ x ∈ U, ∑ k : Fin a, L x k • u k = x) {X : VMat p s} (hX : ∀ (j : Fin s), colOf X j ∈ U) (hY : ∀ (k : Fin a), rowOf ((wedge L) X) k ∈ W) (i : Fin p) : rowOf X i ∈ W

The row condition pulls back: if the rows of wedge L X all lie in W and the columns of X all lie in U, then the rows of X all lie in W (using vee_wedge_of_coords to write the rows of X as combinations of the rows of wedge L X).

6. Main theorem: the dimension of the tensor intersection

theorem QECCertificates.finrank_colsRows {p s : ℕ} (U : Submodule (ZMod 2) (Vec p)) (W : Submodule (ZMod 2) (Vec s)) : Module.finrank (ZMod 2) ↥(colsSub U ⊓ rowsSub W) = Module.finrank (ZMod 2) ↥U * Module.finrank (ZMod 2) ↥W

The dimension of the tensor intersection: the space of matrices with columns in U and rows in W has dimension exactly $\dim U\cdot\dim W$.

This is the only nontrivial dimension input to the tensor formula $k=k_1k_2+k_1^\top k_2^\top$ (the dimension of $U\otimes W$ in the language of matrices). The proof goes through an explicit equivalence:

$$\{X:\mathrm{col}\,X\subseteq U,\ \mathrm{row}\,X\subseteq W\}\;\cong\;\mathrm{Fin}\,a\to W, \qquad a=\dim U,$$

the forward map extracting coordinates with wedge and then taking rows, the backward map forming vee from the W-combinations of the coefficient rows.