Def_1: Boundary and Coboundary Maps #
Statement #
Let $G = (V, E)$ be a graph with a chosen collection $\mathcal{C}$ of cycles. We define the following $\mathbb{Z}_2$-linear maps using binary vector representations:
Boundary map $\partial: \mathbb{Z}_2^{|E|} \to \mathbb{Z}_2^{|V|}$: For a single edge $e = \{v, v'\}$, define $\partial e = v + v'$ (the binary vector with 1s at positions $v$ and $v'$). Extend linearly to edge-sets: $\partial(\sum_i e_i) = \sum_i \partial e_i$. Equivalently, $\partial$ is the incidence matrix of $G$ over $\mathbb{Z}_2$.
Coboundary map $\delta: \mathbb{Z}_2^{|V|} \to \mathbb{Z}_2^{|E|}$: Define $\delta = \partial^T$ (transpose of $\partial$). For a single vertex $v$, we have $\delta v = \sum_{e \ni v} e$ (the binary vector of all edges incident to $v$).
Second boundary map $\partial_2: \mathbb{Z}_2^{|\mathcal{C}|} \to \mathbb{Z}_2^{|E|}$: For a single cycle $c$, define $\partial_2 c = \sum_{e \in c} e$ (the binary vector of edges in $c$). Extend linearly.
Second coboundary map $\delta_2: \mathbb{Z}_2^{|E|} \to \mathbb{Z}_2^{|\mathcal{C}|}$: Define $\delta_2 = \partial_2^T$. For a single edge $e$, we have $\delta_2 e = \sum_{c \ni e} c$ (the binary vector of cycles containing $e$).
Main Definitions #
GraphWithCycles: A simple graph with a chosen collection of cyclesboundaryMap: The boundary map ∂ : Z₂^E → Z₂^VcoboundaryMap: The coboundary map δ : Z₂^V → Z₂^E (transpose of boundary)boundary2Map: The second boundary map ∂₂ : Z₂^C → Z₂^Ecoboundary2Map: The second coboundary map δ₂ : Z₂^E → Z₂^C (transpose of ∂₂)
Key Properties #
coboundaryMap_eq_transpose: δ = ∂ᵀcoboundary2Map_eq_transpose: δ₂ = ∂₂ᵀboundaryMap_single_edge: ∂(e) = v + v' for edge e = {v, v'}coboundaryMap_single_vertex: δ(v) = sum of incident edges
Graph with Chosen Cycles #
A simple graph together with a chosen collection of cycles (represented as sets of edges). The cycles are indexed by a finite type C.
- graph : SimpleGraph V
The underlying simple graph
- decAdj : DecidableRel self.graph.Adj
Decidable adjacency
- edgeEndpoints : E → V × V
Edges are represented by a type E with a way to get endpoints
- edge_adj (e : E) : self.graph.Adj (self.edgeEndpoints e).1 (self.edgeEndpoints e).2
For each edge, the two endpoints are adjacent
- edge_symm (e : E) : self.graph.Adj (self.edgeEndpoints e).2 (self.edgeEndpoints e).1
Edges are symmetric: we don't distinguish (v, v') from (v', v)
- cycles : C → Finset E
The cycles, each represented as a set of edges
Instances For
Incidence Relation #
An edge e is incident to vertex v if v is one of its endpoints
Equations
- G.isIncident e v = ((G.edgeEndpoints e).1 = v ∨ (G.edgeEndpoints e).2 = v)
Instances For
Equations
- G.decIsIncident e v = inferInstanceAs (Decidable ((G.edgeEndpoints e).1 = v ∨ (G.edgeEndpoints e).2 = v))
The set of edges incident to a vertex v
Equations
- G.incidentEdges v = {e : E | G.isIncident e v}
Instances For
The set of vertices incident to an edge e (its two endpoints)
Equations
- G.edgeVertices e = {(G.edgeEndpoints e).1, (G.edgeEndpoints e).2}
Instances For
A cycle contains an edge if the edge is in the cycle's edge set
Equations
- G.cycleContainsEdge c e = (e ∈ G.cycles c)
Instances For
Equations
- G.decCycleContainsEdge c e = inferInstanceAs (Decidable (e ∈ G.cycles c))
The set of cycles containing a given edge
Equations
- G.cyclesContaining e = {c : C | G.cycleContainsEdge c e}
Instances For
Binary Vector Spaces #
Binary vectors over vertices: Z₂^V
Equations
- GraphWithCycles.VectorV' V = (V → ZMod 2)
Instances For
Binary vectors over edges: Z₂^E
Equations
- GraphWithCycles.VectorE' E = (E → ZMod 2)
Instances For
Binary vectors over cycles: Z₂^C
Equations
- GraphWithCycles.VectorC' C = (C → ZMod 2)
Instances For
Standard Basis Vectors #
Standard basis vector for vertices: 1 at position v, 0 elsewhere
Equations
- GraphWithCycles.basisV v = Pi.single v 1
Instances For
Standard basis vector for edges: 1 at position e, 0 elsewhere
Equations
- GraphWithCycles.basisE e = Pi.single e 1
Instances For
Standard basis vector for cycles: 1 at position c, 0 elsewhere
Equations
- GraphWithCycles.basisC c = Pi.single c 1
Instances For
The Boundary Map ∂ : Z₂^E → Z₂^V #
The boundary of a single edge e = {v, v'} is v + v' (the characteristic vector of {v, v'})
Equations
- G.boundaryOfEdge e = match G.edgeEndpoints e with | (v, v') => GraphWithCycles.basisV v + GraphWithCycles.basisV v'
Instances For
The boundary map ∂ : Z₂^E → Z₂^V For edge e = {v, v'}, ∂(e) = v + v'. Extended linearly to all edge vectors.
Equations
- G.boundaryMap = { toFun := fun (f : GraphWithCycles.VectorE' E) => ∑ e : E, f e • G.boundaryOfEdge e, map_add' := ⋯, map_smul' := ⋯ }
Instances For
Notation for boundary map
Equations
- GraphWithCycles.«term∂» = Lean.ParserDescr.node `GraphWithCycles.«term∂» 1024 (Lean.ParserDescr.symbol "∂")
Instances For
Boundary of basis vector is the boundary of that edge
Endpoints of an edge are distinct (since SimpleGraph has no self-loops)
The boundary of an edge has 1s exactly at its endpoints
Alternative characterization: boundary counts (mod 2) how many times v appears as endpoint
The Coboundary Map δ : Z₂^V → Z₂^E #
The coboundary of a single vertex v is the sum of all incident edges
Equations
- G.coboundaryOfVertex v e = if G.isIncident e v then 1 else 0
Instances For
The coboundary map δ : Z₂^V → Z₂^E For vertex v, δ(v) = sum of all edges incident to v. This is the transpose of the boundary map.
Equations
- G.coboundaryMap = { toFun := fun (f : GraphWithCycles.VectorV' V) => ∑ v : V, f v • G.coboundaryOfVertex v, map_add' := ⋯, map_smul' := ⋯ }
Instances For
Notation for coboundary map
Equations
- GraphWithCycles.termδ = Lean.ParserDescr.node `GraphWithCycles.termδ 1024 (Lean.ParserDescr.symbol "δ")
Instances For
Coboundary of basis vector is the coboundary of that vertex
The coboundary map on a vertex gives the characteristic vector of incident edges
Coboundary map applied to a vertex vector at an edge e
Transpose Relationship: δ = ∂ᵀ #
Key property: The coboundary is the transpose of the boundary. This means ⟨∂f, g⟩ = ⟨f, δg⟩ for the natural pairing.
The Second Boundary Map ∂₂ : Z₂^C → Z₂^E #
The boundary of a single cycle c is the sum of its edges
Instances For
The second boundary map ∂₂ : Z₂^C → Z₂^E For cycle c, ∂₂(c) = sum of all edges in c.
Equations
- G.boundary2Map = { toFun := fun (f : GraphWithCycles.VectorC' C) => ∑ c : C, f c • G.boundary2OfCycle c, map_add' := ⋯, map_smul' := ⋯ }
Instances For
Notation for second boundary map
Equations
- GraphWithCycles.«term∂₂» = Lean.ParserDescr.node `GraphWithCycles.«term∂₂» 1024 (Lean.ParserDescr.symbol "∂₂")
Instances For
Second boundary of basis vector is the boundary of that cycle
The boundary of a cycle has 1s exactly at edges in the cycle
Second boundary map applied to edge e
The Second Coboundary Map δ₂ : Z₂^E → Z₂^C #
The coboundary of a single edge e is the sum of all cycles containing e
Instances For
The second coboundary map δ₂ : Z₂^E → Z₂^C For edge e, δ₂(e) = sum of all cycles containing e. This is the transpose of the second boundary map.
Equations
- G.coboundary2Map = { toFun := fun (f : GraphWithCycles.VectorE' E) => ∑ e : E, f e • G.coboundary2OfEdge e, map_add' := ⋯, map_smul' := ⋯ }
Instances For
Notation for second coboundary map
Equations
- GraphWithCycles.termδ₂ = Lean.ParserDescr.node `GraphWithCycles.termδ₂ 1024 (Lean.ParserDescr.symbol "δ₂")
Instances For
Second coboundary of basis vector is the coboundary of that edge
The coboundary of an edge has 1s exactly at cycles containing it
Second coboundary map applied to cycle c
Transpose Relationship: δ₂ = ∂₂ᵀ #
Key property: The second coboundary is the transpose of the second boundary. This means ⟨∂₂f, g⟩ = ⟨f, δ₂g⟩ for the natural pairing.
Special Case Properties #
Zero and Linearity Properties #
Incidence Matrix Interpretation #
The boundary map can be viewed as multiplication by the incidence matrix. The (v, e) entry is 1 if v is incident to e, 0 otherwise.
Equations
- G.incidenceMatrix v e = if G.isIncident e v then 1 else 0
Instances For
The incidence matrix entry equals the boundary of edge evaluated at vertex
Boundary map is multiplication by incidence matrix
Coboundary map is multiplication by transpose of incidence matrix
Cycle Matrix Interpretation #
The cycle-edge incidence matrix: (c, e) entry is 1 if edge e is in cycle c
Instances For
Second boundary map is multiplication by cycle-edge matrix
Second coboundary map is multiplication by transpose of cycle-edge matrix
Summary #
This formalization defines the boundary and coboundary maps for a graph with chosen cycles:
Boundary map ∂ : Z₂^E → Z₂^V
- For edge e = {v, v'}: ∂(e) = v + v' (sum in Z₂)
- Equivalently: the v-th component of ∂(f) counts (mod 2) edges in f incident to v
Coboundary map δ : Z₂^V → Z₂^E
- For vertex v: δ(v) = sum of all edges incident to v
- This is the transpose of ∂ : ⟨∂f, g⟩ = ⟨f, δg⟩
Second boundary map ∂₂ : Z₂^C → Z₂^E
- For cycle c: ∂₂(c) = sum of all edges in c
- Equivalently: the e-th component counts (mod 2) cycles in f containing e
Second coboundary map δ₂ : Z₂^E → Z₂^C
- For edge e: δ₂(e) = sum of all cycles containing e
- This is the transpose of ∂₂ : ⟨∂₂f, g⟩ = ⟨f, δ₂g⟩
Key properties proven:
- All maps are Z₂-linear
- Transpose relationships verified via bilinear pairing identity
- Maps can be expressed as matrix multiplication by incidence/cycle matrices