6 Def 3: Classical Code
A classical linear binary code of block length \(n\) is a subspace \(\mathcal{C} \subseteq \mathbb {F}_2^n\). Formally, it is a structure wrapping a submodule
where \(\mathbb {F}_2^n\) is viewed as the \(\mathbb {F}_2\)-module of functions \(\operatorname {Fin}(n) \to \mathbb {F}_2\).
Let \(\mathcal{C}\) be a classical code of block length \(n\). The dimension of \(\mathcal{C}\) is
the finite rank of \(\mathcal{C}\) as an \(\mathbb {F}_2\)-module. This equals the number of encodable bits.
Let \(\mathcal{C}\) be a classical code of block length \(n\). The distance of \(\mathcal{C}\) is
where \(\operatorname {wt}(x)\) denotes the Hamming weight of \(x\). Here \(\inf \) is taken over \(\mathbb {N}\), and by convention \(\inf \emptyset = 0\), which gives \(d = 0\) for the trivial code \(\mathcal{C} = \{ 0\} \).
A classical code \(\mathcal{C}\) of block length \(n\) is called an \([n, k, d]\)-code if its dimension equals \(k\) and its distance equals \(d\):
Given an \(\mathbb {F}_2\)-linear map \(\partial ^C : \mathbb {F}_2^n \to \mathbb {F}_2^m\) (the parity check map), we construct a classical code of block length \(n\) by taking the kernel:
Given an \(\mathbb {F}_2\)-linear parity check map \(\partial ^C : \mathbb {F}_2^n \to \mathbb {F}_2^m\), the associated two-term chain complex is
where \(C_1 = \mathbb {F}_2^n\) sits in degree \(1\) and \(C_0 = \mathbb {F}_2^m\) sits in degree \(0\). This is constructed via \(\operatorname {HomologicalComplex.double}\) applied to the morphism \(\partial ^C\) in the category of \(\mathbb {F}_2\)-modules, using the complex shape relation \(1 \to 0\).
For a parity check map \(\partial ^C : \mathbb {F}_2^n \to \mathbb {F}_2^m\), there is a canonical isomorphism
between the degree-\(1\) object of the parity check complex \(C\) and \(\mathbb {F}_2^n\), given by \(\operatorname {HomologicalComplex.doubleXIso_0}\).
For any \(\mathbb {F}_2\)-linear parity check map \(\partial ^C : \mathbb {F}_2^n \to \mathbb {F}_2^m\), the underlying submodule of the code constructed from \(\partial ^C\) equals the kernel of \(\partial ^C\):
This holds by reflexivity: \(\operatorname {ofParityCheck}(\partial ^C).\operatorname {code}\) is defined to be \(\ker (\partial ^C)\), so the equality is definitional.
For any \(\mathbb {F}_2\)-linear parity check map \(\partial ^C : \mathbb {F}_2^n \to \mathbb {F}_2^m\), the code \(\mathcal{C} = \ker (\partial ^C)\) equals the image of the degree-\(1\) cycles of the parity check complex \(C\) under the canonical isomorphism \(\varphi : C(1) \xrightarrow {\sim } \mathbb {F}_2^n\):
where \(Z_1(C) = \ker (\partial ^C : C(1) \to C(0))\) is the submodule of \(1\)-cycles.
Let \(C = \operatorname {parityCheckComplex}(\partial ^C)\), let \(\varphi = \operatorname {parityCheckComplexXIso_1}(\partial ^C) : C(1) \xrightarrow {\sim } \mathbb {F}_2^n\), and let \(\psi = \operatorname {HomologicalComplex.doubleXIso_1}(\partial ^C) : C(0) \xrightarrow {\sim } \mathbb {F}_2^m\). We note the factorization
established by \(\operatorname {HomologicalComplex.double_d}\).
By extensionality, it suffices to show that for each \(x \in \mathbb {F}_2^n\):
\((\Rightarrow )\): Assume \(\partial ^C(x) = 0\). We produce the preimage \(y = \varphi ^{-1}(x) \in C(1)\). Using the factorization of the differential, we compute:
where we used \(\varphi \circ \varphi ^{-1} = \operatorname {id}\) (i.e., \((\varphi ^{-1} \circ \varphi )(x) = x\) by the isomorphism identity \(\varphi ^{-1} \circ \varphi = \operatorname {id}\), and \(\psi ^{-1}(0) = 0\) since \(\psi ^{-1}\) is linear). Thus \(y \in Z_1(C)\), and \(\varphi (y) = \varphi (\varphi ^{-1}(x)) = x\) by the isomorphism identity.
\((\Leftarrow )\): Assume \(y \in Z_1(C)\) with \(x = \varphi (y)\). By simplification using the definition of cycles and the differential, \(y \in \ker (d_{1,0})\), meaning \(d_{1,0}(y) = 0\). Using the factorization \(d_{1,0} = \varphi ^{-1} \circ \partial ^C \circ \psi ^{-1}\) and substituting, we obtain
We show \(\psi ^{-1}\) is injective: given \(a, b\) with \(\psi ^{-1}(a) = \psi ^{-1}(b)\), applying \(\psi \) to both sides and using \(\psi \circ \psi ^{-1} = \operatorname {id}\) yields \(a = b\). By injectivity of \(\psi ^{-1}\), from \(\psi ^{-1}(\partial ^C(\varphi (y))) = \psi ^{-1}(0)\) we conclude \(\partial ^C(\varphi (y)) = 0\), i.e., \(\partial ^C(x) = 0\). Thus \(x \in \ker (\partial ^C) = \mathcal{C}\).