7 Def 1: Boundary and Coboundary Maps
Let \(G = (V, E)\) be a graph with a chosen collection \(\mathcal{C}\) of cycles. We define the boundary and coboundary maps as \(\mathbb {Z}_2\)-linear maps using binary vector representations.
A graph with cycles is a structure \((G, V, E, C)\) where:
\(V\), \(E\), \(C\) are finite types with decidable equality,
\(G\) is a simple graph on \(V\) with decidable adjacency,
\(\mathrm{edgeEndpoints} : E \to V \times V\) assigns to each edge its two endpoints,
for each edge \(e\), the endpoints are adjacent: \(G.\mathrm{Adj}(\mathrm{edgeEndpoints}(e)_1, \mathrm{edgeEndpoints}(e)_2)\),
edges are symmetric: adjacency holds in both directions,
\(\mathrm{cycles} : C \to \mathrm{Finset}(E)\) assigns to each cycle index its set of edges.
An edge \(e\) is incident to a vertex \(v\) if \(v\) is one of its endpoints:
The set of edges incident to a vertex \(v\) is:
The set of vertices incident to an edge \(e\) (its two endpoints) is:
For any edge \(e\) and vertex \(v\),
By simplification using the definitions of \(\mathrm{edgeVertices}\) and \(\mathrm{isIncident}\), membership in \(\{ v_1, v_2\} \) is equivalent to \(v = v_1 \lor v = v_2\), which is precisely the definition of incidence. The result follows by propositional logic (tauto).
A cycle \(c\) contains an edge \(e\) if \(e \in \mathrm{cycles}(c)\).
The set of cycles containing a given edge \(e\) is:
We define the binary vector spaces:
\(\mathbb {Z}_2^V := V \to \mathbb {Z}_2\) (binary vectors over vertices),
\(\mathbb {Z}_2^E := E \to \mathbb {Z}_2\) (binary vectors over edges),
\(\mathbb {Z}_2^C := C \to \mathbb {Z}_2\) (binary vectors over cycles).
Each carries a natural \(\mathbb {Z}_2\)-module structure.
The standard basis vectors are defined as:
\(\mathrm{basisV}(v) = \mathbf{e}_v \in \mathbb {Z}_2^V\): the vector with \(1\) at position \(v\) and \(0\) elsewhere,
\(\mathrm{basisE}(e) = \mathbf{e}_e \in \mathbb {Z}_2^E\): the vector with \(1\) at position \(e\) and \(0\) elsewhere,
\(\mathrm{basisC}(c) = \mathbf{e}_c \in \mathbb {Z}_2^C\): the vector with \(1\) at position \(c\) and \(0\) elsewhere.
Formally, \(\mathrm{basisV}(v) = \pi _{\mathrm{single}}(v, 1)\) (and similarly for edges and cycles).
The boundary of a single edge \(e\) with endpoints \((v, v')\) is:
the binary vector with \(1\)s at positions \(v\) and \(v'\).
The boundary map \(\partial : \mathbb {Z}_2^E \to \mathbb {Z}_2^V\) is the \(\mathbb {Z}_2\)-linear map defined by:
where \(\partial e = \mathbf{e}_v + \mathbf{e}_{v'}\) for edge \(e = \{ v, v'\} \).
For any edge \(e\),
By the definition of the boundary map, \(\partial (\mathbf{e}_e) = \sum _{e' \in E} \mathbf{e}_e(e') \cdot \partial e'\). We isolate the term \(e' = e\) using Finset.sum_eq_single. For the term \(e' = e\), we have \(\mathbf{e}_e(e) = 1\), so the contribution is \(1 \cdot \partial e = \partial e\). For any other \(e' \neq e\), we have \(\mathbf{e}_e(e') = 0\) by the definition of the standard basis vector (Pi.single), so the contribution is \(0 \cdot \partial e' = 0\). The remaining case \(e \notin \mathrm{univ}\) is absurd since \(e \in \mathrm{Finset.univ}\).
For any edge \(e\), the two endpoints are distinct:
This follows from the fact that simple graphs have no self-loops: since the endpoints are adjacent, they must be distinct (by \(\mathrm{SimpleGraph.ne\_ of\_ adj}\)).
The boundary of an edge \(e\) evaluated at vertex \(v\) is:
Unfolding the definition, \((\partial e)(v) = \mathbf{e}_{v_1}(v) + \mathbf{e}_{v_2}(v)\) where \((v_1, v_2) = \mathrm{edgeEndpoints}(e)\). We consider three cases:
If \(v_1 = v\): then \(\mathbf{e}_{v_1}(v) = 1\). Since \(v_1 \neq v_2\) (by distinctness of endpoints), \(\mathbf{e}_{v_2}(v) = 0\). Thus \((\partial e)(v) = 1 + 0 = 1\), and \(\mathrm{isIncident}(e, v)\) holds.
If \(v_1 \neq v\) and \(v_2 = v\): then \(\mathbf{e}_{v_1}(v) = 0\) and \(\mathbf{e}_{v_2}(v) = 1\). Thus \((\partial e)(v) = 0 + 1 = 1\), and \(\mathrm{isIncident}(e, v)\) holds.
If \(v_1 \neq v\) and \(v_2 \neq v\): then both basis evaluations are \(0\), giving \((\partial e)(v) = 0\), and \(\mathrm{isIncident}(e, v)\) does not hold.
For any edge-vector \(f \in \mathbb {Z}_2^E\) and vertex \(v\),
By definition, \(\partial (f)(v) = \sum _{e \in E} f(e) \cdot (\partial e)(v)\). Evaluating the pointwise sum, we split \(E\) into edges incident to \(v\) and those not incident to \(v\). For non-incident edges \(e\), we have \((\partial e)(v) = 0\) by the characterization of boundary evaluation, so \(f(e) \cdot 0 = 0\). Thus the sum over non-incident edges vanishes and we add zero. The incident filter equals \(\mathrm{incidentEdges}(v)\) by definition. For incident edges, \((\partial e)(v) = 1\), so \(f(e) \cdot 1 = f(e)\). The result follows by congruence of the sums.
The coboundary of a single vertex \(v\) is the characteristic vector of edges incident to \(v\):
The coboundary map \(\delta : \mathbb {Z}_2^V \to \mathbb {Z}_2^E\) is the \(\mathbb {Z}_2\)-linear map defined by:
where \(\delta v\) is the characteristic vector of edges incident to \(v\).
For any vertex \(v\),
By the definition of the coboundary map, \(\delta (\mathbf{e}_v) = \sum _{w \in V} \mathbf{e}_v(w) \cdot \delta w\). We isolate the term \(w = v\) using Finset.sum_eq_single. For \(w = v\), we have \(\mathbf{e}_v(v) = 1\), giving \(1 \cdot \delta v = \delta v\). For \(w \neq v\), we have \(\mathbf{e}_v(w) = 0\), giving \(0 \cdot \delta w = 0\). The case \(v \notin \mathrm{univ}\) is absurd.
For any vertex-vector \(f \in \mathbb {Z}_2^V\) and edge \(e\),
By definition, \(\delta (f)(e) = \sum _{v \in V} f(v) \cdot (\delta v)(e)\). Evaluating the pointwise sum, we split \(V\) into vertices incident to \(e\) and those not incident. The incident filter equals \(\mathrm{edgeVertices}(e)\) by the characterization of edge vertices via incidence (using the equivalence from the membership lemma and tautological reasoning). For non-incident vertices \(v\), \((\delta v)(e) = 0\), so \(f(v) \cdot 0 = 0\), and the sum vanishes. For incident vertices, \((\delta v)(e) = 1\), so \(f(v) \cdot 1 = f(v)\). The result follows by congruence.
For any \(f \in \mathbb {Z}_2^E\) and \(g \in \mathbb {Z}_2^V\),
That is, \(\langle \partial f, g \rangle = \langle f, \delta g \rangle \), so \(\delta = \partial ^T\).
We proceed by a chain of equalities:
The exchange of summation order is justified by the equivalence: \(e \in \mathrm{incidentEdges}(v) \iff v \in \mathrm{edgeVertices}(e)\), which follows from the membership characterization via incidence.
The boundary of a single cycle \(c\) is the characteristic vector of its edges:
The second boundary map \(\partial _2 : \mathbb {Z}_2^C \to \mathbb {Z}_2^E\) is the \(\mathbb {Z}_2\)-linear map defined by:
where \(\partial _2 c\) is the characteristic vector of edges in cycle \(c\).
For any cycle \(c\),
By the definition of the second boundary map, \(\partial _2(\mathbf{e}_c) = \sum _{d \in C} \mathbf{e}_c(d) \cdot \partial _2 d\). We isolate the term \(d = c\) using Finset.sum_eq_single. For \(d = c\), \(\mathbf{e}_c(c) = 1\), giving \(1 \cdot \partial _2 c = \partial _2 c\). For \(d \neq c\), \(\mathbf{e}_c(d) = 0\), giving \(0 \cdot \partial _2 d = 0\). The case \(c \notin \mathrm{univ}\) is absurd.
For any cycle-vector \(f \in \mathbb {Z}_2^C\) and edge \(e\),
By definition, \(\partial _2(f)(e) = \sum _{c \in C} f(c) \cdot (\partial _2 c)(e)\). Evaluating the pointwise sum, we split \(C\) into cycles containing \(e\) and those not containing \(e\). The containing filter equals \(\mathrm{cyclesContaining}(e)\) by definition. For cycles \(c\) not containing \(e\), \((\partial _2 c)(e) = 0\), so \(f(c) \cdot 0 = 0\), and the sum vanishes. For cycles containing \(e\), \((\partial _2 c)(e) = 1\), so \(f(c) \cdot 1 = f(c)\). The result follows by congruence.
The second coboundary of a single edge \(e\) is the characteristic vector of cycles containing \(e\):
The second coboundary map \(\delta _2 : \mathbb {Z}_2^E \to \mathbb {Z}_2^C\) is the \(\mathbb {Z}_2\)-linear map defined by:
where \(\delta _2 e\) is the characteristic vector of cycles containing \(e\).
For any edge \(e\),
By the definition of the second coboundary map, \(\delta _2(\mathbf{e}_e) = \sum _{e' \in E} \mathbf{e}_e(e') \cdot \delta _2 e'\). We isolate the term \(e' = e\) using Finset.sum_eq_single. For \(e' = e\), \(\mathbf{e}_e(e) = 1\), giving \(1 \cdot \delta _2 e = \delta _2 e\). For \(e' \neq e\), \(\mathbf{e}_e(e') = 0\), giving \(0 \cdot \delta _2 e' = 0\). The case \(e \notin \mathrm{univ}\) is absurd.
For any edge-vector \(f \in \mathbb {Z}_2^E\) and cycle \(c\),
By definition, \(\delta _2(f)(c) = \sum _{e \in E} f(e) \cdot (\delta _2 e)(c)\). Evaluating the pointwise sum, we split \(E\) into edges in cycle \(c\) and those not in cycle \(c\). The filter of edges in cycle \(c\) equals \(\mathrm{cycles}(c)\) (by simplification). For edges \(e \notin \mathrm{cycles}(c)\), \((\delta _2 e)(c) = 0\), so \(f(e) \cdot 0 = 0\), and the sum vanishes. For edges \(e \in \mathrm{cycles}(c)\), \((\delta _2 e)(c) = 1\), so \(f(e) \cdot 1 = f(e)\). The result follows by congruence.
For any \(f \in \mathbb {Z}_2^C\) and \(g \in \mathbb {Z}_2^E\),
That is, \(\langle \partial _2 f, g \rangle = \langle f, \delta _2 g \rangle \), so \(\delta _2 = \partial _2^T\).
We proceed by a chain of equalities:
The exchange of summation order is justified by the equivalence: \(c \in \mathrm{cyclesContaining}(e) \iff e \in \mathrm{cycles}(c)\), which follows from the definitions of \(\mathrm{cyclesContaining}\) and \(\mathrm{cycleContainsEdge}\) by propositional logic.
\(\partial (0) = 0\).
This follows directly from the linearity of \(\partial \) (the map_zero property of linear maps).
\(\delta (0) = 0\).
This follows directly from the linearity of \(\delta \) (the map_zero property of linear maps).
\(\partial _2(0) = 0\).
This follows directly from the linearity of \(\partial _2\) (the map_zero property of linear maps).
\(\delta _2(0) = 0\).
This follows directly from the linearity of \(\delta _2\) (the map_zero property of linear maps).
For \(f, g \in \mathbb {Z}_2^E\), \(\partial (f + g) = \partial (f) + \partial (g)\).
This follows directly from the linearity of \(\partial \) (the map_add property of linear maps).
For \(f, g \in \mathbb {Z}_2^V\), \(\delta (f + g) = \delta (f) + \delta (g)\).
This follows directly from the linearity of \(\delta \) (the map_add property of linear maps).
For \(f, g \in \mathbb {Z}_2^C\), \(\partial _2(f + g) = \partial _2(f) + \partial _2(g)\).
This follows directly from the linearity of \(\partial _2\) (the map_add property of linear maps).
For \(f, g \in \mathbb {Z}_2^E\), \(\delta _2(f + g) = \delta _2(f) + \delta _2(g)\).
This follows directly from the linearity of \(\delta _2\) (the map_add property of linear maps).
The incidence matrix \(M : V \times E \to \mathbb {Z}_2\) is defined by:
For any vertex \(v\) and edge \(e\),
By simplification using the definitions of the incidence matrix and the boundary evaluation characterization, both expressions equal \(1\) if \(\mathrm{isIncident}(e, v)\) and \(0\) otherwise.
For any \(f \in \mathbb {Z}_2^E\) and vertex \(v\),
That is, \(\partial \) is multiplication by the incidence matrix.
By the vertex characterization, \(\partial (f)(v) = \sum _{e \in \mathrm{incidentEdges}(v)} f(e)\). We split the universal sum \(\sum _{e \in E} M(v, e) \cdot f(e)\) into incident and non-incident edges. For incident edges, \(M(v, e) = 1\), so \(M(v, e) \cdot f(e) = f(e)\), matching the restricted sum. For non-incident edges, \(M(v, e) = 0\), so \(M(v, e) \cdot f(e) = 0\), and by summing these to zero and adding zero, both sides agree.
For any \(f \in \mathbb {Z}_2^V\) and edge \(e\),
That is, \(\delta \) is multiplication by the transpose of the incidence matrix.
By the edge characterization, \(\delta (f)(e) = \sum _{v \in \mathrm{edgeVertices}(e)} f(v)\). We split the universal sum \(\sum _{v \in V} M(v, e) \cdot f(v)\) into incident and non-incident vertices. The incident filter equals \(\mathrm{edgeVertices}(e)\) by the equivalence between incidence and edge vertex membership (using the membership lemma and tautological reasoning). For incident vertices, \(M(v, e) = 1\), so the contribution is \(f(v)\). For non-incident vertices, \(M(v, e) = 0\), so the contribution is \(0\). Summing the non-incident terms to zero and adding zero, both sides agree.
The cycle-edge incidence matrix \(N : C \times E \to \mathbb {Z}_2\) is defined by:
For any \(f \in \mathbb {Z}_2^C\) and edge \(e\),
That is, \(\partial _2\) is multiplication by the cycle-edge matrix.
By the edge characterization, \(\partial _2(f)(e) = \sum _{c \in \mathrm{cyclesContaining}(e)} f(c)\). We split the universal sum \(\sum _{c \in C} N(c, e) \cdot f(c)\) into cycles containing \(e\) and those not containing \(e\). For cycles containing \(e\), \(N(c, e) = 1\), so \(N(c, e) \cdot f(c) = f(c)\), matching the restricted sum. For cycles not containing \(e\), \(N(c, e) = 0\), so \(N(c, e) \cdot f(c) = 0\), and the sum vanishes. Adding zero, both sides agree.
For any \(f \in \mathbb {Z}_2^E\) and cycle \(c\),
That is, \(\delta _2\) is multiplication by the transpose of the cycle-edge matrix.
By the cycle characterization, \(\delta _2(f)(c) = \sum _{e \in \mathrm{cycles}(c)} f(e)\). We split the universal sum \(\sum _{e \in E} N(c, e) \cdot f(e)\) into edges in cycle \(c\) and those not in cycle \(c\). The filter of edges in cycle \(c\) equals\(\mathrm{cycles}(c)\) (by simplification). For edges in the cycle, \(N(c, e) = 1\), so \(N(c, e) \cdot f(e) = f(e)\). For edges not in the cycle, \(N(c, e) = 0\), so \(N(c, e) \cdot f(e) = 0\), and the sum vanishes. Adding zero, both sides agree.