Zulip Chat Archive

Stream: graph theory

Topic: infinite union of graphs

Bhavik Mehta (Aug 21 2020 at 19:25):

Something interesting to think about: is there a nice way of doing this construction in Lean? For instance can you show that if G has no cycles of length four, then ext G is a friendship graph

Kyle Miller (Aug 21 2020 at 19:32):

What kind of union? A disjoint union, or a union of subgraphs within a particular universal graph?

Kyle Miller (Aug 21 2020 at 19:34):

Because, rather than defining subgraph G to be a bounded lattice, it could be defined to be a complete lattice, so then an infinite union would be the sup of an indexed family of subgraphs. (For example, G could be a complete graph on some given vertex type.)

Kyle Miller (Aug 21 2020 at 19:37):

What's ext G? (Is it something from Ramsey theory?)

Bhavik Mehta (Aug 21 2020 at 21:17):

Oh oops I meant to attach a picture - sorry

Bhavik Mehta (Aug 21 2020 at 21:18):


Bhavik Mehta (Aug 21 2020 at 21:19):

In particular in this setting when you're just given G, there's not an ambient graph in which all your subgraphs do form a lattice, so just taking sup like you mention isn't immediate

Kyle Miller (Aug 22 2020 at 04:04):

Having colimits of graphs like that would be nice, though in this case you could define ext G using a sup construction on subgraphs of the complete graph on the set of binary trees with leaves being labeled by vertices of G:

variables {α : Type u} [simple_graphs α]

inductive all_deriv_verts (G : α)
| incl (v : V G) : all_deriv_verts
| pair (v w : all_deriv_verts) : all_deriv_verts

def total (G : α) := complete_graph (all_deriv_verts G)

Here, total G is the graph that's universal.

Bhavik Mehta (Aug 22 2020 at 13:16):

I suspect you want pair to take a sym2 or finset of size 2 rather than an ordered pair, but yeah I can see that works

Kyle Miller (Aug 22 2020 at 16:56):

Oh, good catch

Last updated: Aug 03 2023 at 10:10 UTC