Set in definition of Graph

Stream: graph theory

[Jakub Nowak]

I remember reading discussion about this, but I cannot find it on Zulip. Can someone help me find it?

[Snir Broshi]

The title reminds me of #graph theory > (Undirected) hypergraphs @ 💬 but idk if that's what you meant

[Jakub Nowak]

In the definition of docs#Graph, there's vertexSet and edgeSet. I think the other idea was to not have them, in other words basically assume that vertexSet/edgeSet are Set.univ.

[Jakub Nowak]

Oh, maybe I should just look at the commit history for docs#Graph.

[Jakub Nowak]

Ah, yes, I found it.
#graph theory > What kind of graphs are in Mathlib already?
#PR reviews > #24122 Multigraphs

[Snir Broshi]

btw in case you missed it: https://github.com/leanprover-community/mathlib4/pull/31120#issuecomment-3562965722

[Snir Broshi]

I guess this means refactoring SimpleGraph to use a Set

[Jakub Nowak]

Snir Broshi said:

I guess this means refactoring SimpleGraph to use a Set

Well, this already exists as docs#Graph and docs#SimpleGraph.Subgraph.

[Peter Nelson]

@Yaël Dillies @Bhavik Mehta, do you mind elaborating on the github comment linked above?

[Yaël Dillies]

The idea would be to switch to the sort of SimpleGraph definition @Alex Kontorovich wrote in google-deepmind/formal-conjectures#296, and then subgraphs can have the same type as graphs

[Bhavik Mehta]

Essentially the definition that we'd discussed privately in the past, Peter!

[Kevin Buzzard]

This doesn't solve the problem of contractions though, right? You could go even further and have an equivalence relation on V as well, with two terms of type V equivalent meaning "these are the same vertex" and adjacency behaving well wrt this equivalence relation. Then you can contract, delete and add edges to your heart's content.

[Peter Nelson]

We've experimented with that, Kevin, and it seems to be a pain. You have this explicit equivalence relation that needs to carry forward to structure definitions such as walks/paths, and you have to pay enough attention to the equivalence relation explicitly that it becomes a large cognitive load. As I expressed in the other topic, I am leaning more towards the idea the 'retraction' point of view is best for minors.

[Alex Kontorovich]

Yes, I remember messing around with this a while ago. My various attempts at quotienting the vertex set led to subtype hell, and it came out much nicer to just track the equivalence relation explicitly, without changing the underlying types... I think my latest attempt was here: #maths > Graph Minors @ 💬 which was already a while ago... Has there been any progress since then?

[Shreyas Srinivas]

Oh this vertex set thing? I recall offering to make the PR six months ago on discord but @Bhavik Mehta said it wasn’t likely to get a timely review at that time.

[Shreyas Srinivas]

I wanted it partly because we were working on Berge’s lemma and it was frustrating to coerce subgraphs to SimpleGraph.

[Snir Broshi]

Yaël Dillies said:

The idea would be to switch to the sort of SimpleGraph definition Alex Kontorovich wrote in google-deepmind/formal-conjectures#296, and then subgraphs can have the same type as graphs

Sounds good, btw do you think there's a good way to incorporate #4127 into this? (a HasAdj typeclass + instances for Digraph and SimpleGraph)
Also do you have a timeline in mind? Or are you looking for people to take this on? (no pressure)

[Yaël Dillies]

Right now, all my refactoring energy is spent on monoid algebras in #25273. You should feel free to take this refactor on.

[Yaël Dillies]

The HasAdj design is not fleshed out enough that we can use it, and IMO it is more or less orthogonal to making simple graphs supported on a set. Therefore I'd say "don't worry about it"