## Stream: graph theory

### Topic: induced graphs, cliques, coloring bounds

#### Kyle Miller (May 08 2022 at 19:28):

In #14034, I took a stab at defining induced graphs to get characterizations of cliques in terms of induced graphs being complete graphs and to get lower bounds on chromatic numbers from existence of cliques.

After messing with things for a while, it seems like the easiest thing is to have two different types of induced graphs. The first is simple_graph.induce, which takes a simple_graph V and produces a simple_graph s by just restricting the vertex set. The second is simple_graph.subgraph.induce, which takes a G.subgraph and produces another G.subgraph. They both seem useful and have different properties, similar to edge deletion.

With this PR, you can express that a set s of vertices forms a clique by G.induce s = ⊤. This is harder to express using simple_graph.subgraph.induce without, say, introducing an additional simple_graph.subgraph.is_complete predicate.

#### Kyle Miller (May 08 2022 at 19:29):

I wonder if there's a shorter proof for clique_free_iff

#### Yaël Dillies (May 08 2022 at 19:29):

Me too. The current proof is scary!

#### Kyle Miller (May 08 2022 at 19:33):

(Ping: @Joseph Hua I know you were doing some things with induced graphs a while back, and I started with a bit of code of yours from the Zulip. Let me know if you you have anything that we should try merging, and if you want to be listed as a coauthor feel free to add your name and/or add a Co-authored-by in the PR summary.)

#### Yaël Dillies (May 08 2022 at 19:34):

It would be very cool to have induced subgraphs because then I could upgrade our triangle removal to Jacob Fox's graph removal.

#### Kyle Miller (May 08 2022 at 19:46):

Just as a note to the future, some things I started implementing for this PR but deleted:

• if G' : G.subgraph, the map from G'.coe.subgraph to G.subgraph
• the map from simple_graph s to G.subgraph by intersecting with the induced subgraph
• lemmas for double applications of simple_graph.induce (I didn't want to figure out the right way to handle the subtypes)
• vertex deletion for simple_graph (may as well just induce using the complement?)
• a simple_graph.subgraph.is_complete predicate (may as well use G'.coe = ⊤?)

#### Kyle Miller (May 08 2022 at 19:51):

Yaël Dillies said:

It would be very cool to have induced subgraphs because then I could upgrade our triangle removal to Jacob Fox's graph removal.

Then make sure to give #14034 a review at your convenience :smile:

#### Joseph Hua (Jul 02 2022 at 17:04):

Kyle Miller said:

(Ping: Joseph Hua I know you were doing some things with induced graphs a while back, and I started with a bit of code of yours from the Zulip. Let me know if you you have anything that we should try merging, and if you want to be listed as a coauthor feel free to add your name and/or add a Co-authored-by in the PR summary.)

Hi there, sorry I never actually started working on formalising graph theory, as I got absorbed into other projects! (and sorry for the late replay I haven't checked Zulip in a while)

Last updated: Aug 03 2023 at 10:10 UTC