Design question on pushforward / pullback

Stream: graph theory

[Vincent Beffara]

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 :=
{
    adj := G'.adj on f,
    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]

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

[Vincent Beffara]

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]

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]

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]

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

[Vincent Beffara]

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]

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