Combinatorial maps

Stream: maths

[Rida Hamadani]

I want to start formalizing combinatorial maps (aka hypermaps), as the first step to formalize planar graphs. My question is, should the set of darts be a set of docs#SimpleGraph.Dart, or is this too limiting, and I should instead define them over general sets first then consider the darts case when defining planar graphs?
Another question sometimes authors define hypermaps using 3 permutations, and sometimes using 2 permutations (because the 3rd one could be deduced from the other 2). Which one is better for mathlib?
Useful linked:
definition in nlab
definition in coq for the verification of four color theorem

[Rida Hamadani]

Oops, I meant to send this in mathlib4 channel but zulip changed the channel colors for me, can a moderator please move this topic there?

[Yaël Dillies]

I would move this to #maths

[Yaël Dillies]

I would use the three maps definition.

[Yaël Dillies]

Also, cc @Kalle Kytölä !

[Kyle Miller]

In case it's useful, I did a little bit with combinatorial maps here: https://github.com/kmill/lean-graphs/blob/master/src/maps.lean

Over in graphs.lean there's also a related definition, of multigraphs. It also has things like the degree-sum formula for them. This is all from before mathlib had any graph theory.

[Notification Bot]

This topic was moved here from #Is there code for X? > Combinatorial maps by Kim Morrison.

[Rida Hamadani]

/poll What do you think is the best name for combinatorial maps in mathlib?
combinatorialMap
combinatorialEmbedding
hypermap
rotationSystem

[Rida Hamadani]

I've followed the definition on nLab and got the following:

structure hypermap (D : Type) where
  σ : Equiv.Perm D
  α : Equiv.Perm D
  φ : Equiv.Perm D
  transitivity {x y : D} : ∃ g : Subgroup.closure {σ, α, φ}, g • x = y
  composition : φ ∘ σ ∘ α = id
  alpha_involution : Function.Involutive α
  alpha_fixedPoints_isEmpty : IsEmpty (Function.fixedPoints α)

But maybe these are too many conditions? The Wikipedia definition seems more relaxed, what do you think?
Also do the last 2 names follow the naming convention?

[Rida Hamadani]

I just realized that I can use the definition from Kyle's code.

[Kim Morrison]

No need for alpha in the field names. And involutive instead of involution.

[Eric Wieser]

Your composition axiom might be better-stated with Equiv.trans instead of Function.comp; or even with * and 1!

[Kyle Miller]

I'd be interested to know if the three permutation definition can lead to nice defeqs (like could double dual be defeq to op? I think not, but worth verifying)

[Rida Hamadani]

Thanks for the notes, I'll keep them in mind!
I will develop both versions so that we can compare and see which one seems more promising. I will push both versions to a branch after providing a minimal API covering duals, ops and basic lemmas.

[Rida Hamadani]

I've ported parts of Kyle's code into lean4 at #16074, and under it I wrote the definition that uses 3 permutations, with the goal to try and mimic the lemmas proved above but using this new definition.
Note that I decided to go with CombinatorialMap instead of hypermap, because it turns out a hypermap is a a more general structure where α is allowed to have fixed points. Perhaps it could be a good idea to define hypermaps and make combinatorial maps extend them, but if this isn't important, I prefer skipping it for now.

[Rida Hamadani]

@Kyle Miller it turns out that using the definition with 3 permutations, double duals defeq to the original map, not the opposite map. I've pushed that to #16074. Does this mean that we should continue with the 3 permutations definition?

[Rida Hamadani]

I'm struggling to understand how to relate a SimpleGraph to a CombinatorialMap. It seems that in the coq formalization, they just worked with hypermaps, without really relating it to a predefined graph type (maybe they did somewhere and I missed it, I haven't read all the proof of the 4 color theorem). Does anybody have advice on how to approach this?

[Vincent Beffara]

Given a combinatorial map, do you know already how to extract the vertex type for the corresponding graph (i.e., IIRC, the collection of cycles of the first permutation)?

[Rida Hamadani]

Yes!

[Rida Hamadani]

Perhaps I need to formalize this in order to be able to represent a SimpleGraph as a hypermap, but the issue here is that it works only for finite graphs?