Rem_7: Exactness of Boundary and Coboundary Maps

Statement

When a generating set of cycles for graph G is chosen, the maps ∂₂ (boundary from cycles to edges) and ∂ (boundary from edges to vertices) form an exact sequence in the sense that im(∂₂) = ker(∂). That is, the image of ∂₂ equals the kernel of ∂: an edge-set is the boundary of some cycle-set if and only if it has zero boundary (i.e., every vertex has even degree in the edge-set).

Similarly, the coboundary maps δ and δ₂ form an exact sequence: ker(δ₂) = im(δ).

Note that δ has a nontrivial kernel: ker(δ) = {𝟬, 𝟙} where 𝟙 is the all-ones vector (corresponding to the full vertex set), since every edge has exactly two endpoints.

Main Results

• boundary_comp_boundary2_eq_zero : ∂ ∘ ∂₂ = 0 (chain complex property)
• coboundary2_comp_coboundary_eq_zero : δ₂ ∘ δ = 0 (cochain complex property)
• allOnes_in_ker_coboundary : 𝟙 ∈ ker(δ) - follows from "every edge has two endpoints"
• zero_in_ker_coboundary : 0 ∈ ker(δ)
• ker_coboundary_nontrivial : ker(δ) contains both 0 and 𝟙 (nontrivial)
• ker_coboundary_classification : ker(δ) = {0, 𝟙} for connected graphs
• im_coboundary_subset_ker_coboundary2 : im(δ) ⊆ ker(δ₂) (cochain complex property)
• exactness_coboundary_iff : Exactness for coboundary (under cut generation assumption)
• exactness_boundary_iff : Exactness for boundary (under cycle generation assumption)
• boundary_zero_iff_even_degree : Zero boundary ↔ even degree at all vertices

File Structure

1. Definitions and Basic Properties
2. All-Ones Vector and Nontrivial Kernel (key: "every edge has exactly two endpoints")
3. Chain Complex Property: ∂ ∘ ∂₂ = 0
4. Cochain Complex Property: δ₂ ∘ δ = 0
5. Zero Boundary Characterization
6. Connected Graph Kernel Classification
7. Exactness Properties

Section 1: Definitions and Basic Properties

def GraphWithCycles.IsValidCycleEdgeSet {V : Type u_1} {E : Type u_2} {C : Type u_3} [DecidableEq V] [DecidableEq E] [DecidableEq C] [Fintype V] [Fintype E] [Fintype C] (G : GraphWithCycles V E C) (edgeSet : Finset E) : Prop

A cycle property: a set of edges is a valid cycle if every vertex has even degree in it. This is the defining property that makes ∂(cycle) = 0.

Equations

• G.IsValidCycleEdgeSet edgeSet = ∀ (v : V), {e ∈ edgeSet | G.isIncident e v}.card % 2 = 0

structure GraphWithCycles.GraphWithValidCycles {V : Type u_1} {E : Type u_2} {C : Type u_3} [DecidableEq V] [DecidableEq E] [DecidableEq C] [Fintype V] [Fintype E] [Fintype C] extends GraphWithCycles V E C : Type (max (max u_1 u_2) u_3)

Extended graph with valid cycles.

• graph : SimpleGraph V
• decAdj : DecidableRel self.graph.Adj
• edgeEndpoints : E → V × V
• edge_adj (e : E) : self.graph.Adj (self.edgeEndpoints e).1 (self.edgeEndpoints e).2
• edge_symm (e : E) : self.graph.Adj (self.edgeEndpoints e).2 (self.edgeEndpoints e).1
• cycles : C → Finset E
• cycles_valid (c : C) : self.IsValidCycleEdgeSet (self.cycles c)

def GraphWithCycles.allOnesV {V : Type u_1} : VectorV' V

The all-ones vector: 1 at every vertex

Equations

• GraphWithCycles.allOnesV x✝ = 1

def GraphWithCycles.zeroV {V : Type u_1} : VectorV' V

The zero vector: 0 at every vertex

Equations

• GraphWithCycles.zeroV x✝ = 0

def GraphWithCycles.vertexDegreeMod2 {V : Type u_1} {E : Type u_2} {C : Type u_3} [DecidableEq V] [DecidableEq E] [DecidableEq C] [Fintype V] [Fintype E] [Fintype C] (G : GraphWithCycles V E C) (f : VectorE' E) (v : V) : ZMod 2

The degree of vertex v in an edge-vector f: counts edges incident to v (mod 2).

Equations

• G.vertexDegreeMod2 f v = ∑ e ∈ G.incidentEdges v, f e

def GraphWithCycles.AreAdjacent {V : Type u_1} {E : Type u_2} {C : Type u_3} [DecidableEq V] [DecidableEq E] [DecidableEq C] [Fintype V] [Fintype E] [Fintype C] (G : GraphWithCycles V E C) (v w : V) : Prop

Two vertices are adjacent if they share an edge.

Equations

• G.AreAdjacent v w = ∃ (e : E), (G.edgeEndpoints e).1 = v ∧ (G.edgeEndpoints e).2 = w ∨ (G.edgeEndpoints e).1 = w ∧ (G.edgeEndpoints e).2 = v

def GraphWithCycles.IsConnected {V : Type u_1} {E : Type u_2} {C : Type u_3} [DecidableEq V] [DecidableEq E] [DecidableEq C] [Fintype V] [Fintype E] [Fintype C] (G : GraphWithCycles V E C) : Prop

The graph is connected if any two vertices can be connected by a path.

Equations

• G.IsConnected = ∀ (v w : V), Relation.ReflTransGen G.AreAdjacent v w

Section 2: All-Ones Vector and Nontrivial Kernel

The coboundary map δ has a nontrivial kernel: ker(δ) = {0, 𝟙} where 𝟙 is the all-ones vector. This is because every edge has exactly two endpoints, so δ(𝟙)(e) = 1 + 1 = 0.

theorem GraphWithCycles.two_endpoints_sum_eq_zero : 1 + 1 = 0

Every edge has exactly two endpoints, which in ZMod 2 means 1 + 1 = 0.

theorem GraphWithCycles.allOnes_in_ker_coboundary {V : Type u_1} {E : Type u_2} {C : Type u_3} [DecidableEq V] [DecidableEq E] [DecidableEq C] [Fintype V] [Fintype E] [Fintype C] (G : GraphWithCycles V E C) : G.coboundaryMap allOnesV = 0

The all-ones vector is in ker(δ): δ(𝟙) = 0. This is because every edge has exactly two endpoints.

theorem GraphWithCycles.zero_in_ker_coboundary {V : Type u_1} {E : Type u_2} {C : Type u_3} [DecidableEq V] [DecidableEq E] [DecidableEq C] [Fintype V] [Fintype E] [Fintype C] (G : GraphWithCycles V E C) : G.coboundaryMap zeroV = 0

The zero vector is trivially in ker(δ).

theorem GraphWithCycles.ker_coboundary_nontrivial {V : Type u_1} {E : Type u_2} {C : Type u_3} [DecidableEq V] [DecidableEq E] [DecidableEq C] [Fintype V] [Fintype E] [Fintype C] (G : GraphWithCycles V E C) : G.coboundaryMap zeroV = 0 ∧ G.coboundaryMap allOnesV = 0

The kernel of δ is nontrivial: it contains both 0 and 𝟙. This formalizes the remark that "δ has a nontrivial kernel". Note: This holds for ANY graph - no connectedness required! The key insight is that every edge has exactly two endpoints, so 1 + 1 = 0 in ZMod 2.

theorem GraphWithCycles.ker_coboundary_contains_zero_and_allOnes {V : Type u_1} {E : Type u_2} {C : Type u_3} [DecidableEq V] [DecidableEq E] [DecidableEq C] [Fintype V] [Fintype E] [Fintype C] (G : GraphWithCycles V E C) (f : VectorV' V) : f = 0 ∨ f = allOnesV → G.coboundaryMap f = 0

The inclusion {0, 𝟙} ⊆ ker(δ) holds for ANY graph. The original statement "ker(δ) = {0, 1} since every edge has exactly two endpoints" asserts this inclusion - the "two endpoints" argument shows 𝟙 ∈ ker(δ). For connected graphs, this is an equality; for disconnected graphs, ker(δ) may be larger.

theorem GraphWithCycles.allOnesV_ne_zero {V : Type u_1} [DecidableEq V] [Fintype V] [Nonempty V] : allOnesV ≠ 0

The all-ones vector is nonzero if there is at least one vertex.

theorem GraphWithCycles.ker_coboundary_has_nonzero_element {V : Type u_1} {E : Type u_2} {C : Type u_3} [DecidableEq V] [DecidableEq E] [DecidableEq C] [Fintype V] [Fintype E] [Fintype C] (G : GraphWithCycles V E C) [Nonempty V] : ∃ (f : VectorV' V), f ≠ 0 ∧ G.coboundaryMap f = 0

For a nonempty graph, ker(δ) contains a nonzero element.

Section 3: Coboundary Characterization

The coboundary δ(α)(e) = α(v) + α(v') for e = {v, v'}. This is zero iff both endpoints have the same value.

theorem GraphWithCycles.coboundaryMap_at_edge {V : Type u_1} {E : Type u_2} {C : Type u_3} [DecidableEq V] [DecidableEq E] [DecidableEq C] [Fintype V] [Fintype E] [Fintype C] (G : GraphWithCycles V E C) (f : VectorV' V) (e : E) : G.coboundaryMap f e = f (G.edgeEndpoints e).1 + f (G.edgeEndpoints e).2

Coboundary at an edge: δ(f)(e) = f(v) + f(v') where e = {v, v'}.

theorem GraphWithCycles.ZMod2_add_eq_zero_iff (a b : ZMod 2) : a + b = 0 ↔ a = b

In ZMod 2, a + b = 0 iff a = b.

theorem GraphWithCycles.coboundaryMap_zero_at_edge_iff {V : Type u_1} {E : Type u_2} {C : Type u_3} [DecidableEq V] [DecidableEq E] [DecidableEq C] [Fintype V] [Fintype E] [Fintype C] (G : GraphWithCycles V E C) (f : VectorV' V) (e : E) : G.coboundaryMap f e = 0 ↔ f (G.edgeEndpoints e).1 = f (G.edgeEndpoints e).2

Coboundary is zero at edge iff both endpoints have same value.

theorem GraphWithCycles.coboundaryMap_allOnes_at_edge {V : Type u_1} {E : Type u_2} {C : Type u_3} [DecidableEq V] [DecidableEq E] [DecidableEq C] [Fintype V] [Fintype E] [Fintype C] (G : GraphWithCycles V E C) (e : E) : G.coboundaryMap allOnesV e = 0

For the all-ones vector, coboundary is zero at every edge.

Section 4: Chain Complex Property

The key chain complex property: ∂ ∘ ∂₂ = 0. This means im(∂₂) ⊆ ker(∂): the boundary of any cycle-chain is zero.

theorem GraphWithCycles.boundary_of_valid_cycle_eq_zero {V : Type u_1} {E : Type u_2} {C : Type u_3} [DecidableEq V] [DecidableEq E] [DecidableEq C] [Fintype V] [Fintype E] [Fintype C] {G : GraphWithCycles V E C} (edgeSet : Finset E) (hvalid : G.IsValidCycleEdgeSet edgeSet) : (G.boundaryMap fun (e : E) => if e ∈ edgeSet then 1 else 0) = 0

If a set of edges forms a valid cycle, then its boundary is zero.

theorem GraphWithCycles.boundary_comp_boundary2_eq_zero {V : Type u_1} {E : Type u_2} {C : Type u_3} [DecidableEq V] [DecidableEq E] [DecidableEq C] [Fintype V] [Fintype E] [Fintype C] (G : GraphWithCycles V E C) (hvalid : ∀ (c : C), G.IsValidCycleEdgeSet (G.cycles c)) : G.boundaryMap ∘ₗ G.boundary2Map = 0

The chain complex property: ∂ ∘ ∂₂ = 0. This is equivalent to im(∂₂) ⊆ ker(∂).

theorem GraphWithCycles.im_boundary2_subset_ker_boundary {V : Type u_1} {E : Type u_2} {C : Type u_3} [DecidableEq V] [DecidableEq E] [DecidableEq C] [Fintype V] [Fintype E] [Fintype C] (G : GraphWithCycles V E C) (hvalid : ∀ (c : C), G.IsValidCycleEdgeSet (G.cycles c)) (cycleVec : VectorC' C) : G.boundaryMap (G.boundary2Map cycleVec) = 0

The image of ∂₂ is contained in the kernel of ∂.

Section 5: Cochain Complex Property

The cochain complex property: δ₂ ∘ δ = 0. This means im(δ) ⊆ ker(δ₂).

theorem GraphWithCycles.cycle_visits_vertex_even {V : Type u_1} {E : Type u_2} {C : Type u_3} [DecidableEq V] [DecidableEq E] [DecidableEq C] [Fintype V] [Fintype E] [Fintype C] {G : GraphWithCycles V E C} (c : C) (v : V) (cycles_valid : G.IsValidCycleEdgeSet (G.cycles c)) : {e ∈ G.cycles c | G.isIncident e v}.card % 2 = 0

For a valid cycle, the sum over edges in the cycle of (endpoints match v) has even parity. This is because every valid cycle visits each internal vertex an even number of times.

theorem GraphWithCycles.coboundary2_comp_coboundary_eq_zero {V : Type u_1} {E : Type u_2} {C : Type u_3} [DecidableEq V] [DecidableEq E] [DecidableEq C] [Fintype V] [Fintype E] [Fintype C] (G : GraphWithCycles V E C) (hvalid : ∀ (c : C), G.IsValidCycleEdgeSet (G.cycles c)) : G.coboundary2Map ∘ₗ G.coboundaryMap = 0

The cochain complex property: δ₂ ∘ δ = 0. This is equivalent to im(δ) ⊆ ker(δ₂).

theorem GraphWithCycles.im_coboundary_subset_ker_coboundary2 {V : Type u_1} {E : Type u_2} {C : Type u_3} [DecidableEq V] [DecidableEq E] [DecidableEq C] [Fintype V] [Fintype E] [Fintype C] (G : GraphWithCycles V E C) (hvalid : ∀ (c : C), G.IsValidCycleEdgeSet (G.cycles c)) (vertexVec : VectorV' V) : G.coboundary2Map (G.coboundaryMap vertexVec) = 0

The image of δ is contained in the kernel of δ₂.

Section 6: Zero Boundary Characterization

An edge-set has zero boundary iff every vertex has even degree in the edge-set.

theorem GraphWithCycles.boundaryMap_eq_vertexDegreeMod2 {V : Type u_1} {E : Type u_2} {C : Type u_3} [DecidableEq V] [DecidableEq E] [DecidableEq C] [Fintype V] [Fintype E] [Fintype C] {G : GraphWithCycles V E C} (f : VectorE' E) (v : V) : G.boundaryMap f v = G.vertexDegreeMod2 f v

Boundary at vertex equals vertex degree (mod 2).

theorem GraphWithCycles.boundary_zero_iff_all_degrees_zero {V : Type u_1} {E : Type u_2} {C : Type u_3} [DecidableEq V] [DecidableEq E] [DecidableEq C] [Fintype V] [Fintype E] [Fintype C] {G : GraphWithCycles V E C} (f : VectorE' E) : G.boundaryMap f = 0 ↔ ∀ (v : V), G.vertexDegreeMod2 f v = 0

Zero boundary is equivalent to all vertex degrees being zero (mod 2).

theorem GraphWithCycles.boundary_zero_iff_even_degree {V : Type u_1} {E : Type u_2} {C : Type u_3} [DecidableEq V] [DecidableEq E] [DecidableEq C] [Fintype V] [Fintype E] [Fintype C] {G : GraphWithCycles V E C} (f : VectorE' E) : G.boundaryMap f = 0 ↔ ∀ (v : V), G.vertexDegreeMod2 f v = 0

Zero boundary ↔ every vertex has even degree in the edge-set. This is the characterization mentioned in the remark.

Section 7: Connected Graph Kernel Classification

For a connected graph, ker(δ) = {0, 𝟙}. Connectedness means any two vertices can be joined by a path of edges.

theorem GraphWithCycles.ker_coboundary_constant_on_adjacent {V : Type u_1} {E : Type u_2} {C : Type u_3} [DecidableEq V] [DecidableEq E] [DecidableEq C] [Fintype V] [Fintype E] [Fintype C] {G : GraphWithCycles V E C} (f : VectorV' V) (hf : G.coboundaryMap f = 0) (v w : V) (hadj : G.AreAdjacent v w) : f v = f w

If f ∈ ker(δ) and v, w are adjacent, then f(v) = f(w).

theorem GraphWithCycles.ker_coboundary_constant_of_connected {V : Type u_1} {E : Type u_2} {C : Type u_3} [DecidableEq V] [DecidableEq E] [DecidableEq C] [Fintype V] [Fintype E] [Fintype C] {G : GraphWithCycles V E C} (f : VectorV' V) (hf : G.coboundaryMap f = 0) (hconn : G.IsConnected) (v w : V) : f v = f w

For a connected graph, if f ∈ ker(δ), then f is constant on all vertices.

theorem GraphWithCycles.ZMod2_cases (x : ZMod 2) : x = 0 ∨ x = 1

In ZMod 2, every element is 0 or 1.

theorem GraphWithCycles.ker_coboundary_classification {V : Type u_1} {E : Type u_2} {C : Type u_3} [DecidableEq V] [DecidableEq E] [DecidableEq C] [Fintype V] [Fintype E] [Fintype C] {G : GraphWithCycles V E C} (f : VectorV' V) (hf : G.coboundaryMap f = 0) (hconn : G.IsConnected) : f = 0 ∨ f = allOnesV

For a connected graph, ker(δ) = {0, 𝟙}. Every element of ker(δ) is either 0 or the all-ones vector.

theorem GraphWithCycles.ker_coboundary_eq_zero_or_allOnes {V : Type u_1} {E : Type u_2} {C : Type u_3} [DecidableEq V] [DecidableEq E] [DecidableEq C] [Fintype V] [Fintype E] [Fintype C] {G : GraphWithCycles V E C} (f : VectorV' V) (hf : G.coboundaryMap f = 0) (hconn : G.IsConnected) : f = 0 ∨ f = allOnesV

Connected graph version: ker(δ) has exactly two elements {0, 𝟙}.

theorem GraphWithCycles.ker_coboundary_iff {V : Type u_1} {E : Type u_2} {C : Type u_3} [DecidableEq V] [DecidableEq E] [DecidableEq C] [Fintype V] [Fintype E] [Fintype C] {G : GraphWithCycles V E C} (hconn : G.IsConnected) (f : VectorV' V) : G.coboundaryMap f = 0 ↔ f = 0 ∨ f = allOnesV

Classification as an iff statement for connected graphs.

Section 8: Exactness Properties

Exactness at C₁ means im(∂₂) = ker(∂):

• One direction (im(∂₂) ⊆ ker(∂)) follows from ∂ ∘ ∂₂ = 0 for valid cycles
• The other direction requires that the cycles generate all cycles

def GraphWithCycles.CyclesGenerate {V : Type u_1} {E : Type u_2} {C : Type u_3} [DecidableEq V] [DecidableEq E] [DecidableEq C] [Fintype V] [Fintype E] [Fintype C] (G : GraphWithCycles V E C) : Prop

The cycles generate all cycles if every edge-chain with zero boundary can be written as a sum of cycle boundaries.

Equations

• G.CyclesGenerate = ∀ (f : GraphWithCycles.VectorE' E), G.boundaryMap f = 0 → ∃ (g : GraphWithCycles.VectorC' C), G.boundary2Map g = f

theorem GraphWithCycles.exactness_boundary_iff {V : Type u_1} {E : Type u_2} {C : Type u_3} [DecidableEq V] [DecidableEq E] [DecidableEq C] [Fintype V] [Fintype E] [Fintype C] (G : GraphWithCycles V E C) (hvalid : ∀ (c : C), G.IsValidCycleEdgeSet (G.cycles c)) (hgen : G.CyclesGenerate) (f : VectorE' E) : (∃ (g : VectorC' C), G.boundary2Map g = f) ↔ G.boundaryMap f = 0

Exactness at C₁: an edge-chain is in im(∂₂) iff it has zero boundary. This requires that the cycles generate all cycles AND cycles are valid.

def GraphWithCycles.CutsGenerate {V : Type u_1} {E : Type u_2} {C : Type u_3} [DecidableEq V] [DecidableEq E] [DecidableEq C] [Fintype V] [Fintype E] [Fintype C] (G : GraphWithCycles V E C) : Prop

The cuts generate all cocycles if every edge-chain in ker(δ₂) is in im(δ). This is the dual of CyclesGenerate.

Equations

• G.CutsGenerate = ∀ (f : GraphWithCycles.VectorE' E), G.coboundary2Map f = 0 → ∃ (g : GraphWithCycles.VectorV' V), G.coboundaryMap g = f

theorem GraphWithCycles.exactness_coboundary_iff {V : Type u_1} {E : Type u_2} {C : Type u_3} [DecidableEq V] [DecidableEq E] [DecidableEq C] [Fintype V] [Fintype E] [Fintype C] (G : GraphWithCycles V E C) (hvalid : ∀ (c : C), G.IsValidCycleEdgeSet (G.cycles c)) (hcuts : G.CutsGenerate) (f : VectorE' E) : (∃ (g : VectorV' V), G.coboundaryMap g = f) ↔ G.coboundary2Map f = 0

Exactness for coboundary maps: an edge-chain is in im(δ) iff it's in ker(δ₂). This requires valid cycles (for im(δ) ⊆ ker(δ₂)) and cut generation (for the converse).

Section 9: Summary and Simp Lemmas

@[simp]

theorem GraphWithCycles.coboundaryMap_allOnesV {V : Type u_1} {E : Type u_2} {C : Type u_3} [DecidableEq V] [DecidableEq E] [DecidableEq C] [Fintype V] [Fintype E] [Fintype C] {G : GraphWithCycles V E C} : G.coboundaryMap allOnesV = 0

@[simp]

theorem GraphWithCycles.coboundaryMap_zeroV {V : Type u_1} {E : Type u_2} {C : Type u_3} [DecidableEq V] [DecidableEq E] [DecidableEq C] [Fintype V] [Fintype E] [Fintype C] {G : GraphWithCycles V E C} : G.coboundaryMap zeroV = 0

theorem GraphWithCycles.ker_coboundary_is_zero_and_allOnes {V : Type u_1} {E : Type u_2} {C : Type u_3} [DecidableEq V] [DecidableEq E] [DecidableEq C] [Fintype V] [Fintype E] [Fintype C] {G : GraphWithCycles V E C} (hconn : G.IsConnected) (f : VectorV' V) : G.coboundaryMap f = 0 ↔ f = 0 ∨ f = allOnesV

The remark's key assertion: ker(δ) = {0, 𝟙} for connected graphs.