## Stream: graph theory

### Topic: Path metric

#### bottine (Jan 25 2022 at 15:27):

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 (Jan 25 2022 at 15:28):

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

#### bottine (Jan 25 2022 at 15:31):

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

#### Kyle Miller (Jan 25 2022 at 15:31):

I'm in the process of merging it

#### Kyle Miller (Jan 25 2022 at 15:31):

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

#### bottine (Jan 25 2022 at 15:32):

ah, so G.walks is recent?

#### Kyle Miller (Jan 25 2022 at 15:32):

Yeah, recent to mathlib

#### Kyle Miller (Jan 25 2022 at 15:33):

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 (Jan 25 2022 at 15:34):

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 (Jan 25 2022 at 15:37):

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 (Jan 25 2022 at 15:37):

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 (Jan 25 2022 at 15:37):

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

#### Yaël Dillies (Jan 25 2022 at 15:38):

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

#### Kyle Miller (Jan 25 2022 at 15:38):

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

#### Yaël Dillies (Jan 25 2022 at 15:40):

Shitov's counterexample to Hedetniemi's conjecture.

#### bottine (Jan 25 2022 at 15:40):

@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 (Jan 25 2022 at 15:42):

where is that question coming from?

#### Kyle Miller (Jan 25 2022 at 15:42):

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 (Jan 25 2022 at 15:48):

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 (Jan 25 2022 at 16:57):

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 (Jan 25 2022 at 16:58):

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 (Jan 25 2022 at 17:01):

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 (Jan 25 2022 at 17:07):

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 (Jan 25 2022 at 17:07):

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:

fair enough :)

#### Kyle Miller (Jan 25 2022 at 17:11):

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 (Jan 25 2022 at 17:12):

(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 (Jan 25 2022 at 17:13):

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 (Jan 25 2022 at 17:14):

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

#### Kyle Miller (Jan 25 2022 at 17:16):

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

#### bottine (Jan 25 2022 at 17:16):

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 (Jan 25 2022 at 17:17):

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 (Jan 25 2022 at 17:18):

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 (Jan 25 2022 at 17:19):

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 (Jan 25 2022 at 17:19):

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 (Jan 25 2022 at 17:19):

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

#### bottine (Jan 25 2022 at 17:20):

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

#### bottine (Jan 25 2022 at 17:20):

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

#### bottine (Jan 25 2022 at 17:21):

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

#### Kyle Miller (Jan 25 2022 at 17:21):

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 (Jan 25 2022 at 17:22):

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

#### bottine (Jan 25 2022 at 17:23):

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 (Jan 25 2022 at 17:23):

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 (Jan 25 2022 at 17:25):

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 (Jan 25 2022 at 17:30):

alright, thanks for the insights !

#### Kyle Miller (Jan 25 2022 at 17:31):

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 (Jan 25 2022 at 17:31):

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 (Jan 25 2022 at 20:25):

@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 (Jan 26 2022 at 07:49):

That's a motivating thought :)

#### Rémi Bottinelli (Mar 10 2022 at 14:34):

@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 (Mar 10 2022 at 14:42):

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 (Mar 10 2022 at 14:44):

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!

Right now it is

#### Rémi Bottinelli (Mar 10 2022 at 14:44):

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 (Mar 10 2022 at 14:46):

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 (Mar 10 2022 at 14:47):

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

#### Vincent Beffara (Mar 10 2022 at 14:52):

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 (Mar 10 2022 at 14:53):

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

#### Rémi Bottinelli (Mar 10 2022 at 14:56):

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 (Mar 10 2022 at 15:39):

Vincent Beffara said:

these are equivalent modulo computability issues

(what are the computability issues?)

#### Kyle Miller (Mar 10 2022 at 18:33):

@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 (Mar 10 2022 at 18:35):

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 (Mar 10 2022 at 18:38):

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 (Mar 10 2022 at 19:38):

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 (Mar 10 2022 at 20:02):

@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 (Mar 10 2022 at 20:32):

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 (Mar 10 2022 at 21:33):

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 (Mar 10 2022 at 21:34):

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

#### Kyle Miller (Mar 10 2022 at 21:43):

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 (Mar 10 2022 at 21:45):

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 (Mar 10 2022 at 21:46):

That's what we were going for :wink:

#### Yaël Dillies (Mar 10 2022 at 21:46):

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

#### Vincent Beffara (Mar 10 2022 at 21:47):

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

#### Yaël Dillies (Mar 10 2022 at 21:48):

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

#### Yaël Dillies (Mar 10 2022 at 21:48):

instance = @[instance] def

#### Kyle Miller (Mar 10 2022 at 21:48):

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 (Mar 10 2022 at 21:49):

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 (Mar 10 2022 at 21:50):

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 (Mar 10 2022 at 21:53):

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 (Mar 10 2022 at 21:55):

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

#### Vincent Beffara (Mar 10 2022 at 21:56):

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 (Mar 10 2022 at 21:57):

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

#### Sebastien Gouezel (Mar 10 2022 at 22:00):

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 (Mar 10 2022 at 22:02):

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

#### Yaël Dillies (Mar 10 2022 at 22:03):

(or rather declare as an instance)

#### Vincent Beffara (Mar 10 2022 at 22:06):

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 (Mar 10 2022 at 22:07):

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

#### Kyle Miller (Mar 10 2022 at 22:09):

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

#### Vincent Beffara (Mar 10 2022 at 22:13):

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 (Mar 10 2022 at 22:28):

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

Last updated: Dec 20 2023 at 11:08 UTC