Mapping multigraph walks to supergraphs

This file transports an edge-labelled multigraph walk along a graph inclusion and restricts a walk to a subgraph containing all its traversed edges. Since the ambient vertex and edge types do not change, both operations preserve the support and edge list. In particular, they preserve paths, trails, cycles, and reachability. In particular, reachability after deleting a set of edges is witnessed exactly by walks avoiding those edges, and reachability after deleting a set of vertices is witnessed by walks whose support avoids those vertices.

The single-edge deletion results describe the original component as the union of the endpoint components after deletion (Graph.IsLink.reachable_iff_reachable_deleteEdges_or) and show that reachability outside that component is unchanged (Graph.IsLink.reachable_deleteEdges_iff_of_not_reachable). They supply the walk-level input for the bridge/component-count characterization.

The interface follows Mathlib's SimpleGraph.Walk.mapLe, SimpleGraph.Walk.transfer, and SimpleGraph.reachable_deleteEdges_iff_exists_walk, adapted to retain multigraph edge identities.

def Graph.Walk.mapLe {α : Type u} {β : Type v} {G H : Graph α β} (h : G ≤ H) {x y : α} : G.Walk x y → H.Walk x y

Regard a walk in a subgraph as a walk in a supergraph.

@[simp]

theorem Graph.Walk.mapLe_nil {α : Type u} {β : Type v} {G H : Graph α β} {x : α} (h : G ≤ H) : mapLe h nil = nil

@[simp]

theorem Graph.Walk.mapLe_cons {α : Type u} {β : Type v} {G H : Graph α β} {x y z : α} (h : G ≤ H) (e : β) (he : G.IsLink e x y) (p : G.Walk y z) : mapLe h (cons e he p) = cons e ⋯ (mapLe h p)

@[simp]

theorem Graph.IsLink.mapLe_toWalk {α : Type u} {β : Type v} {G H : Graph α β} {x y : α} {e : β} (h : G ≤ H) (he : G.IsLink e x y) : Walk.mapLe h he.toWalk = ⋯.toWalk

@[simp]

theorem Graph.Walk.mapLe_rfl {α : Type u} {β : Type v} {G : Graph α β} {x y : α} (p : G.Walk x y) : mapLe ⋯ p = p

@[simp]

theorem Graph.Walk.mapLe_mapLe {α : Type u} {β : Type v} {G H K : Graph α β} {x y : α} (hGH : G ≤ H) (hHK : H ≤ K) (p : G.Walk x y) : mapLe hHK (mapLe hGH p) = mapLe ⋯ p

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem Graph.Walk.mapLe_append {α : Type u} {β : Type v} {G H : Graph α β} {x y z : α} (h : G ≤ H) (p : G.Walk x y) (q : G.Walk y z) : mapLe h (p.append q) = (mapLe h p).append (mapLe h q)

@[simp]

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

@[simp]

theorem Graph.Walk.mapLe_nil_iff {α : Type u} {β : Type v} {G H : Graph α β} {x y : α} (h : G ≤ H) (p : G.Walk x y) : (mapLe h p).Nil ↔ p.Nil

@[simp]

theorem Graph.Walk.isTrail_mapLe {α : Type u} {β : Type v} {G H : Graph α β} {x y : α} (h : G ≤ H) (p : G.Walk x y) : (mapLe h p).IsTrail ↔ p.IsTrail

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

Alias of the reverse direction of Graph.Walk.isTrail_mapLe.

theorem Graph.Walk.IsTrail.of_mapLe {α : Type u} {β : Type v} {G H : Graph α β} {x y : α} (h : G ≤ H) (p : G.Walk x y) : (Walk.mapLe h p).IsTrail → p.IsTrail

Alias of the forward direction of Graph.Walk.isTrail_mapLe.

@[simp]

theorem Graph.Walk.isPath_mapLe {α : Type u} {β : Type v} {G H : Graph α β} {x y : α} (h : G ≤ H) (p : G.Walk x y) : (mapLe h p).IsPath ↔ p.IsPath

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

Alias of the reverse direction of Graph.Walk.isPath_mapLe.

theorem Graph.Walk.IsPath.of_mapLe {α : Type u} {β : Type v} {G H : Graph α β} {x y : α} (h : G ≤ H) (p : G.Walk x y) : (Walk.mapLe h p).IsPath → p.IsPath

Alias of the forward direction of Graph.Walk.isPath_mapLe.

@[simp]

theorem Graph.Walk.isCycle_mapLe {α : Type u} {β : Type v} {G H : Graph α β} {x : α} (h : G ≤ H) (p : G.Walk x x) : (mapLe h p).IsCycle ↔ p.IsCycle

theorem Graph.Walk.IsCycle.mapLe {α : Type u} {β : Type v} {G H : Graph α β} {x : α} (h : G ≤ H) (p : G.Walk x x) : p.IsCycle → (Walk.mapLe h p).IsCycle

Alias of the reverse direction of Graph.Walk.isCycle_mapLe.

theorem Graph.Walk.IsCycle.of_mapLe {α : Type u} {β : Type v} {G H : Graph α β} {x : α} (h : G ≤ H) (p : G.Walk x x) : (Walk.mapLe h p).IsCycle → p.IsCycle

Alias of the forward direction of Graph.Walk.isCycle_mapLe.

Restriction to a subgraph

def Graph.Walk.transfer {α : Type u} {β : Type v} {G H : Graph α β} (hGH : G ≤ H) {x y : α} (p : H.Walk x y) : (∀ e ∈ p.edges, e ∈ G.edgeSet) → G.Walk x y

Restrict a walk to a subgraph containing every edge that it traverses.

@[simp]

theorem Graph.Walk.transfer_nil {α : Type u} {β : Type v} {G H : Graph α β} {x : α} (hGH : G ≤ H) (hp : ∀ e ∈ nil.edges, e ∈ G.edgeSet) : transfer hGH nil hp = nil

@[simp]

theorem Graph.Walk.transfer_cons {α : Type u} {β : Type v} {G H : Graph α β} {x y z : α} (hGH : G ≤ H) (e : β) (he : H.IsLink e x y) (p : H.Walk y z) (hp : ∀ f ∈ (cons e he p).edges, f ∈ G.edgeSet) : transfer hGH (cons e he p) hp = cons e ⋯ (transfer hGH p ⋯)

theorem Graph.Walk.transfer_congr {α : Type u} {β : Type v} {G H : Graph α β} {x y : α} (hGH : G ≤ H) {p q : H.Walk x y} (hp : ∀ e ∈ p.edges, e ∈ G.edgeSet) (hq : ∀ e ∈ q.edges, e ∈ G.edgeSet) (hpq : p = q) : transfer hGH p hp = transfer hGH q hq

Restriction is independent of the proofs that the traversed edges lie in the subgraph.

@[simp]

theorem Graph.IsLink.transfer_toWalk {α : Type u} {β : Type v} {G H : Graph α β} {x y : α} {e : β} (hGH : G ≤ H) (he : H.IsLink e x y) (hp : ∀ f ∈ he.toWalk.edges, f ∈ G.edgeSet) : Walk.transfer hGH he.toWalk hp = ⋯.toWalk

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem Graph.Walk.transfer_append {α : Type u} {β : Type v} {G H : Graph α β} {x y z : α} (hGH : G ≤ H) (p : H.Walk x y) (q : H.Walk y z) (hpq : ∀ e ∈ (p.append q).edges, e ∈ G.edgeSet) : transfer hGH (p.append q) hpq = (transfer hGH p ⋯).append (transfer hGH q ⋯)

@[simp]

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

@[simp]

theorem Graph.Walk.transfer_nil_iff {α : Type u} {β : Type v} {G H : Graph α β} {x y : α} (hGH : G ≤ H) (p : H.Walk x y) (hp : ∀ e ∈ p.edges, e ∈ G.edgeSet) : (transfer hGH p hp).Nil ↔ p.Nil

@[simp]

theorem Graph.Walk.isTrail_transfer {α : Type u} {β : Type v} {G H : Graph α β} {x y : α} (hGH : G ≤ H) (p : H.Walk x y) (hp : ∀ e ∈ p.edges, e ∈ G.edgeSet) : (transfer hGH p hp).IsTrail ↔ p.IsTrail

@[simp]

theorem Graph.Walk.isPath_transfer {α : Type u} {β : Type v} {G H : Graph α β} {x y : α} (hGH : G ≤ H) (p : H.Walk x y) (hp : ∀ e ∈ p.edges, e ∈ G.edgeSet) : (transfer hGH p hp).IsPath ↔ p.IsPath

@[simp]

theorem Graph.Walk.isCycle_transfer {α : Type u} {β : Type v} {G H : Graph α β} {x : α} (hGH : G ≤ H) (p : H.Walk x x) (hp : ∀ e ∈ p.edges, e ∈ G.edgeSet) : (transfer hGH p hp).IsCycle ↔ p.IsCycle

@[simp]

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

@[simp]

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

theorem Graph.Walk.mapLe_injective {α : Type u} {β : Type v} {G H : Graph α β} (hGH : G ≤ H) (x y : α) : Function.Injective (mapLe hGH)

Mapping a walk to a supergraph is injective.

theorem Graph.Reachable.mono {α : Type u} {β : Type v} {G H : Graph α β} {x y : α} (hGH : G ≤ H) (hxy : G.Reachable x y) : H.Reachable x y

Reachability is monotone under inclusion of multigraphs.

theorem Graph.reachable_mono {α : Type u} {β : Type v} {G H : Graph α β} (hGH : G ≤ H) : G.Reachable ≤ H.Reachable

Pointwise reachability is monotone under inclusion of multigraphs.

theorem Graph.reachable_deleteEdges_iff_exists_walk {α : Type u} {β : Type v} {G : Graph α β} {F : Set β} {x y : α} : (G.deleteEdges F).Reachable x y ↔ x ∈ G.vertexSet ∧ ∃ (p : G.Walk x y), ∀ e ∈ p.edges, e ∉ F

Two points are reachable after deleting a set of edges exactly when the first is an actual vertex and some walk between them traverses none of the deleted edges.

theorem Graph.reachable_deleteVerts_iff_exists_walk {α : Type u} {β : Type v} {G : Graph α β} {S : Set α} {x y : α} : (G.deleteVerts S).Reachable x y ↔ ∃ (p : G.Walk x y), x ∈ G.vertexSet ∧ ∀ z ∈ p.support, z ∉ S

Two points are reachable after deleting a set of vertices exactly when some walk between them avoids all the deleted vertices.

theorem Graph.mem_vertexSet_of_reachable_deleteVerts {α : Type u} {β : Type v} {G : Graph α β} {S : Set α} {x y : α} (h : (G.deleteVerts S).Reachable x y) : x ∈ G.vertexSet ∧ y ∈ G.vertexSet

Points reachable after deleting some vertices are actual vertices of G.

theorem Graph.IsLink.reachable_deleteEdges_or_reachable_deleteEdges_or {α : Type u} {β : Type v} {G : Graph α β} {e : β} {x y u v : α} (h : G.IsLink e x y) (huv : G.Reachable u v) : (G.deleteEdges {e}).Reachable u v ∨ (G.deleteEdges {e}).Reachable u x ∨ (G.deleteEdges {e}).Reachable u y

After deleting an edge joining x and y, a vertex v reachable from u remains reachable from u, unless x or y is reachable from u in the deletion.

theorem Graph.IsLink.reachable_iff_reachable_deleteEdges_or {α : Type u} {β : Type v} {G : Graph α β} {e : β} {x y u : α} (h : G.IsLink e x y) : G.Reachable x u ↔ (G.deleteEdges {e}).Reachable x u ∨ (G.deleteEdges {e}).Reachable y u

After deleting an edge joining x and y, every vertex reachable from x remains reachable from x or from y.

theorem Graph.IsLink.reachable_deleteEdges_or_reachable {α : Type u} {β : Type v} {G : Graph α β} {e : β} {x y u v : α} (h : G.IsLink e x y) (huv : G.Reachable u v) : (G.deleteEdges {e}).Reachable u v ∨ G.Reachable u x

If v is reachable from u, then it remains reachable after deleting an edge joining x and y, unless x is reachable from u.

theorem Graph.IsLink.reachable_deleteEdges_iff_of_not_reachable {α : Type u} {β : Type v} {G : Graph α β} {e : β} {x y u v : α} (h : G.IsLink e x y) (hux : ¬G.Reachable u x) : (G.deleteEdges {e}).Reachable u v ↔ G.Reachable u v

Deleting an edge joining x and y does not change reachability from a vertex u from which x is unreachable: the components not containing the ends of the edge are unaffected.