How to structure Cayley graph API

Stream: mathlib4

[Vlad Tsyrklevich]

I've been cleaning-up a definition and some basic API/proofs for Cayley graphs here that I'd like to upstream to mathlib. There's two things I don't like that I wanted to ask about:

1. I define a CayleyGraph structure like so:

structure CayleyGraph (G : Type*) [Group G] (S : Set G) where
  one_not_mem : 1 ∉ S

one_not_mem is required to satisfy SimpleGraph which does not allow self-loops. I then define the actual SimpleGraph

namespace CayleyGraph

variable {G : Type*} [Group G] {S : Set G} (CG : CayleyGraph G S)

def Graph : SimpleGraph G where
  Adj x y := x * y⁻¹ ∈ S ∨ y * x⁻¹ ∈ S
  symm _ _ h := h.symm
  loopless _ := by simp [CG.one_not_mem]

but this feels awkward, having a (CG : CayleyGraph G S) and needing to reference the actual graph as CG.Graph when CayleyGraph itself has graph in the name. Am I overthinking this, or should I be taking a different approach?

2. Slightly related to the above, the API I've developed so far is specialized to Group and I can't additivize it using @[to_additive] because I don't use Group in the naming. Should I extend to_additive to support AddCayleyGraph, or should this API actually live as Group.CayleyGraph generating_set, or something else? Perhaps to also address the above, Group.Cayley generating_set where (Group.Cayley generating_set).Graph is the SimpleGraph?

Any other feedback/suggestions welcome.

[Violeta Hernández]

Isn't it usually the case that you want to construct a Cayley graph for an entire group?

[Violeta Hernández]

I think you should either use a non-simple graph, or you should avoid drawing edges from x back to itself

[Violeta Hernández]

Then you don't need this extra CayleyGraph structure

[Vlad Tsyrklevich]

Violeta Hernández said:

Isn't it usually the case that you want to construct a Cayley graph for an entire group?

Not sure I understand this question, this object is the Cayley graph for an entire group.

The difficulty with $1 \notin S$ is hard to avoid because the other Graph APIs in mathlib are so undeveloped--and I figured it wasn't worth the investment since 1 is not an interesting generator anyway.

[Violeta Hernández]

Oh, I misunderstood. So S is the set of generators, not the set of elements of the graph.

[Violeta Hernández]

What I tried to say still applies, though. What do you think about allowing 1 in the set of generators, but explicitly omitting any edges between a node and itself?

[Violeta Hernández]

As a more holistic kind of question, what exactly do you want to do with Cayley graphs? I've always viewed them as more of a visualization device, rather than a mathematical tool.

[Vlad Tsyrklevich]

Violeta Hernández said:

What I tried to say still applies, though. What do you think about allowing 1 in the set of generators, but explicitly omitting any edges between a node and itself?

What is the advantage? Just to avoid the hypothesis? Does it allow structuring the code differently somehow? I'm not sure it's particularly useful in practice for developing the theory.

[Vlad Tsyrklevich]

Cayley graphs are often studied in Geometric Group Theory as you can put a geometric representation on a groups, e.g. a metric structure, and then study invariant properties. I'm not an expert, so I was developing some basic theory while following a seminar and thought it'd be nice to contribute them.

[Jakub Nowak]

I'm not sure if you need CayleyGraph structure in the first place. Do you use this CayleyGraph structure for something else than creating SimpleGraph from it, or do you have more constructors?

Something like:

import Mathlib

variable {G : Type*} [Group G] {S : Set G}

def cayleyGraph (h : 1 ∉ S) : SimpleGraph G where
  Adj x y := x * y⁻¹ ∈ S ∨ y * x⁻¹ ∈ S
  symm _ _ h := h.symm
  loopless _ := by simpa

You can still prove properties about cayleyGraph.

[Vlad Tsyrklevich]

Yeah so the reason I had not gone with def cayleyGraph (h : 1 ∉ S) : SimpleGraph G is because I think I was concerned that carrying around the hypothesis in the type was unergonomic, but I'm not really sure if that's a valid concern relative to carrying around a structure instead. I'll give it a try and see how it looks

[Alex Meiburg]

I agree with Vlad there - data-carrying defs that include propositions to be valid pretty much always leads to large pain. (e.g. what if I want to call simp on my set S now?)

I think Violeta's approach will be the right one, i.e define it for any set of generators, and just explicitly include x \ne y \and ... in the definition of Adj x y. And then of course there will be theorems that CayleyGraph S = CayleyGraph (insert 1 S) and CayleyGraph S = CayleyGraph (S \ {1}).

[Alex Meiburg]

Actually, I think there's an even better way: first define CayleyDigraph as the directed version, Digraph, which keeps track of the orientation based on the elements of S. (This does show up in enough contexts to merit talking defining here, I'm pretty sure.) It can have self-loops just fine. Then CayleyGraph S := (CayleyDigraph S).toSimpleGraphInclusive.

Then all a lot of the fussing about what happens with including 1 or not, or symmetrizing or not, would follow from the properties of docs#Digraph.toSimpleGraphInclusive.

[Anatole Dedecker]

I've never interacted with graph theory in Mathlib so take my suggestions with a grain of salt but, if you're going to define the Cayley graph then why not go for the Schreier graph of an arbitrary group action?

Of course the issue is that it is no longer a simple graph even when S does not contain 1 (which I think should be allowed btw). It is naturally built as a subquiver of the action groupoid though (but it seems that these two approaches to graph theory are not connected in Mathlib...)