Definition 26: Balanced Product Tanner Cycle Code

The balanced product Tanner cycle code is C(X,L) ⊗_{ℤ_ℓ} C(C_ℓ) (Def_23), a quantum CSS code whose total complex has three terms corresponding to physical qubits (C_1), Z-checks (∂_2^Tot), and X-checks (∂_1^Tot).

@[reducible, inline]

abbrev BalancedProductTannerCycleCode.C1 {H : Type} [Group H] [Fintype H] (X : GraphWithGroupAction H) : ModuleCat 𝔽₂

Equations

• BalancedProductTannerCycleCode.C1 X = ModuleCat.of 𝔽₂ (X.graph.cells 1 → 𝔽₂)

@[reducible, inline]

abbrev BalancedProductTannerCycleCode.C0 {H : Type} [Group H] [Fintype H] (X : GraphWithGroupAction H) {s : ℕ} : ModuleCat 𝔽₂

Equations

• BalancedProductTannerCycleCode.C0 X = ModuleCat.of 𝔽₂ (X.graph.cells 0 → Fin s → 𝔽₂)

def BalancedProductTannerCycleCode.cellLocalView {H : Type} [Group H] [Fintype H] (X : GraphWithGroupAction H) {s : ℕ} (Λ : X.CellLabeling s) (v : X.graph.cells 0) : (X.graph.cells 1 → 𝔽₂) →ₗ[𝔽₂] Fin s → 𝔽₂

Equations

• BalancedProductTannerCycleCode.cellLocalView X Λ v = { toFun := fun (c : X.graph.cells 1 → 𝔽₂) (i : Fin s) => c ↑((Λ v).symm i), map_add' := ⋯, map_smul' := ⋯ }

def BalancedProductTannerCycleCode.tannerDifferential {H : Type} [Group H] [Fintype H] (X : GraphWithGroupAction H) {s : ℕ} (Λ : X.CellLabeling s) : (X.graph.cells 1 → 𝔽₂) →ₗ[𝔽₂] X.graph.cells 0 → Fin s → 𝔽₂

Equations

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

Direct chain complex constructions

def BalancedProductTannerCycleCode.tannerCodeComplex {H : Type} [Group H] [Fintype H] [DecidableEq H] (X : GraphWithGroupAction H) {s : ℕ} (Λ : X.CellLabeling s) : ChainComplex𝔽₂

Equations

• BalancedProductTannerCycleCode.tannerCodeComplex X Λ = { X := BalancedProductTannerCycleCode.tannerObj✝ X s, d := BalancedProductTannerCycleCode.tannerMor✝ X s Λ, shape := ⋯, d_comp_d' := ⋯ }

theorem BalancedProductTannerCycleCode.tannerCodeComplex_X_subsingleton {H : Type} [Group H] [Fintype H] [DecidableEq H] (X : GraphWithGroupAction H) {s : ℕ} (Λ : X.CellLabeling s) {p : ℤ} (hp0 : p ≠ 0) (hp1 : p ≠ 1) : Subsingleton ↑((tannerCodeComplex X Λ).X p)

The Tanner code chain complex has trivial (PUnit) module at degrees outside {0, 1}.

H-actions

def BalancedProductTannerCycleCode.actionC1 {H : Type} [Group H] [Fintype H] (X : GraphWithGroupAction H) : Representation 𝔽₂ H (X.graph.cells 1 → 𝔽₂)

Equations

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

def BalancedProductTannerCycleCode.actionC0 {H : Type} [Group H] [Fintype H] (X : GraphWithGroupAction H) {s : ℕ} : Representation 𝔽₂ H (X.graph.cells 0 → Fin s → 𝔽₂)

Equations

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

theorem BalancedProductTannerCycleCode.tannerDifferential_equivariant {H : Type} [Group H] [Fintype H] [DecidableEq H] (X : GraphWithGroupAction H) {s : ℕ} (Λ : X.CellLabeling s) (hΛ : GraphWithGroupAction.IsInvariantLabeling Λ) (h : H) : tannerDifferential X Λ ∘ₗ (actionC1 X) h = (actionC0 X) h ∘ₗ tannerDifferential X Λ

def BalancedProductTannerCycleCode.tannerCodeHEquivariant {H : Type} [Group H] [Fintype H] [DecidableEq H] (X : GraphWithGroupAction H) {s : ℕ} (Λ : X.CellLabeling s) (hΛ : GraphWithGroupAction.IsInvariantLabeling Λ) : HEquivariantChainComplex H

Equations

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

Cycle graph chain complex (direct construction)

def BalancedProductTannerCycleCode.cycleComplex (ℓ : ℕ) [NeZero ℓ] : ChainComplex𝔽₂

Equations

• BalancedProductTannerCycleCode.cycleComplex ℓ = { X := BalancedProductTannerCycleCode.cycleObj✝ ℓ, d := BalancedProductTannerCycleCode.cycleMor✝ ℓ, shape := ⋯, d_comp_d' := ⋯ }

theorem BalancedProductTannerCycleCode.cycleComplex_X_subsingleton (ℓ : ℕ) [NeZero ℓ] {p : ℤ} (hp0 : p ≠ 0) (hp1 : p ≠ 1) : Subsingleton ↑((cycleComplex ℓ).X p)

The cycle graph chain complex has trivial (PUnit) module at degrees outside {0, 1}.

H-action on Cycle Graph

def BalancedProductTannerCycleCode.CycleCompatibleAction {H : Type} [Group H] (ℓ : ℕ) [NeZero ℓ] [MulAction H (Fin ℓ)] : Prop

The H-action on Fin ℓ is compatible with the cycle graph boundary: h • pred(i) = pred(h • i) where pred(i) = ⟨(i + ℓ - 1) % ℓ, _⟩.

Equations

• BalancedProductTannerCycleCode.CycleCompatibleAction ℓ = ∀ (h : H) (i : Fin ℓ), h • ⟨(↑i + ℓ - 1) % ℓ, ⋯⟩ = ⟨(↑(h • i) + ℓ - 1) % ℓ, ⋯⟩

def BalancedProductTannerCycleCode.cycleChainAction {H : Type} [Group H] (ℓ : ℕ) [MulAction H (Fin ℓ)] : Representation 𝔽₂ H (Fin ℓ → 𝔽₂)

Equations

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

def BalancedProductTannerCycleCode.cycleGraphHEquivariant {H : Type} [Group H] [Fintype H] [DecidableEq H] (ℓ : ℕ) [NeZero ℓ] [MulAction H (Fin ℓ)] (hcompat : CycleCompatibleAction ℓ) : HEquivariantChainComplex H

Equations

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

The Balanced Product Tanner Cycle Code

def BalancedProductTannerCycleCode.balancedProductTannerCycleCode {H : Type} [Group H] [Fintype H] [DecidableEq H] (X : GraphWithGroupAction H) {s : ℕ} (Λ : X.CellLabeling s) (ℓ : ℕ) [NeZero ℓ] [MulAction H (Fin ℓ)] (hℓ_ge : ℓ ≥ 3) (hℓ_odd : ℓ % 2 = 1) (hΛ : GraphWithGroupAction.IsInvariantLabeling Λ) (hcompat : CycleCompatibleAction ℓ) : ChainComplex𝔽₂

The balanced product Tanner cycle code C(X,L) ⊗_{ℤ_ℓ} C(C_ℓ), a quantum CSS code. Requires ℓ ≥ 3 odd, an H-invariant labeling, and a compatible H-action on the cycle graph. The total complex has three terms: C₂ → C₁ → C₀ where physical qubits correspond to C₁, Z-checks are given by ∂₂ : C₂ → C₁, and X-checks are given by ∂₁ : C₁ → C₀.

Equations

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

Abbreviations for the H-equivariant complexes

Tensor product identifications

The balanced product double complex C(X,L) ⊠_{ℤ_ℓ} C(C_ℓ) has entries at (p,q) where p ∈ {0,1} (Tanner complex degrees) and q ∈ {0,1} (cycle complex degrees). The total complex Tot has three non-trivial degrees:

• C₂ = Tot_2 = (C ⊠ D)_{1,1} = C₁(X,L) ⊗_{ℤ_ℓ} C₁(C_ℓ)
• C₁ = Tot_1 = (C ⊠ D)_{1,0} ⊕ (C ⊠ D)_{0,1} = (C₁(X,L) ⊗_{ℤ_ℓ} C₀(C_ℓ)) ⊕ (C₀(X,L) ⊗_{ℤ_ℓ} C₁(C_ℓ))
• C₀ = Tot_0 = (C ⊠ D)_{0,0} = C₀(X,L) ⊗_{ℤ_ℓ} C₀(C_ℓ)

theorem BalancedProductTannerCycleCode.balancedProductTannerCycleCode_C2_eq {H : Type} [Group H] [Fintype H] [DecidableEq H] (X : GraphWithGroupAction H) {s : ℕ} (Λ : X.CellLabeling s) (ℓ : ℕ) [NeZero ℓ] [MulAction H (Fin ℓ)] (hΛ : GraphWithGroupAction.IsInvariantLabeling Λ) (hcompat : CycleCompatibleAction ℓ) : ((BalancedProductTannerCycleCode.tannerHEq✝ X Λ hΛ).balancedProductDoubleComplex (BalancedProductTannerCycleCode.cycleHEq✝ ℓ hcompat)).obj 1 1 = (BalancedProductTannerCycleCode.tannerHEq✝¹ X Λ hΛ).bpObj (BalancedProductTannerCycleCode.cycleHEq✝¹ ℓ hcompat) 1 1

C₂ = C₁(X,L) ⊗_{ℤ_ℓ} C₁(C_ℓ), the balanced product of the degree-1 components.

theorem BalancedProductTannerCycleCode.balancedProductTannerCycleCode_C0_eq {H : Type} [Group H] [Fintype H] [DecidableEq H] (X : GraphWithGroupAction H) {s : ℕ} (Λ : X.CellLabeling s) (ℓ : ℕ) [NeZero ℓ] [MulAction H (Fin ℓ)] (hΛ : GraphWithGroupAction.IsInvariantLabeling Λ) (hcompat : CycleCompatibleAction ℓ) : ((BalancedProductTannerCycleCode.tannerHEq✝ X Λ hΛ).balancedProductDoubleComplex (BalancedProductTannerCycleCode.cycleHEq✝ ℓ hcompat)).obj 0 0 = (BalancedProductTannerCycleCode.tannerHEq✝¹ X Λ hΛ).bpObj (BalancedProductTannerCycleCode.cycleHEq✝¹ ℓ hcompat) 0 0

C₀ = C₀(X,L) ⊗_{ℤ_ℓ} C₀(C_ℓ), the balanced product of the degree-0 components.

def BalancedProductTannerCycleCode.ιC1_tanner_component {H : Type} [Group H] [Fintype H] [DecidableEq H] (X : GraphWithGroupAction H) {s : ℕ} (Λ : X.CellLabeling s) (ℓ : ℕ) [NeZero ℓ] [MulAction H (Fin ℓ)] (hℓ_ge : ℓ ≥ 3) (hℓ_odd : ℓ % 2 = 1) (hΛ : GraphWithGroupAction.IsInvariantLabeling Λ) (hcompat : CycleCompatibleAction ℓ) : (BalancedProductTannerCycleCode.tannerHEq✝ X Λ hΛ).bpObj (BalancedProductTannerCycleCode.cycleHEq✝ ℓ hcompat) 1 0 ⟶ (balancedProductTannerCycleCode X Λ ℓ hℓ_ge hℓ_odd hΛ hcompat).X 1

The inclusion C₁(X,L) ⊗_{ℤ_ℓ} C₀(C_ℓ) ↪ C₁ into the total complex at degree 1.

Equations

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

def BalancedProductTannerCycleCode.ιC1_cycle_component {H : Type} [Group H] [Fintype H] [DecidableEq H] (X : GraphWithGroupAction H) {s : ℕ} (Λ : X.CellLabeling s) (ℓ : ℕ) [NeZero ℓ] [MulAction H (Fin ℓ)] (hℓ_ge : ℓ ≥ 3) (hℓ_odd : ℓ % 2 = 1) (hΛ : GraphWithGroupAction.IsInvariantLabeling Λ) (hcompat : CycleCompatibleAction ℓ) : (BalancedProductTannerCycleCode.tannerHEq✝ X Λ hΛ).bpObj (BalancedProductTannerCycleCode.cycleHEq✝ ℓ hcompat) 0 1 ⟶ (balancedProductTannerCycleCode X Λ ℓ hℓ_ge hℓ_odd hΛ hcompat).X 1

The inclusion C₀(X,L) ⊗_{ℤ_ℓ} C₁(C_ℓ) ↪ C₁ into the total complex at degree 1.

Equations

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

def BalancedProductTannerCycleCode.ιC2_component {H : Type} [Group H] [Fintype H] [DecidableEq H] (X : GraphWithGroupAction H) {s : ℕ} (Λ : X.CellLabeling s) (ℓ : ℕ) [NeZero ℓ] [MulAction H (Fin ℓ)] (hℓ_ge : ℓ ≥ 3) (hℓ_odd : ℓ % 2 = 1) (hΛ : GraphWithGroupAction.IsInvariantLabeling Λ) (hcompat : CycleCompatibleAction ℓ) : (BalancedProductTannerCycleCode.tannerHEq✝ X Λ hΛ).bpObj (BalancedProductTannerCycleCode.cycleHEq✝ ℓ hcompat) 1 1 ⟶ (balancedProductTannerCycleCode X Λ ℓ hℓ_ge hℓ_odd hΛ hcompat).X 2

The inclusion C₁(X,L) ⊗_{ℤ_ℓ} C₁(C_ℓ) ↪ C₂ into the total complex at degree 2.

Equations

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

def BalancedProductTannerCycleCode.ιC0_component {H : Type} [Group H] [Fintype H] [DecidableEq H] (X : GraphWithGroupAction H) {s : ℕ} (Λ : X.CellLabeling s) (ℓ : ℕ) [NeZero ℓ] [MulAction H (Fin ℓ)] (hℓ_ge : ℓ ≥ 3) (hℓ_odd : ℓ % 2 = 1) (hΛ : GraphWithGroupAction.IsInvariantLabeling Λ) (hcompat : CycleCompatibleAction ℓ) : (BalancedProductTannerCycleCode.tannerHEq✝ X Λ hΛ).bpObj (BalancedProductTannerCycleCode.cycleHEq✝ ℓ hcompat) 0 0 ⟶ (balancedProductTannerCycleCode X Λ ℓ hℓ_ge hℓ_odd hΛ hcompat).X 0

The inclusion C₀(X,L) ⊗_{ℤ_ℓ} C₀(C_ℓ) ↪ C₀ into the total complex at degree 0.

Equations

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

CSS code structure

A chain complex C₂ →[∂₂] C₁ →[∂₁] C₀ with ∂₁ ∘ ∂₂ = 0 determines a CSS code:

• Physical qubits correspond to C₁
• Z-checks are given by ∂₂ : C₂ → C₁
• X-checks are given by ∂₁ : C₁ → C₀ The CSS condition ∂₁ ∘ ∂₂ = 0 is automatic from the chain complex .

def BalancedProductTannerCycleCode.zCheckMap {H : Type} [Group H] [Fintype H] [DecidableEq H] (X : GraphWithGroupAction H) {s : ℕ} (Λ : X.CellLabeling s) (ℓ : ℕ) [NeZero ℓ] [MulAction H (Fin ℓ)] (hℓ_ge : ℓ ≥ 3) (hℓ_odd : ℓ % 2 = 1) (hΛ : GraphWithGroupAction.IsInvariantLabeling Λ) (hcompat : CycleCompatibleAction ℓ) : (balancedProductTannerCycleCode X Λ ℓ hℓ_ge hℓ_odd hΛ hcompat).X 2 ⟶ (balancedProductTannerCycleCode X Λ ℓ hℓ_ge hℓ_odd hΛ hcompat).X 1

The Z-check map ∂₂ : C₂ → C₁ of the balanced product Tanner cycle code.

Equations

• BalancedProductTannerCycleCode.zCheckMap X Λ ℓ hℓ_ge hℓ_odd hΛ hcompat = (BalancedProductTannerCycleCode.balancedProductTannerCycleCode X Λ ℓ hℓ_ge hℓ_odd hΛ hcompat).d 2 1

def BalancedProductTannerCycleCode.xCheckMap {H : Type} [Group H] [Fintype H] [DecidableEq H] (X : GraphWithGroupAction H) {s : ℕ} (Λ : X.CellLabeling s) (ℓ : ℕ) [NeZero ℓ] [MulAction H (Fin ℓ)] (hℓ_ge : ℓ ≥ 3) (hℓ_odd : ℓ % 2 = 1) (hΛ : GraphWithGroupAction.IsInvariantLabeling Λ) (hcompat : CycleCompatibleAction ℓ) : (balancedProductTannerCycleCode X Λ ℓ hℓ_ge hℓ_odd hΛ hcompat).X 1 ⟶ (balancedProductTannerCycleCode X Λ ℓ hℓ_ge hℓ_odd hΛ hcompat).X 0

The X-check map ∂₁ : C₁ → C₀ of the balanced product Tanner cycle code.

Equations

• BalancedProductTannerCycleCode.xCheckMap X Λ ℓ hℓ_ge hℓ_odd hΛ hcompat = (BalancedProductTannerCycleCode.balancedProductTannerCycleCode X Λ ℓ hℓ_ge hℓ_odd hΛ hcompat).d 1 0

theorem BalancedProductTannerCycleCode.css_condition {H : Type} [Group H] [Fintype H] [DecidableEq H] (X : GraphWithGroupAction H) {s : ℕ} (Λ : X.CellLabeling s) (ℓ : ℕ) [NeZero ℓ] [MulAction H (Fin ℓ)] (hℓ_ge : ℓ ≥ 3) (hℓ_odd : ℓ % 2 = 1) (hΛ : GraphWithGroupAction.IsInvariantLabeling Λ) (hcompat : CycleCompatibleAction ℓ) : CategoryTheory.CategoryStruct.comp (zCheckMap X Λ ℓ hℓ_ge hℓ_odd hΛ hcompat) (xCheckMap X Λ ℓ hℓ_ge hℓ_odd hΛ hcompat) = 0

The CSS condition: the composition of the X-check map and Z-check map is zero, i.e., ∂₁ ∘ ∂₂ = 0. This is the fundamental property that makes the code a valid quantum CSS code.

theorem BalancedProductTannerCycleCode.balancedProductTannerCycleCode_ℓ_ge (ℓ : ℕ) [NeZero ℓ] (hℓ_ge : ℓ ≥ 3) : ℓ ≥ 3

The balanced product Tanner cycle code has ℓ ≥ 3.

theorem BalancedProductTannerCycleCode.balancedProductTannerCycleCode_ℓ_odd (ℓ : ℕ) [NeZero ℓ] (hℓ_odd : ℓ % 2 = 1) : ℓ % 2 = 1

The balanced product Tanner cycle code has ℓ odd.