The first cohomology of a simple graph

A simple graph is a one-dimensional cell complex, with its vertices as 0-cells and its edges as 1-cells. With coefficients in a commutative group A, written multiplicatively, a 1-cochain is therefore a function on the darts (oriented edges) which is inverted by reversing a dart, the coboundary of a function φ on the vertices is the 1-cochain d ↦ φ d.snd / φ d.fst, and, since there are no 2-cells, every 1-cochain is a cocycle. The first cohomology H¹(G, A) is the group of 1-cochains modulo coboundaries.

This is the group in which Couture's classification of skew-zigzag algebras takes its values, with A = kˣ the units of the coefficient ring.

Main definitions

• SimpleGraph.oneCochains: the group of A-valued 1-cochains of a simple graph.
• SimpleGraph.coboundary: the coboundary of a function on the vertices.
• SimpleGraph.FirstCohomology: the first cohomology group H¹(G, A).
• SimpleGraph.FirstCohomology.mk: the cohomology class of a 1-cochain.
• SimpleGraph.FirstCohomology.lift: the universal property of first cohomology.

Main results

• SimpleGraph.FirstCohomology.mk_surjective: every cohomology class is the class of a cochain.
• SimpleGraph.FirstCohomology.mk_eq_one_iff: a cochain has trivial class exactly when it is a coboundary.
• SimpleGraph.FirstCohomology.mk_eq_mk_iff: two cochains have the same class exactly when they differ by a coboundary.

References

C. Couture, Skew-Zigzag Algebras, Section 4, https://arxiv.org/abs/1509.08405, for the first cohomology of a graph with coefficients in the units of a field.

def SimpleGraph.oneCochains {V : Type u_1} (G : SimpleGraph V) (A : Type u_2) [CommGroup A] : Subgroup (G.Dart → A)

The group of A-valued 1-cochains of a simple graph: the functions on its darts which are inverted by reversing a dart.

Equations

• G.oneCochains A = { carrier := {σ : G.Dart → A | ∀ (d : G.Dart), σ d.symm = (σ d)⁻¹}, mul_mem' := ⋯, one_mem' := ⋯, inv_mem' := ⋯ }

theorem SimpleGraph.mem_oneCochains_iff {V : Type u_1} {G : SimpleGraph V} {A : Type u_2} [CommGroup A] {σ : G.Dart → A} : σ ∈ G.oneCochains A ↔ ∀ (d : G.Dart), σ d.symm = (σ d)⁻¹

A function on the darts is a 1-cochain exactly when reversing a dart inverts its value.

@[simp]

theorem SimpleGraph.oneCochains_apply_symm {V : Type u_1} {G : SimpleGraph V} {A : Type u_2} [CommGroup A] (σ : ↥(G.oneCochains A)) (d : G.Dart) : ↑σ d.symm = (↑σ d)⁻¹

The value of a 1-cochain on a reversed dart is the inverse of its value on the dart.

def SimpleGraph.coboundary {V : Type u_1} (G : SimpleGraph V) (A : Type u_2) [CommGroup A] : (V → A) →* ↥(G.oneCochains A)

The coboundary of a function φ on the vertices of a simple graph: the 1-cochain whose value on a dart is the value of φ at its target divided by the value at its source.

Equations

• G.coboundary A = { toFun := fun (φ : V → A) => ⟨fun (d : G.Dart) => φ d.toProd.2 / φ d.toProd.1, ⋯⟩, map_one' := ⋯, map_mul' := ⋯ }

@[simp]

theorem SimpleGraph.coboundary_apply {V : Type u_1} {G : SimpleGraph V} {A : Type u_2} [CommGroup A] (φ : V → A) (d : G.Dart) : ↑((G.coboundary A) φ) d = φ d.toProd.2 / φ d.toProd.1

The value of a coboundary on a dart is the quotient of the values at its target and source.

def SimpleGraph.FirstCohomology {V : Type u_1} (G : SimpleGraph V) (A : Type u_2) [CommGroup A] : Type (max u_1 u_2)

The first cohomology H¹(G, A) of a simple graph with coefficients in a commutative group: its 1-cochains modulo the coboundaries of functions on its vertices.

Equations

• G.FirstCohomology A = (↥(G.oneCochains A) ⧸ (G.coboundary A).range)

@[instance_reducible]

instance SimpleGraph.FirstCohomology.instCommGroup {V : Type u_1} (G : SimpleGraph V) (A : Type u_2) [CommGroup A] : CommGroup (G.FirstCohomology A)

Equations

• One or more equations did not get rendered due to their size.

def SimpleGraph.FirstCohomology.mk {V : Type u_1} (G : SimpleGraph V) (A : Type u_2) [CommGroup A] : ↥(G.oneCochains A) →* G.FirstCohomology A

The cohomology class of a 1-cochain.

Equations

• SimpleGraph.FirstCohomology.mk G A = QuotientGroup.mk' (G.coboundary A).range

theorem SimpleGraph.FirstCohomology.mk_surjective {V : Type u_1} {G : SimpleGraph V} {A : Type u_2} [CommGroup A] : Function.Surjective ⇑(mk G A)

Every cohomology class is the class of a 1-cochain.

def SimpleGraph.FirstCohomology.lift {V : Type u_1} {G : SimpleGraph V} {A : Type u_2} [CommGroup A] {M : Type u_3} [Monoid M] (f : ↥(G.oneCochains A) →* M) (h : (G.coboundary A).range ≤ f.ker) : G.FirstCohomology A →* M

Universal property of first cohomology. A homomorphism from 1-cochains which is trivial on coboundaries descends to a homomorphism from H¹(G, A).

Equations

• SimpleGraph.FirstCohomology.lift f h = QuotientGroup.lift (G.coboundary A).range f h

@[simp]

theorem SimpleGraph.FirstCohomology.lift_mk {V : Type u_1} {G : SimpleGraph V} {A : Type u_2} [CommGroup A] {M : Type u_3} [Monoid M] (f : ↥(G.oneCochains A) →* M) (h : (G.coboundary A).range ≤ f.ker) (c : ↥(G.oneCochains A)) : (lift f h) ((mk G A) c) = f c

The descended homomorphism agrees with the original homomorphism on cohomology classes.

theorem SimpleGraph.FirstCohomology.lift_unique {V : Type u_1} {G : SimpleGraph V} {A : Type u_2} [CommGroup A] {M : Type u_3} [Monoid M] (f : ↥(G.oneCochains A) →* M) (h : (G.coboundary A).range ≤ f.ker) (g : G.FirstCohomology A →* M) (hg : ∀ (c : ↥(G.oneCochains A)), g ((mk G A) c) = f c) : g = lift f h

The lift is the unique homomorphism from H¹(G, A) agreeing with the original homomorphism on cohomology classes.

theorem SimpleGraph.FirstCohomology.mk_eq_one_iff {V : Type u_1} {G : SimpleGraph V} {A : Type u_2} [CommGroup A] {σ : ↥(G.oneCochains A)} : (mk G A) σ = 1 ↔ ∃ (φ : V → A), (G.coboundary A) φ = σ

A 1-cochain has trivial cohomology class exactly when it is a coboundary.

@[simp]

theorem SimpleGraph.FirstCohomology.mk_coboundary {V : Type u_1} {G : SimpleGraph V} {A : Type u_2} [CommGroup A] (φ : V → A) : (mk G A) ((G.coboundary A) φ) = 1

The cohomology class of a coboundary is trivial.

theorem SimpleGraph.FirstCohomology.mk_eq_mk_iff {V : Type u_1} {G : SimpleGraph V} {A : Type u_2} [CommGroup A] {σ τ : ↥(G.oneCochains A)} : (mk G A) σ = (mk G A) τ ↔ ∃ (φ : V → A), τ = σ * (G.coboundary A) φ

Two 1-cochains have the same cohomology class exactly when they differ by a coboundary.

@[simp]

theorem SimpleGraph.FirstCohomology.ker_mk {V : Type u_1} {G : SimpleGraph V} {A : Type u_2} [CommGroup A] : (mk G A).ker = (G.coboundary A).range

The kernel of the cohomology class map consists of the coboundaries.

def SimpleGraph.FirstCohomology.congr {V : Type u_1} {G : SimpleGraph V} {A : Type u_2} [CommGroup A] {W : Type u_4} {H : SimpleGraph W} (e : ↥(G.oneCochains A) ≃* ↥(H.oneCochains A)) (he : Subgroup.map (↑e) (G.coboundary A).range = (H.coboundary A).range) : G.FirstCohomology A ≃* H.FirstCohomology A

An equivalence of one-cochain groups preserving coboundaries induces an equivalence of first cohomology groups.

Equations

• SimpleGraph.FirstCohomology.congr e he = QuotientGroup.congr (G.coboundary A).range (H.coboundary A).range e he

@[simp]

theorem SimpleGraph.FirstCohomology.congr_mk {V : Type u_1} {G : SimpleGraph V} {A : Type u_2} [CommGroup A] {W : Type u_4} {H : SimpleGraph W} (e : ↥(G.oneCochains A) ≃* ↥(H.oneCochains A)) (he : Subgroup.map (↑e) (G.coboundary A).range = (H.coboundary A).range) (σ : ↥(G.oneCochains A)) : (congr e he) ((mk G A) σ) = (mk H A) (e σ)

The induced equivalence sends the class of a cochain to the class of its image.