Even graphs are edge-disjoint unions of cycles

Source: url:https://github.com/jtraverso/erdos-81-chordal-clique-partitions/blob/b3423f3e8c8db7c2d1b279673293ef3079faf903/preprints/PAPER_III/05_formalization/lean_v1.4_freeze/Contrib/EvenGraphCycles.lean Authors: Juan Pablo Traverso Gianini, Aristotle Status: verified Main declarations: Finset.exists_cycleDecomp, Finset.exists_edge_pairing_of_even Tags: graph-theory, eulerian-graphs, cycle-decompositions MSC: 05C45

Even graphs are edge-disjoint unions of cycles

A finite graph, encoded as a finite set of edges E : Finset (Sym2 V), all of whose degrees are even is the edge-disjoint union of cycles. As a consequence the edges at each vertex can be paired up, simultaneously at every vertex ("Eulerian pairing").

Main results

• Finset.exists_cycleDecomp: theorem Finset.exists_cycleDecomp {V : Type*} [DecidableEq V] {E : Finset (Sym2 V)} (hdiag : ∀ e ∈ E, ¬ e.IsDiag) (heven : ∀ v : V, Even (E.cycleEdgeDegree v)) : ∃ cs : List (List V), (∀ c ∈ cs, c.Nodup ∧ 3 ≤ c.length) ∧ (cs.flatMap List.cycleEdges).Nodup ∧ (cs.flatMap List.cycleEdges).toFinset = E
• Finset.exists_edge_pairing_of_even: theorem Finset.exists_edge_pairing_of_even {V : Type*} [DecidableEq V] {E : Finset (Sym2 V)} (heven : ∀ v : V, Even (E.cycleEdgeDegree v)) : ∃ pair : V → Sym2 V → Sym2 V, ∀ v : V, ∀ e ∈ E, v ∈ e → pair v e ∈ E ∧ v ∈ pair v e ∧ pair v e ≠ e ∧ pair v (pair v e) = e

Along the way we prove Finset.exists_cycle_of_even (a nonempty loopless even graph contains a cycle), Finset.exists_cycleDecomp_finset (the decomposition stated as a pairwise disjoint family of edge sets) and Finset.exists_involution_of_even_card (a finite set of even size carries a fixed-point-free involution).

Implementation notes

Graphs are encoded as finite sets of edges E : Finset (Sym2 V); E.cycleEdgeDegree v is the number of edges of E incident with v. A cycle is encoded by a list l : List V of pairwise distinct vertices with 3 ≤ l.length, its edge list being l.cycleEdges, the list of pairs of cyclically consecutive entries of l.

The cycle decomposition is proved by strong induction on the edge set: a nonempty even graph has minimum positive degree at least two, so a path of maximal length closes up into a cycle (Finset.exists_cycle_of_even); removing the edges of that cycle keeps all degrees even (List.even_edgeDegree_cycleEdges), and one recurses.

Main definitions

• List.pathEdges, List.cycleEdges: the edges of a walk, resp. of a closed walk, given as a list of vertices;
• Finset.cycleEdgeDegree: the degree of a vertex in a finite edge set;
• Finset.edgeSupport: the set of vertices incident with an edge of a finite edge set.

def List.pathEdges {V : Type u_1} : List V → List (Sym2 V)

The list of edges of the walk l: the pairs of consecutive vertices of l.

Equations

• [].pathEdges = []
• [head].pathEdges = []
• (a :: b :: l).pathEdges = s(a, b) :: (b :: l).pathEdges

def List.cycleEdges {V : Type u_1} (l : List V) : List (Sym2 V)

The list of edges of the closed walk l: the pairs of cyclically consecutive vertices of l.

Equations

• l.cycleEdges = (l ++ List.take 1 l).pathEdges

@[simp]

theorem List.pathEdges_nil {V : Type u_1} : [].pathEdges = []

The empty walk has no edges.

@[simp]

theorem List.pathEdges_singleton {V : Type u_1} (a : V) : [a].pathEdges = []

A one-vertex walk has no edges.

@[simp]

theorem List.pathEdges_cons_cons {V : Type u_1} (a b : V) (l : List V) : (a :: b :: l).pathEdges = s(a, b) :: (b :: l).pathEdges

The edges of the walk a :: b :: l are s(a, b) together with the edges of b :: l.

theorem List.length_pathEdges {V : Type u_1} (l : List V) : l.pathEdges.length = l.length - 1

A walk on n vertices has n - 1 edges.

theorem List.length_cycleEdges {V : Type u_1} (l : List V) : l.cycleEdges.length = l.length

A closed walk on n vertices has n edges.

theorem List.getD_take {V : Type u_1} (l : List V) (d : V) {k i : ℕ} (h : i < k) : (take k l).getD i d = l.getD i d

Taking an initial segment of a list does not change its entries in that segment.

theorem List.pathEdges_getD {V : Type u_1} (d : Sym2 V) (e : V) (l : List V) (i : ℕ) : i + 1 < l.length → l.pathEdges.getD i d = s(l.getD i e, l.getD (i + 1) e)

The i-th edge of a walk joins its i-th and its (i + 1)-st vertex.

theorem List.cycleEdges_getD {V : Type u_1} (d : Sym2 V) (e : V) (l : List V) (i : ℕ) (hi : i < l.length) : l.cycleEdges.getD i d = s(l.getD i e, l.getD ((i + 1) % l.length) e)

The i-th edge of a closed walk joins its i-th and its (i + 1)-st vertex, cyclically.

theorem List.mem_pathEdges_iff {V : Type u_1} (d : V) (l : List V) (e : Sym2 V) : e ∈ l.pathEdges ↔ ∃ (i : ℕ), i + 1 < l.length ∧ e = s(l.getD i d, l.getD (i + 1) d)

The edges of a walk are exactly the pairs of consecutive vertices.

theorem List.mem_cycleEdges_iff {V : Type u_1} (d : V) (l : List V) (e : Sym2 V) : e ∈ l.cycleEdges ↔ ∃ i < l.length, e = s(l.getD i d, l.getD ((i + 1) % l.length) d)

The edges of a closed walk are exactly the pairs of cyclically consecutive vertices.

theorem List.mem_of_mem_cycleEdges {V : Type u_1} {l : List V} {e : Sym2 V} (he : e ∈ l.cycleEdges) {x : V} (hx : x ∈ e) : x ∈ l

An endpoint of an edge of a closed walk is a vertex of that walk.

theorem List.nodup_cycleEdges {V : Type u_1} {l : List V} (hnd : l.Nodup) (hlen : 3 ≤ l.length) : l.cycleEdges.Nodup

The edges of a cycle are pairwise distinct.

theorem List.not_isDiag_of_mem_cycleEdges {V : Type u_1} {l : List V} (hnd : l.Nodup) (hlen : 2 ≤ l.length) {e : Sym2 V} (he : e ∈ l.cycleEdges) : ¬e.IsDiag

A cycle has no loops.

def Finset.cycleEdgeDegree {V : Type u_1} [DecidableEq V] (E : Finset (Sym2 V)) (v : V) : ℕ

The number of edges of E incident with v.

The project-specific name avoids colliding with analogous definitions in other pooled projects.

Equations

• E.cycleEdgeDegree v = {e ∈ E | v ∈ e}.card

theorem Finset.cycleEdgeDegree_edgeFinset {V : Type u_1} [DecidableEq V] {G : SimpleGraph V} [Fintype ↑G.edgeSet] (v : V) [Fintype ↑(G.neighborSet v)] : G.edgeFinset.cycleEdgeDegree v = G.degree v

The raw-edge degree agrees with SimpleGraph.degree on a graph's edge finset.

def Finset.edgeSupport {V : Type u_1} [DecidableEq V] (E : Finset (Sym2 V)) : Finset V

The set of vertices incident with an edge of the finite edge set E.

Equations

• E.edgeSupport = E.biUnion Sym2.toFinset

theorem Finset.mem_edgeSupport {V : Type u_1} [DecidableEq V] {E : Finset (Sym2 V)} {v : V} : v ∈ E.edgeSupport ↔ ∃ e ∈ E, v ∈ e

A vertex lies in the support of E if and only if it is incident with an edge of E.

theorem Finset.edgeDegree_mono {V : Type u_1} [DecidableEq V] {E F : Finset (Sym2 V)} (h : E ⊆ F) (v : V) : E.cycleEdgeDegree v ≤ F.cycleEdgeDegree v

Degrees are monotone in the edge set.

theorem Finset.edgeDegree_sdiff {V : Type u_1} [DecidableEq V] {E A : Finset (Sym2 V)} (h : A ⊆ E) (v : V) : (E \ A).cycleEdgeDegree v = E.cycleEdgeDegree v - A.cycleEdgeDegree v

Deleting a set of edges subtracts its degrees.

The degrees of a cycle

theorem Finset.even_edgeDegree_cycleEdges {V : Type u_1} [DecidableEq V] {l : List V} (hnd : l.Nodup) (hlen : 3 ≤ l.length) (v : V) : Even (l.cycleEdges.toFinset.cycleEdgeDegree v)

Every degree of a cycle is even (in fact 0 or 2).

A nonempty even graph contains a cycle

theorem Finset.exists_cycle_of_even {V : Type u_1} [DecidableEq V] {E : Finset (Sym2 V)} (hne : E.Nonempty) (hdiag : ∀ e ∈ E, ¬e.IsDiag) (heven : ∀ (v : V), Even (E.cycleEdgeDegree v)) : ∃ (l : List V), l.Nodup ∧ 3 ≤ l.length ∧ ∀ e ∈ l.cycleEdges, e ∈ E

Every nonempty loopless graph with all degrees even contains a cycle. The cycle is found at the end of a path of maximal length.

The cycle decomposition

theorem Finset.exists_cycleDecomp {V : Type u_1} [DecidableEq V] {E : Finset (Sym2 V)} (hdiag : ∀ e ∈ E, ¬e.IsDiag) (heven : ∀ (v : V), Even (E.cycleEdgeDegree v)) : ∃ (cs : List (List V)), (∀ c ∈ cs, c.Nodup ∧ 3 ≤ c.length) ∧ (List.flatMap List.cycleEdges cs).Nodup ∧ (List.flatMap List.cycleEdges cs).toFinset = E

Every finite loopless graph with all degrees even is the edge-disjoint union of cycles.

The cycles are given as a list cs of lists of pairwise distinct vertices, each of length at least three; their edge lists concatenate, without repetition, to the edge set E.

theorem Finset.exists_cycleDecomp_finset {V : Type u_1} [DecidableEq V] {E : Finset (Sym2 V)} (hdiag : ∀ e ∈ E, ¬e.IsDiag) (heven : ∀ (v : V), Even (E.cycleEdgeDegree v)) : ∃ (Cs : List (Finset (Sym2 V))), (∀ C ∈ Cs, ∃ (l : List V), l.Nodup ∧ 3 ≤ l.length ∧ C = l.cycleEdges.toFinset) ∧ List.Pairwise Disjoint Cs ∧ ∀ (e : Sym2 V), e ∈ E ↔ ∃ C ∈ Cs, e ∈ C

Every finite loopless graph with all degrees even decomposes into edge-disjoint cycles, stated as a family of edge sets: the cycles are given as a list Cs of edge sets, each of them the edge set l.cycleEdges of a cycle l (a list of pairwise distinct vertices of length at least three); they are pairwise disjoint and their union is E.

Pairing up a set of even size

theorem Finset.exists_involution_of_even_card {α : Type u_2} {S : Finset α} (hev : Even S.card) : ∃ (f : α → α), ∀ a ∈ S, f a ∈ S ∧ f a ≠ a ∧ f (f a) = a

Every finite set of even size carries a fixed-point-free involution.

The Eulerian pairing

theorem Finset.exists_edge_pairing_of_even {V : Type u_1} [DecidableEq V] {E : Finset (Sym2 V)} (heven : ∀ (v : V), Even (E.cycleEdgeDegree v)) : ∃ (pair : V → Sym2 V → Sym2 V), ∀ (v : V), ∀ e ∈ E, v ∈ e → pair v e ∈ E ∧ v ∈ pair v e ∧ pair v e ≠ e ∧ pair v (pair v e) = e

The Eulerian pairing. If every degree of E is even then the edges of E at every vertex v can be paired up: pair v is a fixed-point-free involution of the set of edges of E incident with v. The pairing is defined at every vertex simultaneously, so each edge xy of E is paired with an edge at x and with an edge at y.

theorem SimpleGraph.exists_cycleDecomp_of_even_degree {V : Type u_1} [DecidableEq V] (G : SimpleGraph V) [Fintype ↑G.edgeSet] [(v : V) → Fintype ↑(G.neighborSet v)] (heven : ∀ (v : V), Even (G.degree v)) : ∃ (cs : List (List V)), (∀ c ∈ cs, c.Nodup ∧ 3 ≤ c.length) ∧ (List.flatMap List.cycleEdges cs).Nodup ∧ (List.flatMap List.cycleEdges cs).toFinset = G.edgeFinset

A finite simple graph of even degree decomposes into edge-disjoint simple cycles.

theorem SimpleGraph.exists_edge_pairing_of_even_degree {V : Type u_1} (G : SimpleGraph V) [Fintype ↑G.edgeSet] [(v : V) → Fintype ↑(G.neighborSet v)] (heven : ∀ (v : V), Even (G.degree v)) : ∃ (pair : V → Sym2 V → Sym2 V), ∀ (v : V), ∀ e ∈ G.edgeFinset, v ∈ e → pair v e ∈ G.edgeFinset ∧ v ∈ pair v e ∧ pair v e ≠ e ∧ pair v (pair v e) = e

The incident edges of a finite simple graph of even degree admit Eulerian pairings.