Definition 11: Tensor Product Double Complex

Given two chain complexes C = (C_•, ∂^C) and D = (D_•, ∂^D) over 𝔽₂, the tensor product double complex C ⊠ D is the double complex (Def_9) defined by:

• (C ⊠ D)_{p,q} = C_p ⊗ D_q
• vertical differential ∂^v_{p,q} = id_{C_p} ⊗ ∂^D_q : C_p ⊗ D_q → C_p ⊗ D_{q-1}
• horizontal differential ∂^h_{p,q} = ∂^C_p ⊗ id_{D_q} : C_p ⊗ D_q → C_{p-1} ⊗ D_q

The tensor product complex is C ⊗ D = Tot(C ⊠ D) (Def_10), so that (C ⊗ D)_n = ⊕_{p+q=n} C_p ⊗ D_q with differential ∂ = ∂^C ⊗ id + id ⊗ ∂^D.

Over 𝔽₂ the usual sign (-1)^p is trivial.

When C and D are both 1-complexes (concentrated in degrees 0 and 1), the resulting CSS code obtained from the total complex is called a hypergraph product code.

Main Definitions

• tensorDoubleComplex — the tensor product double complex C ⊠ D
• tensorComplex — the tensor product complex C ⊗ D = Tot(C ⊠ D)
• hypergraphProductCode — the CSS code from the tensor product of two 1-complexes

Main Results

• tensorDoubleComplex_obj — (C ⊠ D)_{p,q} = C_p ⊗ D_q
• tensorDoubleComplex_dv — vertical differential is id_C ⊗ ∂^D
• tensorDoubleComplex_dh — horizontal differential is ∂^C ⊗ id_D

The tensor product double complex

noncomputable def ChainComplex𝔽₂.tensorObj' (C D : ChainComplex𝔽₂) (p q : ℤ) : ModuleCat 𝔽₂

The graded object underlying the tensor product double complex: (C ⊠ D)_{p,q} = C_p ⊗ D_q.

Equations

• C.tensorObj' D p q = CategoryTheory.MonoidalCategoryStruct.tensorObj (C.X p) (D.X q)

noncomputable def ChainComplex𝔽₂.tensorDh (C D : ChainComplex𝔽₂) (p p' q : ℤ) : CategoryTheory.MonoidalCategoryStruct.tensorObj (C.X p) (D.X q) ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj (C.X p') (D.X q)

The horizontal differential ∂^C_p ⊗ id_{D_q} : C_p ⊗ D_q → C_{p'} ⊗ D_q. This maps in the p-direction (first index).

Equations

• C.tensorDh D p p' q = CategoryTheory.MonoidalCategoryStruct.whiskerRight (C.d p p') (D.X q)

noncomputable def ChainComplex𝔽₂.tensorDv (C D : ChainComplex𝔽₂) (p q q' : ℤ) : CategoryTheory.MonoidalCategoryStruct.tensorObj (C.X p) (D.X q) ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj (C.X p) (D.X q')

The vertical differential id_{C_p} ⊗ ∂^D_q : C_p ⊗ D_q → C_p ⊗ D_{q'}. This maps in the q-direction (second index).

Equations

• C.tensorDv D p q q' = CategoryTheory.MonoidalCategoryStruct.whiskerLeft (C.X p) (D.d q q')

Shape conditions

d² = 0 conditions

Commutativity: ∂^h ∘ ∂^v = ∂^v ∘ ∂^h

The tensor product double complex

noncomputable def ChainComplex𝔽₂.tensorDoubleComplex (C D : ChainComplex𝔽₂) : DoubleComplex𝔽₂

The tensor product double complex C ⊠ D as a DoubleComplex𝔽₂. Objects are (C ⊠ D)_{p,q} = C_p ⊗ D_q with:

• horizontal differential ∂^h_{p,q} = ∂^C_p ⊗ id_{D_q} (the paper's ∂^C ⊗ id_D)
• vertical differential ∂^v_{p,q} = id_{C_p} ⊗ ∂^D_q (the paper's id_C ⊗ ∂^D)

Equations

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

Accessor lemmas for the tensor double complex

theorem ChainComplex𝔽₂.tensorDoubleComplex_obj (C D : ChainComplex𝔽₂) (p q : ℤ) : (C.tensorDoubleComplex D).obj p q = CategoryTheory.MonoidalCategoryStruct.tensorObj (C.X p) (D.X q)

The object (C ⊠ D)_{p,q} = C_p ⊗ D_q.

theorem ChainComplex𝔽₂.tensorDoubleComplex_dv_eq (C D : ChainComplex𝔽₂) (p q : ℤ) : ((C.tensorDoubleComplex D).X p).d q (q - 1) = C.tensorDv D p q (q - 1)

The vertical differential of the tensor double complex is id_{C_p} ⊗ ∂^D_q.

theorem ChainComplex𝔽₂.tensorDoubleComplex_dh_eq (C D : ChainComplex𝔽₂) (p q : ℤ) : ((C.tensorDoubleComplex D).d p (p - 1)).f q = C.tensorDh D p (p - 1) q

The horizontal differential of the tensor double complex is ∂^C_p ⊗ id_{D_q}.

HasTotal instance for the tensor double complex

instance ChainComplex𝔽₂.tensorDoubleComplex_hasTotal (C D : ChainComplex𝔽₂) : HomologicalComplex₂.HasTotal (C.tensorDoubleComplex D) (ComplexShape.down ℤ)

The tensor product double complex has a total complex.

The tensor product complex

noncomputable def ChainComplex𝔽₂.tensorComplex (C D : ChainComplex𝔽₂) : ChainComplex𝔽₂

The tensor product complex C ⊗ D = Tot(C ⊠ D) (Def_10). This is a chain complex over 𝔽₂ with (C ⊗ D)_n = ⊕_{p+q=n} C_p ⊗ D_q and differential ∂ = ∂^C ⊗ id + id ⊗ ∂^D. Over 𝔽₂ the sign (-1)^p is trivial.

Equations

• C.tensorComplex D = (C.tensorDoubleComplex D).totalComplex

noncomputable def ChainComplex𝔽₂.ιTensorComplex (C D : ChainComplex𝔽₂) (p q n : ℤ) (h : p + q = n) : CategoryTheory.MonoidalCategoryStruct.tensorObj (C.X p) (D.X q) ⟶ (C.tensorComplex D).X n

The inclusion of the summand C_p ⊗ D_q into (C ⊗ D)_n when p + q = n.

Equations

• C.ιTensorComplex D p q n h = (C.tensorDoubleComplex D).ιTotalComplex p q n h

Hypergraph product code

noncomputable def ChainComplex𝔽₂.hypergraphProductCode {n₁ m₁ n₂ m₂ : ℕ} (dC : (Fin n₁ → 𝔽₂) →ₗ[𝔽₂] Fin m₁ → 𝔽₂) (dD : (Fin n₂ → 𝔽₂) →ₗ[𝔽₂] Fin m₂ → 𝔽₂) : ChainComplex𝔽₂

A hypergraph product code is the CSS code obtained from the tensor product complex of two 1-complexes C₁ →[∂^C] C₀ and D₁ →[∂^D] D₀. The total complex of C ⊠ D has three nontrivial degrees:

• degree 2: C₁ ⊗ D₁
• degree 1: (C₁ ⊗ D₀) ⊕ (C₀ ⊗ D₁)
• degree 0: C₀ ⊗ D₀

The resulting CSS code has H_Z^T as the differential from degree 2 to degree 1 and H_X as the differential from degree 1 to degree 0 in the total complex, shifted by 1 to match the CSS code convention C₁ →[H_Z^T] C₀ →[H_X] C_{-1}.

Equations

• ChainComplex𝔽₂.hypergraphProductCode dC dD = (ClassicalCode.parityCheckComplex dC).tensorComplex (ClassicalCode.parityCheckComplex dD)