Cayley and circulant graph

Stream: mathlib4

[Bhavik Mehta]

Edward van de Meent said:

let me point out that mathlib's definition for the cayley graph (docs#SimpleGraph.circulantGraph, horrible name imo)

That's because this is the circulant graph rather than the general cayley graph!

[Edward van de Meent]

why is it that not (the general definition for) the cayley graph?

[Edward van de Meent]

the definition in mathlib seems like the exact definition of the cayley graph, modulo commutativity/existance of inverse

[Edward van de Meent]

and if i can trust the wikipedia definition, docs#circulantGraph is only a circulant graph when the group is cyclic

[Bhavik Mehta]

(moved this discussion since it's unrelated to the previous)

[Bhavik Mehta]

Yeah, I think you're right - it was intended to be a general definition of circulant graph but I hadn't realised it ended up being Cayley graphs! There's still a distinction in that Cayley graphs typically want their edges labelled by the generator which corresponds to it, and Cayley graphs should be allowed to be multiplicative. But you're right that the current version is essentially an unlabelled Cayley graph! (The history here is that I wanted Paley graphs for computing small Ramsey numbers, and those are nicely generalised as circulant graphs, and cycle graphs are too)

[Edward van de Meent]

should i make a renaming/generalizing PR?

[Snir Broshi]

By "generalizing" do you mean @[to_additive]?

[Bhavik Mehta]

Edward van de Meent said:

should i make a renaming/generalizing PR?

Yeah that'd be good :)

[Edward van de Meent]

yes, and also generalizing to a Semigroup or even Mul context

[Edward van de Meent]

although to be honest, that might get a bit much for a single PR...

[Edward van de Meent]

as in, having SimpleGraph.cayley in the Circulant.lean folder might be confusing...

[Snir Broshi]

That sounds good, but it's worth noting that while this file is barely imported I'd rather it didn't accrue many imports, so that it'll still be okay to import it from other places without it being a significant import

[Edward van de Meent]

let me see where i get...

[Bhavik Mehta]

Bear in mind that the current circulant graph is used to define the cycle graph, and as Snir says, that probably shouldn't have too many big imports. It might be reasonable to have the defs in one file, just enough to get (actual) circulant and cycle graphs, and put the group-theoretically-interesting stuff in a later file

[Snir Broshi]

If there are nice results to be had that use imports from algebra maybe separating cycleGraph from circulantGraph is a good solution

[Edward van de Meent]

/poll What should the PR do? (also naming-wise)
create SimpleGraph.cayley
create SimpleGraph.mulCayley
create SimpleGraph.addCayley
add API (free space for the bingoers)
rename the file/create a folder Cayley.lean
rename add a different file/folder Cayley.lean

[Bhavik Mehta]

I've picked the options I think should happen, at the moment I don't have a strong preference whether it's one or two PRs.

[Vlad Tsyrklevich]

Without labelled generators it seems difficult to use in many of the places you'd use a Cayley graph. Incidentally I had at some point started formalizing some theory for cayley graphs here but I think the feedback I got was the right generality was to formalize Schreier coset graphs #mathlib4 > How to structure Cayley graph API @ 💬 (or at the very least they really should be defined for non-simple digraphs where we have no API.)

[Vlad Tsyrklevich]

Anyways, the cycle graph should probably be redefined to drop the import requirements on groups. I have two PRs related to cycleGraphs right now so I'd be happy to take that (independent of whatever choice is made above)

[Edward van de Meent]

Vlad Tsyrklevich said:

the feedback I got was the right generality was to formalize Schreier coset graphs

in the sense that you'd define Adj u v via ∃ g, g • u = v? (i'm not very familiar with the definitions in this field)
I've thought about this, but i'm not sure how to formally generalize the fact that you want G to induce a (left) graph action if G is not commutative?

[Edward van de Meent]

informally, you could say "let G have a left and right action on X" such that (g •> u) <• f = g •> (u <• f), define the graph using the right action, and show that the left action induces a graph hom (modulo one of the actions being cancellative because simple graphs are irreflexive), but i'm not sure what the right phrasing in lean would be

[Snir Broshi]

Vlad Tsyrklevich said:

Without labelled generators it seems difficult to use in many of the places you'd use a Cayley graph.

If you mean edge labels, we can define a function alongside the cayley one that returns docs#SimpleGraph.EdgeLabeling. For the general Monoid case the labeling can return a set, and for a LeftCancelMonoid it can return an element since it's unique.

[Edward van de Meent]

actually it won't be unique (i think) since SimpleGraph isn't directed...

[Edward van de Meent]

can someone point me to an example where one needs this kind of labeling?

[Edward van de Meent]

for now i made a PR at #35084

[Vlad Tsyrklevich]

Edward van de Meent said:

can someone point me to an example where one needs this kind of labeling?

Looking at the API for circulantGraph again I take back my statement. I misunderstood the definition and what it allowed.

[Daniel Zhou]

Hi! I wanted to flag that I've opened #35467, which takes the quiver-based Schreier coset graph approach mentioned by @Vlad Tsyrklevich earlier in this thread. It defines Schreier graphs, Cayley graphs with labeled edges and covering properties, connectivity, and vertex-transitivity, building on the Lean 3 PR leanprover-community/mathlib3#18693.

I think this complements @Edward van de Meent's #35084 — the quiver approach handles directed labeled graphs with covering theory, while mulCayley/addCayley handles the undirected SimpleGraph
case. The PR also includes Cayley sum graphs (u + v ∈ s) as a separate SimpleGraph construction, which is distinct from both approaches.

Happy to coordinate if there are any concerns about overlap!