Mapping walks between graphs

Functions that map walks between different graphs.

Main definitions

• SimpleGraph.Walk.map: The map on walks induced by a graph homomorphism
• SimpleGraph.Walk.mapLe: Map a walk to a supergraph
• SimpleGraph.Walk.transfer: Map a walk to another graph that contains its edges
• SimpleGraph.Walk.induce: Map a walk that's fully contained in a set of vertices to the subgraph induced by that set
• SimpleGraph.Walk.toDeleteEdges: Map a walk that avoids a set of edges to the subgraph with those edges deleted
• SimpleGraph.Walk.toDeleteEdge: Map a walk that avoids an edge to the subgraph with that edge deleted

Tags

walks

Mapping walks

def SimpleGraph.Walk.map {V : Type u} {V' : Type v} {G : SimpleGraph V} {G' : SimpleGraph V'} (f : G →g G') {u v : V} : G.Walk u v → G'.Walk (f u) (f v)

Given a graph homomorphism, map walks to walks.

@[simp]

theorem SimpleGraph.Walk.map_nil {V : Type u} {V' : Type v} {G : SimpleGraph V} {G' : SimpleGraph V'} (f : G →g G') {u : V} : Walk.map f nil = nil

@[simp]

theorem SimpleGraph.Walk.map_cons {V : Type u} {V' : Type v} {G : SimpleGraph V} {G' : SimpleGraph V'} (f : G →g G') {u v : V} (p : G.Walk u v) {w : V} (h : G.Adj w u) : Walk.map f (cons h p) = cons ⋯ (Walk.map f p)

@[simp]

theorem SimpleGraph.Walk.map_copy {V : Type u} {V' : Type v} {G : SimpleGraph V} {G' : SimpleGraph V'} (f : G →g G') {u v u' v' : V} (p : G.Walk u v) (hu : u = u') (hv : v = v') : Walk.map f (p.copy hu hv) = (Walk.map f p).copy ⋯ ⋯

@[simp]

theorem SimpleGraph.Walk.map_id {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v) : Walk.map Hom.id p = p

@[simp]

theorem SimpleGraph.Walk.map_map {V : Type u} {V' : Type v} {V'' : Type w} {G : SimpleGraph V} {G' : SimpleGraph V'} {G'' : SimpleGraph V''} (f : G →g G') (f' : G' →g G'') {u v : V} (p : G.Walk u v) : Walk.map f' (Walk.map f p) = Walk.map (f'.comp f) p

theorem SimpleGraph.Walk.map_eq_of_eq {V : Type u} {V' : Type v} {G : SimpleGraph V} {G' : SimpleGraph V'} {u v : V} (p : G.Walk u v) {f : G →g G'} (f' : G →g G') (h : f = f') : Walk.map f p = (Walk.map f' p).copy ⋯ ⋯

Unlike categories, for graphs vertex equality is an important notion, so needing to be able to work with equality of graph homomorphisms is a necessary evil.

@[simp]

theorem SimpleGraph.Walk.nil_map_iff {V : Type u} {V' : Type v} {G : SimpleGraph V} {G' : SimpleGraph V'} (f : G →g G') {u v : V} {p : G.Walk u v} : (Walk.map f p).Nil ↔ p.Nil

@[deprecated SimpleGraph.Walk.nil_map_iff (since := "2026-05-12")]

theorem SimpleGraph.Walk.map_eq_nil_iff {V : Type u} {V' : Type v} {G : SimpleGraph V} {G' : SimpleGraph V'} (f : G →g G') {u : V} {p : G.Walk u u} : Walk.map f p = nil ↔ p = nil

@[simp]

theorem SimpleGraph.Walk.length_map {V : Type u} {V' : Type v} {G : SimpleGraph V} {G' : SimpleGraph V'} (f : G →g G') {u v : V} (p : G.Walk u v) : (Walk.map f p).length = p.length

@[simp]

theorem SimpleGraph.Walk.map_append {V : Type u} {V' : Type v} {G : SimpleGraph V} {G' : SimpleGraph V'} (f : G →g G') {u v w : V} (p : G.Walk u v) (q : G.Walk v w) : Walk.map f (p.append q) = (Walk.map f p).append (Walk.map f q)

@[simp]

theorem SimpleGraph.Walk.reverse_map {V : Type u} {V' : Type v} {G : SimpleGraph V} {G' : SimpleGraph V'} (f : G →g G') {u v : V} (p : G.Walk u v) : (Walk.map f p).reverse = Walk.map f p.reverse

@[simp]

theorem SimpleGraph.Walk.support_map {V : Type u} {V' : Type v} {G : SimpleGraph V} {G' : SimpleGraph V'} (f : G →g G') {u v : V} (p : G.Walk u v) : (Walk.map f p).support = List.map (⇑f) p.support

@[simp]

theorem SimpleGraph.Walk.darts_map {V : Type u} {V' : Type v} {G : SimpleGraph V} {G' : SimpleGraph V'} (f : G →g G') {u v : V} (p : G.Walk u v) : (Walk.map f p).darts = List.map f.mapDart p.darts

@[simp]

theorem SimpleGraph.Walk.edges_map {V : Type u} {V' : Type v} {G : SimpleGraph V} {G' : SimpleGraph V'} (f : G →g G') {u v : V} (p : G.Walk u v) : (Walk.map f p).edges = List.map (Sym2.map ⇑f) p.edges

@[simp]

theorem SimpleGraph.Walk.edgeSet_map {V : Type u} {V' : Type v} {G : SimpleGraph V} {G' : SimpleGraph V'} (f : G →g G') {u v : V} (p : G.Walk u v) : (Walk.map f p).edgeSet = Sym2.map ⇑f '' p.edgeSet

@[simp]

theorem SimpleGraph.Walk.getVert_map {V : Type u} {V' : Type v} {G : SimpleGraph V} {G' : SimpleGraph V'} (f : G →g G') {u v : V} (p : G.Walk u v) (n : ℕ) : (Walk.map f p).getVert n = f (p.getVert n)

theorem SimpleGraph.Walk.map_injective_of_injective {V : Type u} {V' : Type v} {G : SimpleGraph V} {G' : SimpleGraph V'} {f : G →g G'} (hinj : Function.Injective ⇑f) (u v : V) : Function.Injective (Walk.map f)

@[reducible, inline]

abbrev SimpleGraph.Walk.mapLe {V : Type u} {G G' : SimpleGraph V} (h : G ≤ G') {u v : V} (p : G.Walk u v) : G'.Walk u v

The specialization of SimpleGraph.Walk.map for mapping walks to supergraphs.

theorem SimpleGraph.Walk.length_mapLe {V : Type u} {G G' : SimpleGraph V} (h : G ≤ G') {u v : V} (p : G.Walk u v) : (mapLe h p).length = p.length

theorem SimpleGraph.Walk.support_mapLe_eq_support {V : Type u} {G G' : SimpleGraph V} (h : G ≤ G') {u v : V} (p : G.Walk u v) : (mapLe h p).support = p.support

theorem SimpleGraph.Walk.edges_mapLe_eq_edges {V : Type u} {G G' : SimpleGraph V} (h : G ≤ G') {u v : V} (p : G.Walk u v) : (mapLe h p).edges = p.edges

theorem SimpleGraph.Walk.edgeSet_mapLe_eq_edgeSet {V : Type u} {G G' : SimpleGraph V} (h : G ≤ G') {u v : V} (p : G.Walk u v) : (mapLe h p).edgeSet = p.edgeSet

theorem SimpleGraph.Walk.reverse_mapLe {V : Type u} {G G' : SimpleGraph V} (h : G ≤ G') {u v : V} (p : G.Walk u v) : (mapLe h p).reverse = mapLe h p.reverse

theorem SimpleGraph.Walk.mapLe_append {V : Type u} {G G' : SimpleGraph V} (h : G ≤ G') {u v w : V} (p : G.Walk u v) (q : G.Walk v w) : mapLe h (p.append q) = (mapLe h p).append (mapLe h q)

Transferring between graphs

def SimpleGraph.Walk.transfer {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v) (H : SimpleGraph V) (h : ∀ e ∈ p.edges, e ∈ H.edgeSet) : H.Walk u v

The walk p transferred to lie in H, given that H contains its edges.

theorem SimpleGraph.Walk.transfer_self {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v) : p.transfer G ⋯ = p

theorem SimpleGraph.Walk.transfer_eq_mapLe {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v) {H : SimpleGraph V} (hp : ∀ e ∈ p.edges, e ∈ H.edgeSet) (GH : G ≤ H) : p.transfer H hp = mapLe GH p

@[deprecated SimpleGraph.Walk.transfer_eq_mapLe (since := "2026-09-14")]

theorem SimpleGraph.Walk.transfer_eq_map_ofLE {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v) {H : SimpleGraph V} (hp : ∀ e ∈ p.edges, e ∈ H.edgeSet) (GH : G ≤ H) : p.transfer H hp = mapLe GH p

Alias of SimpleGraph.Walk.transfer_eq_mapLe.

@[simp]

theorem SimpleGraph.Walk.nil_transfer {V : Type u} {G H : SimpleGraph V} {u v : V} {p : G.Walk u v} {h : ∀ e ∈ p.edges, e ∈ H.edgeSet} : (p.transfer H h).Nil ↔ p.Nil

@[simp]

theorem SimpleGraph.Walk.edges_transfer {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v) {H : SimpleGraph V} (hp : ∀ e ∈ p.edges, e ∈ H.edgeSet) : (p.transfer H hp).edges = p.edges

@[simp]

theorem SimpleGraph.Walk.edgeSet_transfer {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v) {H : SimpleGraph V} (hp : ∀ e ∈ p.edges, e ∈ H.edgeSet) : (p.transfer H hp).edgeSet = p.edgeSet

@[simp]

theorem SimpleGraph.Walk.support_transfer {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v) {H : SimpleGraph V} (hp : ∀ e ∈ p.edges, e ∈ H.edgeSet) : (p.transfer H hp).support = p.support

@[simp]

theorem SimpleGraph.Walk.length_transfer {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v) {H : SimpleGraph V} (hp : ∀ e ∈ p.edges, e ∈ H.edgeSet) : (p.transfer H hp).length = p.length

@[simp]

theorem SimpleGraph.Walk.transfer_transfer {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v) {H : SimpleGraph V} (hp : ∀ e ∈ p.edges, e ∈ H.edgeSet) {K : SimpleGraph V} (hp' : ∀ e ∈ (p.transfer H hp).edges, e ∈ K.edgeSet) : (p.transfer H hp).transfer K hp' = p.transfer K ⋯

@[simp]

theorem SimpleGraph.Walk.transfer_append {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v) {H : SimpleGraph V} {w : V} (q : G.Walk v w) (hpq : ∀ e ∈ (p.append q).edges, e ∈ H.edgeSet) : (p.append q).transfer H hpq = (p.transfer H ⋯).append (q.transfer H ⋯)

@[simp]

theorem SimpleGraph.Walk.reverse_transfer {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v) {H : SimpleGraph V} (hp : ∀ e ∈ p.edges, e ∈ H.edgeSet) : (p.transfer H hp).reverse = p.reverse.transfer H ⋯

Inducing a walk

def SimpleGraph.Walk.induce {V : Type u} {G : SimpleGraph V} (s : Set V) {u v : V} (w : G.Walk u v) (hw : ∀ x ∈ w.support, x ∈ s) : (induce s G).Walk ⟨u, ⋯⟩ ⟨v, ⋯⟩

A walk in G which is fully contained in a set s of vertices lifts to a walk of G[s].

@[simp]

theorem SimpleGraph.Walk.induce_nil {V : Type u} {G : SimpleGraph V} {u : V} {s : Set V} (hw : ∀ x ∈ nil.support, x ∈ s) : Walk.induce s nil hw = nil

@[simp]

theorem SimpleGraph.Walk.induce_cons {V : Type u} {G : SimpleGraph V} {u v u' : V} {s : Set V} (huu' : G.Adj u u') (w : G.Walk u' v) (hw : ∀ x ∈ (cons huu' w).support, x ∈ s) : Walk.induce s (cons huu' w) hw = cons ⋯ (Walk.induce s w ⋯)

@[simp]

theorem SimpleGraph.Walk.support_induce {V : Type u} {G : SimpleGraph V} {s : Set V} {u v : V} (w : G.Walk u v) (hw : ∀ x ∈ w.support, x ∈ s) : (Walk.induce s w hw).support = w.support.attachWith (Membership.mem s) hw

@[simp]

theorem SimpleGraph.Walk.map_induce {V : Type u} {G : SimpleGraph V} {s : Set V} {u v : V} (w : G.Walk u v) (hw : ∀ x ∈ w.support, x ∈ s) : Walk.map (Embedding.induce s).toHom (Walk.induce s w hw) = w

theorem SimpleGraph.Walk.map_induce_induceHomOfLE {V : Type u} {G : SimpleGraph V} {s s' : Set V} (hs : s ⊆ s') {u v : V} (w : G.Walk u v) (hw : ∀ x ∈ w.support, x ∈ s) : Walk.map (G.induceHomOfLE hs).toHom (Walk.induce s w hw) = Walk.induce s' w ⋯

Deleting edges

@[reducible, inline]

abbrev SimpleGraph.Walk.toDeleteEdges {V : Type u} {G : SimpleGraph V} (s : Set (Sym2 V)) {v w : V} (p : G.Walk v w) (hp : ∀ e ∈ p.edges, e ∉ s) : (G.deleteEdges s).Walk v w

Given a walk that avoids a set of edges, produce a walk in the graph with those edges deleted.

@[simp]

theorem SimpleGraph.Walk.toDeleteEdges_nil {V : Type u} {G : SimpleGraph V} (s : Set (Sym2 V)) {v : V} (hp : ∀ e ∈ nil.edges, e ∉ s) : toDeleteEdges s nil hp = nil

@[simp]

theorem SimpleGraph.Walk.toDeleteEdges_cons {V : Type u} {G : SimpleGraph V} (s : Set (Sym2 V)) {u v w : V} (h : G.Adj u v) (p : G.Walk v w) (hp : ∀ e ∈ (cons h p).edges, e ∉ s) : toDeleteEdges s (cons h p) hp = cons ⋯ (toDeleteEdges s p ⋯)

@[reducible, inline]

abbrev SimpleGraph.Walk.toDeleteEdge {V : Type u} {G : SimpleGraph V} {v w : V} (e : Sym2 V) (p : G.Walk v w) (hp : e ∉ p.edges) : (G.deleteEdges {e}).Walk v w

Given a walk that avoids an edge, create a walk in the subgraph with that edge deleted. This is an abbreviation for SimpleGraph.Walk.toDeleteEdges.

@[simp]

theorem SimpleGraph.Walk.mapLe_toDeleteEdges_eq {V : Type u} {G : SimpleGraph V} {v w : V} (s : Set (Sym2 V)) {p : G.Walk v w} (hp : ∀ e ∈ p.edges, e ∉ s) : mapLe ⋯ (toDeleteEdges s p hp) = p

@[deprecated SimpleGraph.Walk.mapLe_toDeleteEdges_eq (since := "2026-09-14")]

theorem SimpleGraph.Walk.map_toDeleteEdges_eq {V : Type u} {G : SimpleGraph V} {v w : V} (s : Set (Sym2 V)) {p : G.Walk v w} (hp : ∀ e ∈ p.edges, e ∉ s) : mapLe ⋯ (toDeleteEdges s p hp) = p

Alias of SimpleGraph.Walk.mapLe_toDeleteEdges_eq.