infinite union of graphs

Stream: graph theory

[Bhavik Mehta]

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]

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

[Kyle Miller]

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]

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

[Bhavik Mehta]

Oh oops I meant to attach a picture - sorry

[Bhavik Mehta]

image.png

[Bhavik Mehta]

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]

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]

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]

Oh, good catch