Definition 1: Boundary and Coboundary Maps

Statement

Let G = (V, E) be a graph. We define ZMod 2-linear maps:

1. Boundary map ∂ : Z₂^E → Z₂^V with (∂ γ)v = Σ{e ∋ v} γ_e (mod 2)
2. Coboundary map δ : Z₂^V → Z₂^E defined as the transpose δ = ∂^T
3. Second boundary map ∂₂ : Z₂^C → Z₂^E with ∂₂(c) = Σ_{e ∈ c} e
4. Second coboundary map δ₂ : Z₂^E → Z₂^C defined as the transpose δ₂ = ∂₂^T

Main Results

• boundaryMap : the boundary map ∂
• coboundaryMap : the coboundary map δ
• coboundaryMap_eq_transpose : δ is the transpose of ∂
• secondBoundaryMap : the second boundary map ∂₂
• secondCoboundaryMap : the second coboundary map δ₂
• secondCoboundaryMap_eq_transpose : δ₂ is the transpose of ∂₂

Boundary Map

noncomputable def GraphMaps.boundaryMap {V : Type u_1} [DecidableEq V] (G : SimpleGraph V) [Fintype ↑G.edgeSet] : (↑G.edgeSet → ZMod 2) →ₗ[ZMod 2] V → ZMod 2

The boundary map ∂ : Z₂^E → Z₂^V. For γ ∈ Z₂^E, (∂ γ)v = Σ{e ∋ v} γ_e (mod 2).

Equations

• GraphMaps.boundaryMap G = { toFun := fun (γ : ↑G.edgeSet → ZMod 2) (v : V) => ∑ e : ↑G.edgeSet, if v ∈ ↑e then γ e else 0, map_add' := ⋯, map_smul' := ⋯ }

Coboundary Map

noncomputable def GraphMaps.coboundaryMap {V : Type u_1} (G : SimpleGraph V) [Fintype ↑G.edgeSet] : (V → ZMod 2) →ₗ[ZMod 2] ↑G.edgeSet → ZMod 2

The coboundary map δ : Z₂^V → Z₂^E. For f ∈ Z₂^V and edge e = {a,b}, (δ f)_e = f(a) + f(b) (mod 2).

Equations

• GraphMaps.coboundaryMap G = { toFun := fun (f : V → ZMod 2) (e : ↑G.edgeSet) => Sym2.lift ⟨fun (a b : V) => f a + f b, ⋯⟩ ↑e, map_add' := ⋯, map_smul' := ⋯ }

Transpose Properties

theorem GraphMaps.coboundaryMap_eq_transpose {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [Fintype ↑G.edgeSet] (f : V → ZMod 2) (γ : ↑G.edgeSet → ZMod 2) : ∑ e : ↑G.edgeSet, (coboundaryMap G) f e * γ e = ∑ v : V, f v * (boundaryMap G) γ v

δ is the transpose of ∂: ⟨δ f, γ⟩_E = ⟨f, ∂ γ⟩_V for the standard Z₂ inner product.

Second Boundary and Coboundary Maps

noncomputable def GraphMaps.secondBoundaryMap {V : Type u_1} (G : SimpleGraph V) {C : Type u_2} [Fintype C] (cycles : C → Set ↑G.edgeSet) [(c : C) → DecidablePred fun (x : ↑G.edgeSet) => x ∈ cycles c] [Fintype ↑G.edgeSet] : (C → ZMod 2) →ₗ[ZMod 2] ↑G.edgeSet → ZMod 2

The second boundary map ∂₂ : Z₂^C → Z₂^E. For σ ∈ Z₂^C, (∂₂ σ)e = Σ{c ∋ e} σ_c (mod 2).

Equations

• GraphMaps.secondBoundaryMap G cycles = { toFun := fun (σ : C → ZMod 2) (e : ↑G.edgeSet) => ∑ c : C, if e ∈ cycles c then σ c else 0, map_add' := ⋯, map_smul' := ⋯ }

noncomputable def GraphMaps.secondCoboundaryMap {V : Type u_1} (G : SimpleGraph V) {C : Type u_2} (cycles : C → Set ↑G.edgeSet) [(c : C) → DecidablePred fun (x : ↑G.edgeSet) => x ∈ cycles c] [Fintype ↑G.edgeSet] : (↑G.edgeSet → ZMod 2) →ₗ[ZMod 2] C → ZMod 2

The second coboundary map δ₂ : Z₂^E → Z₂^C. For γ ∈ Z₂^E, (δ₂ γ)c = Σ{e ∈ c} γ_e (mod 2).

Equations

• GraphMaps.secondCoboundaryMap G cycles = { toFun := fun (γ : ↑G.edgeSet → ZMod 2) (c : C) => ∑ e : ↑G.edgeSet, if e ∈ cycles c then γ e else 0, map_add' := ⋯, map_smul' := ⋯ }

theorem GraphMaps.secondCoboundaryMap_eq_transpose {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] (γ : ↑G.edgeSet → ZMod 2) (σ : C → ZMod 2) : ∑ c : C, (secondCoboundaryMap G cycles) γ c * σ c = ∑ e : ↑G.edgeSet, γ e * (secondBoundaryMap G cycles) σ e

δ₂ is the transpose of ∂₂: ⟨δ₂ γ, σ⟩_C = ⟨γ, ∂₂ σ⟩_E.

Evaluation Lemmas

@[simp]

theorem GraphMaps.boundaryMap_apply {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [Fintype ↑G.edgeSet] (γ : ↑G.edgeSet → ZMod 2) (v : V) : (boundaryMap G) γ v = ∑ e : ↑G.edgeSet, if v ∈ ↑e then γ e else 0

@[simp]

theorem GraphMaps.coboundaryMap_apply {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [Fintype ↑G.edgeSet] (f : V → ZMod 2) (e : ↑G.edgeSet) : (coboundaryMap G) f e = Sym2.lift ⟨fun (a b : V) => f a + f b, ⋯⟩ ↑e

@[simp]

theorem GraphMaps.secondBoundaryMap_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] (σ : C → ZMod 2) (e : ↑G.edgeSet) : (secondBoundaryMap G cycles) σ e = ∑ c : C, if e ∈ cycles c then σ c else 0

@[simp]

theorem GraphMaps.secondCoboundaryMap_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] (γ : ↑G.edgeSet → ZMod 2) (c : C) : (secondCoboundaryMap G cycles) γ c = ∑ e : ↑G.edgeSet, if e ∈ cycles c then γ e else 0

Basis Vector Evaluation

theorem GraphMaps.boundaryMap_single {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [Fintype ↑G.edgeSet] (e : ↑G.edgeSet) (v : V) : (boundaryMap G) (Pi.single e 1) v = if v ∈ ↑e then 1 else 0

The boundary of a single-edge indicator: (∂ 1_e)(v) = 1 iff v is an endpoint of e.

theorem GraphMaps.coboundaryMap_single {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [Fintype ↑G.edgeSet] (v : V) (e : ↑G.edgeSet) : (coboundaryMap G) (Pi.single v 1) e = if v ∈ ↑e then 1 else 0

The coboundary of a single-vertex indicator: (δ 1_v)(e) = 1 iff v ∈ e.

theorem GraphMaps.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] (c : C) (e : ↑G.edgeSet) : (secondBoundaryMap G cycles) (Pi.single c 1) e = if e ∈ cycles c then 1 else 0

∂₂ on a single cycle c: (∂₂ 1_c)(e) = 1 iff e ∈ c.

theorem GraphMaps.secondCoboundaryMap_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] (e : ↑G.edgeSet) (c : C) : (secondCoboundaryMap G cycles) (Pi.single e 1) c = if e ∈ cycles c then 1 else 0

δ₂ on a single edge e: (δ₂ 1_e)(c) = 1 iff e ∈ c.

Zero Properties

@[simp]

theorem GraphMaps.boundaryMap_zero {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [Fintype ↑G.edgeSet] (v : V) : (boundaryMap G) 0 v = 0

@[simp]

theorem GraphMaps.coboundaryMap_zero {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [Fintype ↑G.edgeSet] (e : ↑G.edgeSet) : (coboundaryMap G) 0 e = 0

@[simp]

theorem GraphMaps.secondBoundaryMap_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] (e : ↑G.edgeSet) : (secondBoundaryMap G cycles) 0 e = 0

@[simp]

theorem GraphMaps.secondCoboundaryMap_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] (c : C) : (secondCoboundaryMap G cycles) 0 c = 0