Simple graphs as extensions of digraphs

Stream: mathlib4

[Jeremy Tan]

In #16018 I define a Digraph structure with only an Adj field and make SimpleGraph extend Digraph. But then I have to define aliases involving Adj in some places.

What is the way to remove these aliases in a one-location way?

[Yaël Dillies]

It's hard. @Kyle Miller had some work towards that (and I had a similar but different approach), but it currently gets stuck at multigraphs IIRC

[Jeremy Tan]

In another thread I mentioned trying to port parts of Gonthier's 4CT Coq proof into Lean. He first defines hypermaps, which I have ported as structures with three Perms.

/-- A hypermap consists of three permutations `edge`, `node` and `face` of a dart type `D`
satisfying `edge * node * face = 1`. -/
@[ext]
structure Hypermap (D : Type*) where
  /-- "Edge" permutation on darts -/
  edge : Perm D
  /-- "Node" permutation on darts -/
  node : Perm D
  /-- "Face" permutation on darts -/
  face : Perm D
  /-- The three permutations compose to the identity -/
  enf_one : edge * node * face = 1

Next he defines the genus of a hypermap by a formula involving the number of connected components of the graphs corresponding to each of the three Perms, and their union

[Jeremy Tan]

Assume Fintype D (the Coq proof assumes this from the start) and treat the permutations as elements of the symmetric group on D. For a set s of elements of the symmetric group let C be the number of orbits of the group generated by s. Then the genus is Fintype.card D + 2 * C {edge, node, face} - (C {edge} + C {node} + C {face})

[Jeremy Tan]

I am now massively stuck on trying to formalise the function C in an easy way

[Jeremy Tan]

(btw the whole proof is available at https://github.com/coq-community/fourcolor and the basic definitions are in hypermap.v)

[Jeremy Tan]

I'm thinking that digraphs are the way out of this conundrum, which is why I want to add them to mathlib

[Jeremy Tan]

because later on in hypermap.v this definition appears which crucially depends on directed paths:

(*   Moebius_path q <=> q is a Moebius path: a non-trivial uniq C-path x :: p *)
(*                 with additional "cross" N-links from x to p and from a     *)
(*                 dart y at or before node x in p to the last dart of p      *)
(*                 (i.e., mem2 p y (node x) with node y = last x p).          *)
(* --> Equivalently, such a p can be described as a uniq contour cycle from x *)
(* to node x (closing with an N-link) followed by a "cross-path" that leaves  *)
(* the cycle through an F-link (to face (node x)) and returns to the cycle at *)
(* y through an N-link.                                                       *)

[Rida Hamadani]

Jeremy Tan said:

In another thread I mentioned trying to port parts of Gonthier's 4CT Coq proof into Lean. He first defines hypermaps, which I have ported as structures with three Perms.

/-- A hypermap consists of three permutations `edge`, `node` and `face` of a dart type `D`
satisfying `edge * node * face = 1`. -/
@[ext]
structure Hypermap (D : Type*) where
  /-- "Edge" permutation on darts -/
  edge : Perm D
  /-- "Node" permutation on darts -/
  node : Perm D
  /-- "Face" permutation on darts -/
  face : Perm D
  /-- The three permutations compose to the identity -/
  enf_one : edge * node * face = 1

Next he defines the genus of a hypermap by a formula involving the number of connected components of the graphs corresponding to each of the three Perms, and their union

I am currently working on bringing combinatorial maps to mathlib, I would love to collaborate on this, we are discussing this at #maths > Combinatorial maps
I would like to have the ability to reason about infinite planar graphs, which the coq formalization doesn't cover.

[Rida Hamadani]

(sorry if this is off-topic but I wanted to mention it to avoid duplicating efforts)

[Yaël Dillies]

Rida Hamadani said:

I would like to have the ability to reason about infinite planar graphs, which the coq formalization doesn't cover.

Similarly here. It's important to have infinite planar graphs for the application Kalle and I have to statistical physics

[Kyle Miller]

For this function C, there ought to be some group theory developed somewhere for counting orbits. I'm not sure what digraphs would help you with.