46 Def 28: Iota and Pi Maps
Let \(X\) be a finite graph with a free right \(H\)-action, \(\Lambda \) a cell labeling with \(s\) local code bits, and \(h_\Lambda \) a proof that \(\Lambda \) is \(H\)-invariant. For a vertex orbit \(V \in X_0/H\), the quotient local view is the \(\mathbb {F}_2\)-linear map
defined by \(c \mapsto \bigl(i \mapsto c\bigl((\Lambda ^{X/H}_V)^{-1}(i)\bigr)\bigr)\), where \(\Lambda ^{X/H}_V\) is the quotient labeling bijection at \(V\).
Linearity follows: for \(c_1, c_2 : X_1/H \to \mathbb {F}_2\) and \(r \in \mathbb {F}_2\),
Both properties follow by extensionality and simplification of the pointwise operations.
The quotient Tanner differential is the \(\mathbb {F}_2\)-linear map
defined by \(c \mapsto (V \mapsto \operatorname {quotientLocalView}(V)(c))\).
Linearity: for \(c_1, c_2 : X_1/H \to \mathbb {F}_2\) and \(r \in \mathbb {F}_2\), the result follows by extensionality over vertex orbits \(V\) and local indices \(i\), together with simplification of the pointwise addition and scalar multiplication.
The quotient Tanner code complex \(C(X/H, L)\) is the chain complex over \(\mathbb {F}_2\) with chain spaces
and \(C_i = 0\) for \(i \geq 2\) or \(i {\lt} 0\). The differential is
(the quotient Tanner differential), and all other differentials are zero.
The chain complex condition \(d \circ d = 0\) is verified:
For the pair \((i,j,k) = (1,0,k)\): we have \(d_{1,0} \circ 0 = 0\) by the zero postcomposition rule.
For \(i = 0\): the outgoing differential is zero, so the composition vanishes.
For \(i \geq 2\) or \(i {\lt} 0\): the incoming differential is zero, so the composition vanishes by the zero precomposition rule.
All cases with non-adjacent indices satisfy the shape condition vacuously (the shape predicate fails, verified by positivity or simplification).
The homology in degree 1 is denoted \(H_1(C(X/H, L)) := \ker (d_{1,0}) / \operatorname {im}(0) = \ker (\partial )\).
The quotient Tanner homology is the degree-1 homology of the quotient Tanner code complex:
red[UNPROVEN AXIOM]
There exists an \(\mathbb {F}_2\)-linear map
where \(H_1^h = H_1^h(X, \Lambda , \ell , h_\Lambda , h_{\mathrm{compat}})\) is the horizontal homology of the balanced product Tanner cycle code from Definition 27.
The map \(\iota \) is defined on homology classes as follows: given \([\sum _{\mathcal{E}} a_{\mathcal{E}} \mathcal{E}] \in H_1(C(X/H,L))\) (where \(\mathcal{E} = eH\) ranges over edge orbits), set
where \(y_0\) is a fixed \(0\)-cell of the cycle graph \(C_\ell \).
Well-definedness: the orbit indicator \(\sum _{e \in \mathcal{E}} \delta _e\) is \(H\)-invariant in \(C_1(X,L)\), so tensoring with \(\delta _{y_0} \in C_0(C_\ell )\) gives a well-defined element of \(C_1(X,L) \otimes _H C_0(C_\ell )\). The map sends cycles to cycles (the quotient differential is compatible with the balanced product differential) and boundaries to boundaries (well-defined on homology).
Note: This is stated as an axiom because the full proof was not completed in the formalization.
red[UNPROVEN AXIOM]
There exists an \(\mathbb {F}_2\)-linear map
The map \(\pi \) projects from horizontal homology to quotient Tanner code homology by collapsing orbits. By the Künneth decomposition, elements of \(H_1^h = H_1(C(X,L)) \otimes _H H_0(C_\ell )\) are represented by cycles of the form \((\sum _e a_e\, e \otimes y_0, 0)\) with coefficients \(a_e\) constant on \(H\)-orbits. The map sends this class to
Well-definedness: since \(a_e\) is constant on orbits, each orbit \(\mathcal{E} = eH\) contributes \(a_{\mathcal{E}} \cdot \mathcal{E}\), and the quotient differential is compatible with the balanced product differential.
Note: This is stated as an axiom because the full proof was not completed in the formalization.
red[UNPROVEN AXIOM]
Assuming \(\ell \equiv 1 \pmod{2}\) and \(|H|\) is odd, we have
Each orbit \(\mathcal{E} = eH\) has \(|H| = \ell \) elements. Applying \(\iota \) to \([\mathcal{E}]\) gives \([\sum _{e \in \mathcal{E}} e \otimes y_0]\), and then \(\pi \) maps each \(e \otimes y_0\) back to \(\mathcal{E}\), yielding \(\ell \cdot [\mathcal{E}]\). Since \(\ell \) is odd, \(\ell \equiv 1 \pmod{2}\), so \(\ell \cdot [\mathcal{E}] = [\mathcal{E}]\) in \(\mathbb {F}_2\).
Note: This is stated as an axiom because the full proof was not completed in the formalization.
red[UNPROVEN AXIOM]
Assuming \(\ell \equiv 1 \pmod{2}\) and \(|H|\) is odd, we have
For a horizontal class \([(\sum _e a_e\, e \otimes y_0, 0)]\) with \(a_e\) constant on orbits, \(\pi \) sends it to \([\sum _e a_e\, eH]\), and \(\iota \) lifts back to \([(\sum _e a_e \sum _{e' \in eH} e' \otimes y_0, 0)]\). Since each orbit of size \(\ell \) contributes \(\ell \) copies and \(\ell \equiv 1 \pmod{2}\), this equals the original class.
Note: This is stated as an axiom because the full proof was not completed in the formalization.
The witness graph is a trivial graph with a single vertex and a single edge, equipped with the trivial \(\mathrm{Unit}\)-action: the group \(H = \mathrm{Unit}\) acts on both vertices and edges as the identity. The cell sets are \(\mathrm{cells}(n) = \mathrm{Unit}\) for all \(n\), with empty boundary maps (satisfying \(\partial \circ \partial = 0\) vacuously). Both the vertex and edge actions are free (since the only element of \(\mathrm{Unit}\) fixing a cell is the identity). This provides a non-trivial graph with at least one vertex and one edge on which all required hypotheses hold.
The witness labeling is a cell labeling \(\Lambda : \operatorname {witnessGraph}.\operatorname {CellLabeling}(0)\) with \(s = 0\) local code bits. Since \(s = 0\), the labeling map at any vertex is a bijection from the empty set of incident edges to \(\operatorname {Fin}(0) = \emptyset \). It is defined by: for each vertex, the labeling bijection sends any element \(e\) with \(e \in \emptyset \) to its absurdity (by Finset.notMem_empty), and the inverse sends any element of \(\operatorname {Fin}(0)\) to its absurdity (by Fin.elim0).
The witness labeling is \(H\)-invariant:
For any vertex \(v\), group element \(h\), and incident edge \(e\), we need \(\Lambda (v)(e) = \Lambda (h \cdot v)(h \cdot e)\). Since the labeling has \(s = 0\) and the edge \(e\) must satisfy \(e \in \emptyset \) (the empty boundary), the hypothesis \(e.2 \in \operatorname {Finset.empty}\) is absurd, so the conclusion holds vacuously by Finset.notMem_empty.
The witness \(\mathrm{Unit}\) action on \(\operatorname {Fin}(3)\) is the trivial \(\mathrm{MulAction}\) where the unique group element \(() \in \mathrm{Unit}\) acts on every \(i \in \operatorname {Fin}(3)\) as the identity: \(() \cdot i = i\). The axioms \(\mathtt{one\_ smul}\) and \(\mathtt{mul\_ smul}\) hold by reflexivity.
With the witness \(\mathrm{Unit}\)-action on \(\operatorname {Fin}(3)\), the cycle-compatible action condition holds for \(H = \mathrm{Unit}\) and \(\ell = 3\):
For any \(h : \mathrm{Unit}\) and \(i : \operatorname {Fin}(3)\), the condition requires a compatibility between the group action and the cycle graph structure. By the definition of \(\operatorname {witnessUnitMulAction}\), the action is trivial: \(h \cdot i = i\). The required identity holds after unfolding the definition and simplifying.
The premises of the iota map are satisfiable: there exist a group \(H\), a graph with \(H\)-action \(X\), a cell labeling \(\Lambda \), a natural number \(\ell \), a group action of \(H\) on \(\operatorname {Fin}(\ell )\), invariance \(h_\Lambda \), and cycle-compatibility \(h_{\mathrm{compat}}\), such that the underlying graph has at least one vertex and one edge.
We take \(H = \mathrm{Unit}\), \(X = \operatorname {witnessGraph}\), \(s = 0\), \(\Lambda = \operatorname {witnessLabeling}\), \(\ell = 3\), the action from \(\operatorname {witnessUnitMulAction}\), invariance from \(\operatorname {witnessLabeling_invariant}\), and compatibility from \(\operatorname {witnessCycleCompat}\). The witness graph has \(\operatorname {cells}(0) = \mathrm{Unit}\) and \(\operatorname {cells}(1) = \mathrm{Unit}\), so \((() , \operatorname {trivial})\) witnesses both a vertex and an edge.
The premises of \(\pi \circ \iota = \mathrm{id}\) (including \(\ell \geq 3\), \(\ell \) odd, and \(|H|\) odd) are satisfiable with a non-trivial graph.
We take the same witnesses as in \(\operatorname {iotaMap_satisfiable}\), additionally verifying: \(\ell = 3 \geq 3\) (by reflexivity of \(\leq \)); \(3 \bmod 2 = 1\) (by reflexivity); and \(\operatorname {Fintype.card}(\mathrm{Unit}) = 1\) is odd, witnessed by \((0, \operatorname {rfl})\) since \(1 = 2 \cdot 0 + 1\).
The premises of \(\iota \circ \pi = \mathrm{id}\) (including \(\ell \geq 3\), \(\ell \) odd, and \(|H|\) odd) are satisfiable with a non-trivial graph.
We use the same witnesses as in \(\operatorname {piMap_comp_iotaMap_satisfiable}\). The oddness of \(|H| = |\mathrm{Unit}| = 1\) is witnessed by the pair \((0, \operatorname {rfl})\).
Assuming \(\ell \equiv 1 \pmod{2}\) and \(|H|\) is odd, the map \(\iota \) is injective:
We apply \(\pi \circ \iota = \mathrm{id}\) (from piMap_comp_iotaMap). Let \(a, b\) be such that \(\iota (a) = \iota (b)\). We have
Rewriting using \(\pi \circ \iota = \mathrm{id}\), we obtain \(\mathrm{id}(a) = \mathrm{id}(b)\), i.e., \(a = b\). Concretely, using congr_arg with \(\pi \) applied to the hypothesis \(\iota (a) = \iota (b)\), then rewriting via LinearMap.comp_apply in both directions and applying the composite identity, we get \(\mathrm{id}(a) = \mathrm{id}(b)\), hence \(a = b\).
Assuming \(\ell \equiv 1 \pmod{2}\) and \(|H|\) is odd, the map \(\pi \) is surjective:
We apply \(\pi \circ \iota = \mathrm{id}\). Given any \(y \in H_1(C(X/H,L))\), we claim \(\iota (y)\) is a preimage of \(y\) under \(\pi \). By LinearMap.ext_iff applied to the identity \(\pi \circ \iota = \mathrm{id}\) at \(y\), we get \(\pi (\iota (y)) = \mathrm{id}(y) = y\), after simplifying via LinearMap.comp_apply and LinearMap.id_apply.
Assuming \(\ell \equiv 1 \pmod{2}\) and \(|H|\) is odd, the map \(\pi \) is injective:
We apply \(\iota \circ \pi = \mathrm{id}\) (from iotaMap_comp_piMap). Let \(a, b\) satisfy \(\pi (a) = \pi (b)\). Applying \(\iota \) to both sides via congr_arg, we get \(\iota (\pi (a)) = \iota (\pi (b))\). Rewriting via LinearMap.comp_apply and the identity \(\iota \circ \pi = \mathrm{id}\), we obtain \(\mathrm{id}(a) = \mathrm{id}(b)\), i.e., \(a = b\).
Assuming \(\ell \equiv 1 \pmod{2}\) and \(|H|\) is odd, the map \(\iota \) is surjective:
We apply \(\iota \circ \pi = \mathrm{id}\). Given any \(y \in H_1^h\), we exhibit \(\pi (y)\) as a preimage under \(\iota \). By LinearMap.ext_iff applied to \(\iota \circ \pi = \mathrm{id}\) at \(y\), we get \(\iota (\pi (y)) = \mathrm{id}(y) = y\), after simplifying via LinearMap.comp_apply and LinearMap.id_apply.
Assuming \(\ell \equiv 1 \pmod{2}\) and \(|H|\) is odd, the map \(\iota \) is a linear isomorphism:
This equivalence \(\iota ^{\equiv }\) is constructed via \(\operatorname {LinearEquiv.ofBijective}(\iota , \langle h_{\mathrm{inj}}, h_{\mathrm{surj}}\rangle )\), where \(h_{\mathrm{inj}}\) is from iotaMap_injective and \(h_{\mathrm{surj}}\) from iotaMap_surjective.
Assuming \(\ell \equiv 1 \pmod{2}\) and \(|H|\) is odd, the map \(\pi \) is a linear isomorphism:
This equivalence \(\pi ^{\equiv }\) is constructed via \(\operatorname {LinearEquiv.ofBijective}(\pi , \langle h_{\mathrm{inj}}, h_{\mathrm{surj}}\rangle )\), where \(h_{\mathrm{inj}}\) is from piMap_injective and \(h_{\mathrm{surj}}\) from piMap_surjective.
The quotient Tanner homology \(H_1(C(X/H, L))\) is nonempty.
The zero element \(0 \in H_1(C(X/H, L))\) witnesses non-emptiness: \(\langle 0 \rangle \).
Assuming \(\ell \equiv 1 \pmod{2}\) and \(|H|\) is odd, the type of linear isomorphisms \(H_1(C(X/H, L)) \simeq _{\mathbb {F}_2} H_1^h\) is nonempty.
The equivalence \(\operatorname {iotaEquiv}(X, \Lambda , \ell , h_\Lambda , h_{\mathrm{compat}}, h_{\ell \mathrm{odd}}, h_{\mathrm{odd}})\) witnesses non-emptiness.