Walks in graphs constructed from simple graphs

This file identifies Mathlib's vertex-based walks in a simple graph H with the edge-labelled walks in Graph.ofSimpleGraph H. In the latter graph, the edge joining x and y is the unordered pair s(x, y), so no edge choice is lost in either direction.

The two conversions preserve length, vertex support, edge lists, concatenation, reversal, trails, paths, and cycles. Their equivalence also identifies the two reachability predicates, providing the basic bridge through which simple-graph connectivity results can be used for multigraph walks.

In the other direction, reachability by edge-labelled walks in a multigraph G agrees with reachability in its underlying simple graph G.toSimpleGraph. A walk in the underlying simple graph can be lifted to the multigraph by choosing one actual edge for each adjacency; this lift preserves the vertex sequence and hence the path predicate.

def SimpleGraph.Walk.toGraph {α : Type u} {H : SimpleGraph α} {x y : α} : H.Walk x y → (Graph.ofSimpleGraph H).Walk x y

Regard a simple-graph walk as an edge-labelled walk in Graph.ofSimpleGraph H.

@[simp]

theorem SimpleGraph.Walk.toGraph_nil {α : Type u} {H : SimpleGraph α} {x : α} : nil.toGraph = Graph.Walk.nil

@[simp]

theorem SimpleGraph.Walk.toGraph_cons {α : Type u} {H : SimpleGraph α} {x y z : α} (h : H.Adj x y) (p : H.Walk y z) : (cons h p).toGraph = Graph.Walk.cons s(x, y) ⋯ p.toGraph

@[simp]

theorem SimpleGraph.Walk.length_toGraph {α : Type u} {H : SimpleGraph α} {x y : α} (p : H.Walk x y) : p.toGraph.length = p.length

@[simp]

theorem SimpleGraph.Walk.support_toGraph {α : Type u} {H : SimpleGraph α} {x y : α} (p : H.Walk x y) : p.toGraph.support = p.support

@[simp]

theorem SimpleGraph.Walk.edges_toGraph {α : Type u} {H : SimpleGraph α} {x y : α} (p : H.Walk x y) : p.toGraph.edges = p.edges

@[simp]

theorem SimpleGraph.Walk.toGraph_append {α : Type u} {H : SimpleGraph α} {x y z : α} (p : H.Walk x y) (q : H.Walk y z) : (p.append q).toGraph = p.toGraph.append q.toGraph

@[simp]

theorem SimpleGraph.Walk.toGraph_reverse {α : Type u} {H : SimpleGraph α} {x y : α} (p : H.Walk x y) : p.reverse.toGraph = p.toGraph.reverse

def Graph.Walk.toSimpleGraph {α : Type u} {H : SimpleGraph α} {x y : α} : (ofSimpleGraph H).Walk x y → H.Walk x y

Forget the redundant edge labels of a walk in Graph.ofSimpleGraph H.

@[simp]

theorem Graph.Walk.toSimpleGraph_nil {α : Type u} {H : SimpleGraph α} {x : α} : nil.toSimpleGraph = SimpleGraph.Walk.nil

@[simp]

theorem Graph.Walk.toSimpleGraph_cons {α : Type u} {H : SimpleGraph α} {x y z : α} {e : Sym2 α} (h : (ofSimpleGraph H).IsLink e x y) (p : (ofSimpleGraph H).Walk y z) : (cons e h p).toSimpleGraph = SimpleGraph.Walk.cons ⋯ p.toSimpleGraph

@[simp]

theorem Graph.Walk.length_toSimpleGraph {α : Type u} {H : SimpleGraph α} {x y : α} (p : (ofSimpleGraph H).Walk x y) : p.toSimpleGraph.length = p.length

@[simp]

theorem Graph.Walk.support_toSimpleGraph {α : Type u} {H : SimpleGraph α} {x y : α} (p : (ofSimpleGraph H).Walk x y) : p.toSimpleGraph.support = p.support

@[simp]

theorem Graph.Walk.edges_toSimpleGraph {α : Type u} {H : SimpleGraph α} {x y : α} (p : (ofSimpleGraph H).Walk x y) : p.toSimpleGraph.edges = p.edges

@[simp]

theorem Graph.Walk.toSimpleGraph_append {α : Type u} {H : SimpleGraph α} {x y z : α} (p : (ofSimpleGraph H).Walk x y) (q : (ofSimpleGraph H).Walk y z) : (p.append q).toSimpleGraph = p.toSimpleGraph.append q.toSimpleGraph

@[simp]

theorem SimpleGraph.Walk.toSimpleGraph_toGraph {α : Type u} {H : SimpleGraph α} {x y : α} (p : H.Walk x y) : p.toGraph.toSimpleGraph = p

@[simp]

theorem Graph.Walk.toGraph_toSimpleGraph {α : Type u} {H : SimpleGraph α} {x y : α} (p : (ofSimpleGraph H).Walk x y) : p.toSimpleGraph.toGraph = p

@[simp]

theorem Graph.Walk.toSimpleGraph_reverse {α : Type u} {H : SimpleGraph α} {x y : α} (p : (ofSimpleGraph H).Walk x y) : p.reverse.toSimpleGraph = p.toSimpleGraph.reverse

@[simp]

theorem Graph.Walk.nil_toSimpleGraph_iff {α : Type u} {H : SimpleGraph α} {x y : α} (p : (ofSimpleGraph H).Walk x y) : p.toSimpleGraph.Nil ↔ p.Nil

@[simp]

theorem SimpleGraph.Walk.nil_toGraph_iff {α : Type u} {H : SimpleGraph α} {x y : α} (p : H.Walk x y) : p.toGraph.Nil ↔ p.Nil

def SimpleGraph.walkEquivOfSimpleGraph {α : Type u} (H : SimpleGraph α) (x y : α) : H.Walk x y ≃ (Graph.ofSimpleGraph H).Walk x y

Walks in a simple graph are equivalent to edge-labelled walks in its associated Graph.

@[simp]

theorem SimpleGraph.walkEquivOfSimpleGraph_apply {α : Type u} {x y : α} (H : SimpleGraph α) (p : H.Walk x y) : (H.walkEquivOfSimpleGraph x y) p = p.toGraph

@[simp]

theorem SimpleGraph.walkEquivOfSimpleGraph_symm_apply {α : Type u} {x y : α} (H : SimpleGraph α) (p : (Graph.ofSimpleGraph H).Walk x y) : (H.walkEquivOfSimpleGraph x y).symm p = p.toSimpleGraph

@[simp]

theorem SimpleGraph.Walk.isTrail_toGraph_iff {α : Type u} {H : SimpleGraph α} {x y : α} (p : H.Walk x y) : p.toGraph.IsTrail ↔ p.IsTrail

@[simp]

theorem SimpleGraph.Walk.isPath_toGraph_iff {α : Type u} {H : SimpleGraph α} {x y : α} (p : H.Walk x y) : p.toGraph.IsPath ↔ p.IsPath

@[simp]

theorem SimpleGraph.Walk.isCycle_toGraph_iff {α : Type u} {H : SimpleGraph α} {x : α} (p : H.Walk x x) : p.toGraph.IsCycle ↔ p.IsCycle

The walk equivalence identifies simple-graph cycles with edge-labelled multigraph cycles.

@[simp]

theorem SimpleGraph.reachable_ofSimpleGraph_iff {α : Type u} (H : SimpleGraph α) (x y : α) : (Graph.ofSimpleGraph H).Reachable x y ↔ H.Reachable x y

Multigraph reachability in Graph.ofSimpleGraph H is simple-graph reachability in H.

@[simp]

theorem Graph.Walk.isTrail_toSimpleGraph_iff {α : Type u} {H : SimpleGraph α} {x y : α} (p : (ofSimpleGraph H).Walk x y) : p.toSimpleGraph.IsTrail ↔ p.IsTrail

@[simp]

theorem Graph.Walk.isPath_toSimpleGraph_iff {α : Type u} {H : SimpleGraph α} {x y : α} (p : (ofSimpleGraph H).Walk x y) : p.toSimpleGraph.IsPath ↔ p.IsPath

@[simp]

theorem Graph.Walk.isCycle_toSimpleGraph_iff {α : Type u} {H : SimpleGraph α} {x : α} (p : (ofSimpleGraph H).Walk x x) : p.toSimpleGraph.IsCycle ↔ p.IsCycle

noncomputable def SimpleGraph.Walk.liftToGraph {α : Type u} {β : Type u_1} {G : Graph α β} {x y : ↑G.vertexSet} : G.toSimpleGraph.Walk x y → G.Walk ↑x ↑y

Lift a walk in the underlying simple graph of a multigraph by choosing one actual edge for each adjacency. The lift preserves the visited vertices but makes no canonical choice among parallel edges.

@[simp]

theorem SimpleGraph.Walk.liftToGraph_nil {α : Type u} {β : Type u_1} {G : Graph α β} (x : ↑G.vertexSet) : nil.liftToGraph = Graph.Walk.nil

@[simp]

theorem SimpleGraph.Walk.liftToGraph_cons {α : Type u} {β : Type u_1} {G : Graph α β} {x y z : ↑G.vertexSet} (h : G.toSimpleGraph.Adj x y) (p : G.toSimpleGraph.Walk y z) : (cons h p).liftToGraph = Graph.Walk.cons (Classical.choose ⋯) ⋯ p.liftToGraph

@[simp]

theorem SimpleGraph.Walk.liftToGraph_append {α : Type u} {β : Type u_1} {G : Graph α β} {x y z : ↑G.vertexSet} (p : G.toSimpleGraph.Walk x y) (q : G.toSimpleGraph.Walk y z) : (p.append q).liftToGraph = p.liftToGraph.append q.liftToGraph

@[simp]

theorem SimpleGraph.Walk.support_liftToGraph {α : Type u} {β : Type u_1} {G : Graph α β} {x y : ↑G.vertexSet} (p : G.toSimpleGraph.Walk x y) : p.liftToGraph.support = List.map Subtype.val p.support

Lifting a simplified walk preserves its vertex sequence, after forgetting the actual-vertex membership proofs.

@[simp]

theorem SimpleGraph.Walk.length_liftToGraph {α : Type u} {β : Type u_1} {G : Graph α β} {x y : ↑G.vertexSet} (p : G.toSimpleGraph.Walk x y) : p.liftToGraph.length = p.length

Lifting a simplified walk preserves its length.

@[simp]

theorem SimpleGraph.Walk.isPath_liftToGraph_iff {α : Type u} {β : Type u_1} {G : Graph α β} {x y : ↑G.vertexSet} (p : G.toSimpleGraph.Walk x y) : p.liftToGraph.IsPath ↔ p.IsPath

A lifted walk is a path exactly when the simplified walk is a path.

theorem SimpleGraph.Walk.liftToGraph_injective {α : Type u} {β : Type u_1} {G : Graph α β} {x y : ↑G.vertexSet} : Function.Injective liftToGraph

Lifting is injective: a walk in a simple graph is determined by its vertex sequence, which the lift preserves. Distinct simplified walks therefore lift to distinct multigraph walks, even though the lift chooses arbitrarily among parallel edges.

@[simp]

theorem SimpleGraph.Walk.liftToGraph_inj {α : Type u} {β : Type u_1} {G : Graph α β} {x y : ↑G.vertexSet} {p q : G.toSimpleGraph.Walk x y} : p.liftToGraph = q.liftToGraph ↔ p = q

Two simplified walks have the same lift exactly when they are equal.

def Graph.toSimpleGraphHomOfLE {α : Type u_1} {β : Type u_2} {G H : Graph α β} (hHG : H ≤ G) : H.toSimpleGraph →g G.toSimpleGraph

A subgraph inclusion H ≤ G induces a homomorphism of underlying simple graphs, sending each actual vertex of H to itself.

@[simp]

theorem Graph.coe_toSimpleGraphHomOfLE_apply {α : Type u_1} {β : Type u_2} {G H : Graph α β} (hHG : H ≤ G) (z : ↑H.vertexSet) : ↑((toSimpleGraphHomOfLE hHG) z) = ↑z

theorem Graph.Reachable.toSimpleGraph_reachable {α : Type u_1} {β : Type u_2} {G : Graph α β} {x y : α} (h : G.Reachable x y) : G.toSimpleGraph.Reachable ⟨x, ⋯⟩ ⟨y, ⋯⟩

Reachability by an edge-labelled walk gives reachability in the underlying simple graph.

@[simp]

theorem Graph.toSimpleGraph_reachable_iff {α : Type u_1} {β : Type u_2} {G : Graph α β} {u v : ↑G.vertexSet} : G.toSimpleGraph.Reachable u v ↔ G.Reachable ↑u ↑v

Reachability in the underlying simple graph is reachability by an edge-labelled walk.

theorem Graph.toSimpleGraph_reachable_deleteVerts_iff_exists_walk {α : Type u_1} {β : Type u_2} {G : Graph α β} {S : Set α} {x y : ↑G.vertexSet} : (G.deleteVerts S).Reachable ↑x ↑y ↔ ∃ (p : G.toSimpleGraph.Walk x y), ∀ z ∈ p.support, ↑z ∉ S

Two actual vertices are reachable after deleting S exactly when some walk between them in the underlying simple graph avoids S.

theorem Graph.toSimpleGraph_reachable_induce_compl_iff {α : Type u_1} {β : Type u_2} {G : Graph α β} {X : Set α} {s t : ↑G.vertexSet} (hs : ↑s ∉ X) (ht : ↑t ∉ X) : (SimpleGraph.induce {v : ↑G.vertexSet | ↑v ∉ X} G.toSimpleGraph).Reachable ⟨s, hs⟩ ⟨t, ht⟩ ↔ (G.deleteVerts X).Reachable ↑s ↑t

Deletion in a multigraph agrees with deletion in its simplification, retaining the original endpoints.