21 Def 15: Tanner Code Local System
Let \(G\) be a simple graph on a finite vertex type \(V\), and let \(s \in \mathbb {N}\). A labeling for the Tanner code on \(G\) is a collection
where \(N(v) = G.\operatorname {neighborSet}(v)\) is the set of neighbors of \(v\) and \(\Lambda _v\) is a bijection. The neighbor \((\Lambda _v)^{-1}(i)\) corresponds to the \(i\)-th position in the local code. The existence of such a labeling requires \(|N(v)| = s\) for all \(v\), which holds when \(G\) is \(s\)-regular.
Let \(\Lambda \) be a labeling, \(v \in V\) a vertex, and \(c \in C_1(X) = (G.\operatorname {edgeSet} \to \mathbb {F}_2)\) a 1-chain. The local view at \(v\) is the \(\mathbb {F}_2\)-linear map
defined by
where \((\Lambda _v)^{-1}(i) \in N(v)\) is the neighbor of \(v\) labeled \(i\). This gives the restriction of \(c\) to the star of \(v\), viewed as an element of \(\mathbb {F}_2^s\) via the labeling.
For any vertex \(v \in V\), 1-chain \(c : G.\operatorname {edgeSet} \to \mathbb {F}_2\), and index \(i \in \operatorname {Fin}(s)\),
This holds by reflexivity, as it is the definitional unfolding of \(\operatorname {localView}\).
Let \(m \in \mathbb {N}\) and let \(H : (\operatorname {Fin}(s) \to \mathbb {F}_2) \to _{\mathbb {F}_2} (\operatorname {Fin}(m) \to \mathbb {F}_2)\) be a parity-check map. The differential
is defined by
This is the component form of the differential \(\partial : C_1(X) \to C_0(X) \otimes L_0\) from the paper, using the canonical isomorphism \((V \to \mathbb {F}_2) \otimes (\operatorname {Fin}(m) \to \mathbb {F}_2) \cong V \to \operatorname {Fin}(m) \to \mathbb {F}_2\). For an edge \(e = \{ v,w\} \), the formula \(\partial (e) = e_v \otimes \partial ^L(e_{\Lambda _v(w)}) + e_w \otimes \partial ^L(e_{\Lambda _w(v)})\) becomes \(\partial (e)(v) = \partial ^L(e_{\Lambda _v(w)})\) and \(\partial (e)(w) = \partial ^L(e_{\Lambda _w(v)})\).
For any parity-check map \(H\), 1-chain \(c\), and vertex \(v \in V\),
This holds by reflexivity, as it is the definitional unfolding of \(\partial _\Lambda ^H\).
Let \(m \in \mathbb {N}\) and \(H : (\operatorname {Fin}(s) \to \mathbb {F}_2) \to _{\mathbb {F}_2} (\operatorname {Fin}(m) \to \mathbb {F}_2)\) be a parity-check map. The Tanner code is the submodule
where \(C_1(X) = G.\operatorname {edgeSet} \to \mathbb {F}_2\) is the space of 1-chains. A 1-chain \(c = \sum _e a_e \cdot e\) is a codeword if and only if for every vertex \(v\), the restriction of the \(a_e\) to edges incident to \(v\), read via \(\Lambda _v\), is a codeword of the local code \(L = \ker (H)\).
Let \(H : (\operatorname {Fin}(s) \to \mathbb {F}_2) \to _{\mathbb {F}_2} (\operatorname {Fin}(m) \to \mathbb {F}_2)\) be a parity-check map. A 1-chain \(c \in C_1(X)\) belongs to the Tanner code if and only if for every vertex \(v \in V\),
We unfold the definitions: \(c \in C(X, L, \Lambda )\) means \(\partial _\Lambda ^H(c) = 0\), i.e., the function \(v \mapsto H(\operatorname {localView}_\Lambda (v)\, c)\) is the zero function.
\((\Rightarrow )\): Assume \(\partial _\Lambda ^H(c) = 0\). For an arbitrary vertex \(v\), applying \(\operatorname {congr_fun}\) to the equality yields \(H(\operatorname {localView}_\Lambda (v)\, c) = 0\), so \(\operatorname {localView}_\Lambda (v)\, c \in \ker (H)\).
\((\Leftarrow )\): Assume that for every \(v\), \(\operatorname {localView}_\Lambda (v)\, c \in \ker (H)\). By function extensionality, for each \(v\) the hypothesis gives \(H(\operatorname {localView}_\Lambda (v)\, c) = 0\). Therefore \(\partial _\Lambda ^H(c) = 0\), i.e., \(c \in C(X, L, \Lambda )\).
By simplification using the definitions of \(\operatorname {tannerCode}\), \(\operatorname {LinearMap.mem_ker}\), and \(\operatorname {differential}\), both directions are established.
Let \(H : (\operatorname {Fin}(s) \to \mathbb {F}_2) \to _{\mathbb {F}_2} (\operatorname {Fin}(m) \to \mathbb {F}_2)\) be a parity-check map. A 1-chain \(c \in C_1(X)\) belongs to the Tanner code if and only if for every vertex \(v \in V\),
where \(\operatorname {ofParityCheck}(H)\) is the classical code (Definition 41) associated to the parity-check matrix \(H\).
We rewrite using \(\operatorname {mem_tannerCode_iff}\) (Theorem 252). It then suffices to show that \(\operatorname {localView}_\Lambda (v)\, c \in \ker (H)\) if and only if \(\operatorname {localView}_\Lambda (v)\, c \in \operatorname {ofParityCheck}(H).\operatorname {code}\). By simplification using the definitions of \(\operatorname {ClassicalCode.ofParityCheck}\) and \(\operatorname {ClassicalCode.code_eq_ker}\) (Theorem 48), these two conditions are definitionally equal.
Let \(H : (\operatorname {Fin}(s) \to \mathbb {F}_2) \to _{\mathbb {F}_2} (\operatorname {Fin}(m) \to \mathbb {F}_2)\) be a parity-check map. The Tanner code equals the intersection of pullbacks of the local code along all local views:
By extensionality, it suffices to show that for any \(c \in C_1(X)\), \(c \in C(X, L, \Lambda )\) if and only if \(c \in \bigcap _{v \in V} (\operatorname {localView}_\Lambda (v))^{-1}(\ker (H))\).
By simplification using \(\operatorname {Submodule.mem_iInf}\), \(\operatorname {Submodule.mem_comap}\), and \(\operatorname {LinearMap.mem_ker}\), the right-hand side states: for all \(v\), \(H(\operatorname {localView}_\Lambda (v)\, c) = 0\).
\((\Rightarrow )\): Assume \(c \in C(X, L, \Lambda )\). For any \(v\), by Theorem 252, \(\operatorname {localView}_\Lambda (v)\, c \in \ker (H)\), so applying \(\operatorname {LinearMap.mem_ker}\) gives \(H(\operatorname {localView}_\Lambda (v)\, c) = 0\).
\((\Leftarrow )\): Assume that for all \(v\), \(H(\operatorname {localView}_\Lambda (v)\, c) = 0\). Then for each \(v\), \(\operatorname {localView}_\Lambda (v)\, c \in \ker (H)\) by \(\operatorname {LinearMap.mem_ker}\). By Theorem 252, \(c \in C(X, L, \Lambda )\).