induced graphs, cliques, coloring bounds

Stream: graph theory

[Kyle Miller]

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]

I wonder if there's a shorter proof for clique_free_iff

[Yaël Dillies]

Me too. The current proof is scary!

[Kyle Miller]

(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]

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]

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]

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]

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)