reasoning about graph classes

Stream: graph theory

[Marcin Pilipczuk]

I was trying to imagine how a formalization of basics of the theory of sparse graphs (aka sparsity, see these lecture notes: https://www.mimuw.edu.pl/~mp248287/sparsity3/) and I realized I don't know what the correct way of stating a property of a graph class is. And the essence of this theory are graph classes, not individual graphs.

For example, let's look at the notion of degeneracy. I want to say that a graph class is degenerate if there exists d such that every graph in the graph class is degenerate. How this statement should look like with the design of SimpleGraph that each has a separate type for its vertex set?

[Shreyas Srinivas]

I think you just define a Set (SimpleGraph V)

[Snir Broshi]

You can also take Set G.Subgraph for a given (G : SimpleGraph V) if you want each member to be able to have a different vertex set (at least until a refactor of SimpleGraph happens that adds vertex sets)

[Shreyas Srinivas]

Like abbrev sparse1 (d :Nat) := { G : SimpleGraph V | G.mad \leq d}

And then you can take (H : sparse d)as an element of this graph in the type theoretic sense

[Shreyas Srinivas]

It will automatically coerce H to an element of the subtype.

[Snir Broshi]

Or you can Set (Σ (V : Type*), SimpleGraph V) for maximum generality, though note that a graph class still has to choose a specific universe of types

[Shreyas Srinivas]

Btw I created a PR #33466 to refactor digraphs to have vertex sets. It’s still sitting in cold storage. Reason no. (n + 1) to have vertex sets. CC :@Yaël Dillies

[Yaël Dillies]

If you don't request my review, I won't review it. I forget about things that don't end up in my github notifications

[Shreyas Srinivas]

Until then we won’t be able to split a graph class into subclasses of a specific vertex set conveniently. You can use @Snir Broshi ‘s Subgraph trick by setting G to be the completeGraph. But because of this ugly separation between SimpleGraph and Subgraph you will have issues like last time.

[Shreyas Srinivas]

Yaël Dillies said:

If you don't request my review, I won't review it. I forget about things that don't end up in my github notifications

Ah sorry. Can I actually explicitly request your review? I thought I had to pick from one of the suggestions. Currently only copilot is suggested for me.

[Yaël Dillies]

Do you not have triage rights? If not, we probably should give them to you!

[Shreyas Srinivas]

I don’t think I have any specific rights

[Shreyas Srinivas]

@Yaël Dillies : I don’t see any option to request reviews to anyone on GitHub other than copilot. So for now I have made a comment tagging you on GitHub

[Shreyas Srinivas]

To return to Marcin’s question I think we need vertex sets to stratify graph classes by cardinality of vertex sets

[Yaël Dillies]

Yep, that worked. It's in my inbox now

[Marcin Pilipczuk]

Shreyas Srinivas said:

I think you just define a Set (SimpleGraph V)

It forces me to use the same vertex set in every graph? That won't work, we need infinite graph classes of finite graphs, so the number of vertices is unbounded.

[Marcin Pilipczuk]

Snir Broshi said:

You can also take Set G.Subgraph for a given (G : SimpleGraph V) if you want each member to be able to have a different vertex set (at least until a refactor of SimpleGraph happens that adds vertex sets)

Yes, using finite subgraphs of complete (SimpleGraph Nat) would work to some extent, but we will hit annoying problems with for example graph products, where it is natural to label vertices by pairs of vertices of the ingredient of the product. With this, one would probably need to explicitly keep track of some functions relabelling the vertices.

[Marcin Pilipczuk]

Snir Broshi said:

Or you can Set (Σ (V : Type*), SimpleGraph V) for maximum generality, though note that a graph class still has to choose a specific universe of types

For a moment, this looks good enough :-)

In graph theory, we usually do not care about "names" the vertices have, and treat isomorphic graphs as the same graphs. This is not formally representable in ZFC, because you cannot have a set of all possible vertex sets, so a formal representation needs to restrict the scope of "labels" for vertices somehow. I guess this is best we can hope for.

[Shreyas Srinivas]

Marcin Pilipczuk said:

Snir Broshi said:

Or you can Set (Σ (V : Type*), SimpleGraph V) for maximum generality, though note that a graph class still has to choose a specific universe of types

For a moment, this looks good enough :-)

In graph theory, we usually do not care about "names" the vertices have, and treat isomorphic graphs as the same graphs. This is not formally representable in ZFC, because you cannot have a set of all possible vertex sets, so a formal representation needs to restrict the scope of "labels" for vertices somehow. I guess this is best we can hope for.

This is true in real math, but in formal math you have to deal with explicit types or sets of vertices, and the mess of equivalences and isomorphisms, congruence of properties over isomoprhisms etc.

[Shreyas Srinivas]

I get your point about being stuck with V. This is why I have been advocating for vertex sets in SimpleGraph since last year.