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?

[Bolton Bailey]

To discuss the topological definition more: Would it be possible to get a relatively succinct definition through docs#Geometry.SimplicialComplex ? I am thinking something like:

1. Define the space of finitely supported functions V -> NNReal that sum to 1.
2. Define the simplicial complex as a subspace of this space consisting of only the parts corresponding to vertices and edges of the graph.
3. A graph is planar iff there exists a continuous embedding of this space into the plane.

[Snir Broshi]

I am working on something pretty similar to that, but a complex sounds a bit more complicated than what I had in mind.
I defined it as https://en.wikipedia.org/wiki/Graph_(topology) defines it: A quotient on a union of unit intervals.

[Snir Broshi]

Planning to open a PR soon

[Snir Broshi]

Btw, what do you think about an embedding vs an continuous injection?
These are equivalent in the usual planar case (the space is compact when the graph is finite, and a continuous injection from a compact space to a T2 space (e.g. the plane) is an embedding), but in general a continuous injection is weaker

[Snir Broshi]

And since we're already on the topic, I'll post the definition I have to maybe get feedback:

import Mathlib
namespace SimpleGraph
open unitInterval
variable {V V' : Type*} {G : SimpleGraph V} {M : Type*} [TopologicalSpace M]

/-- An equivalence relation on pairs of vertices and a real number that identifies equal vertices
and edges going in opposite directions -/
def topologySpaceSetoid (V : Type*) : Setoid (Σ _ _ : V, ℝ) where
  r := fun ⟨u₁, v₁, t₁⟩ ⟨u₂, v₂, t₂⟩ ↦
    (u₁ = u₂ ∧ v₁ = v₂ ∧ t₁ = t₂) ∨ (u₁ = v₂ ∧ v₁ = u₂ ∧ t₁ + t₂ = 1) ∨
    (u₁ = u₂ ∧ t₁ = 0 ∧ t₂ = 0) ∨ (v₁ = v₂ ∧ t₁ = 1 ∧ t₂ = 1) ∨
    (u₁ = v₂ ∧ t₁ = 0 ∧ t₂ = 1) ∨ (v₁ = u₂ ∧ t₁ = 1 ∧ t₂ = 0)
  iseqv := {
    refl := by grind
    symm := by grind
    trans h₁ h₂ := by
      obtain _ | _ | _ | _ | _ | _ := h₁ <;> obtain _ | _ | _ | _ | _ | _ := h₂ <;> grind only
  }

/-- The quotient space containing graph topologies on `V` -/
def TopologySpace (V : Type*) : Type _ :=
  Quotient <| topologySpaceSetoid V

instance : TopologicalSpace (TopologySpace V) := inferInstanceAs <| TopologicalSpace <| Quotient _

variable (G) in
/-- The topology of the graph `G`, as a subtype of the topology space -/
abbrev topology : Set (TopologySpace V) :=
  .mk _ '' ({⟨v, v, 0⟩ | v} ∪ {⟨d.fst, d.snd, t⟩ | (d : G.Dart) (t : unitInterval)})

variable (G M) in
/-- An embedding of a simple graph in a topological space is a continuous injective function from
the graph's topology to the space.
This is equivalent to a `Topology.IsEmbedding` in the case of a finite graph with a Hausdorff space
(see `Continuous.isClosedEmbedding` and `isCompact_topology_iff`) but not in general. -/
structure TopologicalEmbedding extends C(G.topology, M) where
  toFun_injective : toFun.Injective

[Snir Broshi]

(this is defined using docs#Sigma since we don't have a way to force V to have the discrete topology yet, and requiring [DiscreteTopology V] is too harsh)
(the hope is to also have an EMetricSpace for it and prove EMetricSpace.edist = G.edist, but this requires more work on metric spaces in Mathlib)
(also regardless if planar graphs are defined with this or with combinatorial maps, this introduces the field "topological graph theory" so it's still worth having)

[Violeta Hernández]

A graph is just a simplicial complex with no 2-faces or higher, is it not? Surely there's some benefit to developing them as a special case.

[Snir Broshi]

Yes, and I think we should have all of them (combinatorial maps, quotient space, complex) and prove equivalences.
But I tried complexes (not sure what's the difference between a CW complex and a simplicial complex) and ran into the problem that I cannot apply a quotient to join the 1-faces which are an edge and its inverse edge, I think I'm only allowed to join the boundary of each (k+1)-face to a k-face.
Also thought about not adding the reverse edges by only adding a 1-face per member of G.edgeSet, but then the gluing to the vertices is harder. Essentially I want to keep everything symmetrical and avoid choosing a direction for every edge (either by Quot.out on the Sym2 V or by asking the caller to provide a direction function).

[Robert Maxton]

(A a side note, topological graph theory is why I went to all the trouble of proving the equivalence between the classical/concrete docs#Topology.RelCWComplex and the abstract docs#TopCat.RelativeCWComplex ... though I'm having trouble getting the PRs through review -_-)

[Robert Maxton]

(but with that, we automatically have objects-in-TopCat for CW complexes)

[Snir Broshi]

This symmetric issue is also why I didn't use Σ (e : G.edgeSet), unitInterval, since it makes me choose which endpoint is 0 and which is 1

[Bolton Bailey]

Here is a simple version of the definition I was thinking of, adapted from @Snir Broshi 's example, which avoids having to write many lines of code to define the setoid

import Mathlib
namespace SimpleGraph
open unitInterval
variable {V V' : Type*} {G : SimpleGraph V}

instance {X Y} [Zero Y] [TopologicalSpace Y] : TopologicalSpace (Finsupp X Y) := sorry -- where is this instance as a subtype of the pi topology?

/-- The type of nonnegative finite weightings of a graphs vertices -/
def VertexWeights (V : Type*) := Finsupp V NNReal

instance : TopologicalSpace (VertexWeights V) :=
  inferInstanceAs (TopologicalSpace (Finsupp V NNReal))

open Classical in
/-- The space of points on a graph as a subtype of the weightings. This is just the set of finitely supported nonnegative functions on the vertex set which sum to 1 and have support which is either a particular vertex or an edge. Vertices correspond to the  finsupps with singleton support and points along edges correspond to finsupps supported by that edge. -/
def topologySpace {V : Type*} (G : SimpleGraph V) :=
  {x : VertexWeights V //
     Finsupp.sum x (fun _ w => w) = 1 ∧
    ∃ edge ∈ G.edgeSet, x.support = edge.toFinset ∨ x.support.card = 1 }

instance : TopologicalSpace (topologySpace G) := by
  apply instTopologicalSpaceSubtype

def IsPlanar (G : SimpleGraph V) : Prop :=
  ∃ (f : topologySpace G → EuclideanSpace ℝ (Fin 2)),
    Continuous f ∧
    Function.Injective f

end SimpleGraph

[Bolton Bailey]

I don't really get why Geometry.SimplicialComplex makes you specify E as a module, I just want to provide a downward closed set of finsets and get a topological space back.

[Snir Broshi]

This looks cool! Though if we're using NNReal which is a Subtype we might as well use unitInterval, no?
I opted for using Reals to avoid Subtype altogether, then the topologySpace definition can ask for non-negativity

[Snir Broshi]

Another problem I have with it is that the natural metric space doesn't seem natural here anymore.
There is a notion of inducing a metric on a quotient (not in Mathlib yet), but I'm not sure how it applies to Finsupp here. We can define it manually though

[Bolton Bailey]

Yes I feel the most natural metric space would be the one that causes the distance between vertex points to be the minimal path length, that seems trickier to get here, especially because of the case of disconnected graphs, maybe an emetric space is more appropriate.

[Kevin Buzzard]

Robert Maxton said:

(A a side note, topological graph theory is why I went to all the trouble of proving the equivalence between the classical/concrete docs#Topology.RelCWComplex and the abstract docs#TopCat.RelativeCWComplex ... though I'm having trouble getting the PRs through review -_-)

What are the PR numbers?

[Robert Maxton]

#29792 is the 'second to last' PR of the forward direction; I haven't made the actual last PR because #29792 is already blocked by a) #29788 and b) #29790 (which depends on (a)).

[Bolton Bailey]

I have gone ahead and made #33364 for this construction of simplicial complexes I felt was missing

[Bolton Bailey]

I have to admit, I also don't know/remember the difference between a simplicial complex and a CW complex, @Robert Maxton if I define a simplical complex for a SimpleGraph does that make it easier to then connect to your work, or do you think the connection of Graph theory to topology should be done in a different way / through CW complexes directly?

[Robert Maxton]

AIUI, a simplicial complex requires that the intersections of $n$-cells at each level be distinct existing $(n-1)$-cells; a CW complex allows arbitrary subsets of unions of existing cells/permits general gluing maps. For 'just' graphs they should be the same I think, but for higher-order graphs, hypergraphs, graph embeddings, and similar, they'll be different.

As such, you may wish to check out/coordinate your definition of simplicial complexes with the concrete docs#Topology.RelCWComplex, as mathematically speaking there should be no obstacles to directly 'reinterpreting' a simplicial complex as a CW complex and it's certainly always valuable to be able to reuse existing code. My own work would only become relevant if and when someone wants to work with graph topologies in a categorical way, I think. (Which is something I personally plan to do, but I'm not sure anyone else does yet!)

[Robert Maxton]

Correction: a 1D simplicial complex is a simple graph; a 1D CW complex is a general graph with self-edges and multiedges allowed

[Robert Maxton]

If you assume a simple graph then they're the same