## Stream: graph theory

### Topic: Design question on pushforward / pullback

#### Vincent Beffara (Feb 01 2022 at 13:04):

Hi,

So I rewrote a big part of what I had done on contractions in terms of pushforwards and pullbacks for graph structures, and I have questions about how to proceed. The pushforward operation for simple_graph is natural enough:

def push (f : V → V') (G : simple_graph V) : simple_graph V' :=
{
adj := λ x' y', x' ≠ y' ∧ ∃ x y : V, f x = x' ∧ f y = y' ∧ G.adj x y,
symm := λ x' y' ⟨h₀,x,y,h₁,h₂,h₃⟩, ⟨h₀.symm,y,x,h₂,h₁,h₃.symm⟩,
loopless := λ _ ⟨h₀,_⟩, h₀ rfl
}


(well, natural up to the presence of the x' ≠ y' which makes me feel that it would be more natural to push into a graph or multigraph and then restrict back to simple_graph but that will be for after the big transition). Then, a contraction is just a push by a function with connected cosets.

On the other hand, for the pullback operation, there are two natural options, the first is

def pull (f : V → V') (G' : simple_graph V') : simple_graph V :=
{
symm := λ _ _ h, G'.symm h,
loopless := λ _, G'.loopless _
}


and the second is

def pull' (f : V → V') (G' : simple_graph V') : simple_graph V :=
{
adj := λ x y, x ≠ y ∧ (f x = f y ∨ G'.adj (f x) (f y)),
symm := λ x y ⟨h₁,h₂⟩, by { refine ⟨h₁.symm,_⟩, cases h₂, left, exact h₂.symm, right, exact h₂.symm },
loopless := λ x, by { push_neg, intro, contradiction }
}


(which is like the first except the cosets are filled with edges; somehow pull is the minimal version and pull' is maximal, still with the constraint that x ≠ y is needed for a simple_graph). The first one is easier to work with and feels more universal, the second one is sometimes more useful especially wrt contractions).

The rest of the code is here: https://github.com/vbeffara/lean/blob/main/src/graph_theory/pushforward.lean

So, the question is: which one of these pulls should be the pullback?

(BTW, this feels very much like reinventing the wheel, probably all of that is already somewhere in mathlib in a level of generality that is so high that I would not recognize it :wink:)

#### Eric Wieser (Feb 05 2022 at 07:10):

docs#relation.map and docs#relation.comap are the general versions, with α = {e : sym2 V // ¬e.is_diag}

#### Vincent Beffara (Feb 05 2022 at 09:15):

Ah, thanks! But unfortunately the image under relation.map is not right because for a simple_graph it needs to be irreflexive, so using it would mean saying neq \inf relation.map G.adj f f or something, which I find more awkward than defining it by hand.

The link to comap is broken :sad: ... probably because the most common use case is just r on f (or maybe precisely because there are several natural choices?)

#### Eric Wieser (Feb 05 2022 at 11:55):

As far as I can tell, (≠) ⊓ relation.map G.adj f f is defeq to your definition, so might still be worth using as it makes it clear it's the same meaning of map

#### Vincent Beffara (Feb 05 2022 at 11:58):

Yes, that's probably a good idea, I will do that (and rename to map then). But the difference means that really the push forward operation should be defined for graphs and not simple graphs, once the hierarchy is in place.

#### Yaël Dillies (Feb 05 2022 at 12:22):

It can be defined for both, just as we define composition of functions, continuous maps and homemorphisms separately and show they agree

#### Vincent Beffara (Feb 05 2022 at 13:19):

Yes but at the moment I think I would rather say that map sends graph to graph, that a simple graph is a graph, and that a graph can be turned into a simple graph in a canonical way. Because here they do not quite exactly agree...

#### Vincent Beffara (Feb 05 2022 at 13:24):

Anyway, this is probably a discussion to be had later.

Last updated: Dec 20 2023 at 11:08 UTC