Cutting and closing up paths and cycles

This file collects general facts about paths and cycles in a simple graph, complementing Mathlib's Mathlib/Combinatorics/SimpleGraph/Paths.lean.

Main results

• SimpleGraph.Walk.IsPath.start_notMem_tail_support: a path does not return to its start.
• SimpleGraph.Walk.IsPath.exists_support_eq_cons_append: the support of a path between distinct endpoints splits as a :: (I ++ [b]) with duplicate-free internal vertices and adjacent predecessor and successor sublists.
• SimpleGraph.Walk.IsCycle.isPath_append_of_append_append: cutting an arc of positive length out of a cycle leaves a path.
• SimpleGraph.Walk.mem_support_append_of_mem_support_append_append: the vertices of a closed walk outside the interior of such an arc lie on the remaining path.
• SimpleGraph.Walk.IsPath.isCycle_append_append_reverse: two paths from a common vertex close up with a third path into a cycle.
• SimpleGraph.Walk.IsPath.isCycle_cons_append_cons_reverse: two vertex-disjoint paths joined at both ends by distinct edges form a cycle.
• SimpleGraph.Walk.exists_eq_append_of_exists_mem_support: a walk meeting a finset splits at its first vertex in it.
• SimpleGraph.Walk.exists_eq_append_append_of_countP_lt: a walk starting in F with fewer vertices of T \ F than of F has an arc between consecutive vertices of F whose interior avoids T.
• SimpleGraph.Walk.IsCycle.exists_eq_append_append: a cycle with fewer vertices of T outside F than in F has an arc between two distinct vertices of F whose interior avoids T.
• SimpleGraph.exists_isPath_notMem_support_iff: every walk avoiding one vertex can be shortened to a path avoiding it.

theorem SimpleGraph.Walk.IsPath.start_notMem_tail_support {V : Type u} {G : SimpleGraph V} {u v : V} {p : G.Walk u v} (hp : p.IsPath) : u ∉ p.support.tail

A path does not return to its start.

theorem SimpleGraph.Walk.IsPath.exists_support_eq_cons_append {V : Type u} {G : SimpleGraph V} {a b : V} {R : G.Walk a b} (hR : R.IsPath) (hab : a ≠ b) : ∃ (I : List V), R.support = a :: (I ++ [b]) ∧ I.Nodup ∧ (∀ v ∈ I, v ≠ a ∧ v ≠ b) ∧ ∀ v ∈ I, (∃ (u : V), G.Adj u v ∧ [u, v].Sublist R.support) ∧ ∃ (w : V), G.Adj v w ∧ [v, w].Sublist R.support

Decompose the support of a path R : G.Walk a b between distinct endpoints a ≠ b as a :: (I ++ [b]), where the internal-vertex list I is duplicate-free, contains neither endpoint, and gives every vertex in I both an adjacent predecessor and an adjacent successor in R.support.

theorem SimpleGraph.Walk.IsCycle.isPath_append_of_append_append {V : Type u} {G : SimpleGraph V} {u a b : V} {W₁ : G.Walk u a} {A : G.Walk a b} {W₂ : G.Walk b u} (hc : (W₁.append (A.append W₂)).IsCycle) (hA : ¬A.Nil) : (W₂.append W₁).IsPath

Removing a subwalk of positive length from a cycle leaves a path: if W₁, A, W₂ traverse a cycle in turn and A is not trivial, then W₂ followed by W₁ is a path.

theorem SimpleGraph.Walk.mem_support_append_of_mem_support_append_append {V : Type u} {G : SimpleGraph V} {u a b v : V} {W₁ : G.Walk u a} {A : G.Walk a b} {W₂ : G.Walk b u} (hv : v ∈ (W₁.append (A.append W₂)).support) (hA : v ∈ A.support → v = a ∨ v = b) : v ∈ (W₂.append W₁).support

If W₁, A, W₂ traverse a closed walk in turn, then every vertex of it that is not an interior vertex of A lies on W₂ followed by W₁.

theorem SimpleGraph.Walk.IsPath.isCycle_append_append_reverse {V : Type u} {G : SimpleGraph V} {x a b : V} {P : G.Walk x a} {Q : G.Walk x b} {R : G.Walk b a} (hP : P.IsPath) (hQ : Q.IsPath) (hR : R.IsPath) (hab : a ≠ b) (hPQ : ∀ v ∈ P.support, v ∈ Q.support → v = x) (hPR : ∀ v ∈ P.support, v ∈ R.support → v = a) (hQR : ∀ v ∈ Q.support, v ∈ R.support → v = b) : ((Q.append R).append P.reverse).IsCycle

Two paths P and Q from x to distinct vertices a and b, sharing only x, close up with a path R from b to a meeting them only at a and b into a cycle.

theorem SimpleGraph.Walk.IsPath.isCycle_cons_append_cons_reverse {V : Type u} {G : SimpleGraph V} {x x' y y' : V} {P : G.Walk x y} {Q : G.Walk x' y'} (hP : P.IsPath) (hQ : Q.IsPath) (hPQ : P.support.Disjoint Q.support) (hx : G.Adj x x') (hy : G.Adj y' y) (hxy : s(x, x') ≠ s(y', y)) : (cons hx (Q.append (cons hy P.reverse))).IsCycle

Two vertex-disjoint paths P from x to y and Q from x' to y', joined by distinct edges s(x, x') and s(y', y), close up into a cycle through both edges.

theorem SimpleGraph.Walk.exists_eq_append_of_exists_mem_support {V : Type u} {G : SimpleGraph V} [DecidableEq V] (F : Finset V) {v w : V} (W : G.Walk v w) (h : ∃ y ∈ W.support, y ∈ F) : ∃ (b : V) (B : G.Walk v b) (W₂ : G.Walk b w), W = B.append W₂ ∧ b ∈ F ∧ (∀ y ∈ B.support, y ≠ b → y ∉ F) ∧ List.countP (fun (x : V) => decide (x ∈ F)) B.support = 1

A walk meeting a set F splits at its first vertex b in F: the first part has b as its only vertex in F, occurring once.

theorem SimpleGraph.Walk.exists_eq_append_append_of_countP_lt {V : Type u} {G : SimpleGraph V} [DecidableEq V] (F T : Finset V) {u w : V} (W : G.Walk u w) (hu : u ∈ F) (hW : List.countP (fun (x : V) => decide (x ∈ T \ F)) W.support.tail < List.countP (fun (x : V) => decide (x ∈ F)) W.support.tail) : ∃ (a : V) (b : V) (W₁ : G.Walk u a) (A : G.Walk a b) (W₂ : G.Walk b w), W = W₁.append (A.append W₂) ∧ a ∈ F ∧ b ∈ F ∧ ¬A.Nil ∧ List.countP (fun (x : V) => decide (x ∈ F)) A.support.tail = 1 ∧ ∀ y ∈ A.support, y ≠ a → y ≠ b → y ∉ T

Let W be a walk starting in F, with fewer vertices of T \ F than of F after its start, counted with multiplicity. Then some subwalk A of W of positive length runs between two vertices of F, has its end as its only vertex in F after its start, and has no vertex of T other than its ends.

theorem SimpleGraph.Walk.IsCycle.exists_eq_append_append {V : Type u} {G : SimpleGraph V} [DecidableEq V] {F T : Finset V} {r : V} {c : G.Walk r r} (hc : c.IsCycle) (hr : r ∈ F) (hF : ∀ v ∈ F, v ∈ c.support) (hF2 : 2 ≤ F.card) (hTF : (T \ F).card < F.card) : ∃ (a : V) (b : V) (W₁ : G.Walk r a) (A : G.Walk a b) (W₂ : G.Walk b r), c = W₁.append (A.append W₂) ∧ a ∈ F ∧ b ∈ F ∧ a ≠ b ∧ ¬A.Nil ∧ ∀ y ∈ A.support, y ≠ a → y ≠ b → y ∉ T

Let F be a set of at least two vertices of a cycle c starting in F, with fewer vertices of T outside F than vertices in F. Then c has an arc between two distinct vertices of F whose interior avoids T.

theorem SimpleGraph.exists_isPath_notMem_support_iff {V : Type u} {G : SimpleGraph V} {s t x : V} : (∃ (p : G.Walk s t), p.IsPath ∧ x ∉ p.support) ↔ ∃ (p : G.Walk s t), x ∉ p.support

A walk avoiding a vertex can be shortened to a path avoiding that vertex.