Definition of minors using minor maps

Stream: graph theory

[Chris Wong]

Coq's graph library uses a "minor map" representation for graph minors. A minor map from G to H maps every vertex in H to the set of vertices in G which are contracted into it.

See pages 14–15 of https://hal.science/hal-02316859v2/preview/graphscoq.pdf
And the Coq code: https://github.com/coq-community/graph-theory/blob/34242fdee8c3e1edd455afd10930ded633237a03/theories/core/minor.v#L14-L26

I also started playing with the definitions in Lean here: https://gist.github.com/lambda-fairy/e1d33e968fc0f03683a81319989f7745 (It's a Gist because I'm away from my main machine right now.)

@Kyle Miller how does this compare to the interval idea that you brought up a while ago?

I'm interested in graph minors because I found a nice elegant five-color proof using only deletion/contraction. So we can prove this theorem with only minors and ignore the planar stuff (for now).
https://www.ams.org/journals/proc/1974-045-03/S0002-9939-1974-0345861-4/S0002-9939-1974-0345861-4.pdf

[Chris Wong]

I've still got a few weeks in my holiday, so I'm tempted to push through and try prove five color with what I have. The actual theorem is quite short and I feel well equipped for it.

[Shreyas Srinivas]

Chris Wong said:

Coq's graph library uses a "minor map" representation for graph minors. A minor map from G to H maps every vertex in H to the set of vertices in G which are contracted into it.

See pages 14–15 of https://hal.science/hal-02316859v2/preview/graphscoq.pdf
And the Coq code: https://github.com/coq-community/graph-theory/blob/34242fdee8c3e1edd455afd10930ded633237a03/theories/core/minor.v#L14-L26

I also started playing with the definitions in Lean here: https://gist.github.com/lambda-fairy/e1d33e968fc0f03683a81319989f7745 (It's a Gist because I'm away from my main machine right now.)

Kyle Miller how does this compare to the interval idea that you brought up a while ago?

I'm interested in graph minors because I found a nice elegant five-color proof using only deletion/contraction. So we can prove this theorem with only minors and ignore the planar stuff (for now).
https://www.ams.org/journals/proc/1974-045-03/S0002-9939-1974-0345861-4/S0002-9939-1974-0345861-4.pdf

IIRC, a minor of a graph must be formed by contracting edges, and not deleting vertices and edges. So over all $x\in G$, $\{ toFun\ x\ |\ x\in V\}$ must be a partition

[Shreyas Srinivas]

OTOH, this is fine if we accept wikipedia's definition and allow subgraphs as minors

[Mauricio Collares]

@Shreyas Srinivas I think Diestel defines "Y is a model of X" if you can obtain X by starting from Y and repeatedly contracting edges. Is that the definition you're thinking of?

[Shreyas Srinivas]

Yeah

[Shreyas Srinivas]

But honestly the definition Chris has is better for most uses.

[Shreyas Srinivas]

I have only ever heard someone quibble about how the graph minor was constructed when doing some case analysis in a talk

[Kyle Miller]

I've always heard of a minor of a graph as being the result of deleting edges, deleting vertices, and contracting edges.

[Kyle Miller]

@Chris Wong These minor maps are a neat idea.

I think it would make sense to implement these. (I'm not sure whether it should be minor_map, minor_rmap, or both. I see you implemented minor_rmap.)

I think the interval idea I had still makes sense to have in addition to this. It gives you a type with all the minors of a graph, where minor_rmap gives you a relationship between two graphs. The first can give you different sorts of contraction/deletion relations, since everything is all on the same type.

[Vincent Beffara]

One thing that would make sense is to extend SimpleGraph.map to non-injective maps, and then say that a contraction of a graph G is the map of it via a function with connected fibers, kind of the dual version of your MinorMap. I played a bit with it here https://github.com/vbeffara/lean/blob/main/src/graph_theory/contraction.lean and https://github.com/vbeffara/lean/blob/main/src/graph_theory/pushforward.lean but this was in Lean 3...

[Chris Wong]

Thanks all!

Kyle Miller said:

I think it would make sense to implement these. (I'm not sure whether it should be minor_map, minor_rmap, or both. I see you implemented minor_rmap.)

I'm not sure either. I picked minor_rmap because I noticed the definition of minor_map used the preimage a lot, whereas the _rmapaxioms talked about the function directly. Then again, the paper says that the minor_map formulation is "more convenient", whatever that means. I think it's worth trying both and checking if that claim applies to Lean.

I think the interval idea I had still makes sense to have in addition to this. It gives you a type with all the minors of a graph, where minor_rmap gives you a relationship between two graphs. The first can give you different sorts of contraction/deletion relations, since everything is all on the same type.

That sounds reasonable to me. If we stick to a non-committal name like MinorMap then that can leave space for other representations.

[Kyle Miller]

I think it's similar to how it's helpful having both a Subgraph type and injective graph homomorphisms.

[Kyle Miller]

Something to consider for minor maps: it would be good having, for example, both an analytic and a synthetic notion of "contracting an edge". By 'analytic' I mean that there's a predicate that says "this minor map is the contraction of this edge" and by 'synthetic' I mean there's a construction that gives a minor map that is the contraction of an edge. Contracting edges is a commutative operation, and you should be able to set things up so that at least you can say in an analytic way "given a minor map that is the composition of two edge contractions, then we can factor the minor map as a composition of edge contractions in the opposite order."

You can also state that synthetically, but rather than equalities you need to say that contracting in each order gives isomorphic minors. (And there are plenty of dependent types to wrangle.)

One of the reasons for that interval idea for a Minor type is to be able to state these relations using equalities, without needing to carry anything between different types.

[Chris Wong]

Here's what I've got so far:
https://github.com/leanprover-community/mathlib4/blob/lambda-fairy/minor/Mathlib/Combinatorics/SimpleGraph/MinorMap.lean

One thing I find interesting is that using the minor_rmap approach makes it easy to convert from Hom/Embedding/LE. If we had used minor_map instead, we would needed to use preimages.

[Chris Wong]

Also, the "subgraph" definition in Coq graph-theory wraps an injective hom :thinking:

[Chris Wong]

Hmm, now I'm formalizing contraction, and it seems to favor the opposite direction. If we model contraction as quotienting together a set of connected vertices, then Quotient.mk maps the vertices in the larger graph to the smaller graph. Contrast with deletion / graph homs, which map from smaller to larger.