planar graphs

Stream: Is there code for X?

[Alex Kontorovich]

Someone asked me about planar graphs in Mathlib; I couldn't find anything after a quick search in docs, and then google found this: https://manifold.markets/tfae/will-lean-mathlib-have-a-definition?play=true. Do we really not have them? Naively, I would think you do something like this (cobbled together with help from GPT, untested!):

import Mathlib

structure Graph (V : Type) :=
  (E : V → V → Prop) -- Edge relations, no further assumptions like simplicity, finiteness, etc

structure PlaneEmbedding (V : Type) :=
  (E : V → V → Prop) -- Edge relation
  (embedding : V → ℝ × ℝ) -- Map vertices to points in ℝ²
  (edge_curves : ∀ {v w : V}, E v w → ℝ → ℝ × ℝ)
    -- Map each edge to a curve
  (edge_continuous : ∀ {v w : V} (h : E v w), Continuous (edge_curves h))
    -- Curves must be continuous
  (edge_ends : ∀ {v w : V} (h : E v w),
    edge_curves h 0 = embedding v ∧ edge_curves h 1 = embedding w)
    -- Curve endpoints match vertex positions
  (non_intersecting : ∀ {v₁ w₁ v₂ w₂ : V} (h₁ : E v₁ w₁) (h₂ : E v₂ w₂),
    (v₁ ≠ v₂ ∨ w₁ ≠ w₂) →
    Set.PairwiseDisjoint
      {t₁ | edge_curves h₁ t₁}
      {t₂ | edge_curves h₂ t₂})
    -- Edges do not intersect, except possibly at endpoints

def PlaneEmbedding.toGraph {V : Type} (emb : PlaneEmbedding V) : Graph V :=
  ⟨emb.E⟩

def IsPlanar {V : Type} (G : Graph V) : Prop :=
  ∃ (emb : PlaneEmbedding V), emb.toGraph = G

The PlaneEmbedding structure isn't quite right yet (especially non-intersecting). But it certainly doesn't seem not doable...? What am I missing? Thanks!

[Jireh Loreaux]

I would think that you would want to define planar graphs in terms of the equivalent graph-theoretic properties (i.e., does not contain a subgraph isomorphic to K_5 or K_{3,3}, IIRC). Then you would prove a theorem that this is equivalent to the PlaneEmbedding version you describe.

[Jireh Loreaux]

But I can't imagine PlaneEmbedding being particularly nice to work with in practice.

[Mitchell Lee]

I agree that there could be situations in which it is easier to work with the forbidden minor characterization, but I don't see why it follows that it should be the definition.

[Jireh Loreaux]

I would imagine that it should be the definition because it's intrinsic, and therefore doesn't require importing anything about ℝ. This is common practice throughout Mathlib, and formalization more generally.

[Mitchell Lee]

What about this: a planar graph is the 1-skeleton of a CW complex which is homeomorphic to the 2-sphere.

[Mitchell Lee]

I know this isn't intrinsic either, but I suspect it is easier to work with in a lot of situations

[Jireh Loreaux]

My initial inclination would again be: why not just make that a theorem? In any case, it's not really my area of Mathlib, so I'll shut up now.

[Kevin Buzzard]

I guess it's worth pointing out the obvious: Gonthier already thought about this question a lot (and wasn't his answer "combinatorial hypermaps"?)

[Joseph Myers]

Defining combinatorial maps is straightforward (and may have been done outside mathlib, though in mathlib we might want a maximally general version covering spaces in more than two dimensions etc.), and it seems they are convenient for formal proof. Defining plane embeddings of graphs is also straightforward. Linking the two, so that you can use results proved with combinatorial maps on graphs / maps given as plane embeddings (which is something I'll want eventually for AperiodicMonotilesLean - Euler's theorem for plane maps on actual (polygonal) maps in the plane), requires a lot more work (the Jordan curve theorem).

[Joseph Myers]

I think Wagner's and Kuratowski's theorems should definitely be theorems about planar graphs, not definitions.

[Kim Morrison]

Yes, the definition should certainly be combinatorial, either Gonthier's approach, or just lots of explicit incidence data about edges and faces.

[Yaël Dillies]

cc @Kalle Kytölä who has been thinking about combinatorial maps in Lean

[Kyle Miller]

As a semi-intrinsic definition, I like Euler characteristic: say a combinatorial map is planar if V - E + F is twice the number of connected components. Then, say a graph is planar if it is the skeleton of a planar combinatorial map.

Connecting this up to a topological definition requires the Jordan curve theorem, some homology, and some bit of the classification of compact closed surfaces. But, at least on paper, I find it to be a lot more workable than the Kuratowski criterion.

[Antoine Chambert-Loir]

Note that the idea of planar graphs had been reworked out by Gonthier and his team when they formalized the 4-colour theorem. I suspect that mathlib could/should make good profit of their work.

[Kyle Miller]

Indeed, they use the Euler characteristic in the definition of a planar map. (https://inria.hal.science/hal-04034866/document)

[Alex Kontorovich]

I'm surprised that the list of 100 theorems to formalize doesn't include proving that (connected) planar graphs have Euler characteristic = 2. (In which case, you can't solve it by definition!...) Seems like the kind of result that should have been included...?

[Joseph Myers]

It seems Gonthier has an approach for proving this Euler characteristic property that bypasses the Jordan curve theorem.

Gonthier also has a very general topological definition of planar maps that allows regions in the map whose boundaries aren't made up of Jordan arcs (see the discussion of corners not necessarily being isolated points, which is not something you can get with a locally finite map where each region's boundary is made up of finitely many Jordan arcs, disjoint except at endpoints).

[Peter Nelson]

The existence of an “abstract dual” of a graph is one way to define planarity. But this needs to be done at a level that allows for multigraphs.

[Peter Nelson]

More concretely: a definition of planarity that doesn’t allow for duality (for each embedding there is a dual embedding where faces and vertices are swapped) is the wrong definition - it would mean that the dual version of every theorem about planar graphs would have to be proved separately.

And any definition of planarity that has duality needs to allow for non-simple graphs, since degree-2 primal vertices correspond to parallel edges in the dual.

Combinatorial hypermaps are one way to do this, and are probably the right one, because they encode precisely the combinatorially relevant geometric information about an embedding. Abstracts duals are a ‘lighter’ way to give the same definition.

I keep banging this multigraph drum because I am constantly worried about certain things in graph theory being developed only for simple graphs, which will mean redoing a lot of stuff down the line.

[Rida Hamadani]

I tried to formalize planar graphs a while ago but then got busy with other things. But after seeing this topic I decided to work on it again, so here is a draft PR with a definition of planar graphs using combinatorial maps: #16074
I realize that this code has many issues, please feel free to suggest improvements.

[Rida Hamadani]

I think characterizing planarity using Euler's formula is not well-suited for infinite graphs, this is unfortunate as some people have shown interest in formalizing results related to infinite planar graphs, and it seems that if we want to do that we will need to come up with different ideas.

[Kyle Miller]

I have reason to believe this is true: if every finite connected sub-map is planar, then the map is planar.

[Kyle Miller]

Perhaps there are counterexamples in the general case, but it should be true at least for locally finite maps (ones with finite degree and finite face sizes)

[Rida Hamadani]

Ah that is true! I'll work on this as soon as I get some free time again.

[Chris Wong]

If that's the case, does that mean the main PR is unblocked? Since the infinite case builds upon the finite case; it does not obsolete it.

[Chris Wong]

Though I am interested in how much we can generalize to infinite things, since IIRC the Coq version assumes everything is Fintype, which is good for the four color theorem but might not be the most general form.

[Kyle Miller]

@Chris Wong docs#SimpleGraph.nonempty_hom_of_forall_finite_subgraph_hom is anticipating this. The finite case is all you need, since there's a compactness argument to lift the result to the infinite case.

[Peter Nelson]

This finiteness/compactness machinery will cause issues with duality, though, because of pictures like this: 34157D36-B21C-4129-B09F-82EF80606993.jpg

Local finiteness is not preserved by duality.

I think that ‘graph-like spaces’ might be the appropriate objects to give you both infinite graphs and planar duality.

[Peter Nelson]

Picture taken from here: https://www.sciencedirect.com/science/article/pii/S0012365X09003823

[Peter Nelson]

This paper also clarifies some of these issues, possibly without needing to define a new object.

https://www.uni-ulm.de/fileadmin/website_uni_ulm/mawi.inst.081/Henning/Duality.pdf

I think that a ‘dual map exists’ definition of planarity will extend fine to infinite graphs. The subtle question is to what extent that definition actually relates to the plane as a manifold.

[Kyle Miller]

I'm trying to understand what that picture has to do with planar graphs. It seems like this is not a graph embedding, since the underlying graph has its top two vertices being adjacent only to the top edge, right? The induced topology is very different. Why does this cause issues for planar embeddings of infinite graphs?

---

That Bruhn-Diestel paper reminds me of some of the details of Stalling's theorem on ends of groups (notes, starts on page 7), where for infinite locally-finite graphs, the finitely-supported 1-cocycles are related to ends.

[Peter Nelson]

That picture isn’t a planar graph, but I think its ‘topological dual’ is a planar graph.

[Peter Nelson]

(I’m certainly not claiming to be an expert on this stuff, but I’ve been exposed to enough of it that I know that reconciling infinite graphs, plane embeddings and duality in a satisfying way is not easy)

[Kyle Miller]

Ah, ok, got it. I guess at least it's the dual of a planar graph that's not locally finite.

[Rida Hamadani]

I expected to use the fact that the edges permutation of a combinatorial map have no fixed points in order to prove the irreflexive property of the simple graph it induces, but I couldn't find a nice way to do this. Here is the current code (from the PR above):

def fromCombinatorialMap (M : CombinatorialMap D) : SimpleGraph M.vertices where
  Adj v₁ v₂ := ∃ d₁ d₂ : D, M.dartVertex d₁ = v₁ ∧ M.dartVertex d₂ = v₂ ∧ M.α d₁ = d₂ ∧ v₁ ≠ v₂
  symm := by
    intro v₁ v₂ ⟨d₁, d₂, h₁, h₂, h₃, h₄⟩
    use d₂, d₁
    exact ⟨h₂, h₁, (M.involutive.eq_iff.mp h₃).symm, h₄.symm⟩
  loopless := by tauto

Does anybody have an idea on how to induce a SimpleGraph from a CombinatorialMap in a way that uses M.fixedPoints_isEmpty instead of relying on v₁ ≠ v₂?

[Robert Maxton]

Mitchell Lee said:

What about this: a planar graph is the 1-skeleton of a CW complex which is homeomorphic to the 2-sphere.

I've been playing around with planar graphs in Mathlib for my own purposes (can't easily make a properly diagrammatic proof widget for foo-monoidal categories without being able to talk about the topology of a graph), and this approximately was the approach I was working with. Or rather, I used docs#Quiv for my graph representation, showed that it had all pullbacks, and then defined a functor Quiv ⥤ TopCat by following the docs#CWComplex model, pulling the vertex-level map back over 𝕊 0 → 𝔻 1. Then a planar graph is just a graph whose corresponding object in TopCat has a mono into EuclideanSpace ℝ 2.

(Working with Quiv also has the nice feature that multigraphs are automatically allowed... though rather than the current suggestion of using Quiv.{0} for simple graphs, the usual issues with handling Sort 0 and Sort (u + 1) homogenously led me to prefer using Quiv.{1} and just defining homs in Squash.)

I think you can get dual graphs out of this fairly easily as well -- just build an appropriate pair of natural transformations between $\operatorname{Hom}(\mathbb{D}^0, -)$ and $\operatorname{Hom}(\mathbb{D}^2, -)$ -- but I'm not entirely sure, and at any rate my graph theory chops are probably not really up to providing results in the proper generality ^.^;

[Peter Nelson]

How would you state Euler’s genus formula for planar multigraphs in that language? (Not suggesting it can’t be done, but seeing a statement would give me a better understanding of the approach you outline)

[Robert Maxton]

Well, you can brute-force it just by asking for the cardinality of {f : 𝔻 n ⟶ G // Mono f} for a graph topology G and n = 0, 1, 2

But Euler characteristic can be defined in a pure categorical way, and upon doing so can be generalized significantly to enriched categeories and certain suitably well behaved infinite objects, if I'm understanding what ncatLab is calling "dualizable" right: https://ncatlab.org/nlab/show/Euler+characteristic

[Robert Maxton]

So I'd probably do it by defining the Euler characteristic of a dualizable object in a symmetric monoidal category, then expressing the genus formula in reference to the graph as an object in Quiv directly

[Peter Nelson]

I suppose what I'm getting at is that graph theorists tend to want to use things like Euler's formula in calculations, and I would worry that, while possible with this approach, this is very far from ergonomic.

As a concrete example, one of the first lemmas one proves about colouring planar graphs is that every planar graph has a vertex of degree at most 5. This follows from Euler's formula and the handshake lemma. How much DTT and abstraction needs to be waded through to produce this proof?

[Rida Hamadani]

I've dusted off #16074, and would like to add an initial API for planar graphs to it (including the lemma Peter mentions above). I have two questions and would really appreciate if someone can take a look at the file containing the planar graph definition in the PR and help:

• Currently combinatorial maps don't include isolated points. Is there a way to circumvent this and prove something such as:

lemma bot_isPlanar [Fintype D] : IsPlanar (D := D) (⊥ : SimpleGraph V) := by
  sorry

• Notice how I had to add (D := D) above. The planarity of a graph shouldn't depend on some type unrelated to its vertices, so it doesn't make sense to add D as an explicit variable, is there a way to not require us to choose a type D first? For example, would it make since to add an existential quantifier in the definition of Graph.IsPlanar that takes a D : Type and a condition Fintype D?

[Peter Nelson]

I think both point are symptom of combinatorial maps and SimpleGraph not fitting together well - maps are screaming for multigraphs with an abstract edge type!

Instead of using a graph isomorphism, could you ask for an edge bijection and an injection from the vertices of the map to those of the graph with certain properties, where isolated vertices are elements outside the image?

[Peter Nelson]

Why do you need the Fintype?

Presumably you can put the D behind an existential quantifier with the same universe as V. That way planarity is an intrinsic property.

[Rida Hamadani]

The reason I'm adding Fintype is so I can write the eulerCharacteristic in terms of Fintype.cards of faces, edges, and vertices.

But maybe that is not as valuable as I thought it is and I can do something like:

/-- The Euler characteristic of a `CombinatorialMap`. -/
noncomputable def eulerCharacteristic : ℤ :=
  Nat.card M.Vertex - Nat.card M.Edge + Nat.card M.Face

[Rida Hamadani]

Assuming I put D behind an existential quantifier, do I need to assume any additional conditions, for example, non-emptiness?