Rank-nullity and the X-projection / diagonal-orthogonal identity.

def LeanPool.SingleCopyStabilizer.dotForm {𝕜 : Type u_1} [Field 𝕜] {ι : Type u_2} [Fintype ι] : LinearMap.BilinForm 𝕜 (Vec 𝕜 ι)

The coordinate dot product regarded as a bilinear form.

Equations

• LeanPool.SingleCopyStabilizer.dotForm = dotProductBilin 𝕜 𝕜

theorem LeanPool.SingleCopyStabilizer.dotForm_nondegenerate {𝕜 : Type u_1} [Field 𝕜] {ι : Type u_2} [Fintype ι] : dotForm.Nondegenerate

theorem LeanPool.SingleCopyStabilizer.dotForm_refl {𝕜 : Type u_1} [Field 𝕜] {ι : Type u_2} [Fintype ι] : dotForm.IsRefl

def LeanPool.SingleCopyStabilizer.dotOrthogonal {𝕜 : Type u_1} [Field 𝕜] {ι : Type u_2} [Fintype ι] (D : Submodule 𝕜 (Vec 𝕜 ι)) : Submodule 𝕜 (Vec 𝕜 ι)

The annihilator of a subspace under the coordinate dot product.

Equations

• LeanPool.SingleCopyStabilizer.dotOrthogonal D = LeanPool.SingleCopyStabilizer.dotForm.orthogonal D

@[simp]

theorem LeanPool.SingleCopyStabilizer.mem_dotOrthogonal {𝕜 : Type u_1} [Field 𝕜] {ι : Type u_2} [Fintype ι] (D : Submodule 𝕜 (Vec 𝕜 ι)) (x : Vec 𝕜 ι) : x ∈ dotOrthogonal D ↔ ∀ s ∈ D, x ⬝ᵥ s = 0

theorem LeanPool.SingleCopyStabilizer.finrank_dotOrthogonal {𝕜 : Type u_1} [Field 𝕜] {ι : Type u_2} [Fintype ι] (D : Submodule 𝕜 (Vec 𝕜 ι)) : Module.finrank 𝕜 ↥(dotOrthogonal D) = Fintype.card ι - Module.finrank 𝕜 ↥D

def LeanPool.SingleCopyStabilizer.xProjection {𝕜 : Type u_1} [Field 𝕜] {ι : Type u_2} (L : Submodule 𝕜 (Label 𝕜 ι)) : Submodule 𝕜 (Vec 𝕜 ι)

The X-coordinate image of a space of Pauli labels.

Equations

• LeanPool.SingleCopyStabilizer.xProjection L = Submodule.map (LinearMap.fst 𝕜 (LeanPool.SingleCopyStabilizer.Vec 𝕜 ι) (LeanPool.SingleCopyStabilizer.Vec 𝕜 ι)) L

@[simp]

theorem LeanPool.SingleCopyStabilizer.mem_xProjection {𝕜 : Type u_1} [Field 𝕜] {ι : Type u_2} (L : Submodule 𝕜 (Label 𝕜 ι)) (x : Vec 𝕜 ι) : x ∈ xProjection L ↔ ∃ (z : Vec 𝕜 ι), (x, z) ∈ L

def LeanPool.SingleCopyStabilizer.xRestricted {𝕜 : Type u_1} [Field 𝕜] {ι : Type u_2} (L : Submodule 𝕜 (Label 𝕜 ι)) : ↥L →ₗ[𝕜] Vec 𝕜 ι

The X projection with domain restricted to a given label space.

Equations

• LeanPool.SingleCopyStabilizer.xRestricted L = (LinearMap.fst 𝕜 (LeanPool.SingleCopyStabilizer.Vec 𝕜 ι) (LeanPool.SingleCopyStabilizer.Vec 𝕜 ι)).domRestrict L

def LeanPool.SingleCopyStabilizer.diagonalKernelEquiv {𝕜 : Type u_1} [Field 𝕜] {ι : Type u_2} (L : Submodule 𝕜 (Label 𝕜 ι)) : ↥(diagonalSpace L) ≃ₗ[𝕜] ↥(xRestricted L).ker

Identify diagonal labels with the kernel of the restricted X projection.

Equations

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

theorem LeanPool.SingleCopyStabilizer.finrank_xProjection_add_diagonal {𝕜 : Type u_1} [Field 𝕜] {ι : Type u_2} [Finite ι] (L : Submodule 𝕜 (Label 𝕜 ι)) : Module.finrank 𝕜 ↥(xProjection L) + Module.finrank 𝕜 ↥(diagonalSpace L) = Module.finrank 𝕜 ↥L

Rank-nullity with the diagonal kernel explicitly identified.

theorem LeanPool.SingleCopyStabilizer.xProjection_le_orthogonal {𝕜 : Type u_1} [Field 𝕜] {ι : Type u_2} [Fintype ι] (L : Submodule 𝕜 (Label 𝕜 ι)) (hL : IsIsotropic L) : xProjection L ≤ dotOrthogonal (diagonalSpace L)

theorem LeanPool.SingleCopyStabilizer.lagrangian_xProjection_eq {𝕜 : Type u_1} [Field 𝕜] {ι : Type u_2} [Fintype ι] (L : Submodule 𝕜 (Label 𝕜 ι)) (hL : IsIsotropic L) (hdim : Module.finrank 𝕜 ↥L = Fintype.card ι) : xProjection L = dotOrthogonal (diagonalSpace L)

For a Lagrangian label space, the X projection is exactly the orthogonal complement of the diagonal labels.

theorem LeanPool.SingleCopyStabilizer.low_nullity_projection_codimension {𝕜 : Type u_1} [Field 𝕜] {ι : Type u_2} [Fintype ι] (L : Submodule 𝕜 (Label 𝕜 ι)) (r : ℕ) (hdim : Module.finrank 𝕜 ↥L + r = Fintype.card ι) : Module.finrank 𝕜 ↥(xProjection L) + r = Module.finrank 𝕜 ↥(dotOrthogonal (diagonalSpace L))

The general dimension identity underlying the nullity argument.

theorem LeanPool.SingleCopyStabilizer.isotropic_finrank_le {𝕜 : Type u_1} [Field 𝕜] {ι : Type u_2} [Fintype ι] (L : Submodule 𝕜 (Label 𝕜 ι)) (hL : IsIsotropic L) : Module.finrank 𝕜 ↥L ≤ Fintype.card ι

Isotropy bounds stabilizer dimension by the number of sites.

theorem LeanPool.SingleCopyStabilizer.all_diagonal_of_max_dimension {𝕜 : Type u_1} [Field 𝕜] {ι : Type u_2} [Finite ι] (L : Submodule 𝕜 (Label 𝕜 ι)) (hdim : Module.finrank 𝕜 ↥(diagonalSpace L) = Module.finrank 𝕜 ↥L) (a : Label 𝕜 ι) : a ∈ L → a.1 = 0

When diagonal dimension reaches total stabilizer dimension, every stabilizer is diagonal. This applies to the low-nullity stopping criterion.

theorem LeanPool.SingleCopyStabilizer.diagonalSpace_eq_top_of_full_dimension {𝕜 : Type u_1} [Field 𝕜] {ι : Type u_2} [Fintype ι] (L : Submodule 𝕜 (Label 𝕜 ι)) (hdim : Module.finrank 𝕜 ↥(diagonalSpace L) = Fintype.card ι) : diagonalSpace L = ⊤

Full diagonal dimension means all diagonal labels are present.