Cycles through prescribed vertices

This file proves Dirac's theorem on cycles through prescribed vertices: for k ≥ 2, every set of at most k vertices of a k-vertex-connected simple graph on a finite vertex type lies on a common cycle. No cyclic order of the prescribed vertices is imposed.

Main results

• SimpleGraph.Walk.IsCycle.exists_isCycle_forall_mem_support_insert: for 2 ≤ k, a cycle through a set T of fewer than k vertices can be replaced by a cycle through T and any vertex that is k-vertex-reachable from every vertex of the cycle.
• SimpleGraph.IsVertexConnected.exists_isCycle_forall_mem_support: Dirac's theorem.

Implementation notes

Given a cycle C through T and a vertex x off C, the fan lemma SimpleGraph.exists_fan_of_forall_isVertexReachable joins x to min k |C| distinct vertices of C by paths meeting only at x and avoiding C otherwise. These ends cut C into as many arcs, which outnumber the vertices of T not among the ends, so the interior of some arc between two consecutive ends avoids T. Replacing that arc by the two fan paths to its ends gives the new cycle. The arc is found by scanning the cycle, rotated to start at an end, for consecutive ends. The path and cycle surgery used here is in TauCeti.Combinatorics.SimpleGraph.Paths.

References

• G. A. Dirac, In abstrakten Graphen vorhandene vollständige 4-Graphen und ihre Unterteilungen, Math. Nachr. 22 (1960), 61–85.
• J. A. Bondy and U. S. R. Murty, Graph Theory, Graduate Texts in Mathematics 244, Springer, 2008, Chapter 9.

theorem SimpleGraph.Walk.IsCycle.exists_isCycle_forall_mem_support_insert {V : Type u} {G : SimpleGraph V} [Finite V] [DecidableEq V] {k : ℕ} {r x : V} {c : G.Walk r r} (hc : c.IsCycle) (hk : 2 ≤ k) (h : ∀ y ∈ c.support, G.IsVertexReachable (↑k) x y) {T : Finset V} (hT : ∀ v ∈ T, v ∈ c.support) (hTk : T.card < k) : ∃ (u : V) (c' : G.Walk u u), c'.IsCycle ∧ ∀ v ∈ insert x T, v ∈ c'.support

Let c be a cycle in a simple graph on a finite vertex type, through a set T of fewer than k of its vertices, where 2 ≤ k. If a vertex x is k-vertex-reachable from every vertex of c, then x lies on a cycle through all of T.

theorem SimpleGraph.IsVertexConnected.exists_isCycle_forall_mem_support {V : Type u} {G : SimpleGraph V} [Finite V] {k : ℕ} (hk : 2 ≤ k) (h : G.IsVertexConnected ↑k) {S : Finset V} (hS : S.card ≤ k) : ∃ (u : V) (c : G.Walk u u), c.IsCycle ∧ ∀ v ∈ S, v ∈ c.support

Dirac's theorem. For 2 ≤ k, every set of at most k vertices of a k-vertex-connected simple graph on a finite vertex type lies on a common cycle.