Remark 5: Exactness of Sequences

Statement

For a graph G = (V, E) with a collection of cycles C (where each cycle c ∈ C is specified by its edge set, and each vertex of G that appears in c is incident to exactly two edges of c), the maps ∂₂ and ∂ satisfy the chain complex property ∂ ∘ ∂₂ = 0.

Similarly, δ₂ ∘ δ = 0 holds by transposition.

For a connected graph, ker(δ) = {0, 1} (constant functions), so the sequences are not short exact since ker(δ) ≠ 0.

If C generates the cycle space (im(∂₂) = ker(∂)), then ker(∂) = im(∂₂).

Main Results

• boundary_comp_secondBoundary_eq_zero : ∂ ∘ ∂₂ = 0 (chain complex property)
• secondCoboundary_comp_coboundary_eq_zero : δ₂ ∘ δ = 0 (by transposition)
• range_secondBoundary_le_ker_boundary : im(∂₂) ≤ ker(∂)
• range_coboundary_le_ker_secondCoboundary : im(δ) ≤ ker(δ₂)
• allOnes_mem_ker_coboundary : the all-ones vector is in ker(δ)
• ker_coboundary_connected : for connected G, ker(δ) = {0, 1}
• ker_coboundary_ne_bot : ker(δ) ≠ 0 (sequences are not short exact)

Chain Complex Property: ∂ ∘ ∂₂ = 0

theorem GraphMaps.boundary_of_cycle_eq_zero {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] {C : Type u_2} [Fintype C] [DecidableEq C] (cycles : C → Set ↑G.edgeSet) [(c : C) → DecidablePred fun (x : ↑G.edgeSet) => x ∈ cycles c] [Fintype ↑G.edgeSet] (hcyc : ∀ (c : C) (v : V), Even {e : ↑G.edgeSet | e ∈ cycles c ∧ v ∈ ↑e}.card) (c : C) (v : V) : (boundaryMap G) (fun (e : ↑G.edgeSet) => if e ∈ cycles c then 1 else 0) v = 0

Helper: if every cycle in the collection has the property that each vertex is incident to an even number of its edges, then the boundary of a single cycle indicator is zero.

theorem GraphMaps.boundaryMap_comp_secondBoundaryMap_single {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] {C : Type u_2} [Fintype C] [DecidableEq C] (cycles : C → Set ↑G.edgeSet) [(c : C) → DecidablePred fun (x : ↑G.edgeSet) => x ∈ cycles c] [Fintype ↑G.edgeSet] (hcyc : ∀ (c : C) (v : V), Even {e : ↑G.edgeSet | e ∈ cycles c ∧ v ∈ ↑e}.card) (c : C) (v : V) : (boundaryMap G) ((secondBoundaryMap G cycles) (Pi.single c 1)) v = 0

∂₂(1_c) applied through ∂ gives zero for each cycle c.

theorem GraphMaps.boundary_comp_secondBoundary_eq_zero {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] {C : Type u_2} [Fintype C] [DecidableEq C] (cycles : C → Set ↑G.edgeSet) [(c : C) → DecidablePred fun (x : ↑G.edgeSet) => x ∈ cycles c] [Fintype ↑G.edgeSet] (hcyc : ∀ (c : C) (v : V), Even {e : ↑G.edgeSet | e ∈ cycles c ∧ v ∈ ↑e}.card) : boundaryMap G ∘ₗ secondBoundaryMap G cycles = 0

Chain complex property: ∂ ∘ ∂₂ = 0, given that each cycle in the collection has the property that each vertex is incident to an even number of its edges.

theorem GraphMaps.range_secondBoundary_le_ker_boundary {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] {C : Type u_2} [Fintype C] [DecidableEq C] (cycles : C → Set ↑G.edgeSet) [(c : C) → DecidablePred fun (x : ↑G.edgeSet) => x ∈ cycles c] [Fintype ↑G.edgeSet] (hcyc : ∀ (c : C) (v : V), Even {e : ↑G.edgeSet | e ∈ cycles c ∧ v ∈ ↑e}.card) : (secondBoundaryMap G cycles).range ≤ (boundaryMap G).ker

im(∂₂) ≤ ker(∂).

Coboundary Chain Complex: δ₂ ∘ δ = 0

theorem GraphMaps.secondCoboundary_comp_coboundary_eq_zero {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] {C : Type u_2} [Fintype C] [DecidableEq C] (cycles : C → Set ↑G.edgeSet) [(c : C) → DecidablePred fun (x : ↑G.edgeSet) => x ∈ cycles c] [Fintype ↑G.edgeSet] (hcyc : ∀ (c : C) (v : V), Even {e : ↑G.edgeSet | e ∈ cycles c ∧ v ∈ ↑e}.card) : secondCoboundaryMap G cycles ∘ₗ coboundaryMap G = 0

Coboundary chain complex property: δ₂ ∘ δ = 0. By transposition from ∂ ∘ ∂₂ = 0.

theorem GraphMaps.range_coboundary_le_ker_secondCoboundary {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] {C : Type u_2} [Fintype C] [DecidableEq C] (cycles : C → Set ↑G.edgeSet) [(c : C) → DecidablePred fun (x : ↑G.edgeSet) => x ∈ cycles c] [Fintype ↑G.edgeSet] (hcyc : ∀ (c : C) (v : V), Even {e : ↑G.edgeSet | e ∈ cycles c ∧ v ∈ ↑e}.card) : (coboundaryMap G).range ≤ (secondCoboundaryMap G cycles).ker

im(δ) ≤ ker(δ₂).

Kernel of the Coboundary Map

def GraphMaps.allOnes {V : Type u_1} : V → ZMod 2

The all-ones function 1 : V → ZMod 2.

Equations

• GraphMaps.allOnes x✝ = 1

theorem GraphMaps.allOnes_mem_ker_coboundary {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [Fintype ↑G.edgeSet] : allOnes ∈ (coboundaryMap G).ker

The all-ones vector is in ker(δ).

theorem GraphMaps.constant_mem_ker_coboundary {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [Fintype ↑G.edgeSet] (a : ZMod 2) : (fun (x : V) => a) ∈ (coboundaryMap G).ker

Any constant function is in ker(δ).

theorem GraphMaps.ker_coboundary_constant_on_adj {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [Fintype ↑G.edgeSet] {f : V → ZMod 2} (hf : f ∈ (coboundaryMap G).ker) {a b : V} (hab : G.Adj a b) : f a = f b

f ∈ ker(δ) implies f(a) = f(b) for adjacent a, b.

theorem GraphMaps.ker_coboundary_constant_on_walk {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [Fintype ↑G.edgeSet] {f : V → ZMod 2} (hf : f ∈ (coboundaryMap G).ker) {u w : V} (p : G.Walk u w) : f u = f w

f ∈ ker(δ) implies f is constant along walks.

theorem GraphMaps.ker_coboundary_constant_on_reachable {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [Fintype ↑G.edgeSet] {f : V → ZMod 2} (hf : f ∈ (coboundaryMap G).ker) {u w : V} (hr : G.Reachable u w) : f u = f w

f ∈ ker(δ) implies f is constant on reachable vertices.

theorem GraphMaps.ker_coboundary_is_constant {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [Fintype ↑G.edgeSet] (hconn : G.Connected) {f : V → ZMod 2} (hf : f ∈ (coboundaryMap G).ker) : ∃ (a : ZMod 2), f = fun (x : V) => a

For a connected graph, f ∈ ker(δ) implies f is a constant function.

theorem GraphMaps.ker_coboundary_connected {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [Fintype ↑G.edgeSet] (hconn : G.Connected) (f : V → ZMod 2) : f ∈ (coboundaryMap G).ker ↔ f = 0 ∨ f = allOnes

For a connected graph, ker(δ) consists exactly of the constant functions {0, 1}.

theorem GraphMaps.ker_coboundary_ne_bot {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [Fintype ↑G.edgeSet] [Nonempty V] : (coboundaryMap G).ker ≠ ⊥

ker(δ) ≠ 0: the sequences are not short exact.

Corollaries

@[simp]

theorem GraphMaps.zero_mem_ker_coboundary {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [Fintype ↑G.edgeSet] : 0 ∈ (coboundaryMap G).ker

theorem GraphMaps.boundary_secondBoundary_apply {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] {C : Type u_2} [Fintype C] [DecidableEq C] (cycles : C → Set ↑G.edgeSet) [(c : C) → DecidablePred fun (x : ↑G.edgeSet) => x ∈ cycles c] [Fintype ↑G.edgeSet] (hcyc : ∀ (c : C) (v : V), Even {e : ↑G.edgeSet | e ∈ cycles c ∧ v ∈ ↑e}.card) (σ : C → ZMod 2) : (boundaryMap G) ((secondBoundaryMap G cycles) σ) = 0

For any σ, ∂(∂₂ σ) = 0.

theorem GraphMaps.secondCoboundary_coboundary_apply {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] {C : Type u_2} [Fintype C] [DecidableEq C] (cycles : C → Set ↑G.edgeSet) [(c : C) → DecidablePred fun (x : ↑G.edgeSet) => x ∈ cycles c] [Fintype ↑G.edgeSet] (hcyc : ∀ (c : C) (v : V), Even {e : ↑G.edgeSet | e ∈ cycles c ∧ v ∈ ↑e}.card) (f : V → ZMod 2) : (secondCoboundaryMap G cycles) ((coboundaryMap G) f) = 0

For any f, δ₂(δ f) = 0.