Robertson–Seymour theorem

Stream: general

[Daniel Weber]

Would people be interested in formalizing the Robertson–Seymour theorem as a community project?

[Yaël Dillies]

I would love to see it done but I probably won't have time myself!

[Alex Meiburg]

Iirc, something like ~half of the work is proving the Graph Structure Theorem first. That would be a satisfying milestone to hit

[Rida Hamadani]

Count me in!

[Daniel Weber]

Are there expositions of the proof other then the original papers of Robertson and Seymour?

[Rida Hamadani]

There is a chapter in Diestel with the whole purpose of proving it, but I admit I haven't read it yet.

[Rida Hamadani]

Chapter 12: Minors, Trees, and WQO from Diestel's Graph Theory

[Daniel Weber]

Yes, I saw it, and there's a lot of graph minor theory there which would surely be helpful, but there's only a rough sketch of the proof of the theorem itself there

[Alena Gusakov]

I'll join where I can!

[Peter Nelson]

I think there is a lot of infrastructure that is still needed before even stating the structure theorem is possible.

A good (but tiny) first step would be to figure out how to formalize the notion of a multigraph in such a way that Kuratowski's theorem can be reasonably stated.

[Peter Nelson]

For a sense of what stating the actual GM structure theorem would involve, see Theorem 2 of this paper, which is a simplification of the original Robertson-Seymour version. It relies on a technical notion of 'richness' of a graph embedding, which is a seven-part definition with complicated parts.

I don't think this is an FLT-sized project, but it is orders of magnitude larger than anything attempted in formalization in combinatorics in lean, and is much bigger than the four-colour theorem. It will need a lot of input from experts.

[Rida Hamadani]

Peter Nelson said:

I think there is a lot of infrastructure that is still needed before even stating the structure theorem is possible.

A good (but tiny) first step would be to figure out how to formalize the notion of a multigraph in such a way that Kuratowski's theorem can be reasonably stated.

I'm currently working on defining planar graphs using combinatorial maps. #16074 introduces these maps (it is still a WIP), but we don't have orientable manifolds in mathlib yet, I will define those in order to define a graph embedding into an orientable surface then show that such an embedding is equivalent to a combinatorial map. The details of implementation are still not very clear to me but that's the general idea. I wonder if this would cover multigraphs too.

[Peter Nelson]

That sounds great!

I think that defining graph embeddings without the generality of multigraphs would be a mistake. I still don't know how to define multigraphs in a way that plays nice with edge contraction, though...

[Rida Hamadani]

In a multigraph edge contraction, do we do contract all parallel edges at once, or are we allowed to remove only 1 edge while the others turn into loops?
Another question, is the edge contraction allowed to turn a SimpleGraph into a multigraph?

[Jeremy Tan]

@Rida Hamadani what I really want to do is generalise combinatorial maps and hypermaps to the band decompositions described in https://jeffe.cs.illinois.edu/teaching/comptop/2020/notes/19-surface-maps.pdf (Wikipedia calls them generalised maps)

[Jeremy Tan]

Band decompositions also allow representing non-orientable surfaces, which form half of the Ringel–Youngs theorem

[Rida Hamadani]

This is very nice, I'll look more into it.

[Peter Nelson]

Rida Hamadani said:

In a multigraph edge contraction, do we do contract all parallel edges at once, or are we allowed to remove only 1 edge while the others turn into loops?
Another question, is the edge contraction allowed to turn a SimpleGraph into a multigraph?

In a multigraph, contracting one edge should turn the parallel edges into loops.

In a SimpleGraph, contracting an edge e should identify pairs of edges x,y for which exy is a triangle, to give another simple graph. But if G : SimpleGraph a is coerced to a multigraph, then x,y should become parallel in the contraction.

[Peter Nelson]

The 'should' in my statements above is a value judgment. What I really mean is that this is the way to make edge contraction and deletion be dual operations with respect to planar/surface duality.

[Kevin Buzzard]

You seem to be saying that even though we think of simple graphs as a "special case" of multigraphs, really they are distinct structures, and there are (distinct) contraction functions from simple graphs to multigraphs and from simple graphs to simple graphs.

[Rida Hamadani]

How are we going to save the data in a SimpleGraph that x,y are parallel if the graph gets coerced into a multigraph?

[Rida Hamadani]

In my opinion, we can make the contraction function return a multigraph even when its input is a SimpleGraph, and then we can coerce this multigraph into a SimpleGraph if we want by deleting parallel edges.

[Mario Carneiro]

I think the point is that in simple graph contraction, you don't, parallel edges are lost after a contraction. Instead, you have two different contraction functions, where the multigraph one doesn't flatten parallel edges, and the simple graph contraction is related to the multigraph contraction via SimpleGraph -embed-> MultiGraph -contract-> MultiGraph -quotient-> SimpleGraph

[Alex Meiburg]

At one point I tried to survey some literature to how these words ("contraction", "dissolution", "vertex identification", etc.) are used in the settings of simple graph / digraphs / multigraphs ... Basically I found that there is a combinatorial explosion of what these mean. :) For instance, how to handle self-loops? If I contract an edge x-y, do I end up with a loop on the resulting vertex? For some contexts it's crucial that you do.

This was my partial progress: https://ohaithe.re/graph_substructure#modifications

[Alex Meiburg]

The only thing that seemed really consistent across all contexts was "edge deletion". That's removing an edge, no two bones about it.

[Alex Meiburg]

In the context of the RS theorem obviously there is a preferred meaning, but when people talk about e.g. topological minors vs minors vs immersion minors, which are ingredients of the proof, there end up being some annoying subtleties of convention

[Vincent Beffara]

Peter Nelson said:

That sounds great!

I think that defining graph embeddings without the generality of multigraphs would be a mistake. I still don't know how to define multigraphs in a way that plays nice with edge contraction, though...

One option that I played around with a little is to consider a contraction as a special case of a pushforward of graph, where the map has connected fibers. This allows the contraction of many edges at once (which will likely be necessary if we want to look at infinite graphs, and generally makes life easier). Then if one wants to contract a single edge, one has to construct a vertex type for the contraction which does not feel so nice...

One way to do this with the Serre version of multigraphs:

import Mathlib

variable {V V' E : Type*} {e : E} {x y : V}

structure SerreGraph (V : Type*) (E : Type*) where
  o : E → V
  r : E → E
  r_ne e : r e ≠ e
  r_inv e : r (r e) = e

def SerreGraph.map (G : SerreGraph V E) (f : V → V') : SerreGraph V' E where
  o := f ∘ G.o
  r := G.r
  r_ne := G.r_ne
  r_inv := G.r_inv

def ContractRel (G : SerreGraph V E) (e : E) (x y : V) : Prop :=
  (x = y) ∨ (x = G.o e ∧ y = G.o (G.r e)) ∨ (x = G.o (G.r e) ∧ y = G.o e)

lemma contractRel_equiv : Equivalence (ContractRel G e) := sorry

def ContractSetoid (G : SerreGraph V E) (e : E) : Setoid V := ⟨ContractRel G e, contractRel_equiv⟩

def ContractType (G : SerreGraph V E) (e : E) := Quotient (ContractSetoid G e)

def Contract (G : SerreGraph V E) (e : E) : SerreGraph (ContractType G e) E :=
  SerreGraph.map G (Quotient.mk _)

(The second half is likely done somewhere already.)

[Vincent Beffara]

(Also, it might make sense to instead keep V and use update id (G.o e) (G.o (G.r e)) as a map, it is much simpler but has the drawback of creating an isolated vertex.)

[Vincent Beffara]

The version with SimpleGraph is not so nice because of all the edge merging and having to take care of removing self-loops ...

[Peter Nelson]

I like the Serre graphs.

But another part of me still wants a set-theoretic notion of contraction. It is very frustrating to contract a single edge e to get G / e, and then have a vertex x somewhere else in the graph be a one-element set/ equivalence class in the contracted graph, rather than just a vertex.

This would have some form like

import Mathlib.Data.Set.Card

variable {α β : Type*}

structure Multigraph (α β : Type*) where
  V : Set α
  E : Set β
  inc : β → α → Prop
  inc_mem_edge : ∀ e v, inc e v → e ∈ E
  inc_mem_vx : ∀ e v, inc e v → v ∈ V
  inc_exists : ∀ e, ∃ v ∈ V, inc e v
  inc_card : ∀ e, {v | inc e v}.encard ≤ 2

namespace Multigraph

def deleteEdges (G : Multigraph α β) (F : Set β) : Multigraph α β where
  V := G.V
  E := G.E \ F
  inc e v := e ∉ F ∧ G.inc e v
  inc_mem_edge := sorry
  inc_mem_vx := sorry
  inc_exists := sorry
  inc_card := sorry

/-- identify a set `S` of vertices to a vertex named `z`, which can be inside or outside `V`.
edges with both ends in `S` become loops at `z`.  Probably inadvisible to use if `z ∈ G.V \ S` --/
def identify (G : Multigraph α β) (S : Set α) (z : α) : Multigraph α β where
  V := insert z (G.V \ S)
  E := G.E
  inc e v := (v ∉ S ∧ G.inc e v) ∨ (v = z ∧ ∃ x ∈ S, G.inc e x)
  inc_mem_edge := sorry
  inc_mem_vx := sorry
  inc_exists := sorry
  inc_card := sorry

/-- contract an edge `e` to a vertex `z`. We can choose `z` as an existing end of `e`, or
give it a new name from a vertex outside `V`.  Probably a bad idea if neither is the case. --/
def contractEdge (G : Multigraph α β) (e : β) (z : α) : Multigraph α β :=
  (G.identify {v | G.inc e v} z).deleteEdges {e}

There are tradeoffs, but I think this might be a better way to avoid DTT hell.

Doing things like contracting a single edge and comparing the state of things before and after contraction is very common in actual written graph theory proofs, and this kind of approach removes the need for quotients.

[Vincent Beffara]

You can always replace quotients with subtypes to remove the extra vertex:

def merge (x y : V) (z : V) : {v : V // v ≠ x ∨ v = y} := by
  refine ⟨Function.update id x y z, ?_⟩
  by_cases h : z = x
  · subst h ; simp
  · simp [h]

but it's possibly even worse :-(

[Vincent Beffara]

Here https://github.com/vbeffara/lean/tree/main/src/graph_theory I implemented (in Lean 3) the proof of Menger's theorem from Diestel's book, using the Function.update version with all the extra single vertices, and it went kind of ok - OTOH it's an induction on the number of edges so isolated vertices don't hurt.