22 Def 16: Dual Code
Let \(\mathcal{C}\) be a classical code, i.e. a subspace \(L \subseteq \mathbb {F}_2^n\). The dual code is
where \(\langle w, c \rangle = \sum _i w_i c_i\) is the standard \(\mathbb {F}_2\)-dot product. Concretely, \(L^\perp \) is defined as the pullback of the dual annihilator \(L^{\circ } \subseteq \operatorname {Dual}(\mathbb {F}_2^n)\) through the canonical linear isomorphism
Let \(\mathcal{C}\) be a classical code of block length \(n\) and let \(w \in \mathbb {F}_2^n\). Then
We unfold the definition of the dual code: \(L^\perp = (L^{\circ }).\operatorname {comap}(\operatorname {dotProductEquiv})\). By simplification using the definitions of Submodule.mem_comap and Submodule.mem_dualAnnihilator, membership \(w \in L^\perp \) is equivalent to \((\operatorname {dotProductEquiv}\, w)(c) = 0\) for all \(c \in L\). We prove both directions separately. In each direction, let the respective hypothesis hold and let \(c \in L\) be arbitrary; simplifying the definition of \(\operatorname {dotProductEquiv}\), the condition \((\operatorname {dotProductEquiv}\, w)(c) = 0\) is exactly \(w \cdot c = 0\), which gives the result.
Let \(w \in \mathbb {F}_2^n\). Then
Over \(\mathbb {F}_2\), the dot product is commutative: \(w \cdot c = c \cdot w\).
We rewrite using mem_dualCode_iff. It then suffices to show that \((\forall \, c \in L,\, w \cdot c = 0) \Leftrightarrow (\forall \, c \in L,\, c \cdot w = 0)\). We prove both implications simultaneously: given each direction, let \(c \in L\) be arbitrary and rewrite using commutativity of the dot product (\(w \cdot c = c \cdot w\)) to obtain the claim from the hypothesis.
There is a \(\mathbb {F}_2\)-linear equivalence
between the dual code \(L^\perp \) and the dual annihilator \(L^{\circ } \subseteq \operatorname {Dual}(\mathbb {F}_2^n)\), induced by the canonical isomorphism \(\operatorname {dotProductEquiv}\). Since \((L^\perp ).\mathtt{code} = L^{\circ }.\operatorname {comap}(\operatorname {dotProductEquiv})\), the restriction of \(\operatorname {dotProductEquiv}^{-1}\) to \(L^{\circ }\) gives the desired equivalence.
Let \(\mathcal{C}\) be a classical \([n,k,d]\)-code. Then
We unfold the definition of dimension. First, we transfer the rank of \(L^\perp \) to that of the dual annihilator: by the linear equivalence \(\operatorname {dualCodeEquivDualAnnihilator}\), we have
We rewrite using this equality. Next, we apply the dual annihilator dimension formula
and use the fact that \(\operatorname {finrank}_{\mathbb {F}_2}(\mathbb {F}_2^n) = n\) (by Module.finrank_fin_fun). The result \(\operatorname {finrank}_{\mathbb {F}_2}(L^{\circ }) = n - \operatorname {finrank}_{\mathbb {F}_2}(L)\) then follows by integer arithmetic.
Let \(\mathcal{C}\) be a classical \([n,k,d]\)-code. Then the dual code \(L^\perp \) is an \([n,\, n-k,\, d_{L^\perp }]\)-code, where \(k = \dim L\) and \(d_{L^\perp }\) is the minimum distance of \(L^\perp \).
We verify both components of the IsNKDCode predicate. The first component, namely \(\dim (L^\perp ) = n - k\), is exactly dimension_dualCode. The second component, that the distance of \(L^\perp \) equals itself, holds by reflexivity.