The graph traced by a multigraph walk

This file associates to an edge-labelled multigraph walk the graph consisting exactly of its visited vertices and traversed edge identities. This graph retains the ambient vertex and edge types, so it can be compared directly with the ambient graph and combined with other traced graphs. The construction records an isolated vertex for a zero-length walk, including when that vertex is not an actual vertex of the ambient graph.

The interface follows Mathlib's SimpleGraph.Walk.toSubgraph, adapted to Mathlib's multigraph representation in which a subgraph is itself a Graph and parallel edges retain their identities.

def Graph.walkGraph {α : Type u} {β : Type v} (G : Graph α β) {x y : α} (p : G.Walk x y) : Graph α β

The graph consisting of the vertices and edge identities traversed by a walk.

@[simp]

theorem Graph.Walk.vertexSet_walkGraph {α : Type u} {β : Type v} {G : Graph α β} {x y : α} (p : G.Walk x y) : (G.walkGraph p).vertexSet = {a : α | a ∈ p.support}

@[simp]

theorem Graph.Walk.walkGraph_isLink {α : Type u} {β : Type v} {G : Graph α β} {x y : α} (p : G.Walk x y) (e : β) (a b : α) : (G.walkGraph p).IsLink e a b ↔ G.IsLink e a b ∧ e ∈ p.edges

The links of a traced graph are precisely the ambient links whose identities occur in the walk.

theorem Graph.Walk.mem_edgeSet_walkGraph {α : Type u} {β : Type v} {G : Graph α β} {x y : α} (p : G.Walk x y) (e : β) : e ∈ (G.walkGraph p).edgeSet ↔ e ∈ p.edges

An edge belongs to the graph traced by a walk exactly when the walk traverses it.

@[simp]

theorem Graph.Walk.edgeSet_walkGraph {α : Type u} {β : Type v} {G : Graph α β} {x y : α} (p : G.Walk x y) : (G.walkGraph p).edgeSet = {e : β | e ∈ p.edges}

The edge set of a traced graph is the set represented by the walk's edge list.

theorem Graph.Walk.walkGraph_le {α : Type u} {β : Type v} {G : Graph α β} {x y : α} (p : G.Walk x y) (hx : x ∈ G.vertexSet) : G.walkGraph p ≤ G

A traced graph is a subgraph of the ambient graph when the walk starts at an actual vertex.

@[simp]

theorem Graph.Walk.walkGraph_le_iff {α : Type u} {β : Type v} {G : Graph α β} {x y : α} (p : G.Walk x y) : G.walkGraph p ≤ G ↔ x ∈ G.vertexSet

A walk traces a subgraph of its ambient graph exactly when its starting point is an actual ambient vertex.

theorem Graph.Walk.walkGraph_le_of_pos {α : Type u} {β : Type v} {G : Graph α β} {x y : α} (p : G.Walk x y) (hp : 0 < p.length) : G.walkGraph p ≤ G

A positive-length walk always traces a subgraph of its ambient graph.

theorem Graph.Walk.reachable_walkGraph {α : Type u} {β : Type v} {G : Graph α β} {x y : α} (p : G.Walk x y) : (G.walkGraph p).Reachable x y

The endpoints of a walk are reachable within the graph traced by that walk.

theorem Graph.Walk.reachable_walkGraph_of_mem_support {α : Type u} {β : Type v} {G : Graph α β} {x y : α} (p : G.Walk x y) {a b : α} (ha : a ∈ p.support) (hb : b ∈ p.support) : (G.walkGraph p).Reachable a b

Any two vertices visited by a walk are reachable in its traced graph.

theorem Graph.Walk.walkGraph_le_walkGraph_iff {α : Type u} {β : Type v} {G : Graph α β} {w x y z : α} (p : G.Walk x y) (q : G.Walk z w) : G.walkGraph p ≤ G.walkGraph q ↔ (∀ ⦃a : α⦄, a ∈ p.support → a ∈ q.support) ∧ ∀ ⦃e : β⦄, e ∈ p.edges → e ∈ q.edges

Inclusion between two traced graphs is equivalent to inclusion of their vertex and edge lists, regarded as sets.

@[simp]

theorem Graph.Walk.walkGraph_mapLe {α : Type u} {β : Type v} {G H : Graph α β} {x y : α} (h : G ≤ H) (p : G.Walk x y) : H.walkGraph (mapLe h p) = G.walkGraph p

Mapping a walk to a supergraph does not change its traced graph.

@[simp]

theorem Graph.Walk.walkGraph_transfer {α : Type u} {β : Type v} {G H : Graph α β} {x y : α} (h : G ≤ H) (p : H.Walk x y) (hp : ∀ e ∈ p.edges, e ∈ G.edgeSet) : G.walkGraph (transfer h p hp) = H.walkGraph p

Restricting a walk to a subgraph containing its edges does not change its traced graph.

@[simp]

theorem Graph.Walk.walkGraph_nil {α : Type u} {β : Type v} (G : Graph α β) (x : α) : G.walkGraph nil = noEdge {x} β

A zero-length walk traces the edgeless graph on its base vertex.

@[simp]

theorem Graph.IsLink.walkGraph_toWalk {α : Type u} {β : Type v} {G : Graph α β} {x y : α} {e : β} (h : G.IsLink e x y) : G.walkGraph h.toWalk = (G.induce {x, y}).restrict {e}

A one-edge walk traces exactly that edge and its endpoints.

theorem Graph.Walk.walkGraph_compatible {α : Type u} {β : Type v} {G : Graph α β} {w x y z : α} (p : G.Walk x y) (q : G.Walk z w) : (G.walkGraph p).Compatible (G.walkGraph q)

Traced graphs of walks in one ambient graph are compatible.

theorem Graph.Walk.walkGraph_append {α : Type u} {β : Type v} {G : Graph α β} {x y z : α} (p : G.Walk x y) (q : G.Walk y z) : G.walkGraph (p.append q) = ⋯.union

Concatenating walks takes the compatible union of their traced graphs.

theorem Graph.Walk.walkGraph_cons {α : Type u} {β : Type v} {G : Graph α β} {x y z : α} (e : β) (h : G.IsLink e x y) (p : G.Walk y z) : G.walkGraph (cons e h p) = ⋯.union

Prepending an edge takes the compatible union of its one-edge trace and the remaining walk's trace.

@[simp]

theorem Graph.Walk.walkGraph_reverse {α : Type u} {β : Type v} {G : Graph α β} {x y : α} (p : G.Walk x y) : G.walkGraph p.reverse = G.walkGraph p

Reversing a walk does not change its traced graph.

theorem Graph.Walk.walkGraph_bypass_le {α : Type u} {β : Type v} {G : Graph α β} {x y : α} [DecidableEq α] (p : G.Walk x y) : G.walkGraph p.bypass ≤ G.walkGraph p

Bypassing repeated vertices (removing closed sub-walks) can only shrink a walk's traced graph.