bottine

Stream: new members

[bottine]

Hey! I'm thinking on trying to formalize geometric group theory, and it seams LEAN is the place to do this. I have pretty much zero knowledge of proof assistants, but I'm trying to learn now. Anyone has done some work in GGT already?

[Huỳnh Trần Khanh]

oh hello I'm not a mathematician so I'm afraid I can't answer your question, but I believe it might be helpful to check out our learning resources https://leanprover-community.github.io/learn.html, especially the Logical Verification course

[Eric Wieser]

I'm not sure logical verification is the best start for someone interested in formalizing math, I suspect it aligns much better with Huỳnh Trần Khanh's interests than the ones in your message.

[Sebastien Gouezel]

I don't think we have anything on geometric group theory. Even the definition of the Cayley graph with respect to some generating set, as a metric space for the word distance, is missing.

[Sebastien Gouezel]

There is some difficulty here: should you put in the edges (to get a geodesic space) or just the vertices (then the Cayley graph would be a copy of the group, with the additional data of a distance).

[Sebastien Gouezel]

Probably a good place to start is to define quasi-isometries between metric spaces (or extended metric spaces) and prove their basic properties, as it would require less know-how.

[bottine]

Yes, I think starting with quasi-isometries of metric spaces in general is probably the best way to go. I would not make Cayley graphs into a geodesic spaces, but only keep the vertices and the metric itself (as a discrete distance). I think a good test would then be to verify that two different generating sets for your group induce quasi isometric graphs. And then probably try and see if we can show that Ends(G) \in {0,1,2,\infty}.

Then, longer term goals would be the ability to talk about, say, hyperbolicity, growth, and eventually even to prove Stalling's result about ends, and even Gromov result. At first, I thought Gromov's would be "impossible" due to its resilience on stuff like Lie groups, real vector spaces, etc, which I thought were quite far off in terms of formalization. But I see LEAN has quite a large library already, so who knows…

[bottine]

Does that make sense? Is it a too lofty goal?

[bottine]

ah, I see Gromov-Hausdorff has been done already: https://github.com/leanprover-community/mathlib/blob/master/src/topology/metric_space/gromov_hausdorff.lean

[Sebastien Gouezel]

Defining quasi-isometries, putting a distance on the group associated to a finite generating set, and checking that two such distances are quasi-isometric, looks completely reasonable.

Classifying the number of ends is harder, I think (first, one should define the space of ends), but not completely crazy.

[Sebastien Gouezel]

As for Gromov theorem (the one on groups with polynomial growth, right?), Kleiner's proof has less prerequisites and would therefore be a better choice for formalization. But this is clearly a long-term goal.

[bottine]

Great, thanks for your input @Sebastien Gouezel! This looks like something I will try and pursue then.
Actually, re Gromov's theorem (yes, the polynomial growth one), I had a look at the blog post by Tao and it looks like the proof can be neatly cut into preliminary results which are then relatively easily combined; I think/hope this makes it at least superficially amenable to formalization.

[Daniel Roca González]

Are you still interested in this @bottine ?

[Vincent Beffara]

Hi, the graph theory part of mathlib is in the process of a big refactor so formalizing things like Cayley graphs right now is probably not the right time, better wait for a few weeks. I should know because I did it myself some time ago, see https://github.com/vbeffara/lean/blob/lean-3.4.2/src/graph_theory/cayley.lean (that is the definition of the Cayley graph and the proof of quasi-isometry under change of generator set, using the current simple_graph API, but it is still draftish). But nice to know that there is work happening in that direction :-)

[bottine]

Indeed I am :) I'm currently writing out a research proposal to try and get a postdoc grant to pursue this.

[Daniel Roca González]

@Vincent Beffara Thank you, that sounds nice. Although I don't really understand what you're doing: how are you talking about quasiisomorphisms?

[Vincent Beffara]

Not quasi-isomorphisms but quasi-isometries, in the sense that on a group equipped with two (finite) generator sets, identity on the group induces a bi-Lipschitz map between the corresponding Cayley graphs.

[bottine]

Vincent Beffara said:

Hi, the graph theory part of mathlib is in the process of a big refactor so formalizing things like Cayley graphs right now is probably not the right time, better wait for a few weeks. I should know because I did it myself some time ago, see https://github.com/vbeffara/lean/blob/lean-3.4.2/src/graph_theory/cayley.lean (that is the definition of the Cayley graph and the proof of quasi-isometry under change of generator set, using the current simple_graph API, but it is still draftish). But nice to know that there is work happening in that direction :-)

What changes are planned for the simple_graph API? Also, do you have an ETA on the refactoring landing?

[Kyle Miller]

We're working to make things generic so that there's shared API between many different kinds of graph-like structures. The ETA is Soon (on the order of weeks rather than months).

I'm also hoping that things will look roughly the same for simple_graph, just that lemmas will find some new homes in other namespaces. I'd say, if you want to get to work on graphs, you should feel free. Just be aware that things might change a bit.

[Kyle Miller]

@Vincent Beffara There's a question about whether Cayley graphs should be graphs, or whether they should be some kind of docs#quiver on a group-with-presentation (like docs#presented_group). It seems like it would be an easier design for the metric_space structure. Is this something you've considered?

[bottine]

what's the advantage of using quivers here? (first time I'm learning about those)

[bottine]

Also, I don't have the experience for my opinion to count for much, but I would expect Cayley graphs should be definable for "abstract" groups, without necessarily having a presentation, no?

[bottine]

OK, I'm in the process of trying to set up a basic layout for quasi-isometries/coarse geometry. Is there a standard way to discuss design choices?

[Vincent Beffara]

TBH I did not ask myself such design questions, I was merely looking for nice examples of graphs (and possibly for a nice way of putting a graph structure on Z^2 along the way of defining planarity, but probably that was overkill).

[Vincent Beffara]

What is gained by defining a Cayley graph as a quiver? I am also completely ignorant about those ...

[Vincent Beffara]

BTW it also likely makes sense to define the word metric on a group independently of the graph structure

[Vincent Beffara]

One related design question: is there a reason for walks, paths and so on to grow from their heads like lists rather than from their tails like quiver paths and instances of refl_trans_gen?

[Kyle Miller]

Vincent Beffara said:

What is gained by defining a Cayley graph as a quiver? I am also completely ignorant about those ...

Quivers are the typeclass version of directed graphs. (Quivers hold arrows.)

Here's an idea for how you might set things up (but I have no promises that this ends up being a good idea!)

import group_theory.presented_group
import combinatorics.quiver.basic

inductive arrow (α : Type*)
| gen : α → arrow
| inv : α → arrow

def presented_group.of_arrow {α : Type*} (rels : set (free_group α)) :
  arrow α → presented_group rels
| (arrow.gen x) := presented_group.of x
| (arrow.inv x) := (presented_group.of x)⁻¹

instance {α : Type*} (rels : set (free_group α)) : quiver (presented_group rels) :=
⟨λ _ _, arrow α⟩

structure presentation (G : Type*) [group G] :=
(α : Type*)
(rels : set (free_group α))
(iso : G ≃* presented_group rels)

def presented_by (G : Type*) [group G] (p : presentation G) := G

instance (G : Type*) [group G] (p : presentation G) : quiver (presented_by G p) :=
⟨λ _ _, arrow p.α⟩

[Kyle Miller]

Then you can put a metric_space structure directly on the presented_group rels or the presented_by G p

[Kyle Miller]

(Ping @David Wärn, who's been working on quivers recently.)

[Daniel Roca González]

Cayley graphs should be defined for generated groups, not presented ones. Other than that that looks good, yes.

[Kyle Miller]

I was figuring it's a way to show that the generating set actually does generate the group. Feel free to substitute other ways of formalizing that!

[Kyle Miller]

For example, the data of a surjective homomorphism from a free group.