Relabelling the edges of a multigraph

Mathlib's Graph.map changes vertex names and deliberately leaves edge names fixed. The ear construction needs the complementary operation: give the finitely many edges of an ambient path fresh abstract cell names while retaining every vertex and every incidence.

The relabelling map only has to be injective on the graph's edge set. Walks, paths, and path graphs then push forward by mapping their edge lists.

def Graph.relabelEdges {α : Type u_1} {β : Type u_2} {δ : Type u_3} (G : Graph α β) (f : β → δ) (hf : Set.InjOn f G.edgeSet) : Graph α δ

Relabel every edge of G by a map injective on E(G), without changing its vertices.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Graph.vertexSet_relabelEdges {α : Type u_1} {β : Type u_2} {δ : Type u_3} (G : Graph α β) (f : β → δ) (hf : Set.InjOn f G.edgeSet) : (G.relabelEdges f hf).vertexSet = G.vertexSet

@[simp]

theorem Graph.edgeSet_relabelEdges {α : Type u_1} {β : Type u_2} {δ : Type u_3} (G : Graph α β) (f : β → δ) (hf : Set.InjOn f G.edgeSet) : (G.relabelEdges f hf).edgeSet = f '' G.edgeSet

@[simp]

theorem Graph.relabelEdges_isLink {α : Type u_1} {β : Type u_2} {δ : Type u_3} (G : Graph α β) (f : β → δ) (hf : Set.InjOn f G.edgeSet) (d : δ) (x y : α) : (G.relabelEdges f hf).IsLink d x y ↔ ∃ e ∈ G.edgeSet, f e = d ∧ G.IsLink e x y

theorem Graph.IsLink.relabelEdges {α : Type u_1} {β : Type u_2} {δ : Type u_3} {G : Graph α β} {f : β → δ} {e : β} {x y : α} (hf : Set.InjOn f G.edgeSet) (h : G.IsLink e x y) : (G.relabelEdges f hf).IsLink (f e) x y

An old link survives after its edge receives its new name.

theorem Graph.relabelEdges_inc {α : Type u_1} {β : Type u_2} {δ : Type u_3} (G : Graph α β) (f : β → δ) (hf : Set.InjOn f G.edgeSet) (d : δ) (x : α) : (G.relabelEdges f hf).Inc d x ↔ ∃ e ∈ G.edgeSet, f e = d ∧ G.Inc e x

Incidence in an edge-relabelled graph is exactly incidence of the uniquely represented old edge.

theorem Graph.coveredVertices_relabelEdges {α : Type u_1} {β : Type u_2} {δ : Type u_3} {G : Graph α β} {f : β → δ} (hf : Set.InjOn f G.edgeSet) {W : List β} (hW : ∀ e ∈ W, e ∈ G.edgeSet) : (G.relabelEdges f hf).coveredVertices (List.map f W) = G.coveredVertices W

Relabelling an edge list does not change the vertices it covers.

theorem Graph.walkVertices_relabelEdges {α : Type u_1} {β : Type u_2} {δ : Type u_3} {G : Graph α β} {f : β → δ} (hf : Set.InjOn f G.edgeSet) (u : α) {W : List β} (hW : ∀ e ∈ W, e ∈ G.edgeSet) : (G.relabelEdges f hf).walkVertices u (List.map f W) = G.walkVertices u W

Relabelling a walk's edge list does not change its visited vertices.

theorem Graph.IsWalk.relabelEdges {α : Type u_1} {β : Type u_2} {δ : Type u_3} {G : Graph α β} {f : β → δ} {u : α} {W : List β} {v : α} (hf : Set.InjOn f G.edgeSet) (h : G.IsWalk u W v) : (G.relabelEdges f hf).IsWalk u (List.map f W) v

A walk pushes forward along an injective relabelling of its edges.

theorem Graph.IsPath.relabelEdges {α : Type u_1} {β : Type u_2} {δ : Type u_3} {G : Graph α β} {f : β → δ} {u : α} {W : List β} {v : α} (hf : Set.InjOn f G.edgeSet) (h : G.IsPath u W v) : (G.relabelEdges f hf).IsPath u (List.map f W) v

A path pushes forward along an injective relabelling of its edges.

theorem Graph.IsPathGraph.relabelEdges {α : Type u_1} {β : Type u_2} {δ : Type u_3} {f : β → δ} {u : α} {W : List β} {v : α} {P : Graph α β} (hf : Set.InjOn f P.edgeSet) (h : P.IsPathGraph u W v) : (P.relabelEdges f hf).IsPathGraph u (List.map f W) v

A graph which is exactly a path remains so after an injective edge relabelling.

theorem Graph.Finite.relabelEdges {α : Type u_1} {β : Type u_2} {δ : Type u_3} {G : Graph α β} {f : β → δ} [G.Finite] (hf : Set.InjOn f G.edgeSet) : (G.relabelEdges f hf).Finite

Relabelling preserves graph finiteness.

theorem Graph.Connected.relabelEdges {α : Type u_1} {β : Type u_2} {δ : Type u_3} {G : Graph α β} {f : β → δ} (h : G.Connected) (hf : Set.InjOn f G.edgeSet) : (G.relabelEdges f hf).Connected

Relabelling preserves connectedness because every old walk pushes forward.

theorem Graph.IsWalk.relabelEdges_deleteVerts {α : Type u_1} {β : Type u_2} {δ : Type u_3} {G : Graph α β} {f : β → δ} {X : Set α} {u v : α} {W : List β} (hf : Set.InjOn f G.edgeSet) (h : (G.deleteVerts X).IsWalk u W v) : ((G.relabelEdges f hf).deleteVerts X).IsWalk u (List.map f W) v

A walk surviving a vertex deletion still survives that deletion after edge relabelling.

theorem Graph.IsTwoConnected.relabelEdges {α : Type u_1} {β : Type u_2} {δ : Type u_3} {G : Graph α β} {f : β → δ} (h : G.IsTwoConnected) (hf : Set.InjOn f G.edgeSet) : (G.relabelEdges f hf).IsTwoConnected

Edge relabelling preserves 2-connectivity, including connectedness after deleting any one vertex.

Relabelling a drawing

noncomputable def Graph.relabelDrawing {α : Type u_1} {β : Type u_2} {δ : Type u_3} [Nonempty β] (G : Graph α β) (f : β → δ) (drawing : β → ℝ → Schoenflies.Plane) : δ → ℝ → Schoenflies.Plane

The drawing with its edge argument translated back through an injective relabelling.

Equations

• G.relabelDrawing f drawing d = drawing (Function.invFunOn f G.edgeSet d)

@[simp]

theorem Graph.relabelDrawing_apply {β : Type u_2} {δ : Type u_3} {f : β → δ} {G : Graph Schoenflies.Plane β} {drawing : β → ℝ → Schoenflies.Plane} [Nonempty β] (hf : Set.InjOn f G.edgeSet) {e : β} (he : e ∈ G.edgeSet) : G.relabelDrawing f drawing (f e) = drawing e

theorem Graph.edgeArc_relabelDrawing {β : Type u_2} {δ : Type u_3} {f : β → δ} {G : Graph Schoenflies.Plane β} {drawing : β → ℝ → Schoenflies.Plane} [Nonempty β] (hf : Set.InjOn f G.edgeSet) {e : β} (he : e ∈ G.edgeSet) : edgeArc (G.relabelDrawing f drawing) (f e) = edgeArc drawing e

theorem Graph.pointSet_relabelEdges {β : Type u_2} {δ : Type u_3} {f : β → δ} {G : Graph Schoenflies.Plane β} {drawing : β → ℝ → Schoenflies.Plane} [Nonempty β] (hf : Set.InjOn f G.edgeSet) : (G.relabelEdges f hf).pointSet (G.relabelDrawing f drawing) = G.pointSet drawing

Edge relabelling changes neither the occupied point set nor any geometric edge arc.

theorem Graph.IsDrawing.relabelEdges {β : Type u_2} {δ : Type u_3} {f : β → δ} {G : Graph Schoenflies.Plane β} {drawing : β → ℝ → Schoenflies.Plane} [Nonempty β] (h : G.IsDrawing drawing) (hf : Set.InjOn f G.edgeSet) : (G.relabelEdges f hf).IsDrawing (G.relabelDrawing f drawing)

Injectively changing edge names preserves a plane drawing and all of its drawn arcs.