Word metric on group -- a new attempt

Stream: new members

[Laurent Bartholdi]

Hi all, I tried to start from scratch with a definition of the word metric on a group, and I'm stuck at some basics. Here is where I am now: I'm thinking of a basic object which is a group with fixed generating set

import analysis.normed.group.basic
import group_theory.free_group

noncomputable theory
open set function real

namespace word_metric

section marked_group

variables {G S : Type*} [group G]

"""an S-generated group"""
class marked_group (G S : Type*) extends group G :=
(marking : free_group S → G)
(is_surjective : function.surjective marking)

variables [decidable_eq S] [marked_group G S]

def free_group_norm : free_group S → ℕ := λf, (free_group.to_word f).length

lemma marked_group_marking (G S : Type*) [marked_group G S] : free_group S → G := marked_group.marking

def group_norm : G → ℕ := λg, Inf ((free_group_norm)'' ((marked_group_marking G S)⁻¹' {g}))

variables [fintype S]

lemma group_norm_finite (x : G) : group_norm x ≠ ⊤ := begin
  -- say that the Inf argument is non-empty because of marked_group.is_surjective
  sorry
end

lemma group_norm_one (x : G) : group_norm x = 0 ↔ x = 1 := begin
  sorry
end

-- etc.

end marked_group

end word_metric

My basic questions, for which I hope I can get help, are:

• Why do I have to repeat the assumptions [decidable_eq S] in unpredictable ways?
• In group_norm_finite there is an error that Lean doesn't know how to synthesize a placeholder at group_norm
• I intend to define class normed_group extends group G, has_norm G, metric_space G and create an instance of it from a marked_group G S. Does this sound reasonable?

Many thanks in advance! Laurent

[Riccardo Brasca]

The second [decidable_eq S] is needed because you introduced a new S in `def free_group_norm.

[Riccardo Brasca]

The third one should be useless, but beware that you repeated [group G], so now you have two group structure on G, and this surely not what you want.

[Riccardo Brasca]

Also, you may want to use finite S instead of fintype S (and you need this only once).

[Laurent Bartholdi]

OK, thanks! I cleaned up a bit the code with these suggestions, and edited my first message. (sorry if the beginning of the conversation now looks strange).

I forgot another question: I couldn't access the field "marking" in the marked_group G from group_norm, so I resorted to writing the lemma marked_group_marking to access it. What's the correct way of doing this?

[Heather Macbeth]

@Laurent Bartholdi @Jim Fowler Just making sure you are aware of each others' work here!

[Jim Fowler]

Yes, I have some code posted at https://github.com/kisonecat/word-metric/tree/main/src

[Jim Fowler]

I do think 'marked_group' is a better name than 'generated_group'.

[Yaël Dillies]

Let me ping @Georgi Kocharyan here too.

[Junyan Xu]

@Laurent Bartholdi

In group_norm_finite there is an error that Lean doesn't know how to synthesize a placeholder at group_norm

This is because the statement doesn't mention S at all, so Lean doesn't know what to fill in for the S in group_norm. Making S explicit in group_norm helps; if you don't want to write S all the time you should probably include it as a field in the structure marked_group.

If you don't choose to include S inside the structure, then it seems necessary to define marked_group_marking as you did, because S is implicit in marked_group.marking. If you change the inverse image ⁻¹' by an explicit expression as I did above, you can make G implicit in marked_group_marking (btw, it should be a def not a lemma).

Note that ⊤ still doesn't work since ℕ doesn't has_top. It seems nicer to use docs#well_founded.min to define group_norm (see below).

Another comment: since your marked_group extends group, you should probably require marking to be a homomorphism.

import analysis.normed.group.basic
import group_theory.free_group

noncomputable theory
open set function real

namespace word_metric

section marked_group

-- an S-generated group
class marked_group (G S : Type*) extends group G :=
(marking : free_group S → G)
(is_surjective : function.surjective marking)

variables {G : Type*} (S : Type*) [marked_group G S]

def marked_group_marking : free_group S → G := marked_group.marking

variables {S} [decidable_eq S]
def free_group_norm (f : free_group S) : ℕ := (free_group.to_word f).length

variables (S)
def group_norm (g : G) : ℕ := nat.lt.is_well_order.wf.min
  (free_group_norm '' {x | marked_group_marking S x = g})
  (by { apply set.nonempty.image, exact marked_group.is_surjective g })
-- Inf (free_group_norm '' {x | marked_group_marking S x = g})

variable (x : G)
#check group_norm S x -- now works

[Georgi Kocharyan]

Yaël Dillies said:

Let me ping Georgi Kocharyan here too.

thanks - my current attempt for the word metric and Cayley graphs is at https://github.com/GregorSamsa42/svarc-milnor/blob/main/src/cayleygraphs.lean

[Eric Wieser]

marked_group doesn't look like it can safely extend group to me

[Eric Wieser]

Although maybe it's safe if you change S : Type* to S : out_param Type*

[Laurent Bartholdi]

Thanks to all!
@Jim Fowler , I see you're done a lot, and it will be very inspiring. However, I think that the notion of "marked group" is important enough to be in Lean, not just for the word metric. See e.g. http://math.univ-lyon1.fr/~altinel/ModelsGroupsArx/benli_gm2015.pdf for some slides. @Yaël Dillies , it looks like a very nice shortcut to use simple_graph.dist. Are you working with Clara Löh on this? I see her name in a header. The Svarc-Milnor theorem is a great goal, it was on my todo list but I'll cross it out now :)

I would nevertheless like the code to be a bit more general. In particular, separate the notions of marked_group and normed_group; and within normed_group, have word_normed_group in which one specifies a (positive real) length for each generator. That will make induction harder, since we'll have a well-founded set of real lengths to work with.

WRT the first class, my heart goes now more in the direction of

class marked_group (G : Type*) extends group G :=
(S : Type*)
(decidable : decidable_eq S)
(marking : free_group S →* G)
(is_surjective : function.surjective marking)

Comments as always appreciated!

[Junyan Xu]

If you have real numbers then the minimum may not be achieved, e.g. if G is the additive group of ℚ, S is {1/n | n ∈ ℕ+}, and 1/n is assigned length 1/n^2. But if S is finite then there's only a finite number of elements in free_group S of bounded norm.

[Eric Wieser]

I'd also perhaps suggest:

class marked_group (G : Type*) (S : out_param Type*) [group G] :=
(marking : free_group S →* G)
(is_surjective : function.surjective marking)

and then you don't need the decidable instance as a field

[Eric Wieser]

This has the bonus of working for comm_group too, in case that's relevant'; with your spelling, you can't talk about marked commutative groups.

[Sebastien Gouezel]

If you want to register your group as a metric space (where the distance depends on S), you will need to embrace the type synonym trick. Instead of a class, define a structure marking S G as you did. And then given a group G and a marking m, define a new type marked_group m G := G. On this new type, you can register the same group structure as on G, but you can also register a distance as m is now available to the system when you consider x y : marked_group m G.

[Sebastien Gouezel]

The out_param idea I don't like so much because often we discuss several generating sets on a given group.

[Laurent Bartholdi]

OK! @Eric Wieser , I followed your suggestion, so the beginning looks like

class marked_group (G : Type*) (S : out_param Type*) [group G] :=
(marking : free_group S →* G)
(is_surjective : function.surjective marking)

variables {S : Type*} [decidable_eq S]

def free_group_norm (f : free_group S) : ℕ := (free_group.to_word f).length

variables {MG : Type*} [group MG] [marked_group MG S]

def group_norm [decidable_eq S] (g : MG) : ℕ := nat.lt.is_well_order.wf.min
  (free_group_norm '' {x | marked_group.marking x = g})
  (by { apply set.nonempty.image, exact marked_group.is_surjective g })

lemma group_norm_one [decidable_eq S] (x : MG) : group_norm x = 0 ↔ x = 1 := sorry

Is this what you had in mind? I don't seem to be able to get away without repeating the assertions [decidable_eq S] everywhere, otherwise Lean doesn't know anything about S.

Extra question: what is the interface for nat.lt.is_well_order.wf.min? All I want is to extract an element representing the minimum, and provide witnesses that upper-bound the minimum.

@Sebastien Gouezel , I just saw your message while typing. Do you think it's then best to keep it the way I did it before, with an explicit S field? (and of course your splitting into struct and type

[Rémi Bottinelli]

IIrc nat.find was a good alternative to ….wf.min in the case of naturals?
See here.

[Yaël Dillies]

Laurent Bartholdi said:

Are you working with Clara Löh on this? I see her name in a header.

No, but Georgi is! and I'm casually helping Georgi out.

[Rémi Bottinelli]

By the way, at the risk of thread-jacking, would it make sense to set up a space to coordinate the progress on formalizing GGT? I admit I haven't made nearly as much progress as expected until now, but would like to get back to it, and would love to have the possibility to work outside of my bubble and discuss formalization strategies and goals in a kind of communal way.

[Yaël Dillies]

I am not quite the person to ask about this, but I strongly suggest you do! The most effective way to do this is to work on a common branch of mathlib (and create a new directory in there to keep the new files close to each other) or to create a new repository with CI (which is arguably much more work) + have either a Discord group chat, a Zulip topic or a Zulip stream.

[Eric Wieser]

The out_param should mean that lean works out what S is

[Eric Wieser]

Sebastien Gouezel said:

The out_param idea I don't like so much because often we discuss several generating sets on a given group.

If my understanding is correctout_param doesn't really require that the generating set be unique, it just means that you can leave it unspecified and lean will find a default.

[Anne Baanen]

The rule is that for a given choice of non-instance-implicit non-out_param arguments, you can't have two instances that are not equal. (Instance-implicit parameters are the ones in [square brackets].) Equality of instances means:

• the fields of the underlying structure are definitionally equal, up to a reducibility somewhere between reducible and semireducible (I believe the correct reducibility depends on the specific situation)
• all values for out_param and instance-implicit parameters are similarly definitionally equal

[Anne Baanen]

If you break this rule, you will get diamond errors (unless you are very careful with what you do).

[Eric Wieser]

Equality doesn't even make sense to state though if the out_params arguments (indices) are different

[Sebastien Gouezel]

out_param stuff should definitely be unique, yes, otherwise you run into diamonds.

A tentative scheme avoiding out_params would be the following:

• First, work with normed groups, and prove whatever you like here. Possibly adding new typeclass assumptions that say that the distance is proper or hyperbolic or whatever.
• Then, to construct instances of such normed groups, do it on type synonyms. For instance, given two types S and G with [group G], define marking S G as the space of markings of G parameterized by S. Then, given a group G and a marking m, define a typemarked_group G S := G as a copy of G, then define on it the group structure coming fro G (with @[derive ...]) and the norm associated to S. Then marked_group G S will be an instance of a normed group.

[Sebastien Gouezel]

If you want to have real distances, this fits perfectly well in this scheme, with another type synonym in which you will register a marking together with the length of each edge for each element of S.

[Eric Wieser]

Sebastien Gouezel said:

out_param stuff should definitely be unique, yes, otherwise you run into diamonds.

Do you have an example in mind for what this looks like? Maybe you're right that out_params aren't the right solution here, but I don't believe that diamonds (at least not in the usual sense) are possible from them

[Anne Baanen]

Does this count as a diamond?

import data.fin.basic

class artificial_example (i : Type) (o : out_param ℕ) :=
(foo : fin o)

instance ex0 : artificial_example ℕ 1 := ⟨0⟩

theorem ex0_eq_0 : artificial_example.foo ℕ = 0 := rfl

instance ex1 : artificial_example ℕ 2 := ⟨0⟩

theorem ex0_eq_0' : artificial_example.foo ℕ = 0 := ex0_eq_0 -- Error: type mismatch

[Anne Baanen]

Of course, this will work once you make o explicit in foo, but at that point you don't need the out_param anymore.

[Eric Wieser]

Oh I see, the diamond no longer happens in the instance itself (because you can't state that any more), but the operations/projections derived from it. Thanks!

[Anne Baanen]

That's one way to see it indeed!

[Jim Fowler]

@Rémi Bottinelli it'd be great to coordinate formalization efforts around GGT!

[Jim Fowler]

I agree with you Laurent Bartholdi that marked_group is the correct notion.

[Rémi Bottinelli]

OK, I guess the best place to start is by setting up a stream, but it seems you need to be an admin to do that. Am I right, @Yaël Dillies ? OK, started with a topic here

[Yaël Dillies]

I would suggest creating a stream only if the project starts getting big. There are only 39 public streams.

[Jim Fowler]

Perhaps create a ggt branch in mathlib, create a subdirectory geometric_group_theory ?

[Yaël Dillies]

Or group_theory.geometry?

[Junyan Xu]

Extra question: what is the interface for nat.lt.is_well_order.wf.min? All I want is to extract an element representing the minimum, and provide witnesses that upper-bound the minimum.

The interface you want is provided by docs#well_founded.min_le and docs#well_founded.min_mem.
But indeed docs#nat.find is better. Thanks Rémi Bottinelli!

[Laurent Bartholdi]

OK, I just created a minuscule file at group_theory/geometric/marked_group.lean in a branch geometric-group-theory. All are welcome to play with it and modify! For now, I'm just testing whether the basic idea is sound. I'll try to incorporate the changes suggested by @Sebastien Gouezel

@Rémi Bottinelli and @Yaël Dillies and @Jim Fowler , perhaps we can put all our ideas together in this subdirectory and sort out which approach works best?

I hope I'm not doing anything untoward. Hopefully everybody has access to this branch and can make coordinated changes.

[Rémi Bottinelli]

I had some very WIP code on the ends of graphs and also a basic pull request about nets and separated sets in metric spaces here. I'm not sure either belongs to group_theory/geometric though?

[Laurent Bartholdi]

@Rémi Bottinelli definitely they do!
A very nice result to formalize could be the 0-1-2-infty theorem on ends; and, perhaps even better, the new take by Yves de Cornulier that does not restrict to finitely generated groups. In essence, he considers a group G acting on a space X; the Boolean algebra of X-subsets modulo finite ones; its G-invariant subalgebra; and the Stone dual thereof. This is the space of ends of X_G, and for X=G has 0,1,2 elements or is a Cantor set. See [https://www.normalesup.org/~cornulier/spaends.pdf]
Particularly interesting would be to connect to the classical theory of ends in graph theory when the group is f.g.

[Rémi Bottinelli]

Hah, I had exactly that thing in mind (see the topic I started on General). I was thinking it might be easier to define both "coarse" and "graphical" notions of ends separately and link them later on. But that really stemmed from my failure at defining a coarse notion for which the 0-1-2-oo theorem is easily shown.
So, it's a good question whether we should directly start with the most general result or not.

By the way, it's not clear from just reading the abstract, but does Cornulier actually prove the "generalized" version of 0-1-2-oo ?

[Jim Fowler]

@Laurent Bartholdi thank you for getting this going!

[Jim Fowler]

@Rémi Bottinelli I think it would be helpful to collect anything related (like ends of graphs) in group_theory/geometric.

[Jim Fowler]

I recall seeing some QIE definitions by Clara Löh which could also be put in this branch (or maybe quasi-isometry lives somewhere in mathlib already?).

[Rémi Bottinelli]

As far as I knew, quasi-isometries weren't there yet. This one (I mean, the notion of quasi-isometry) also has lots of different definitions, and I'm not sure which one to start with first. My PR was actually headed in this direction, since some implications need to start with a maximal separated subset.

[Laurent Bartholdi]

OK, it's 1am and I just managed to prove that |g|=0 iff g=1. If anyone wants to give a look to group_theory/geometric/marked_group.lean and provide golfing / structure suggestions, I'd love it!

[Jim Fowler]

@Laurent Bartholdi I moved some things into variables and implicit arguments.

[Rémi Bottinelli]

Ah, damn, I'm getting the yellow bar and vscodium crashes wnen trying to work with the geometric-group-theory branch. Should leanproject get-cache --fallback=download-firstbe the correct command to get the cache?

[Rémi Bottinelli]

After some more work, I got to the following:

lemma to_word_inv_length (x : free_group S) : x⁻¹.to_word.length ≤ x.to_word.length :=
begin
  sorry,
end
lemma to_word_mul_length (x y : free_group S) : (x*y).to_word.length ≤ x.to_word.length + y.to_word.length :=
begin
  sorry,
end

lemma group_norm_comm_le (x : G) : group_norm m x⁻¹ ≤ group_norm m x :=
begin
  have h : (group_norm m x) ∈ (group_norms m x) := nat.lt.is_well_order.wf.min_mem (group_norms m x) (group_norms_nonempty m x),
  rcases set.mem_image_iff_bex.1 h with ⟨y,ytox,yneqxn⟩,

  have yitoxi : m.marking y⁻¹ = x⁻¹, by
  { rw map_inv,simp only [inv_inj],exact ytox },

  have mon : (y⁻¹).to_word.length ≤ y.to_word.length, from to_word_inv_length y,
  have : (y⁻¹).to_word.length ∈ (group_norms m x⁻¹),
    from set.mem_image_iff_bex.2 ⟨y⁻¹, yitoxi, rfl⟩,
  apply le_trans (well_founded.min_le nat.lt.is_well_order.wf this (group_norms_nonempty m x⁻¹)),
  rw [←yneqxn],
  exact mon,
end

lemma group_norm_comm (x : G) : group_norm m x = group_norm m x⁻¹ := begin
  apply has_le.le.antisymm,
  { have := group_norm_comm_le m x⁻¹,
    rw (inv_inv x) at this,
    assumption, },
  { exact group_norm_comm_le m x, },
end

lemma group_norm_ineq (x y : G) : group_norm m (x*y) ≤ group_norm m x + group_norm m y := begin
  -- extract reps for x, y, use product for x*y
  have h : (group_norm m x) ∈ (group_norms m x) := nat.lt.is_well_order.wf.min_mem (group_norms m x) (group_norms_nonempty m x),
  rcases set.mem_image_iff_bex.1 h with ⟨z,ztox,zneqxn⟩,
  have k : (group_norm m y) ∈ (group_norms m y) := nat.lt.is_well_order.wf.min_mem (group_norms m y) (group_norms_nonempty m y),
  rcases set.mem_image_iff_bex.1 k with ⟨w,wtoy,wneqyn⟩,
  have one : m.marking w = y, from wtoy,
  have two : m.marking z = x, from ztox,

  have zwtoxy : m.marking (z*w) = x * y, by { rw map_mul, rw [one,two],},
  have mon : (z*w).to_word.length ≤ z.to_word.length + w.to_word.length, from to_word_mul_length z w,

  have : (z*w).to_word.length ∈ (group_norms m (x*y)),
    from set.mem_image_iff_bex.2 ⟨z*w, zwtoxy, rfl⟩,

  apply le_trans (well_founded.min_le nat.lt.is_well_order.wf this (group_norms_nonempty m (x * y))),
  rw [←zneqxn,←wneqyn],
  exact mon,
end

I'm not sure of the best way to prove the first two lemmas above. Surely they should follow from relatively simple manipulations in the free group: If w is a reduced word for x, then w.reverse.map … is a representative of x⁻¹, hence in the same class as x⁻¹.to_word, hence reduces to it, and by monotonocity we're done… but I can't quite get the correct tools to use for that. By the way, please tell me if I should play with something else while you're working on this file!

[Laurent Bartholdi]

@Jim Fowler great! I looked at your "properties.lean" and added some stuff. Out of curiosity, why did you go to monoid quotients in "residually P"?

[Laurent Bartholdi]

@Rémi Bottinelli Very nice, of course I'm very happy to see you filled some sorries. Should I paste it into the file, or do you want to commit it yourself?

About to_word_inv_length: the lemmas are definitely there, but I can't put them together: free_group.mk takes a list and uses red, free_group.red.length proves that length decreases under red, and free_group.inv_mk reverses a list, so preserves length. Hope that helps!

[Rémi Bottinelli]

Feel free to paste if you feel it's going in the direction you were headed at (this way there is fewer chances of commits crossing, etc). I'll think more about how to go forward with it, without much guarantee!

[Jim Fowler]

I had added some of the inv_rev lemmas to free_group on another branch -- it is in https://github.com/leanprover-community/mathlib/pull/15503

[Jim Fowler]

@Laurent Bartholdi the monoid stuff in the def of residually is just there to get it to find the instance of has_one. I'm not sure how to quantify over groups and get type class inference to pick up the group instance.

[Jim Fowler]

@Laurent Bartholdi Your additions to properties.lean are great!

[Rémi Bottinelli]

@Jim Fowler Great, do you have any when your PR will get merged?

In the meantime, I've tried tackling to_word_inv_length below: as far as I know, it works correctly, though the code is far from good.

lemma to_word_inv_length (x : free_group S) : x⁻¹.to_word.length ≤ x.to_word.length :=
begin

  let xi := x⁻¹,
  let xw := x.to_word,
  let xiw := x⁻¹.to_word,
  let xwi := (x.to_word.map (λ (y : S × bool), (y.fst, !y.snd))).reverse,

  have xi_eq_mk_xwi : xi = free_group.mk xwi, by rw [←free_group.inv_mk, free_group.to_word.mk],
  have : free_group.reduce xwi = (free_group.mk xwi).to_word, by simpa only,
  have : free_group.reduce xwi = xiw, by rw [this, ←xi_eq_mk_xwi],
  have : free_group.red xwi xiw , from this ▸ free_group.reduce.red,

  have : xwi.length ≥ xiw.length, by {
    rcases free_group.red.length this with ⟨n,p⟩,
    exact le_iff_exists_add.mpr ⟨2*n,p⟩,
  },
  rw [list.length_reverse,list.length_map] at this,
  exact this,
end

[Laurent Bartholdi]

Perhaps it's best to wait till @Jim Fowler 's PR is merged? That will make all the lemmas shorter in marked_groups. I can then do the integration. Or is there a way to temporarily merge your PR without completely messing up git?

[Andrew Yang]

(deleted)

[Rémi Bottinelli]

@Laurent Bartholdi (I've updated my snippet with an impl for to_word_mul_length too)
Whichever way you prefer, though note that @Jim Fowler 's PR is for master, if I'm not mistaken. This means both that it may take some time to get merged, and that our including a patchy version for the time being in geometric-group-theory won't mess up anything with git as far as I'm aware.

[Laurent Bartholdi]

OK, I've included @Rémi Bottinelli 's code in marked_group.lean. In principle, we have all the lemmas to assert the existence of a metric space!

I confess I haven't totally [= not at all] understood how to create a new type such that [marked_group MG] asserts that MG is a group with marking. I have created a tentative growth.lean file to see how the API could develop.

For some practical applications I have in mind, it may be nice to have more general metrics: word metrics with weights, and restrictions of the word metric to a subgroup. There too, I'm not yet sure about how best to create the structures.

[Rémi Bottinelli]

I've made a few changes to marked_group.lean but it's not pushed to your branch: see my repo. I've split the group_norm_one into a sublemma because I needed it later on, and mostly I've started an attempt at showing that two finite generating sets induce equivalent norms. For this I've had to define a few more lemmas on the free group (unproved yet but should be easy enough). I've also added a few natural stubs: e.g. the only elements of norm one are letters.

[Laurent Bartholdi]

Yes, that's definitely the right direction!
0) if I may ask, why do you prefer working in a fork?
1) my aims are multiple:
1.1) to be able to formalize lots of geometric group theory, which relies on having a metric space instance starting from a finitely generated group; this includes the Svarc-Milnor lemma, ends of groups, hyperbolic, CAT(0) groups, etc.
1.2) to formalize growth of groups; in particular, the Dixmier-Bass-Guivarch result that virtually nilpotent groups have polynomial growth; the Milnor-Wolf result that virtually solvable groups have either polynomial or exponential growth; the Grigorchuk result that there are groups of intermediate growth; and (probably harder) the Gromov result that polynomial-growth groups are virtually nilpotent.
1.3) to formalize, more generally, the "space of marked groups" as a compact topological space; and results about openness / closedness / G_delta genericity of various group properties.
2) here is my idea of a roadmap:
2.1) have a robust class "marked_group" which is a group on which a marking is registered; this will be useful for all the goals in 1)
2.2) different people can then develop independently the different consequences: growth, group properties, space of marked groups, and "pure geometric group theory" i.e. ends and actions on nice spaces (CAT(0), delta-hyperbolic, wall space, median space, ...)
3) in your lemma lemma group_norm_letter on line 120 there's a good reason the proof is sorry, and that the lemma's wrong! indeed nothing prevents an element of S to be mapped to 1:G. The correct one would have "\le 1". For the same reason, lemma group_norm_one_iff_is_letter on line 121 is wrong if G is the trivial group.

Now I must confess I feel a bit bad about writing this roadmap, feeling like an orchestra conductor who can't play a single instrument. It's just my opinion on what would be good, and I'd love a discussion about it.

[Rémi Bottinelli]

0) I don't prefer working in a fork at all: it's just that I'm not sure my changes were agreeable, and wanted to share them before committing them (my own "fork" is just a way to work without polluting the official repo).
1) Great: I pretty much have the exact same goals. I would very much like to prove Stalling's ends theorem eventually, hence working on ends and Bass-Serre seems like a good start.
2) I know the feeling!
3) Good point, what about adding m.marking (free_group.mk p) ≠ 1? Maybe that's useless as a lemma…

[Yaël Dillies]

Please avoid touching the branch right now! I am implementing the type synonym approach.

[Laurent Bartholdi]

@Yaël Dillies great, I'll keep my hands off the keyboard.
@Rémi Bottinelli , I don't think it's a good idea to forbid trivial generators; for example, it's nice to know that if G is a marked group then every quotient of G inherits the marking. Also, you must have the trivial group in the space of marked groups. Also, your lemmas at line 120-121 aren't used. Did you have an application in mind?

[Rémi Bottinelli]

no use, I just felt they (or a suitably corrected versions) might come handy later on.
And from the little I learned about mathlib, the rule of thumb looks to be: as few defs as possible, as many lemmas as possible.
But we can drop them, obviously.

[Jim Fowler]

@Rémi Bottinelli Line 51 is

lemma free_group.mk.singleton (p : S × bool) : (free_group.mk [p]).to_word = [p] := sorry

and this isn't in https://github.com/leanprover-community/mathlib/pull/15503 but it could be added. There's a lot of relevant lemmas for words and the free group...

[Jim Fowler]

In terms of goals, I think ends of groups would be a great first goal.

[Sebastien Gouezel]

I am not convinced that the basic object is marked groups. Instead, I'd go for groups with a left-invariant distance: there are many examples where the relevant distance is not a word distance (as a basic example, just think of the case where you don't give length 1 to all generators). Unfortunately, in mathlib currently normed_group is reserved for additive groups, but we could make the case that this should be renamed to normed_add_group.

[Yaël Dillies]

Have you seen the definitions of normed_mul_group and isom_action on branch#geometric-group-theory?

[Yaël Dillies]

I am currently PRing group seminorms with the hope to turn around the dependency between seminorm and normed_group and eventually move normed_mul_group to mathlib.

[Sebastien Gouezel]

No, I haven't opened the branch, I'm just writing random thoughts on Zulip :-)

Changing the current normed_group to normed_add_group would make a lot of sense, IMHO.

[Yaël Dillies]

I agree, but I didn't dare to suggest it because it's used in 182 files :P

[Jim Fowler]

normed_add_group seems like a great improvement. I don't think there is any sort of automated way of renaming identifiers?

[Yaël Dillies]

No but it's not hard to do by hand. If people agree on the rename, I can do that in a few minutes.

[Jim Fowler]

I would like to better understand current mathlib idioms for attaching a symmetry group to an object.

[Jim Fowler]

It's really great to see all of @Georgi Kocharyan 's work in this branch too.

[Laurent Bartholdi]

@Sebastien Gouezel : in fact it was my initial hope to have more general metrics. The worry I had is that the process would never leave the ground if we aim for too general in the beginning: for example, you'll have to make the metric be proper even before mentioning growth functions. In an ideal world, I would see the following:

• metric spaces with a left action by isometries
• as a special case, a homogeneous space G/P with metric induced from a metric on G
• as a sub-special case, G/P with a metric induced by weights on a [finite?] generating set of G
• as a sub^2-special case, G/P with the word metric from G
• as another sub^2-special case, G with a metric induced by weights on a [finite?] generating set of G
• as a sub^3 special case, G with the word metric

and automatic ways of converting each special case to less special one whenever the more general theorem holds.

I don't think I have enough wizard powers to implement this, though. Do you think it's feasible?

[Laurent Bartholdi]

@Yaël Dillies I just looked at your code, it's beautiful!
Though I have a problem with the "normed_mul_group": defining the metric by dist x y = ∥x/y∥ makes is right invariant, while all of lean seems to be built on left actions and left invariance. I tried to change it to dist x y = ∥x⁻¹*y∥ (see the most recent commit), but of course nothing works quite as before. Feel free to revert.

[Yaël Dillies]

Thanks! Glad you like it :smiling_face:

[Yaël Dillies]

I picked this direction because eventually we will refactor docs#normed_group to be the additivized version of normed_mul_group, and it uses dist x y = ∥x - y∥.

[Yaël Dillies]

Note however that normed_group is already assumed to be commutative, so we might be able to work around it, but it will be painful.

[Sebastien Gouezel]

There's no doubt that mathematically Laurent's definition is the right one. Even in the additive case, it would feel more natural to me to have dist x y = ∥y - x∥, by the way.

[Yaël Dillies]

∥y - x∥ is still right-invariant, right?

[Laurent Bartholdi]

On a side note, I had to add lemmas

lemma mul_mul_inv_cancel (x y z : E) [group E] : (x⁻¹*z) = (x⁻¹*y * (y⁻¹*z)) := by group
lemma inv_of_inv_mul (x y : E) [group E] : (x⁻¹*y)⁻¹ = y⁻¹*x := by group

which I couldn't find in the library -- algebra.group.basic seems to mainly consist of lemmas for commutative (multiplicative and additive) groups, and I found no basic lemmas in group_theory.

Yet another side note: I would like (with the help of a student) to extend group_theory.commutator. I respect the fact that left actions are used by default in Lean; but it would be nice to have a notation for it (it's exponentiation for a right action). Is there some standard one? Otherwise, I would propose ⇀, ⇁ or ⊸, something like infix `⊸`:200 := λ x y,x*y/x . It would also be nice to have iterated commutators; I can use

notation `⁅`x`,` y`,` z`⁆` := (has_bracket.bracket x (has_bracket.bracket y z))
example (E : Type*) [group E] (x y : E) : ⁅x,y,y⁆=1 := by group

but it would be nice to have right associativity for the non-infix operation.

[Laurent Bartholdi]

@Yaël Dillies and @Sebastien Gouezel we want ∥-x + y∥ if we're ever going to consider non-commutative additive groups :tongue-in-cheek:

[Yaël Dillies]

There is little point in adding all possible lemmas about group operations, when you can get there with one or two existing ones. The first is rw [mul_assoc, mul_inv_cancel_left], and the second is rw [mul_inv_rev, inv_inv].

[Yaël Dillies]

file#algebra.group.basic is the right file to look at. I do not quite get what you mean about it being mostly for commutative groups, given that there are 99 lemmas in there that apply to the noncommutative setting.

[Laurent Bartholdi]

Thanks, I golfed the proofs and just pushed them using your suggestion. I also removed a sorry from instance:normed_mul_group

[Rémi Bottinelli]

Re "the right basic object", the Proposition 1.A.1 in Cornulier & de la Harpe,p. 10 seemed to me to be exactly what we should aim for (see also the text up until 1.B) but I had the same fear that it might be too general to start with?

[Georgi Kocharyan]

Looking forward to working on this with everyone! Would I be able to have writing rights on the repo? My github is GregorSamsa42 :)

[Rémi Bottinelli]

@Georgi Kocharyan: by the way, if there are places in your code where you'd trust a beginner to fill in some holes, I'd welcome the opportunity.

[Georgi Kocharyan]

As I am also a beginner you are more than welcome !

[Rémi Bottinelli]

Alright! anything in particular?

[Laurent Bartholdi]

@Rémi Bottinelli I just pushed some definitions from Cornulier&Harpe to your (nice) new file on coarse pseudometric spaces. Hopefully this will connect nicely with the rest of the code

[Rémi Bottinelli]

Beware, though! After discussing on github (I have a pull request open for this file), i noticed that my definitions are quite (dangerously?) different from the official ones. For density, I'm using the existence of a close point with "≤", instead of Hausdorff distance with "<", and for separation I use "<" instead of "≤". I admit I like my definitions, since they allow a very clean statement in the last theorem, but wonder if they are dangerous as of now…