Definition of planar graphs

Stream: graph theory

[Chris Wong]

What's our current state of the art on defining planar graphs?

I see a lot of discussion in this thread but I don't know if things have changed since then.

It looks like Gonthier's triple of permutations representation is most promising?

I'd like to prove the five color theorem at some point. That appears to depend on planarity in two ways:

1. There exists a vertex with at most 5 neighbors. (This follows from the Euler characteristic)
2. If you delete this vertex, then some of the paths between neighbors must intersect. (I don't know how to justify this. Is this related to the Jordan curve theorem?)

[Yaël Dillies]

There have been some attempts but nothing made it to mathlib. Definitely talk to @Kyle Miller.

[Kevin Buzzard]

I should think that you can use the Jordan curve theorem to prove the intersection property. Consider for example four reals a<b<c<d. Then I claim that any continuous paths in the upper half plane from a to c and from b to d must intersect, and this is because the path from a to c can be joined up by a path in the lower half plane, and now b is in the interior and d in the exterior of that closed path

[Bhavik Mehta]

I've thought about this a fair amount, I think what's most important for a mathlib definition of planar graphs is that it allows conversion between any of the definitions. As Kevin says, one of the biggest blockers to this is the Jordan curve theorem...

[Vincent Beffara]

I once convinced myself that this https://www.tandfonline.com/doi/abs/10.1080/00029890.1988.11972008 was formalizable within a reasonable timeframe. But I don't remember if I am still convinced ...

[Kyle Miller]

@Chris Wong I think combinatorial maps are the right structure to work with a combinatorial version of planarity via Euler characteristic.

The definition Gonthier uses (which is from Cori and Tutte from the mid-70s) is appealing due to its symmetry. There's another version where you use only two darts per edge rather than four (that's the one I used here in the linked thread), but perhaps four darts makes gluing arguments easier? I don't know. I do like that the three-permutation definition sort of immediately gives you a handle structure (0-handles are vertices, 1-handles are edges, and 2-handles are the faces).

Something I noticed is that if you define the dual of a combinatorial map, you don't get that the double dual is exactly the original graph -- you only get something isomorphic by swapping the roles of all the pairs of darts -- but the quadruple dual is exactly the original graph. It seems the triple permutation definition is affected by the same thing. This isn't a problem, but it's curious.

Combinatorial maps might encode the local structure of a planar graph, and you can reconstruct the planar embedding if the graph is connected, but for non-connected graphs you use unique(-up-to-homemorphism) reconstruction. However, the existence of an euler-characteristic-2 combinatorial map representing a graph is equivalent to the existence of a planar embedding of a graph, so this might still fulfill Bhavik's criterion that all notions of planarity are equivalent.

[Kyle Miller]

I think there's a purely algebraic version of the 5-color theorem where you use the contraction-deletion relation and you verify that a certain reduction rule holds, without any need for the Jordan curve theorem. It's probably more convenient to represent planar graphs for this argument using monoidal categories (the relation you verify can be stated as showing that a certain linear combination of morphisms is in the trace radical of this category -- modulo deletion-contraction, the morphism sets are finite dimensional vector spaces, and so the check amounts to a bit of linear algebra) but at some point you want to be able to go back and forth between morphisms in monodial category and combinatorial maps.

One point in using monoidal categories is that it's a natural way to formulate fragments of combinatorial maps, cutting them apart, and gluing them together.

[Vincent Beffara]

@Kyle Miller I don't really remember but isn't the equivalence between planarity and existence of a combinatorial map of genus 2 essentially equivalent to the (discrete) Jordan curve theorem?

[Kyle Miller]

(I assume you mean genus-0 there. I made a mistake too in what I said, which is that it should be euler characteric $2c$, where $c$ is the number of connected components.) Yeah, I think so, you need that cycles in the image of the planar embedding bound disks, in particular the cycles that correspond to faces.

[Vincent Beffara]

(Yes sorry $\chi=2$.)

[Chris Wong]

There's category theory too!? Just when I thought I understood this... :laughing:

[Karl Palmskog]

Coq's MathComp-based graph-theory library was recently reorganized to package results about planar graph results separately, since they depend on Gonthier's fourcolor code. If anyone here can read both Coq and Lean (there is also a paper about Coq side), I'd be interested in a comparison of what the relative statuses of graph-theory and Lean's mathlib are w.r.t. planar graphs.

[Peter Nelson]

I think that Thomassen's proof of JCT has a chance of being a reasonable way to go: see https://www.maths.ed.ac.uk/~v1ranick/jordan/thomass.pdf

[Peter Nelson]

He gives a JCT-free proof that every planar graph is planar with all arcs polygonal, then proves in this framework that K_{3,3} is nonplanar, and gets to JCT from there.