Expanding the definitions, we rewrite each side using the defining sums. We then apply the commutativity of the double summation via Finset.sum_comm. For each edge \(e = \{ a, b\} \), we use the fact that the graph is loopless (so \(a \neq b\)) and decompose \((f(a) + f(b)) \cdot \gamma _e = f(a) \cdot \gamma _e + f(b) \cdot \gamma _e\). We then establish a key identity: for each vertex \(x\), \(f(x) \cdot (\text{if } x \in \{ a,b\} \text{ then } \gamma _e \text{ else } 0)\) equals \(f(a) \cdot \gamma _e\) when \(x = a\), \(f(b) \cdot \gamma _e\) when \(x = b\), and \(0\) otherwise. Rewriting with this identity and splitting the sum into two parts (one for \(a\) and one for \(b\)), we apply Finset.sum_add_distrib and simplify using Finset.sum_ite_eq’ to conclude.

Expanding the definitions, we distribute multiplication over the inner sums on both sides. We then exchange the order of summation via Finset.sum_comm. The result follows by showing that the summands agree: when the membership condition holds, the terms are equal by ring arithmetic; when the condition fails, both sides are zero.

We apply linear map extensionality: let \(\sigma \) be arbitrary and show \((\partial \circ \partial _2)(\sigma ) = 0\) pointwise at each vertex \(v\). Expanding both definitions, we exchange the order of summation (swapping the sum over edges with the sum over cycles). After combining conditionals using the identity \((\text{if } P \text{ then } (\text{if } Q \text{ then } a \text{ else } 0) \text{ else } 0) = (\text{if } P \wedge Q \text{ then } a \text{ else } 0)\), we rewrite each inner sum as \(|\{ e : e \in \text{cycles}(c) \wedge v \in e\} | \cdot \sigma (c)\). By hypothesis, \(p\) divides this cardinality, so its cast to \(\mathbb {Z}_p\) is zero, giving \(0 \cdot \sigma (c) = 0\). The outer sum of zeros is zero.

Let \(\gamma \in \operatorname {im}(\partial _2)\), so \(\gamma = \partial _2(\sigma )\) for some \(\sigma \). We need \(\partial (\gamma ) = 0\). By the chain complex property \(\partial \circ \partial _2 = 0\), we have \(\partial (\partial _2(\sigma )) = 0\), and substituting \(\gamma = \partial _2(\sigma )\) gives \(\partial (\gamma ) = 0\).

This holds by simplification, as both definitions compute the same conditional sum over incident edges.

This holds by simplification of the definitions.

This holds by simplification of the definitions.

This holds by simplification of the definitions.

This follows directly from Equiv.sum_comp, which states that summing a function over a permutation of the index set gives the same result.

Simplifying List.prod on two-element lists, we have \(\prod [g_1, g_2] = g_1 \cdot g_2 \cdot 1 = g_1 \cdot g_2\) and similarly \(\prod [g_2, g_1] = g_2 \cdot g_1\). The conclusion follows directly from the hypothesis \(g_1 \cdot g_2 \neq g_2 \cdot g_1\).

Expanding the definitions, we distribute multiplication over the inner sums on both sides, then exchange the order of summation via Finset.sum_comm. For each pair \((v, e)\), when the incidence condition holds, the terms agree by ring arithmetic; when it fails, both sides are zero.

This holds by simplification of the definitions.

This holds by simplification of the definitions.

Assume for contradiction that all permutations preserve products. The lists \([g_1, g_2]\) and \([g_2, g_1]\) are permutations of each other (by a swap). By the assumption, \(\prod [g_1, g_2] = \prod [g_2, g_1]\). Simplifying, \(g_1 \cdot g_2 = g_2 \cdot g_1\), contradicting the hypothesis.

The four components are established as follows:

1. The transpose property of qudit maps follows from quditCoboundaryMap_eq_transpose.

2. Specialization to \(\mathbb {Z}_2\) follows from quditBoundaryMap_specializes_to_qubit.

3. Abelian permutation invariance follows from Equiv.sum_comp.

4. Nonabelian order dependence follows from nonabelian_product_order_dependent.