Clique

Stream: graph theory

[Yaël Dillies]

@Kyle Miller, are you happy with this definition of cliques, or do you want them to be images of graph embeddings or something similar?

/-- A `n`-clique in a graph is a set of `n` vertices which are pairwise connected. -/
def is_n_clique (n : ℕ) (s : finset α) : Prop := s.card = n ∧ (s : set α).pairwise G.adj

[Arthur Paulino]

Does it make sense to use complete_graph to define cliques?

[Yaël Dillies]

That was my question, because they are embeddings of complete graphs.

[Arthur Paulino]

I know you didn't ask me but I'm practicing my Lean reasoning :sweat_smile:
Maybe it's good to characterize cliques as you're proposing and then prove that complete_graphs are cliques

[Kyle Miller]

That seems like a reasonably straightforward definition, though another option is to say that a subgraph is a clique:

def is_complete (G : simple_graph V) : Prop := set.univ.pairwise G.adj
def subgraph.is_clique {G : simple_graph V} (G' : G.subgraph) : Prop := G'.coe.is_complete
lemma subgraph.is_clique_prop {G : simple_graph V} (G' : G.subgraph) : G'.verts.pairwise G'.adj := sorry

I guess a question is what is a clique? Is it the vertex set like in your definition, or is it important that it's a subgraph? (Can this difference matter for multigraphs?)

[Mauricio Collares]

I just took a look at the literature, and this is even more of a mess than I remembered! Both Bollobás and Harary define it as a maximal complete subgraph (I found the "maximal" part very surprising!), while Bondy--Murty defines it as a vertex set inducing a complete subgraph. So none of them define it the way I expected it to! Diestel just avoids using the word "clique" altogether, except in the context of "clique number".

[Kyle Miller]

Interesting. It seems like it would be good having cliques and maximal cliques distinguished (the set of all cliques, including non-maximal ones, forms a simplicial complex, which seems like interesting structure to have around).

[Kyle Miller]

Though it does seem common to have a clique be, specifically, the subset of vertices, and not the subgraph.

[Yaël Dillies]

So, should I PR the above definition and call it a day?

[Kyle Miller]

Do cliques have to be finite subsets though?

def simple_graph.is_clique (G : simple_graph V) (W : set V) : Prop := W.pairwise G.adj

[Yaël Dillies]

No, but with your definition I can't say that something is a triangle.

[Kyle Miller]

It might also be nice if this were a set

def simple_graph.cliques (G : simple_graph V) : set (set V) := {W | W.pairwise G.adj}

since then it has a lattice structure, and talking about maximality is easier.

[Yaël Dillies]

My goal is to be able to say that something is a triangle.

[Kyle Miller]

Maybe this?

def simple_graph.is_triangle (G : simple_graph V) (W : finset V) : Prop :=
W.card = 3 /\ (W : set V) \in G.cliques

[Kyle Miller]

If you want, you can make is_triangle be is_n_clique and generalize 3

[Kyle Miller]

So, in short, use your original definition but factoring out this cliques set would be nice

[Arthur Paulino]

If we have a way to characterize n-cliques we will be able to prove lower bounds of n for the chromatic number

[Kyle Miller]

@Arthur Paulino The general version is something like

example (C : G.proper_coloring α) (W : set V) (h : W ∈ G.cliques) :
  function.injective (C ∘ coe : W → α) :=
sorry

and then you can use this when things are finite to show that W.card <= card α and then bound the chromatic number.