11 Def 8: Cycle Graph
Let \(\ell \geq 1\) be a natural number. The differential \(\partial _1 : \mathbb {F}_2^\ell \to \mathbb {F}_2^\ell \) of the cycle graph is the linear map defined by
for \(f : \operatorname {Fin}(\ell ) \to \mathbb {F}_2\) and \(i \in \operatorname {Fin}(\ell )\). On basis vectors \(e_j\), one has \(\partial _1(e_j) = e_j + e_{(j+1) \bmod \ell }\), so column \(j\) of the corresponding matrix has \(1\)-entries in rows \(j\) and \((j+1) \bmod \ell \), encoding the boundary relation \(\partial \sigma _j = \{ \tau _j, \tau _{(j+1) \bmod \ell }\} \).
The all-ones vector \(\mathbf{1} \in \mathbb {F}_2^\ell \) is defined by \(\mathbf{1}(i) = 1\) for all \(i \in \operatorname {Fin}(\ell )\).
\(\partial _1(\mathbf{1}) = 0\) in \(\mathbb {F}_2^\ell \).
By extensionality, it suffices to show that \((\partial _1 \mathbf{1})(i) = 0\) for each \(i \in \operatorname {Fin}(\ell )\). Unfolding the definitions, \((\partial _1 \mathbf{1})(i) = \mathbf{1}(i) + \mathbf{1}((i+\ell -1)\bmod \ell ) = 1 + 1 = 0\) in \(\mathbb {F}_2\), where the last equality holds by \(x + x = 0\) in \(\mathbb {F}_2\).
Let \(f : \operatorname {Fin}(\ell ) \to \mathbb {F}_2\) satisfy \(\partial _1 f = 0\). For any \(i \in \mathbb {N}\) with \(i + 1 {\lt} \ell \), we have \(f(i+1) = f(i)\).
Let \(h\) denote the hypothesis \(\partial _1 f = 0\). Evaluating at position \(i+1\), we obtain \(h_{i+1} : (\partial _1 f)(i+1) = 0\), which by the definition of the differential gives \(f(i+1) + f\! \left((i+1+\ell -1)\bmod \ell \right) = 0\). We compute \((i+1+\ell -1)\bmod \ell = (i+\ell )\bmod \ell = i\bmod \ell = i\) (since \(i {\lt} \ell \)), so after rewriting we get \(f(i+1) + f(i) = 0\). It follows that \(f(i+1) - f(i) = 0\), and since subtraction equals addition in \(\mathbb {F}_2\) (using \(\mathbb {F}_2.\mathtt{sub\_ eq\_ add}\)), this gives \(f(i+1) = f(i)\).
If \(\partial _1 f = 0\), then \(f(i) = f(0)\) for all \(i \in \operatorname {Fin}(\ell )\).
Write \(i = \langle n, h_n \rangle \). We proceed by induction on \(n\). In the base case \(n = 0\), the equality \(f(0) = f(0)\) holds by reflexivity. In the inductive step, assuming \(f(k) = f(0)\) for \(k\) with \(k {\lt} \ell \), we apply the lemma \(\mathtt{ker\_ differential\_ succ}\) to obtain \(f(k+1) = f(k)\), and the result follows by the inductive hypothesis.
\(\ker (\partial _1) = \operatorname {span}_{\mathbb {F}_2}\{ \mathbf{1}\} \) as submodules of \(\mathbb {F}_2^\ell \).
By extensionality, it suffices to show for all \(f\) that \(f \in \ker (\partial _1)\) if and only if \(f \in \operatorname {span}\{ \mathbf{1}\} \), i.e., \(\partial _1 f = 0 \Leftrightarrow \exists \, c \in \mathbb {F}_2,\ f = c \cdot \mathbf{1}\).
\((\Rightarrow )\): Suppose \(\partial _1 f = 0\). We claim \(f = f(0) \cdot \mathbf{1}\). By extensionality at \(i\), we need \(f(i) = f(0) \cdot \mathbf{1}(i) = f(0) \cdot 1 = f(0)\). This follows from \(\mathtt{ker\_ differential\_ const}\), applying the symmetry of the equality.
\((\Leftarrow )\): Suppose \(f = c \cdot \mathbf{1}\) for some \(c \in \mathbb {F}_2\). Then for each \(i\), \((\partial _1 f)(i) = (\partial _1(c \cdot \mathbf{1}))(i) = c \cdot (\partial _1 \mathbf{1})(i) = c \cdot (c + c) = c \cdot 0\). More precisely, unfolding the differential, \((\partial _1(c\cdot \mathbf{1}))(i) = c\cdot \mathbf{1}(i) + c\cdot \mathbf{1}((i+\ell -1)\bmod \ell ) = c + c = 0\) by \(x + x = 0\) in \(\mathbb {F}_2\).
If \(\ell \geq 1\), then \(\mathbf{1} \neq 0\) in \(\mathbb {F}_2^\ell \).
Suppose for contradiction that \(\mathbf{1} = 0\). Evaluating both sides at \(\langle 0, h_\ell \rangle \in \operatorname {Fin}(\ell )\) (which exists since \(\ell \geq 1\)), we obtain \(\mathbf{1}(0) = 1 = 0\), which is a contradiction since \(1 \neq 0\) in \(\mathbb {F}_2\).
If \(\ell \geq 1\), then \(\dim _{\mathbb {F}_2} \ker (\partial _1) = 1\).
We rewrite using \(\mathtt{ker\_ differential\_ eq\_ span}\), which gives \(\ker (\partial _1) = \operatorname {span}\{ \mathbf{1}\} \). Since \(\mathbf{1} \neq 0\) by \(\mathtt{onesVec\_ ne\_ zero}\) (using \(\ell \geq 1\)), the span of a single nonzero vector in a vector space over a field has dimension \(1\) (by \(\mathtt{finrank\_ span\_ singleton}\)).
The cell type function for the cycle graph assigns to each integer dimension \(n\) the type of \(n\)-cells:
Thus the cycle graph has \(\ell \) vertices (0-cells) and \(\ell \) edges (1-cells), and no cells in any other dimension.
The boundary map for the cycle graph \(C_\ell \) assigns to each cell its boundary:
For a 1-cell \(\sigma _i\) (with \(i \in \operatorname {Fin}(\ell )\)): \(\partial \sigma _i = \{ \tau _i,\, \tau _{(i+1)\bmod \ell }\} \subseteq \operatorname {Fin}(\ell )\), encoding the incidence relation of each edge with its two endpoint vertices.
For a 0-cell: \(\partial \tau _i = \varnothing \) (the boundary of a vertex is empty, valued in \(\operatorname {cellType}(\ell ,-1) = \varnothing \)).
For cells in all other dimensions: the boundary is vacuously empty (the cell type is \(\varnothing \)).
For all \(n \in \mathbb {Z}\), all \(n\)-cells \(\sigma \), and all \((n-2)\)-cells \(\rho \), the number of \((n-1)\)-cells in \(\partial \sigma \) whose boundary contains \(\rho \) is even.
We verify by cases on \(n\). For \(n = 1\): the target type \(\operatorname {cellType}(\ell , -1) = \varnothing \), so \(\rho : \varnothing \) is absurd; the statement holds vacuously. For \(n = 0\): similarly, \(\operatorname {cellType}(\ell , -2) = \varnothing \) gives an absurd \(\rho \). For \(n = k+2\) with \(k \geq 0\): \(\operatorname {cellType}(\ell , k+2) = \varnothing \), so \(\sigma : \varnothing \) is absurd. For \(n {\lt} 0\): similarly \(\operatorname {cellType}(\ell , n) = \varnothing \) gives an absurd \(\sigma \). In all cases the condition is vacuously satisfied.
The cycle graph \(C_\ell \) is the cell complex (Definition 81) with:
cells given by \(\operatorname {cellType}(\ell )\): \(\ell \) vertices (0-cells) and \(\ell \) edges (1-cells), all indexed by \(\operatorname {Fin}(\ell )\);
boundary map given by \(\operatorname {cellBdry}(\ell )\): \(\partial \sigma _i = \{ \tau _i, \tau _{(i+1)\bmod \ell }\} \);
the chain complex condition \(\partial \circ \partial = 0\) verified by \(\mathtt{cellBdry\_ bdry}\).
The type of 1-cells of \(C_\ell \) equals \(\operatorname {Fin}(\ell )\), i.e., \((C_\ell ).\mathtt{cells}(1) = \operatorname {Fin}(\ell )\).
This holds by reflexivity, since \(\operatorname {cellType}(\ell , 1) = \operatorname {Fin}(\ell )\) by definition.
The type of 0-cells of \(C_\ell \) equals \(\operatorname {Fin}(\ell )\), i.e., \((C_\ell ).\mathtt{cells}(0) = \operatorname {Fin}(\ell )\).
This holds by reflexivity, since \(\operatorname {cellType}(\ell , 0) = \operatorname {Fin}(\ell )\) by definition.
For \(\ell \geq 1\) and \(i \in \operatorname {Fin}(\ell )\), we have \(\left((i + \ell - 1)\bmod \ell + 1\right)\bmod \ell = i\).
We rewrite using \(\mathtt{Nat.add\_ mod}\) and \(\mathtt{Nat.mod\_ mod}\). Observe that \((i + \ell - 1) + 1 = i + 1 \cdot \ell \), so \((i + \ell - 1 + 1) \bmod \ell = (i + \ell )\bmod \ell = i\bmod \ell = i\) (since \(i {\lt} \ell \)). By \(\mathtt{Nat.add\_ mul\_ mod\_ self\_ right}\) and \(\mathtt{Nat.mod\_ eq\_ of\_ lt}\), the claim follows.
For \(\ell \geq 2\) and \(x \in \operatorname {Fin}(\ell )\), we have \(x \neq \langle (x + 1)\bmod \ell ,\, \cdot \rangle \) as elements of \(\operatorname {Fin}(\ell )\).
Suppose for contradiction that \(x = \langle (x+1)\bmod \ell , \cdot \rangle \), i.e., \(x = (x+1)\bmod \ell \). We split on whether \(x + 1 {\lt} \ell \) or \(x + 1 \geq \ell \). If \(x + 1 {\lt} \ell \), then \((x+1)\bmod \ell = x+1\), giving \(x = x+1\), a contradiction by integer arithmetic. If \(x + 1 \geq \ell \), then since \(x {\lt} \ell \) we have \(x + 1 = \ell \), so \((x+1)\bmod \ell = 0\), giving \(x = 0\) and thus \(\ell = 1\), contradicting \(\ell \geq 2\).
For \(\ell \geq 2\) and \(i \in \operatorname {Fin}(\ell )\), we have \(i \neq \langle (i + \ell - 1)\bmod \ell ,\, \cdot \rangle \) as elements of \(\operatorname {Fin}(\ell )\).
Suppose for contradiction that \(i = (i + \ell - 1)\bmod \ell \). We split on \(i = 0\) and \(i \geq 1\). If \(i = 0\): \((0 + \ell - 1)\bmod \ell = (\ell - 1)\bmod \ell = \ell - 1\) (since \(\ell - 1 {\lt} \ell \)), giving \(0 = \ell - 1\), i.e., \(\ell = 1\), contradicting \(\ell \geq 2\). If \(i \geq 1\): \(i + \ell - 1 = (i-1) + 1\cdot \ell \), so by \(\mathtt{Nat.add\_ mul\_ mod\_ self\_ right}\) we get \((i+\ell -1)\bmod \ell = (i-1)\bmod \ell = i-1\) (since \(i-1 {\lt} \ell \)), giving \(i = i-1\), a contradiction.
For \(\ell \geq 2\) and \(i \in \operatorname {Fin}(\ell )\), letting \(j = \langle (i + \ell - 1)\bmod \ell ,\, \cdot \rangle \), the set of 1-cells \(\sigma \) of \(C_\ell \) whose boundary contains \(i\) equals \(\{ i, j\} \):
By extensionality, for any \(\sigma \in \operatorname {Fin}(\ell )\) we show \(i \in \partial \sigma \Leftrightarrow \sigma \in \{ i, j\} \).
Recall \(\partial \sigma = \{ \sigma , \langle (\sigma +1)\bmod \ell ,\cdot \rangle \} \), so \(i \in \partial \sigma \) iff \(i = \sigma \) or \(i = \langle (\sigma +1)\bmod \ell ,\cdot \rangle \).
\((\Rightarrow )\): If \(i = \sigma \), then \(\sigma \in \{ i,j\} \) directly (as the left member). If \(i = \langle (\sigma +1)\bmod \ell , \cdot \rangle \), then \(i = (\sigma +1)\bmod \ell \), i.e., \(\sigma = (i+\ell -1)\bmod \ell = j\) by the modular identity \(\mathtt{pred\_ mod\_ succ}\), so \(\sigma \in \{ i,j\} \) as the right member.
\((\Leftarrow )\): If \(\sigma = i\), then \(i = \sigma \in \partial \sigma \) directly. If \(\sigma = j = \langle (i+\ell -1)\bmod \ell ,\cdot \rangle \), then \(\langle (\sigma +1)\bmod \ell ,\cdot \rangle = \langle (j+1)\bmod \ell ,\cdot \rangle = i\) by \(\mathtt{pred\_ mod\_ succ}\), so \(i \in \partial j\).
By extensionality of linear maps and of functions, it suffices to show that for every \(f \in \mathbb {F}_2^\ell \) and every \(i \in \operatorname {Fin}(\ell )\), the two maps agree at \((f, i)\). We apply \(\mathtt{CellComplex.differentialMap\_ apply}\) to rewrite the left side as a sum:
Setting \(j = \langle (i+\ell -1)\bmod \ell ,\cdot \rangle \) and applying \(\mathtt{differentialMap\_ filter\_ eq}\), the filter set equals \(\{ i, j\} \). Since \(i \neq j\) by \(\mathtt{fin\_ ne\_ pred\_ mod}\) (using \(\ell \geq 2\)), the sum over the pair \(\{ i, j\} \) equals \(f(i) + f(j)\) by \(\mathtt{Finset.sum\_ pair}\). This is precisely \((\partial _1 f)(i) = f(i) + f\! \left((i+\ell -1)\bmod \ell \right)\), completing the proof.
\(\dim _{\mathbb {F}_2}(\operatorname {Fin}(\ell ) \to \mathbb {F}_2) = \ell \).
This follows directly from \(\mathtt{Module.finrank\_ fin\_ fun}\), which gives \(\dim _F(F^n) = n\) for any field \(F\).
If \(\ell \geq 1\), then \(\dim _{\mathbb {F}_2}\operatorname {im}(\partial _1) = \ell - 1\).
By the rank–nullity theorem (\(\mathtt{LinearMap.finrank\_ range\_ add\_ finrank\_ ker}\)):
Substituting \(\dim \mathbb {F}_2^\ell = \ell \) (by \(\mathtt{finrank\_ F2\_ fin}\)) and \(\dim \ker (\partial _1) = 1\) (by \(\mathtt{finrank\_ ker\_ differential}\), using \(\ell \geq 1\)), we obtain \(\dim \operatorname {im}(\partial _1) + 1 = \ell \), hence \(\dim \operatorname {im}(\partial _1) = \ell - 1\) by integer arithmetic.
If \(\ell \geq 1\), then \(\dim _{\mathbb {F}_2} H_1(C_\ell ) = 1\).
Since \(C_\ell \) has no 2-cells, the image of \(\partial _2\) is zero, so \(H_1(C_\ell ) = \ker (\partial _1) / \operatorname {im}(\partial _2) \cong \ker (\partial _1)\). Thus \(\dim H_1(C_\ell ) = \dim \ker (\partial _1) = 1\) by \(\mathtt{finrank\_ ker\_ differential}\) (using \(\ell \geq 1\)).
If \(\ell \geq 1\), then \(\dim _{\mathbb {F}_2}\left(\mathbb {F}_2^\ell \big/ \operatorname {im}(\partial _1)\right) = 1\).
By \(\mathtt{Submodule.finrank\_ quotient\_ add\_ finrank}\):
Substituting \(\dim \mathbb {F}_2^\ell = \ell \) (by \(\mathtt{finrank\_ F2\_ fin}\)) and \(\dim \operatorname {im}(\partial _1) = \ell - 1\) (by \(\mathtt{finrank\_ range\_ differential}\), using \(\ell \geq 1\)), we get \(\dim H_0 + (\ell - 1) = \ell \), so \(\dim H_0 = 1\) by integer arithmetic.
The repetition code of length \(\ell \) is the classical code (Definition 41) defined by
i.e., it is the classical code whose codeword space is \(\ker (\partial _1) = \operatorname {span}\{ \mathbf{1}\} \subseteq \mathbb {F}_2^\ell \).
The codeword space of the repetition code equals the kernel of \(\partial _1\):
This holds by reflexivity, as \(\mathtt{ClassicalCode.ofParityCheck}(\partial _1).\mathtt{code}\) is defined to be \(\ker (\partial _1)\).
If \(\ell \geq 1\), then \(\operatorname {repetitionCode}(\ell ).\mathtt{dimension} = 1\).
Unfolding \(\mathtt{ClassicalCode.dimension}\), the dimension is defined as \(\dim _{\mathbb {F}_2}(\mathtt{code})\). Rewriting by \(\mathtt{repetitionCode\_ eq\_ ker}\), this becomes \(\dim _{\mathbb {F}_2}\ker (\partial _1)\), which equals \(1\) by \(\mathtt{finrank\_ ker\_ differential}\) using \(\ell \geq 1\).