Transferring a walk to a subgraph

Stream: Is there code for X?

[Snir Broshi]

Is there an easy way of transferring a walk to a subgraphs of a graph, given that the edges of the walk are contained in the subgraph?

import Mathlib
namespace SimpleGraph.Walk
variable {V : Type*} {G : SimpleGraph V} {u v : V} (w : G.Walk u v)
theorem snd_mem_edges (hnil : ¬w.Nil) : s(u, w.snd) ∈ w.edges := sorry
theorem penultimate_mem_edges (hnil : ¬w.Nil) : s(w.penultimate, v) ∈ w.edges := sorry
def transferSubgraph (hnil : ¬w.Nil) {G' : G.Subgraph} (hw : ∀ e ∈ w.edges, e ∈ G'.edgeSet) :
    G'.coe.Walk
      ⟨u, G'.mem_verts_of_mem_edge (hw _ <| w.snd_mem_edges hnil) ⟨_, rfl⟩⟩
      ⟨v, G'.mem_verts_of_mem_edge (hw _ <| w.penultimate_mem_edges hnil) ⟨w.penultimate, by simp⟩⟩
  := sorry

docs#SimpleGraph.Walk.transfer requires the graphs to have the same vertex set, and #30590 targets induced subgraphs only.

[Shreyas Srinivas]

I would suggest working entirely in Subgraphs.

[Snir Broshi]

Shreyas Srinivas said:

I would suggest working entirely in Subgraphs.

How? Transferring between 2 subgraphs also seems hard.

[Jakub Nowak]

This generalization might be useful to have.

def SimpleGraph.Walk.backward_map {V : Type u} {V' : Type v} {G : SimpleGraph V} {G' : SimpleGraph V'} (f : G' ↪g G) {u v : V'} (p : G.Walk (f u) (f v)) (h : ∀ w ∈ p.support, { w' // w = f w' }) : G'.Walk u v

transferSubgraph should follow from this.

[Snir Broshi]

It needs the fact that edges are in the smaller graph, not just vertices.
Although I'm having trouble getting the subgraph version from it:

import Mathlib
namespace SimpleGraph.Walk
variable {V V' : Type*} {G : SimpleGraph V} {G' : SimpleGraph V'} {u v : V} (w : G.Walk u v)

theorem snd_mem_edges (hnil : ¬w.Nil) : s(u, w.snd) ∈ w.edges := sorry
theorem penultimate_mem_edges (hnil : ¬w.Nil) : s(w.penultimate, v) ∈ w.edges := sorry

def transferSubgraph (hnil : ¬w.Nil) {G' : G.Subgraph}
    (hw : ∀ e ∈ w.edges, e ∈ G'.edgeSet) : G'.coe.Walk
      ⟨u, G'.mem_verts_of_mem_edge (hw _ <| w.snd_mem_edges hnil) ⟨_, rfl⟩⟩
      ⟨v, G'.mem_verts_of_mem_edge (hw _ <| w.penultimate_mem_edges hnil) ⟨w.penultimate, by simp⟩⟩
  := sorry

def comap (f : G ↪g G') (w' : G'.Walk (f u) (f v))
    (h : ∀ e' ∈ w'.edges, { e // e ∈ G.edgeSet ∧ e' = e.map f }) :
    G.Walk u v
  := sorry

def transferSubgraph' {G' : G.Subgraph} {u v : G'.verts} (w : G.Walk u v)
    (hw : ∀ e ∈ w.edges, e ∈ G'.edgeSet) : G'.coe.Walk u v
  := w.comap G'.hom sorry

[Jakub Nowak]

Ah yes, my mistake, I didn't use subgraph API much. Subgraph is Copy, not an Embedding.

[Jakub Nowak]

So something like this:

def comap (f : G.Copy G') (w' : G'.Walk (f u) (f v))
    (h : ∀ e' ∈ w'.edges, { e // e ∈ G.edgeSet ∧ e' = e.map f }) :
    G.Walk u v :=
  sorry

def transferSubgraph' {G : G'.Subgraph} {u v : G.verts} (w : G'.Walk u v)
    (hw : ∀ e ∈ w.edges, e ∈ G'.edgeSet) : G.coe.Walk u v :=
  comap G.coeCopy w sorry

[Snir Broshi]

I think having this will solve things:

def mapToSubgraph (w : G.Walk u v) : w.toSubgraph.coe.Walk
    ⟨_, w.start_mem_verts_toSubgraph⟩
    ⟨_, w.end_mem_verts_toSubgraph⟩
  := sorry

Then we can .map the result with any f : w.toSubgraph.coe →g G which is pretty similar to the hw hypothesis.

[Snir Broshi]

Success: #30826

[Snir Broshi]

The original transferToSubgraph successfully implemented using mapToSubgraph:
(but with 3 sorried lemmas)

import Mathlib
namespace SimpleGraph.Walk
variable {V V' : Type*} {G : SimpleGraph V} {G' : SimpleGraph V'} {u v v' : V} (w : G.Walk u v)

theorem snd_mem_edges (hnil : ¬w.Nil) : s(u, w.snd) ∈ w.edges := sorry
theorem penultimate_mem_edges (hnil : ¬w.Nil) : s(w.penultimate, v) ∈ w.edges := sorry
def containingEdge (hnil : ¬w.Nil) (hsupp : v' ∈ w.support) : { e // e ∈ w.edges ∧ v' ∈ e } := sorry

/-- Map a walk to its own subgraph. -/
def mapToSubgraph {u v : V} : ∀ w : G.Walk u v, w.toSubgraph.coe.Walk
    ⟨_, w.start_mem_verts_toSubgraph⟩ ⟨_, w.end_mem_verts_toSubgraph⟩
  | nil => nil
  | cons .. =>
    let h : cons .. |>.toSubgraph.Adj .. := (le_sup_left : _ ≤ Walk.toSubgraph _).right rfl
    let h : cons .. |>.toSubgraph.coe.Adj ⟨_, h.fst_mem⟩ ⟨_, h.snd_mem⟩ := h
    cons h <| mapToSubgraph _ |>.map <| Subgraph.inclusion le_sup_right

/-- Transfer a non-nil walk to a subgraph that contains all of its edges. -/
def transferToSubgraph (hnil : ¬w.Nil) {G' : G.Subgraph}
    (hw : ∀ e ∈ w.edges, e ∈ G'.edgeSet) : G'.coe.Walk
      ⟨u, G'.mem_verts_of_mem_edge (hw _ <| w.snd_mem_edges hnil) ⟨_, rfl⟩⟩
      ⟨v, G'.mem_verts_of_mem_edge (hw _ <| w.penultimate_mem_edges hnil) ⟨w.penultimate, by simp⟩⟩
    :=
  let f : w.toSubgraph.coe →g G'.coe := {
    toFun v' := ⟨v', let e := w.containingEdge hnil <| w.mem_verts_toSubgraph.mp v'.prop
      Subgraph.mem_verts_of_mem_edge (hw _ e.prop.left) e.prop.right⟩
    map_rel' h := hw _ <| w.mem_edges_toSubgraph.mp (h : s(_, _) ∈ _)
  }
  w.mapToSubgraph.map f