[Merged by Bors] - feat(Combinatorics/SimpleGraph): A graph has 3-clique iff it has a cycle of length 3

[Rida-Hamadani]

This is nice to have because when combined with is3Clique_iff, we will be able to prove that a graph has a cycle by just proving that 3 vertices are pairwise adjacent.

---

[eric-wieser]

Am I right in saying this is true as an Equiv between subtypes too?

[Rida-Hamadani]

I think so too, but I'm not sure how to state it that way (I'm new to Lean). Do you have any suggestions?

[semorrison]

We discussed this in the FRO office hours this morning, and I think @Rida-Hamadani is looking into this now.

[Rida-Hamadani]

Yes, but I'm doubting the existence of an Equiv now. At least this Equiv:

{s : Finset α // G.IsNClique 3 s} ≃ (u : α) × {w : G.Walk u u // w.IsCycle ∧ w.length = 3}

My reasoning is that any function that maps length 3 cycles to 3-cliques will not be injective, since let's say s = {a, b, c}, then the following cycles will map to s: abc, bca, cab, etc.

As I understand the way walks are defined in mathlib, lean treats the cycles above as different. Maybe an Equiv can be established if there is a way to tell lean that these cycles are the same?

Do you agree @eric-wieser ?

[kmill]

To state this Equiv right, you need to quotient the right-hand side by cycle rotation and reversal. That seems like more trouble than it's worth if no one needs it right now, so I'm happy with this theorem stated as an iff.

By the way, the mathlib way of defining a cycle is how many graph theory textbooks define them. One of those technical details combinatorialists sweep under the rug is the difference between (1) a cycle graph, (2) a subgraph that's a cycle, (3) a collection of vertices that form a cycle, and (4) a walk that's a cycle. The definition of G.Walk is the fourth, and this theorem is relating the third and the fourth. At least the second and third are "the same" using induced graphs, but there are more of the fourth than the third due to reflections and rotations.

Combinatorialists can navigate these by force of pure intuition, but in mathlib we have to fill in the gaps.

[Rida-Hamadani]

Thank you for the insights! I think that if someone has to go through the trouble of formulating this Equiv and proving it, then it should be between (3) and (4) in general instead of it being just the case where the number of vertices is 3, and as far as I know, the general definition of (3) doesn't seem to exist yet, adding even more work to be done.

Maybe I (or someone else) will work on this later on, but until then, I think it is convenient to have a way to deduce that 3 adjacent vertices give a cycle. The whole reason I proved this statement is to use that fact in a proof of the Hoffman-Singleton theorem.

[YaelDillies]

To state this Equiv right, you need to quotient the right-hand side by cycle rotation and reversal. That seems like more trouble than it's worth if no one needs it right now, so I'm happy with this theorem stated as an iff.

Actually, there is another solution, which is to add the cycle rotation and reversal on the LHS:
{f : Fin 3 → α // G.IsNClique 3 s} ≃ ∑ u : α, {w : G.Walk u u // w.IsCycle ∧ w.length = 3}
But that's far enough away from the current statement that it's worth having the statement anyway.

[YaelDillies]

Thanks!

maintainer merge

[github-actions]

🚀 Pull request has been placed on the maintainer queue by YaelDillies.

[jcommelin]

Thanks 🎉

bors merge

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Check all files imported
• Lint style