# Zulip Chat Archive

## 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 :=
{
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 `pull`

s 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