Path metric

Stream: graph theory

[bottine]

Hey! I need to use the notion of path metric on a graph, and was wondering if:
1) This would be fit for combinatorics/graph_theory
2) If so, anyone would coach me through mergeable code? I'm starting lean and feeling quite overwhelmed by it all, so some quidance would be welcome.
3) Whether it would be better to have a code for a "path metric" associated to any type with a notion of paths that have well-behaved a length. This way, say the path metric of an arbitrary metric space could also be defined more easily.

[Yaël Dillies]

Have a look at #8737 to see what we're on about with paths :smile:

[bottine]

mmh, is that different from what's in the main branch? I think I can already use G.walks x y etc.

[Kyle Miller]

I'm in the process of merging it

[Kyle Miller]

I've only gotten through about 1/3-1/2 of it, I think

[bottine]

ah, so G.walks is recent?

[Kyle Miller]

Yeah, recent to mathlib

[Kyle Miller]

For path metrics, I don't have a good sense of how it should be designed. What sort of theorems do you want to prove?

[bottine]

Well, I mostly want to be able to get the metric space associated to a graph, so no particular theorem. But I feel like having an emetric space would be nice, and I guess something about the distance being realized by some path.

[bottine]

I had the idea that (probably using quivers?) we could define a structure of "paths between two points" + concatenation, inversion, and empty path, and construct the path metric abstractly with this data only. Then the specific graph construction would follow easily, I guess, from what's already there. But I can't even write proofs now, so it's all hot air

[Kyle Miller]

Is there something you're wanting to get to, though? Knowing what you (eventually) want to prove can help guide what will be good as a notion of a metric of a graph. (And guide what kind of graph.)

[bottine]

I'm aiming at formalizing geometric group theory, or at least the basics.

[Yaël Dillies]

Also have a look at branch#hedetniemi. A lot of cool stuff too.

[Kyle Miller]

Is there something like if you choose a metric space structure for a group, then it's unique up to quasi-isometry?

[bottine]

@Yaël Dillies what's that about?

[Yaël Dillies]

Shitov's counterexample to Hedetniemi's conjecture.

[bottine]

@Kyle Miller hum, it's a good question actually. the usual thing is "no matter the choice of finitely many generators", the result is quasi-isometric, but you know that already, I gues

[bottine]

where is that question coming from?

[Kyle Miller]

Because then you might consider using quivers for groups, and have a typeclass to associate some finite generating set for a group, and use all that to give a metric_space on the underyling type of the group, since any other choices lead to something that's quasi-isometric anyway.

[Kyle Miller]

In another topic you brought up Stalling's theorem on ends, right? That seems like a nice sort of theorem to come up a plan for things to formalize. Or maybe even trying to prove subgroups of free groups are free by considering actions on trees?

[bottine]

Indeed for Stalling (that's the long-term goal), but I want to try and cover some general constructs of geometric group theory. So, on one hand, I'd like to have code for coarse Lipschitz maps and quasi-isometries, quasi-isometry groups, etc, eventually leading to a notion of ends for metric spaces. And on the other, I need Cayley graphs, and I'm not sure whether it's better to go directly from finitely generated groups to metric spaces, or first to define the Cayley graph, and the the metric associated to it.

[bottine]

I'll also need to deal with HNN and amalgamated products,… for which I think defining Bass-Serre would perhaps be best, although complicated.

[bottine]

I mean, it's all a bit fuzzy for now… my goals here are probably quite lofty, and for now it's very far away (still can't prove basic things) but we'll see how it fares.

[bottine]

Is there something like if you choose a metric space structure for a group, then it's unique up to quasi-isometry?

I got confused by this question, which I interpreted as "is any metric on G preserved by G (acting on itself by multiplication) quasi-isometric to a metric given by a Cayley graph of a finite generating set", but taking, say, \delta_{x,y} as your metric clearly says this is false.  I wonder now under what conditions a transitive metric is QI to a word metric.

[Kyle Miller]

Let's try to keep some of these lofty goals in mind since we'd want all that work leading up to it to actually be able to support the big theorems :smile:

[bottine]

fair enough :)

[Kyle Miller]

Maybe you could start trying to formalize something in the realm of Bass-Serre theory? Maybe this is too challenging right now, but I think that'd give some ideas of what you'd need to be able to set things up correctly?

[Kyle Miller]

(And full disclosure: I merely have colleagues who are geometric group theorists, and I went through part of Office Hours with a Geometric Group Theorist with one of my DRP students. I've seen some of Stallings's work because of its applications to 3-manifolds, which are more my interest.)

[bottine]

The problem with Basse-Serre is that I'm really not familiar with it, and it's not "elementary", as say the Cayley graph is, so I fear I'd get lost trying to work both fronts (math + formalization), but maybe not. What makes you think Bass-Serre is a good place to start?

[Kyle Miller]

I'm afraid that Cayley graphs might be too elementary to see what problems there might be in formalization

[Kyle Miller]

Can you remind me how ends work with respect to groups and group actions in geometric group theory?

[bottine]

mmh, I see. Say I start with B-S, then I stumble upon problems-in-factorization. What kind of problems should I expect, or more to the point, what kind of scenario "problem-reaction" can come up?

[Kyle Miller]

Isn't there something where you study groups acting by quasiisometries on spaces? And then there's a map from ends of the group to ends of the space? (Is this where you need Cayley graphs, to be able to define the right kind of action here?

[bottine]

huh, well, ends are "directions at infinity", and you can see that they are QI-invariant. Then by an argument that I tried to do in my head this night but didn't manage, you can see that in the case of finitely generated groups you have 0,1,2 or infinitely many ends.

[bottine]

I don't know about that, but that sounds like a reasonable path to Stalling actually (I think you're not less knowledgeable about this than I am)

[Kyle Miller]

What I was thinking with Bass-Serre is sort of simple: you've got this graph of groups, and you want to make a group out of it. There's a question of just how do you represent all this data. Ideally so that you can easily represent HNN extensions and amalgamated products.

[bottine]

there is this Svarc-Milnor result about your group acting on a space and getting its geometry out of that.

[bottine]

right: I recently saw a paper dealing only with groupoids, which removes some arbitrary choices

[bottine]

then you have the "fundamental groupoid" instead of the fundamental group, and "action on a forest" instead of "action on a tree"

[bottine]

The nice thing with B-S is that then you get Nielsen-Schreier and Kurosh and Grushko almost for free I believe.

[Kyle Miller]

Another nice checkpoint that's come to mind is being able to show different basic groups are hyperbolic (esp. the free group of course)

[bottine]

yeah, lots of things :) which is a bit overwhelming

[bottine]

also amenability, but I figured having a robust base involving Cayley graphs, the metric, and all the basic quasi-isometry vocabulary is a good place to start (also allowing to learn the language)

[Kyle Miller]

It's sounding like using quiver to model a Cayley graph on a group G will be a good plan (and if not, sorry ahead of time :smile:)

[Kyle Miller]

I'm not sure how you'd go about giving a group a metric structure, but you can always start by doing it for presented_group and see how that goes

[bottine]

alright, thanks for the insights !

[Kyle Miller]

You can also ask @David Wärn about path metrics in quivers, maybe when you get to that point, creating a post in #Is there code for X? and pinging him by invoking his name like I did. He's not subscribed to this stream so he won't see this one.

[Kyle Miller]

I don't really know what he's doing with quivers, other than I noticed a PR or two in the past month.

[Kevin Buzzard]

@bottine having big goals seems to work really well here. Even if you don't make it there, the process of trying to figure out how to get there makes mathlib grow in what are "clearly the right directions". And then later on if someone else enthusiastic comes along with similar goals they start where you stopped. The key is to aim for theorems which should be feasible, even if they're a long way away. Geometric group theory would be a brilliant thing to work towards in Lean and we certainly get passers-by who express an interest in this area. You'll certainly find people here who are happy to help if you make a start, and working on a project is by far the best way to learn Lean.

[bottine]

That's a motivating thought :)

[Rémi Bottinelli]

@Kyle Miller I was wondering what the status was for a metric on a simple graph. I see @Vincent Beffara has working code. What do you think would be needed to get something merged?

[Vincent Beffara]

As far as I understand, there is a big design question about whether connected_graph should be a class or an assumption, and minor questions that I still have about using well_founded.min on the range of the distance function or nat.find, and I was waiting on that before sending a PR, but if it is something you are interested in right now I could clean up the code a little and submit, see what happens

[Sebastien Gouezel]

If it is a class, then it makes it possible for typeclass inference to find the metric space structure on the graph. Which looks like a good idea to me!

[Vincent Beffara]

Right now it is

[Rémi Bottinelli]

Gladly, yeah. Is nat.find maybe preferred for computability reasons?

I'd like to give a try at formalizing ends of a graph, and it seems a good idea to have the metric at hand for this.

[Vincent Beffara]

nat.find has a nicer API, but I had trouble with it because "the smallest int such that there exists something" made it difficult for lean to infer implicit arguments. well_founded.min is closer to the metal

[Vincent Beffara]

The graph structure itself OTOH is not a class at the moment

[Vincent Beffara]

Also I had a question about whether connectivity in a graph should be defined as refl_trans_gen G.adj x y or as nonempty (G.walk x y), but these are equivalent modulo computability issues on which I understand very little - though the definition would need to be in mathlib before that of the distance

[Vincent Beffara]

(although now I would choose the nonempty version because it feels more general wrt other types of graph-like objects)

[Rémi Bottinelli]

fwiw, I feel like nonempty (…) at least has the advantage of readability: it's immediately clear that it's says what it should

[James Gallicchio]

Vincent Beffara said:

these are equivalent modulo computability issues

(what are the computability issues?)

[Kyle Miller]

@Vincent Beffara Is your branch up to date? I have a PR with basic definitions but not metrics, and I can merge in what you have here to check that it's compatible.

Regarding classes, I hesitate to make connected_graph a class, and I'm not sure it would help the problem of making graphs be metric spaces since they're not types so they can't be metric spaces anyway (it would make sense to me for docs#quiver to have a connected class if it doesn't already have one). I tend to think of classes being used for values whose representations you think will remain fixed, and simple graphs can potentially change, similar to morphisms being rewritten.

[Kyle Miller]

Vincent Beffara said:

The graph structure itself OTOH is not a class at the moment

Just to clarify, graphs will always be terms. Any classes we have will just be about having an interface to get things like the graph's adj relation, which will, generally speaking, ultimately have to be stored within the graph term.

[Kyle Miller]

Vincent Beffara said:

refl_trans_gen G.adj x y or as nonempty (G.walk x y), but these are equivalent modulo computability issues

I believe you can strengthen your equivalence relation there and just say they're equivalent. Anything that's Prop-valued is going to be computationally irrelevant, and to use them in computation you need to use decidable_rel instances.

[Vincent Beffara]

Kyle Miller said:

Vincent Beffara Is your branch up to date? I have a PR with basic definitions but not metrics, and I can merge in what you have here to check that it's compatible.

My branch is up to date, I merged mathlib on March 8 after your updates to simple_graph and it builds fine. In path.lean I put basic definitions about connectivity, hopefully they match yours :-)

[Kyle Miller]

@Vincent Beffara I took another chunk of one of my branches and mixed in a chunk of your branch: #12574

I think it's best to just go with a noncomputable graph metric for now. We can add a computable algorithm later, but Inf is mathematically more convenient.

This is still a draft, but it shouldn't be too much more work. Please let me know what you think!

[Vincent Beffara]

Nice, I just had a look.

I still have trouble with the whole junk value thing, especially since here we use nat.Inf_eq_zero where the garbage value is explicitly 0 and not something like 42. I would feel better defining an edist with infinite value when the vertices are not connected. That's a minor issue anyway.

How about a metric_space instance then?

[Kyle Miller]

Yeah, some enat-valued metric would be good for the case of disconnected graphs. I figured that we can define that once there's a need for it (probably most things will be about connected graphs).

We can't have that metric_space instance, unfortunately, because if both G and G' are connected simple graphs on vertex type V, they'd give conflicting metric_space V instances.

[Yaël Dillies]

You mean enat-valued, not pnat-valued, right?

[Kyle Miller]

Potentially in the future we might have G.V being the vertex type, and it would be safe to do metric_space G.V, but that would probably cause difficulties with simple_graph V because V and G.V wouldn't syntactically be the same.

For metric_space, I still think you'd rather be dealing with quiver, since that's attaching a graph structure to a particular type. There could be

def G.quiver := V

instance : quiver G.quiver := ...

or something like that if you do want to work with the graph type.

[Vincent Beffara]

Wait, can't we just define the instance and use letI? It would be unfortunate to define a graph metric and then not be able to use the whole metric space API with it

[Yaël Dillies]

That's what we were going for :wink:

[Yaël Dillies]

But it's not an "instance" anymore. That's the point.

[Vincent Beffara]

I don't get your point. Isn't it an instance that is not discovered by typeclass inference?

[Yaël Dillies]

What we call instances are precisely the definitions which are discoverable by typeclass inference.

[Yaël Dillies]

instance = @[instance] def

[Kyle Miller]

A rule of thumb for typeclasses: metric_space V should be a function of V. Things can get very difficult when you violate this, even with letI.

[Kyle Miller]

This is why I keep suggesting that you use quiver, since it's designed in such a way that this rule won't be violated.

[Yaël Dillies]

Kyle Miller said:

Things can get very difficult when you violate this, even with letI.

Really? I would like an example because I really can't see would go wrong if you endow V with the metric coming from one graph.

[Vincent Beffara]

Ah but we want to endow V with the metrics coming from different graphs sometimes (e.g. two Cayley graphs on the same group are quasi-isometric)

[Kyle Miller]

Yeah, I was going to answer Yael by mentioning Cayley graphs.

[Vincent Beffara]

If I can ask, what exactly is solved by using quiver? Can't there be two different quivers on the same Type like for a simple_graph?

class quiver (V : Type u) := (hom : V → V → Sort v)
class graph_like (V : Type u) := (adj : V → V → Prop)

these look identical to me ...

[Yaël Dillies]

If you want several metrics then yeah you're screwed.

[Sebastien Gouezel]

Just passing by, but the Cayley graph of a group G associated to a generating set S should probably be a type synonym cayley G S, which can be endowed with a canonical metric.

[Yaël Dillies]

Yes, but quiver is a class, meaning that we vow not to ever declare twice quiver α for any α.

[Yaël Dillies]

(or rather declare as an instance)

[Vincent Beffara]

Yaël Dillies said:

Yes, but quiver is a class, meaning that we vow not to ever declare twice quiver α for any α.

I'm not ready to vow not to ever define different graphs on the same vertex set (especially given that I would rather define a probability measure on the set of all those graphs on the same vertex set).

[Kyle Miller]

@Sebastien Gouezel That's exactly what I had in mind with my suggestion

[Kyle Miller]

Here's a link to an example implementation, not to say it's how it should go.

[Vincent Beffara]

I think I get it now, I had completely missed the implication about multiple definitions being prohibited and was scratching my head trying to figure out how replacing Prop with Sort v was helping in any way. Thanks for the clarification!

[Kevin Buzzard]

topological_space is a class and yet we still manage to do things like define (and use) a lattice structure on the type of topological space structures on a type