Geometric group theory

Stream: maths

[Yaël Dillies]

@Georgi Kocharyan, @Rémi Bottinelli, @Laurent Bartholdi, @Jim Fowler, let's coordinate in this thread.

[Yaël Dillies]

I just refactored marked groups to be type synonyms (rather than classes). I am now copying over Georgi's material and adapting it to the new paradigm.

[Rémi Bottinelli]

Wow, that's contentful!
Personally, I'd like to try and cover the ends of graphs first, and use that as a stepping stone for the ends of groups hopefully; and Bass-Serre at some point in the near future.
Other than that I'd be happy to collaborate on whatever should come first, but there is some (a lot of) getting up to speed for me I see (even more so after seeing your transformation up there!).

[Re ends of graphs: I have some code here but it's very messy and I have a feeling it's not headed in the right direction; I'd welcome some coaching on the coding side!]

(I'm heading off for today)

[Heather Macbeth]

Link to other threads:

https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/Word.20metric.20on.20group.20--.20a.20new.20attempt

https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Geometric.20Group.20Theory.20coordination.20.3F

[Yaël Dillies]

#15594 for group seminorms.

[Rémi Bottinelli]

Is it all-right if I bring my file on nets and separated subsets here?

[Yaël Dillies]

Please do!

[Rémi Bottinelli]

Done. The theorem therein might be useful when/if one wants to show that from a quasi-isometry one can get a bilipschitz bijection between nets contained in the spaces.

[Rémi Bottinelli]

By the way, about quasi-isometries: Is it worth it to also define coarsely Lipschitz maps and closeness for two maps into a metric space and have equivalence between all possible notions of equivalences, or should one stick to only talking about quasi-isometries for now?
One definition I liked was: X and Y are QI if there exists a pair f:X ->Y, g:Y->X, both coarsely Lipschitz, and such that both f o g and g o f are close to the identity.

here I've got stuff about close maps and coarse Lipschitz maps.

[Rémi Bottinelli]

Would it make sense to set up some variation of a roadmap.txt file with a list of goals and subgoals and who is working on what?

[Anand Rao]

I have been following this and related threads for a while and would also like to contribute to building geometric group theory in mathlib. I have a nearly complete proof of the fact that the Cayley graph is connected (modulo two very easy sorrys), and I would like to push the changes to the geometric-group-theory branch. Can I please have write access to the non-master branches of mathlib? My GitHub username is 0art0. Thanks!

[Kevin Buzzard]

@maintainers

[Markus Himmel]

@Anand Rao I sent you an invitation

[Anand Rao]

Got it, thanks. I have pushed my code.

[Rémi Bottinelli]

I've been trying to make some progress on my code for ends of graphs, and am getting sort of lost starting from here.
The point is that I want to show that given any finite set of vertices and infinite connected component outside this set, I can define an end that corresponds to this component. My problem is that I have to do some transports along equalities for it to make sense, and I feel like I'm not going in the right direction.

For instance, the definition extend_along_fam seems quite complicated, and the lemma extend_along_const needs transport even just to get correctly stated.
I believe I'm missing some theoretical/technical aspect here.

Any idea on how I should proceed to make sense of this all? I'd welcome some structuring insights too!

[Kyle Miller]

I'm not sure it would simplify anything, but I thought I'd mention we now have docs#simple_graph.subgraph.delete_verts so you can define

def simple_graph.connected_outside (G : simple_graph V) (s : set V) : Prop :=
((⊤ : G.subgraph).delete_verts s).coe.connected

and if you have s : finset V you can write G.connected_outside s. (This definition means "G as a subgraph itself, once you delete the vertices from s, it is connected.")

[Kyle Miller]

For ends of graphs, I imagined that one might take the poset of finite sets, which is closed under intersections, then define an inverse system over finite sets s of the types ((⊤ : G.subgraph).delete_verts s).coe.connected_component. The limit of this inverse system consists of the ends.

We have a theorem that if these types are always finite and nonempty then this limit is nonempty too (docs#nonempty_sections_of_fintype_inverse_system) so in that case you'd have the graph has at least one end.

I'm not sure how good this definition of ends would be to work with, but it at least wouldn't be too much work to set up. (Modulo some missing API around delete_verts and connected_component.)

[Rémi Bottinelli]

Thanks! I'm wary of swapping out my constructions for the alternatives you provided though since as of now, my definitions do sort of work… but yeah, the inverse system theorem is a nice tool.

[Rémi Bottinelli]

Would you go with something like this ?

import data.set.finite
import data.sym.sym2
import combinatorics.simple_graph.basic
import combinatorics.simple_graph.connectivity
import topology.metric_space.basic
import data.setoid.partition
import category_theory.functor.basic

open function
open finset
open set
open classical
open simple_graph.walk
open relation

universes u v w



noncomputable theory

--local attribute [instance] prop_decidable

namespace simple_graph


variables  {V : Type u}
           (G : simple_graph V)

section ends

def conn_comp_outside (s : finset V) : Type u :=
((⊤ : G.subgraph).delete_verts s).coe.connected_component

lemma conn_comp_outside.finite [locally_finite G] [preconnected G] (s : finset V) :
  fintype (conn_comp_outside G s) := sorry

lemma conn_comp_outside.nonempty  [locally_finite G] [preconnected G] (Ginf : (@set.univ V).infinite) (s : finset V) :
  nonempty (conn_comp_outside G s) := sorry

def conn_comp_outside.to_set (s : finset V) (c : conn_comp_outside G s) : set V :=
  { v : V | ∃ (p:v ∉ s), ((⊤ : G.subgraph).delete_verts s).coe.connected_component_mk (⟨v,by {simp,exact p}⟩) = c }

lemma conn_comp_outside_back_unique {s t : finset V} (h : s ⊆ t) :
∀ c : conn_comp_outside G t,
  ∃! d : conn_comp_outside G s,
    (conn_comp_outside.to_set G t c) ⊆ (conn_comp_outside.to_set G s d) := sorry

def conn_comp_outside_back {s t : finset V} (h : s ⊆ t) (c : conn_comp_outside G t) : conn_comp_outside G s :=
  classical.some (exists_of_exists_unique (conn_comp_outside_back_unique G h c))

def conn_comp_outside_back.iff {s t : finset V} (h : s ⊆ t) (c : conn_comp_outside G t) (d : conn_comp_outside G s):
  conn_comp_outside_back G h c = d ↔ (conn_comp_outside.to_set G t c) ⊆ (conn_comp_outside.to_set G s d) :=
begin
  split,
  { rintro equ, induction equ, exact (exists_of_exists_unique (conn_comp_outside_back_unique G h c)).some_spec},
  { exact unique_of_exists_unique (conn_comp_outside_back_unique G h c) (exists_of_exists_unique (conn_comp_outside_back_unique G h c)).some_spec},
end

lemma conn_comp_outside_back.refl (s : finset V) (c : conn_comp_outside G s) :
  conn_comp_outside_back G (finset.subset.refl s) c = c :=
unique_of_exists_unique
  (conn_comp_outside_back_unique G (finset.subset.refl s) c)
  (classical.some_spec (exists_of_exists_unique (conn_comp_outside_back_unique G (finset.subset.refl s) c)))
  (set.subset.refl (conn_comp_outside.to_set G s c))

lemma conn_comp_outside_back.comm  {r s t : finset V} (k : r ⊆ s) (h : s ⊆ t) (c : conn_comp_outside G t) :
  conn_comp_outside_back G k (conn_comp_outside_back G h c) = conn_comp_outside_back G (k.trans h) c :=
unique_of_exists_unique
  (conn_comp_outside_back_unique G (k.trans h) c)
  ((exists_of_exists_unique (conn_comp_outside_back_unique G h c)).some_spec.trans
     (exists_of_exists_unique (conn_comp_outside_back_unique G k (conn_comp_outside_back G h c))).some_spec)
  (classical.some_spec (exists_of_exists_unique (conn_comp_outside_back_unique G (k.trans h) c)))


-- def ends_system := category_theory.functor.mk (conn_comp_outside G) (conn_comp_outside_back G)


end ends

end simple_graph

[Rémi Bottinelli]

mmh, or I might as well take a hybrid approach: sticking with my version of connected components, but then using the inverse systems machinery…

[Rémi Bottinelli]

@Kyle Miller Do we have lemmas stating that the sections of your functor over an inverse system are in bijection with the sections over a suitably cofinite subsystem?

[Rémi Bottinelli]

Well, after cleaning up my code a bit here I think I'll stay with the elementary approach I took until now. I'll leave the surjectivity of ends onto connected components alone while I try to attack Hopf-Freudenthal and come back to it afterwards, hopefully with a clearer mind. The inverse system approach is probably better all things compared, but in the end you still have to deal with pretty much the same things, and my elementary approach is easier for me still.

[Georgi Kocharyan]

I asked in another thread but would I be able to get writing access on the branch? I have a bunch of stuff on svarcmilnor i'd like to push! my github is GregorSamsa42

[Kevin Buzzard]

@maintainers

[Bryan Gin-ge Chen]

Invite sent! https://github.com/leanprover-community/mathlib/invitations

[Kyle Miller]

Rémi Bottinelli said:

Kyle Miller Do we have lemmas stating that the sections of your functor over an inverse system are in bijection with the sections over a suitably cofinite subsystem?

I haven't seen that in mathlib, and I presume it doesn't exist yet (but maybe I just haven't found it).

It's fine continuing with an elementary approach to get a better understanding of formalization issues -- that limit nonemptiness lemma started out that way as a first project, until it eventually morphed into a specialization of a statement about cofiltered limits of nonempty compact hausdorff spaces.

[Anand Rao]

@Rémi Bottinelli I think the following strategy (inspired heavily by the equivalence of different characterisations of ends described on Wikipedia) may work for getting a lower bound on the number of ends:

• To show that the number of ends of an infinite graph is bounded below by the number of infinite connected components, it suffices to show that every infinite connected graph $G$ has at least one end.
• Since "infinite" is defined as "not finite" in mathlib, it should be fairly easy to show the existence of arbitrarily large paths in the graph $G$. Consequently, it should be possible to show the existence of a ray $R$ (i.e., a semi-infinite path, which can be described concretely as an embedding of $\mathbb{N}$, considered as a graph, into $G$).
• To finally construct the end, we define its value on a finite set of vertices $K$ to be the unique connected component of $G \backslash K$ containing infinitely many vertices of $R$.
• More concretely, the set $\{n : \mathbb{N} \vert R(n) \in K\}$ is finite, and has an upper bound $m$. The value of the end of $K$ can be defined to be the connected component of $R(m+1)$. It can be proved as a theorem that the ray $R'(n) := R((m + 1) + n)$ is contained entirely within this connected component.

[Rémi Bottinelli]

Mmh, I was aiming for an adaptation of the proof in the stacks project here to my specific case.
The problem I foresee with the infinite ray approach is that it's not so immediate to construct the equivalence between ends as equivalence classes of rays and as limits.

[Anand Rao]

The proof I outlined actually uses the definition of ends described in your code - as a function that takes in a finite set $K$ of the graph and returns a connected component of $G \backslash K$ and satisfying the consistency condition on subsets (I should have mentioned this earlier).

The definition of ends as equivalence classes of rays is not necessary here, and only the existence of a single ray in an infinite connected graph is required.

The inverse limit approach is fine too, and I may also contribute to the proof.

[Rémi Bottinelli]

That's good to hear!

[Rémi Bottinelli]

I've worked some more, and have a rough outline of the proof of Hopf-Freudenthal.

There are now plenty of missing pieces:

• The surjectivity of the eval map is the big one.
• The fact that taking a finite set of vertices, one can extend it so that it is both connected, and all connected components outside of this finite set are infinite. (that's used in one of the preliminary lemmas towards Hopf-Freudenthal)
• The fact that applying an automorphism sends connected components to connected components, etc (should be easy with enough simple_graph-fu).
• Lots of small things for which I'm not good enough with lean to figure out efficiently.

But all in all, I think I'm getting to something viable.
The next step is probably to sort of clean up the structure a bit, reorganize as necessary, and then fill out the sorrys.
@Anand Rao: What do you think of that plan?

(I'm heading off for today!)

[Anand Rao]

Sounds good! I will try to familiarise myself with the code a bit more soon. I will start with some of the easier sorrys.

[Rémi Bottinelli]

@Kyle Miller I have a few questions about simple_graph if I may:

First, would the following lemmas fit in the api:

lemma walk.mem_support_iff_exists_append  {V : Type u} {G : simple_graph V} {u v w : V} {p : G.walk u v} :
  w ∈ p.support ↔ ∃ (q : G.walk u w) (r : G.walk w v), p = q.append r := sorry

lemma walk.support_append_subset_left {V : Type u} {G : simple_graph V} {u v w : V} (p : G.walk u v) (q : G.walk v w) :
  p.support ⊆ (p.append q).support := by simp only [walk.support_append,list.subset_append_left]

lemma walk.support_append_subset_right {V : Type u} {G : simple_graph V} {u v w : V} (p : G.walk u v) (q : G.walk v w) :
  q.support ⊆ (p.append q).support := by {
    rw walk.support_append,
    induction q,
    {simp only [support_nil, list.tail_cons, list.append_nil, list.cons_subset, end_mem_support, list.nil_subset, and_self],},
    {simp only [support_cons, list.tail_cons, list.cons_subset, list.mem_append, end_mem_support, true_or, list.subset_append_right,and_self],},
  }

Second, is there a nice way to deal with walks and their images via an automorphism and such?
Finally, is there something like lemma {V : Type *} {G : simple_graph V} [locally_finite G] [preconnected G] (v : V) (n : nat) : (ball v n).finite := sorry ?

[Kyle Miller]

@Rémi Bottinelli Yes, these would be nice to have. The first one seems like it might be more convenient in many cases than using take_until and drop_until manually.

-- right after `walk.take_spec`?
lemma walk.mem_support_iff_exists_append {V : Type u} {G : simple_graph V} {u v w : V} {p : G.walk u v} :
  w ∈ p.support ↔ ∃ (q : G.walk u w) (r : G.walk w v), p = q.append r :=
begin
  classical,
  split,
  { exact λ h, ⟨_, _, (p.take_spec h).symm⟩ },
  { rintro ⟨q, r, rfl⟩,
    simp, },
end

-- right after `walk.mem_support_append_iff`?

lemma walk.subset_support_append_left {V : Type u} {G : simple_graph V} {u v w : V} (p : G.walk u v) (q : G.walk v w) :
  p.support ⊆ (p.append q).support :=
by simp [walk.support_append, list.subset_append_left]

lemma walk.subset_support_append_right {V : Type u} {G : simple_graph V} {u v w : V} (p : G.walk u v) (q : G.walk v w) :
  q.support ⊆ (p.append q).support :=
by { intro h, simp { contextual := tt } }

[Rémi Bottinelli]

Shall I just copy, insert, and do a PR?

[Kyle Miller]

@Rémi Bottinelli The function for mapping walks over a graph equivalence has some dependent type complexity, and I'm not really sure the best way to deal with it. Here's most of one possibility:

protected def equiv (f : G ≃g G') {u v : V} : G.walk u v ≃ G'.walk (f u) (f v) :=
{ to_fun := walk.map (f : G →g G'),
  inv_fun := λ p, by { convert p.map (f.symm : G' →g G); simp },
  left_inv := begin
    intro p,
    induction p with _ _ _ _ _ _ ih,
    { simp,
      have : ∀ {a b} {h : a = b}, cast (by rw h) (nil : G.walk a a) = (nil : G.walk b b),
      { rintros _ _ rfl, refl, },
      apply this,
      simp, },
    { simp, simp at ih,
      have : ∀ {a a' b b' c c'} (ha : a = a') (hb : b = b') (hc : c = c')
        {he : G.adj a b} {p : G.walk b c},
        cast (by rw [ha, hc]) (cons he p)
          = cons (cast (by rw [ha, hb]) he : G.adj a' b') (cast (by rw [hb, hc]) p : G.walk b' c'),
      { rintros _ _ _ _ _ _ rfl rfl rfl _ _, refl },
      rw this,
      { congr' },
      all_goals { simp }, },
  end,
  right_inv := begin
    sorry
  end }

[Kyle Miller]

Rémi Bottinelli said:

Finally, is there something like lemma {V : Type *} {G : simple_graph V} [locally_finite G] [preconnected G] (v : V) (n : nat) : (ball v n).finite := sorry ?

The "walks of a given length" section of simple_graph/connectivity could be generalized to this situation. I think you can drop the preconnected assumption.

[Rémi Bottinelli]

Ah, yeah, right, I was thinking of something else for the preconnected assumption: namely that in this case the graph is countable.

[Rémi Bottinelli]

Could elaborate on the use of contextual := tt ? The docs aren't very helpful as far as I could find.

[Kyle Miller]

There's a little bit at https://leanprover-community.github.io/extras/simp.html

When it simplifies a -> b, it simplifies b with a added as a simp lemma.

[Rémi Bottinelli]

Thanks, I'm sort of mystified that you made the append_right version shorter than the append_left one, given that it's not as direct as far as I understood.

[Kyle Miller]

Here's a locally finite version:

variables (G) [locally_finite G] [decidable_rel G.adj] [decidable_eq V]

/-- The `finset` of length-`n` walks from `u` to `v`.
This is used to give `{p : G.walk u v | p.length = n}` a `fintype` instance, and it
can also be useful as a recursive description of this set when `V` is finite.

See `simple_graph.coe_finset_walk_length_eq` for the relationship between this `finset` and
the set of length-`n` walks. -/
def finset_walk_length : Π (n : ℕ) (u v : V), finset (G.walk u v)
| 0 u v := if h : u = v
           then by { subst u, exact {walk.nil} }
           else ∅
| (n+1) u v := (G.neighbor_finset u).attach.bUnion (λ (w : G.neighbor_finset u),
                  have h : G.adj u w := by simpa using w.2,
                  (finset_walk_length n w v).map ⟨λ p, walk.cons h p, λ p q, by simp⟩)

lemma coe_finset_walk_length_eq (n : ℕ) (u v : V) :
  (G.finset_walk_length n u v : set (G.walk u v)) = {p : G.walk u v | p.length = n} :=
begin
  induction n with n ih generalizing u v,
  { obtain rfl | huv := eq_or_ne u v;
    simp [finset_walk_length, set_walk_length_zero_eq_of_ne, *], },
  { simp only [finset_walk_length, set_walk_length_succ_eq,
      finset.coe_bUnion, finset.mem_coe, finset.mem_univ, set.Union_true],
    ext p,
    simp only [set.mem_Union, finset.mem_coe, set.mem_image, set.mem_set_of_eq],
    simp only [mem_neighbor_finset, finset.mem_attach, finset.mem_map, embedding.coe_fn_mk, exists_prop, exists_true_left,
  subtype.exists],
    dsimp,
    congr',
    ext w,
    congr',
    ext huw,
    congr',
    ext p',
    simp only [set.ext_iff, finset.mem_coe, set.mem_set_of_eq] at ih,
    simp [ih],
    rintro rfl,
    refl, },
end

[Kyle Miller]

The proof of coe_finset_walk_length_eq isn't pretty -- I was just trying to get it to work quickly

[Kyle Miller]

If you wanted to PR this sort of generalization (with a nicer proof), that'd be great! If not, I'll get around to it at some point.

[Kyle Miller]

Rémi Bottinelli said:

I'm sort of mystified that you made the append_right version shorter than the append_left one

You can actually use the append_right proof for append_left too, but I left it since your proof was a simp only. It's too bad that walk.support_append has that asymmetry...

[Rémi Bottinelli]

right, I originally planned it by way of enough reverses, but it felt ugly.

[Rémi Bottinelli]

As for contributing to the ball and other lemmas, I hope to do at some point. But I also would like to sort of stay focused on my ends code for now, and every little things takes lots of time still, so it may not be so soon.

[Rémi Bottinelli]

PR here: https://github.com/leanprover-community/mathlib/pull/15687

[Rémi Bottinelli]

I made your simp into simp only since I believe it's what should be done but maybe I was mistaken. I also made the two subset lemmas into @[simp].

[Rémi Bottinelli]

huh, I don't understand why the bulid fails :(

[Kyle Miller]

@Rémi Bottinelli Here's the finite ball. It's intended to go right after fintype_set_walk_length.

def ball_finset : Π (n : ℕ) (u : V), finset V
| 0 u := {u}
| (n+1) u := {u} ∪ (G.neighbor_finset u).bUnion (λ w, ball_finset n w)

lemma coe_ball_finset_eq (n : ℕ) (u : V) :
  (G.ball_finset n u : set V) = {v : V | ∃ (p : G.walk u v), p.length ≤ n} :=
begin
  induction n with n ih generalizing u,
  { simp [ball_finset], },
  { ext v,
    simp [ball_finset],
    split,
    { rintro (rfl | h),
      { use walk.nil,
        simp, },
      { obtain ⟨w, huw, h⟩ := h,
        have := congr_arg (λ (s : set V), v ∈ s) (ih w),
        simp [h] at this,
        obtain ⟨p, h⟩ := this,
        use [walk.cons huw p],
        simp [h, nat.succ_eq_add_one], } },
    { rintro ⟨p, h⟩,
      cases p,
      { simp },
      { right,
        use [p_v, p_h],
        have := congr_arg (λ (s : set V), v ∈ s) (ih p_v),
        simp at this,
        rw this,
        use p_p,
        simpa [nat.succ_eq_add_one] using h, } } },
end

def ball {V : Type u} (G : simple_graph V) [locally_finite G] (u : V) (n : ℕ) : set V :=
{v : V | ∃ (p : G.walk u v), p.length ≤ n}

lemma ball_finite {V : Type u} {G : simple_graph V} [locally_finite G]
  (u : V) (n : ℕ) : (G.ball u n).finite :=
begin
  classical,
  rw [ball, ← coe_ball_finset_eq],
  apply set.to_finite,
end

[Kyle Miller]

Rémi Bottinelli said:

huh, I don't understand why the bulid fails :(

I just retriggered the linting job. Sometimes things fail for no discernible reason.

[Kyle Miller]

It might be easier to prove that set is finite by induction on n more directly than by going through finsets. The algorithm I wrote for ball_finset is really bad -- it doesn't need to be exponential like that -- so it's not useful having that as a computable definition.

[Rémi Bottinelli]

and it might make sense to use the induced metric directly, so that the balls really are the metric ball, I guess?

[Kyle Miller]

Ah, that's where connected comes in, for simple_graph.dist to be meaningful here.

[Yaël Dillies]

I just opened #15705 for multiplicative normed groups.

[Rémi Bottinelli]

@Kyle Miller thanks for correcting the PR :) Can you tell me how you knew what made the linter unhappy ? I ran scripts/lint-style.sh but that didn't spot anything iirc.

[Kyle Miller]

Once the linter finally ran, it gave some error messages that you can see inline in the code view on GitHub. It's derived from this output: https://github.com/leanprover-community/mathlib/runs/7518225899?check_suite_focus=true

/- The `dup_namespace` linter reports: -/
/- DUPLICATED NAMESPACES IN NAME: -/
-- combinatorics/simple_graph/connectivity.lean
#check @simple_graph.walk.walk.subset_support_append_left /- The namespace `walk` is duplicated in the name -/
Error: simple_graph.walk.walk.subset_support_append_left - The namespace `walk` is duplicated in the name
... etc. ...

[Rémi Bottinelli]

Ah, thanks, I tried to see the output on the first run but somehow it seemed to be empty. Is there a way to do it locally?

[Alex J. Best]

You can add #lint to the end of every file you touch to see the output, make sure you remove it before committing though!

[Georgi Kocharyan]

My proof of svarc-milnor is now (virtually) complete, along with an example that proves Z quasi-isometric to R.
It relies on a few easy lemmas about marked_group which i've added to the file now (I think most should be one liners, but my knowledge doesn't suffice).
If anyone is bored you're welcome to have a look at them :)

[Rémi Bottinelli]

We're making some progress on the Freundenthal-Hopf theorem, but have some trouble dealing with instances/typeclasses, as typically shown here. How should I proceed to assume throughout (without the need to reference it explicitely) that my graph is locally finite and preconnected?
In the same vein, under the hypotheses, I would like to assume everywhere that a specific set is finite (as shown here but the instance doesn't "take", it seems.

[Yaël Dillies]

Are you writing instances that depend on a locally_finite assumption? If not, I would stick with passing it around explicitly.

[Rémi Bottinelli]

I am, yeah: I need locally_finite G to say that removing a finite set of vertices yield a finite number of connected components.

[Rémi Bottinelli]

That's the type inf_ro_components G K. I'd like to have [fintype (inf_ro_components G K)] everywhere (well, once I actually prove it).

[Yaël Dillies]

Yes but again do you need to go through typeclass inference for this?

[Rémi Bottinelli]

Mmh, I admit I don't understand the question: I'm not sure what typeclass inference is. Maybe it's time to look at the docs instead of blindly swapping out () for [] and see what sticks

[Yaël Dillies]

Basically you shouldn't treat TC inference as a big theorem bookkeeper. Instead (at least for Prop-valued stuff), it should be used for assumptions that are derived structurally (typically, p ∧ q ∨ r will be decidable because p, q, r is).

[Rémi Bottinelli]

Mmh, I see, and what's the rationale for this? "structurally derived" theorems are easier for lean to understand/bookkeep?

[Yaël Dillies]

TC inference is not meant to nor can be used as a SMT solver.

[Rémi Bottinelli]

Alright, thanks! I'll try and look at the docs in a bit more depth.

[Rémi Bottinelli]

Isn't gen_norm_le_one in marked_group wrong for exactly the reason @Laurent Bartholdi mentionned above: a generator might be mapped to the identity ?

[Kyle Miller]

For what it's worth, my motivation for slipping in locally_finite was to support different limiting arguments on subgraphs, for instance defining ends of graphs or lifting properties about finite graphs to infinite graphs (like how you can lift the 4-color theorem of finite planar graphs to infinite planar graphs).

Generally you'd be looking at the instances [locally_finite G] giving [locally_finite (G.delete_verts s)] or [locally_finite (G.induce s)] (or however those graphs are written), and you won't be doing any algebraic manipulation of G itself -- it's being used more like a type than a term, so to speak.

That's not to say I knew what I was doing back when I slipped it in, but given what I've learned in the meantime I think locally_finiteinstances are still justifiable for this application.

[Rémi Bottinelli]

Actually, locally_finite is not the worst offender here (lean seems to like it being an instance well enough), but preconnected G and the diverse fintype X are.

[Junyan Xu]

Kyle Miller said:

Rémi Bottinelli The function for mapping walks over a graph equivalence has some dependent type complexity, and I'm not really sure the best way to deal with it. Here's most of one possibility:

I've made a definitionally better version of the walk equiv but unfortunately it requires a re-definition of simple_graph.walk:

import combinatorics.simple_graph.basic

universes u v
namespace simple_graph
variables {V : Type u} {V' : Type v} {G : simple_graph V} {G' : simple_graph V'}

inductive walk (G : simple_graph V) : V → V → Type u
| nil {u v : V} (h : u = v) : walk u v
| cons {u} (v) {w} (h : G.adj u v) (p : walk v w) : walk u w

def walk.map (f : G →g G') : Π {u v : V} {u' v' : V'} (hu : f u = u') (hv : f v = v'),
  G.walk u v → G'.walk u' v'
| u v u' v' hu hv (walk.nil h) := walk.nil (by rw [← hu, h, hv])
| u v u' v' hu hv (walk.cons w h p) := walk.cons (f w) (hu ▸ f.map_adj h) (walk.map rfl hv p)

protected def walk.equiv (f : G ≃g G') {u v : V} {u' v' : V'} (hu : f u = u') (hv : f v = v') :
  G.walk u v ≃ G'.walk u' v' :=
{ to_fun := walk.map (f : G →g G') hu hv,
  inv_fun := walk.map (f.symm : G' →g G) (by simp [← hu]) (by simp [← hv]),
  left_inv := λ p, begin
    induction p with _ _ _ _ _ _ ih generalizing u',
    { refl },
    { change walk.cons _ _ _ = _, congr' 1,
      { simp }, { conv_rhs { rw ← p_ih hv rfl }, congr; simp } },
  end,
  right_inv := λ p, begin
    induction p with _ _ _ _ _ _ ih generalizing u,
    { refl },
    { change walk.cons _ _ _ = _, congr' 1,
      { simp }, { conv_rhs { rw ← @p_ih hv (f.symm p_v) (by simp) }, congr; simp } },
  end }

protected def walk.equiv' (f : G ≃g G') {u v : V} : G.walk u v ≃ G'.walk (f u) (f v) :=
walk.equiv f rfl rfl

end simple_graph

[Junyan Xu]

I'm not sure if allowing equality in walk.nil is really necessary; we may use eq.rec (walk.nil ...), and if f (g v) = v definitionally then it would compute to walk.nil ....

[Kyle Miller]

@Junyan Xu That's a good idea. There's a trick that lets us avoid needing to modify the inductive type itself that is theoretically equivalent, which is to add in a copy function:

def walk.copy (p : G.walk u v) (hu : u = u') (hv : v = v') : G.walk u' v' :=
by { subst hu, subst hv, exact p }

Then the modified inductive type corresponds to wrapping constructors with this copy function.

With this and some accompanying lemmas, the left_inv and right_inv proofs are simp (in my code below it's longer because there are still some missing lemmas).

import combinatorics.simple_graph.connectivity

variables {V : Type*} {G : simple_graph V} {V' : Type*} {G' : simple_graph V'}
variables {V'' : Type*} {G'' : simple_graph V''}
variables {u v w u' v' w' u'' v'' w'' : V}

namespace simple_graph

def walk.copy (p : G.walk u v) (hu : u = u') (hv : v = v') : G.walk u' v' :=
by { subst hu, subst hv, exact p }

@[simp] lemma walk.copy_rfl_rfl (p : G.walk u v) (hu : u = u) (hv : v = v) :
  p.copy hu hv = p := rfl

@[simp]
lemma walk.copy_copy (p : G.walk u v)
  (hu : u = u') (hv : v = v') (hu' : u' = u'') (hv' : v' = v'') :
  (p.copy hu hv).copy hu' hv' = p.copy (hu.trans hu') (hv.trans hv') :=
by { subst_vars, refl }

@[simp]
lemma walk.copy_nil (hu : u = u') : (walk.nil : G.walk u u).copy hu hu = walk.nil :=
by { subst_vars, refl }

lemma walk.copy_cons (h : G.adj u v) (p : G.walk v w) (hu : u = u') (hw : w = w') :
  (walk.cons h p).copy hu hw = walk.cons (by { subst hu, exact h }) (p.copy rfl hw) :=
by { subst_vars, refl }

@[simp]
lemma walk.cons_copy (h : G.adj u v) (p : G.walk v' w') (hv : v' = v) (hw : w' = w) :
  walk.cons h (p.copy hv hw) = (walk.cons (by { subst hv, exact h }) p).copy rfl hw :=
by { subst_vars, refl }

@[simp]
lemma walk.map_copy (f : G →g G') (p : G.walk u v) (hu : u = u') (hv : v = v') :
  (p.copy hu hv).map f = (p.map f).copy (by subst hu) (by subst hv) :=
begin
  induction p with _ _ _ _ _ _ ih generalizing u' v',
  { subst_vars, refl, },
  { rw [walk.copy_cons],
    simp only [walk.map],
    rw [walk.copy_cons, ih], }
end

lemma walk.map_map (f : G →g G') (f' : G' →g G'') (p : G.walk u v) :
  (p.map f).map f' = p.map (f'.comp f) := by { induction p; simp [*] }

@[simp] lemma walk.map_id (p : G.walk u v) : p.map hom.id = p := by { induction p; simp [*] }

lemma walk.map_of_eq {f : G →g G'} (f' : G →g G') (h : f = f') (p : G.walk u v) :
  p.map f = (p.map f').copy (by rw h) (by rw h) :=
by { subst_vars, refl }

protected def walk.equiv (f : G ≃g G') :
  G.walk u v ≃ G'.walk (f u) (f v) :=
{ to_fun := walk.map (f : G →g G'),
  inv_fun := λ p, (p.map (f.symm : G' →g G)).copy (by simp) (by simp),
  left_inv := λ p, begin
    simp [walk.map_map],
    rw walk.map_of_eq hom.id, swap, { ext, simp },
    simp,
  end,
  right_inv := λ p, begin
    simp [walk.map_map],
    rw walk.map_of_eq hom.id, swap, { ext, simp },
    simp,
  end }

end simple_graph

[Kyle Miller]

This is somewhat like manipulating sigma types, however with this you get constant definitional control over the endpoints of walks, which is quite nice!

[Junyan Xu]

If you #print walk.copy you see it's just eq.rec (eq.rec p hv) hu though and not of the form nil or cons. If hu and hv are not defeqs it doesn't compute/reduce.

[Kyle Miller]

I almost wrote it as eq.rec directly, but I thought using subst was clearer.

[Kyle Miller]

That's true they don't reduce, however having a custom eq.rec means it's easier to write all the supporting simp lemmas, which is a point I forgot to mention explicitly.

[Junyan Xu]

Yeah eq_to_hom is also secretely an eq.rec...

[Kyle Miller]

This lets us deal with the "evilness" of rewriting morphisms(/functors):

lemma walk.map_of_eq {f : G →g G'} (f' : G →g G') (h : f = f') (p : G.walk u v) :
  p.map f = (p.map f').copy (by rw h) (by rw h)

[Kyle Miller]

The idea is that the simp normal form for copy is to be the outermost thing in an expression, so that way copy_copy merges them, and eventually you can (hopefully) eliminate them completely.

[Kyle Miller]

Unlike for category theory, this evilness is a necessary evil since we aren't working with vertices up to isomorphism, but actually up to equality. There are no higher morphisms to save us.

[Georgi Kocharyan]

Rémi Bottinelli said:

Isn't gen_norm_le_one in marked_group wrong for exactly the reason Laurent Bartholdi mentionned above: a generator might be mapped to the identity ?

uh yes true, the version for subsets is right but I forgot to change the original version (the name le_one is correct though ^^)

[Rémi Bottinelli]

Hey, so we've been working on Freudenthal-Hopf with @Anand Rao for a while, and are getting sort of stuck/unsure about how to architect things. The "pure graph theoretical" part is mostly done, with a few sorries, but to prove the surjectivity of ends onto infinite connected components, we finally decided on using the lemma from mathlib about finite nonempty filtered inverse systems, and this cascaded into wanting to define ends really as limits, rather than as our own type, and then noticing that most of our code really should be stated in this more general setting. The code is here if anyone wants to chime in with some feedback. I believe the correct way wrt mathlib would be to have as much general stuff out of our code as possible, but it seems there is a pretty heavy infrastructure code to this.

[Rémi Bottinelli]

OK, after some more work here, we're planning on merging our work with the geometric-group-theory branch: anybody minds?

We're close to having:

• Ends for (locally finite, connected) graphs in ends_limit_construction.lean.
• A slightly modified statement of Freudenthal-Hopf in Freudenthal_Hopf.lean.
• A notion of "coarse maps" of graphs and closeness for such maps, in order to have functoriality of ends in functoriality.lean.
• The fact that quasi-isometries of graphs yield bijections of ends (again, slightly modified to match our definitions).
• Plenty of sorrys peppered around, but mostly stuff that we feel should be easy from (eventual) mathlib lemmas.
• The set of connected components outside of a finite set is defined in comp_out.lean: we took a kind of hybrid approach: defining the connected components outside of K as (G.remove_verts K).connected_component made coercions sort of unmanageable.
  Instead, we define a subgraph on the same vertex set that deconnects all of K, and then we just look at the components disjoint from K.
  This worked well enough for us.

The plan now is to do some cleanup and reorganization of the files, and then merge, assuming that's OK with people.

[Rémi Bottinelli]

And now I want to start working on Bass-Serre theory, and for this I'd welcome some opinions:

• I was thinking of starting with The fundamental groupoid of a graph of groups by Higgins.
  It seems to work at a nice abstraction level, but:

• This relies on presentations of groupoids, e.g. Presentations of groupoids, with applications to groups by Higgins also.

As far as I could find, there is essentially no code for presentations of groupoids in mathlib: the closest is the code for Nielsen-Schreier.
Does it make sense to start this low down the hierarchy and actually take the time to define presentations of groupoids, and then go up again via Higgins' paper, to, eventually, start working on Bass-Serre, or is a hands-on approach (maybe even forsaking groupoids) more reasonable?

The paper Presentations of groupoids… actually has Nielsen-Schreier and Kurosh as applications, which makes me believe that it might not be a bad idea to start here: we can already get non-trivial stuff from that approach, and in any case, I guess presentations of groupoids might prove useful more generally than for Bass-Serre?

[Yaël Dillies]

By the way, I am still reorganising norms to defin multiplicative normed groups. It's taking ages.

[Antoine Labelle]

I think that presentations of groupoids would definitely be useful by itself, independantly of Bass-Serre theory.

[Rémi Bottinelli]

OK, I imported our work into the geometric-group-theory branch.
@Yaël Dillies before doing the (manual) import, I tried running leanproject rebase on the ggt branch, but the rebase failed because of a duplicate definition of seminorm (or something like that). I expect that is because you had a preliminary definition locally in the ggt branch and you're now comitting bits on master. Can I safely remove the local definition?

[Yaël Dillies]

I think so, but what definition is it exactly?

[Rémi Bottinelli]

oh, maybe I misread the error:

> leanproject rebase
Checking out master...
Pulling...
`get-mathlib-cache` is for projects which depend on mathlib, not for mathlib itself. Running `get-cache` instead.
Looking for mathlib oleans for 75cc1ae964
  locally...
  Found local mathlib oleans
Using matching cache
Applying cache
  files extracted: 2674 [00:14, 179.97/s]
Checking out geometric-group-theory...
Rebasing...
Cmd('git') failed due to: exit code(1)
  cmdline: git rebase master
  stdout: 'Auto-merging src/analysis/seminorm.lean
CONFLICT (content): Merge conflict in src/analysis/seminorm.lean'
error: could not apply 8bbccf027f... use type synonyms, group seminorms
hint: Resolve all conflicts manually, mark them as resolved with
hint: "git add/rm <conflicted_files>", then run "git rebase --continue".
hint: You can instead skip this commit: run "git rebase --skip".
hint: To abort and get back to the state before "git rebase", run "git rebase --abort".
Could not apply 8bbccf027f... use type synonyms, group seminorms'

[Yaël Dillies]

Ah yes, that's different. You will have to fix conflicts by hand. I can do it if you promise me not to touch the branch for the next half hour

[Rémi Bottinelli]

Alright, informing @Anand Rao too, thanks!

[Yaël Dillies]

Done!

[Rémi Bottinelli]

quick half hour, thanks a lot!

[Antoine Chambert-Loir]

Rémi Bottinelli said:

And now I want to start working on Bass-Serre theory, and for this I'd welcome some opinions:

• I was thinking of starting with The fundamental groupoid of a graph of groups by Higgins.
  It seems to work at a nice abstraction level, but:

• This relies on presentations of groupoids, e.g. Presentations of groupoids, with applications to groups by Higgins also.

As far as I could find, there is essentially no code for presentations of groupoids in mathlib: the closest is the code for Nielsen-Schreier; but category_theory.path_category and category_theory.quotient should provide good building blocks.
Does it make sense to start this low down the hierarchy and actually take the time to define presentations of groupoids, and then go up again via Higgins' paper, to, eventually, start working on Bass-Serre, or is a hands-on approach (maybe even forsaking groupoids) more reasonable?

The paper Presentations of groupoids… actually has Nielsen-Schreier and Kurosh as applications, which makes me believe that it might not be a bad idea to start here: we can already get non-trivial stuff from that approach, and in any case, I guess presentations of groupoids might prove useful more generally than for Bass-Serre?

Chapter IV of Bourbaki's Topologie algébrique has another result on these lines, which looks more general than Higgins, at least it is framed in terms of coequalizers of groupoids. With applications to the van Kampen theorem where they give formulas that I do not think exist at other places.

[Rémi Bottinelli]

I'll take things slow and start with trying to mimick the subgroup API for subgroupoids

[Yaël Dillies]

Can't you just use subobject C where C is a groupoid ?

[Kyle Miller]

@Yaël Dillies I imagine that word "just" is standing in for various design tradeoffs and how you imagine subobjects working in general. Would you mind elaborating? (That's docs#category_theory.subobject correct?)

[Kyle Miller]

It seems to me that it's easier to work with explicit subsets rather than isomorphism classes of monomorphisms, sort of like how for simple graphs we can represent a subgraph as a subset of vertices and a sub-relation. Maybe it's workable building up API around category_theory.subobject for concrete categories, to let you ignore the quotient in practice.

[Yaël Dillies]

That wasn't a rhetorical question! What I have in mind, in decreasing order of preference and increasing of boilerplate, is:

1. We can just use subobject C and its API
2. We can just use subobject C but we need specific API
3. We introduce a new structure for subgroupoids, show its equivalence to subobject C and use the subobject API through that equivalence
4. We introduce a new structure for subgroupoids, show its equivalence to subobject C and transfer the subobject API through that equivalence
5. We introduce a new structure for subgroupoids, build its API separately, and possibly show its equivalence to subobject C
6. We introduce a new structure for subgroupoids that's not equivalent to subobject C, and build its API separately

[Rémi Bottinelli]

uh, I was heading in this direction. which I now understand not to be ideal.

[Rémi Bottinelli]

But both groups and graphs are sort of following this pattern, so I thought I was safe. Aren't I?

[Kyle Miller]

@Rémi Bottinelli That's a nice encoding trick you have, where the existence of an identity arrow corresponds to whether an object is present in the subgroupoid. I wonder if it would make sense, though, to introduce subquiver and have subgroupoid extend that? Or maybe you keep it the same but have it extend docs#wide_subquiver? (I'm not sure if this leads to any issues.)

[Kyle Miller]

I think Yael's suggestion is reasonable but more on the speculative end of things -- @Yaël Dillies Do we have much experience in mathlib with defining subobjects using docs#category_theory.subobject? I think we understand how to create subobjects using custom structures fairly well.

[Adam Topaz]

Using docs#category_theory.subobject is great if all you care about is the lattice structure of the type of subobjects, but I think making a custom structure is a better approach whenever you want to work with actual elements of the subobject.

[Rémi Bottinelli]

What would subquiver bring to the table? I think in that case we would lose the "trick" you're refering to, right?

[Rémi Bottinelli]

(deleted)

[Rémi Bottinelli]

I'm working on the free groupoid and have a question:
I've defined a custom inductive type of "words" on my initial quiver as here but there is also quiver.path and quiver.symmetrify.
The problem with using quiver.path and quiver.symmetrify is mostly that I have to deal with the type synonym introduced by quiver.symmetrify.

Should I work with what's already here anyway?

[Junyan Xu]

Just wanna let you geometric group theory folks know about the amenable group PRs (Zulip discussion); maybe you would be interested in helping reviewing them? The code looks like it needs to go through a lot of revisions, but firstly we need to make some design decisions. The references listed in the PRs are:

• [C. Löh, Geometric Group Theory, Definition 9.1.1][loeh17]
• https://en.wikipedia.org/wiki/Amenable_group
• [A.L.T. Paterson, Amenability, Definition 0.2][Paterson1988]

[Yaël Dillies]

Heads up that #15705 is in, so we now can PR marked groups and such!

[Rémi Bottinelli]

Great! For now I'm busy trying to deal with groupoids and eventually Bass-Serre hopefully.
There was a discussion about marked groups perhaps not being the best place to start with the geometry of groups: is there a consensus on that?

By the way, I noticed I'm starting to use quivers quite extensively, and will probably use them to do graph theory: say talk about the existence of maximal trees, etc. There already was [has_reverse] on quivers, and I added [has_involutive_reverse] and now I feel this is dangerously close to simply talking of graphs.
Would it make sense to take this as an opportunity to make this the official definition of "unoriented multigraph" ? (opinion, @Kyle Miller ?)

[Yaël Dillies]

Do you know about #16100?

[Rémi Bottinelli]

I didn't, no! hum, this makes my stuff quite redundant… Why not base it on quivers?

[Yaël Dillies]

There are several reasons, really. But I think both approaches are viable.

[Rémi Bottinelli]

I like using quivers since it allows a natural "symmetrization", and you have fewer equalities to deal with I'm used to it already, in some sense… I assume changing the implementation of multigraphs isn't acceptable? What do you recommend I do, then?

[Yaël Dillies]

#16100 is just experimental, but I do not believe your "there are fewer equalities to deal with". Multigraphs are so that you should never need defeq on the type of edges.

[Rémi Bottinelli]

I see, yeah. I wanted to use the "Serre" definition of graphs to begin with, but after looking at what they do in Bass-Serre, it's always orientation-preserving actions (and the involution on edges has no fixed points), meaning you can just choose an orientation and be done with it: hence quivers.

[Rémi Bottinelli]

OK, so what's the way forward with this, and how can I help it making progress?

Note also that the quiver definition make the passage to categories very easy but with this custom definition you need to add more glue code as far as I can see.

[Rémi Bottinelli]

Something else I'd like to get some opinions on: I need to talk about "free products" and quotients of groupoids. My first instinct was to define this by hand, but actually I see that there is code for Cats and Groupoids talking about limits and such, and I'm wondering how much of the existing tooling I should/can use.

• If I'm not mistaken, I can take limits/colimits in Cats and they'll actually also define limits/colimits in Groupoids (that's a general mathematical statement, not talking about mathlib).
• On the other hand, I actually don't see that Cats has coequalizers in mathlib, is that right?
• Also, I'm wondering if defining those construction via "the category of …" will involve much more boilerplate than defining them by hand.

So, in short, where should I draw the line, and what's the correct way to proceed here?

[Junyan Xu]

Limits in Cat was done by Joseph Hua in this thread back in February, but was added to mathlib by @Scott Morrison in March in #12979, maybe using a different approach, I didn't check. I'm pretty sure we don't have colimits yet, given that category_theory.category.Cat.limit has no siblings in the same directory.

[Scott Morrison]

(Sorry, I had completely missed Joseph's thread, I think.)

[Rémi Bottinelli]

As an aside, there is something I don't totally get with the organization of mathlib.
What does the organization wrt "what should be included in what order using which construction" look like?
This might be a bit naive of my part, but it feels like it's some kind of a big soup of people contributing what they feel like and reviewers accepting on a case-by-case basis without much "long-term"/organizational thought. I'd expect to see some kind of hierarchy of subjects, with working groups deciding on the design and strategy of the subject in a way that makes it harder for people to work blindly on something that will be useless or already worked on. I don't want to spit in the soup, and am very grateful to everyone involved for the coaching and help in getting stuff included, but I'm wondering if these is some margin for streamlining of the process?

[Yaël Dillies]

Have you seen https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/mathlib.20organization ?

[Rémi Bottinelli]

I have, but missed the "teams" part.
It's indeed part of what I'm talking about, but doesn't seem to cover a more involved hierarchy of subjects and plans as for how to cover them, does it? Is having such a specified plan just too ambitious and bureaucratic, and a risk of killing the "organic" flow mathlib is currently working with?

[Andrew Yang]

I'd think that the current canonical answer to "How to prevent oneself from working blindly on something that will be useless or already worked on" is to ask on zulip before starting.

[Scott Morrison]

I think the answer is mostly that the "long-term organizational thought" doesn't actually come to much without someone able/willing to write the code, and so we mostly prefer to let mathlib grow organically according to what people actually want to write.

We're mostly extremely liberal on what counts as "appropriate to mathlib", with occasional exceptions.

That said, I think there is a lot of "organizational planning" that happens off in branches, and during the PR process. It's not at all unusual that it takes several developments of the same material before it actually makes it into mathlib.

[Jireh Loreaux]

Perhaps they are underutilized, but we also have projects on GitHub for this sort of thing.

[Rémi Bottinelli]

Hey, so I've finally managed to get the quotient construction for groupoids working, and thus presentations.
My construction for the quotient is perhaps unorthodox, in that (as said above) I first quotient by the isotropy groups only, which means no collapsing of vertices, and then quotient by what remains, which is always graph_like i.e. has at most one edge between two vertices.

I'd be thankful if someone could have a look at the code here and tell me if it's worth cleaning up to make a PR, of if this approach is considered too dirty.