## Stream: graph theory

### Topic: Clique

#### Yaël Dillies (Nov 10 2021 at 14:43):

@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 (Nov 10 2021 at 14:52):

Does it make sense to use complete_graph to define cliques?

#### Yaël Dillies (Nov 10 2021 at 15:03):

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

#### Arthur Paulino (Nov 10 2021 at 15:22):

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 (Nov 10 2021 at 16:32):

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 (Nov 10 2021 at 16:45):

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 (Nov 10 2021 at 17:04):

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 (Nov 10 2021 at 17:07):

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

#### Yaël Dillies (Nov 10 2021 at 17:09):

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

#### Kyle Miller (Nov 10 2021 at 17:09):

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 (Nov 10 2021 at 17:11):

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

#### Kyle Miller (Nov 10 2021 at 17:12):

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 (Nov 10 2021 at 17:12):

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

#### Kyle Miller (Nov 10 2021 at 17:14):

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 (Nov 10 2021 at 17:14):

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

#### Kyle Miller (Nov 10 2021 at 17:15):

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

#### Arthur Paulino (Nov 10 2021 at 17:17):

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 (Nov 10 2021 at 17:25):

@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.

Last updated: Aug 03 2023 at 10:10 UTC