# Zulip Chat Archive

## 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_graph`

s 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: Dec 20 2023 at 11:08 UTC