Geometric Group Theory coordination ?

Stream: general

[Rémi Bottinelli]

Hey,

I've seen a few people have started working on geometric group theory (mostly Cayley graphs, the word metric, Švarc–Milnor and some coarse geometry afaik). Earlier this year, I tried attacking this without much success and am now getting back to it. I would very much like to start working in a synchronized way with people tackling the same subject, and thus propose to set up some kind of coordination.

Ideally, we'd have a sort of clear roadmap of what comes before what and what level of generality should be aimed for in each case, but maybe that's too early planning. A typical example of questions which I got bogged down on is: In what setting should the end space of a group be defined. In a sense, graphs are maybe not the most natural/ideal setting to define that, because the "coarse metric" aspect gets lost in translation, but then what is? Similar questions got in my way for Cayley graphs (e.g. don't we want to have an emetric space to keep things as general as possible?)
Anyway, my plans now would be to try to deal with Bass-Serre theory, since it's much more algebraic, and thus probably less prone to this problem of not knowing how to set things down.

What do you think?

[Sebastien Gouezel]

Easy answer for the space of ends: this should first be defined for any topological space. Then given a generating set you get the space of ends of the corresponding Cayley graph (with edges added), and then you have to check that it does not depend on the choice of the generating set. But doing it for any topological space first is important, as this notion also shows up in the classification theorem of surfaces, for instance.

[Rémi Bottinelli]

That makes sense, though I sort of still have a problem with that, in that I have a feeling getting topology into play when talking about coarse geometry is kind of a wrong direction. As I see it, you can define a topological notion of ends, and a “graphical” one, and they agree when realizing certain well-behaved enough graphs as topological spaces, but does that mean the topological notion really is the most natural one ? Going further in this direction: When talking about ends of a group, I feel like it would be best to have a notion which is more naturally quasi-isometry invariant, or more generally, a coarser notion. Do we really need to do the topological détour, when topology really hasn't much to do with coarse geometry ? We care about large scale stuff, and topology is made for small-scale stuff, no?

I know there exists a notion of “binary Higson Corona” for coarse structures that, I believe, strictly generalize that of ends of graphs.
A strategy I had in mind was then to define ends in two ways: a very general one for coarse spaces, and a very restricted one for graphs, and prove that they agree when your graph has the path metric. This would get QI-invariance for free I believe.
This strategy brings up the question/problem of maybe directly defining a coarse structure on finitely generated groups, without the metric intermediate representation. And that's where I start to see the analysis paralysis getting closer!

[Junyan Xu]

Independent question: maybe GGT people can comment on whether you want noncommutative linearly ordered groups? https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Why.20linear_ordered_ring

[Antoine Labelle]

It would be super cool indeed to have some Bass-Serre theory :smile:

[Oliver Nash]

cc @Jim Fowler

[Jim Fowler]

I'd love to see Bass-Serre theory.

[Jim Fowler]

I guess one can consider mul_actions on graphs which are trees?

[Kevin Buzzard]

cc @Siddhartha Gadgil

[Antoine Labelle]

Jim Fowler said:

I guess one can consider mul_actions on graphs which are trees?

I think a group action on a graph should be expressed as a mul_action on vertices + a mul_action on edges + the compatibility condition between those two.

[Siddhartha Gadgil]

For a lot of stuff (e.g. as defined in Lyndon-Schupp) we do not need topology associated to a graph. This matters more to me because I use lean 4 which does not yet have topology, but the principle of keeping things lighter is reasonable anyway.

For example, one can define graphs and 2-complexes prove stuff like Fenchel-Nielsen theorem and even (with some work) Stalling's topological proof of Grushko's theorem defining fundamental groups and coverings in the category of combinatorial 2-complexes. Serre-Bass also fits in well here, as does ends of groups.

[Siddhartha Gadgil]

The relation to topological spaces is important but parallel to GGT and "topological methods in group theory"

[Antoine Labelle]

I also think that this stuff would be more easily expressed with Serre's definition of a (multi)graph rather than the current simple_graph. This has been discussed here but I don't know what this discussion became.

[Rémi Bottinelli]

To be totally honest, I planned on getting acquainted with Bass-Serre in parallel to the formalization process, and working with an ad-hoc definition of graphs (Serre's definition with sets E, V, two functions E -> V and an involution on E) before trying to use most of mathlib. In a sense, stay as close to the presentation at hand. Open to changing the plan though.

[Yaël Dillies]

Let me plug #11000

[Jim Fowler]

I also pushed some code to properties.lean on the geometric-group-theory branch to (badly) define things like residually and

def virtually (property : group_property) (G : Type*) [group G] : Prop :=
∃ (H : subgroup G), H.index > 0 ∧ property H

It would be nice to be able to say things like virtually is_free_group but is_free_group isn't a Prop. Are there other instances in mathlib where structure or properties are transformed with adverbs like virtually, residually, etc.?

[Eric Wieser]

You can say virtually (λ G, nonempty (is_free_group G)) or similar

[Rémi Bottinelli]

By the way, is it better to stick everything to a single group_theory/geometric folder, or should we allow messing with the hierarchy more freely? Say, defining the ends of a graph maybe should still live in combinatorics/graph_theory?

[Yaël Dillies]

For the purpose of writing stuff, I highly suggest sticking to a single place. You can then put the files in the right place when PRing.

[Jim Fowler]

I added some code to properties.lean at https://github.com/leanprover-community/mathlib/blob/geometric-group-theory/src/group_theory/geometric/properties.lean#L11-L13 which includes

class mul_equiv_respects (property : group_property) :=
(eq_preserves: Π {G : Type*} [group G], Π {H : Type*} [group H],
(G ≃* H) → (property G) → (property H))

since I don't see any other way to ensure that a "property of a group" is actually a property of a group up to equivalence of groups. I'm not super clear how lean and mathlib handle transporting things like Props across equivs. I still feel like I'm fighting against typeclass inference with the definition of residually.

[Yaël Dillies]

The philosophy that mathlib adopts is that <some object> properties usually transfer along maps weaker than <some object> isomorphisms. Hence we basically never write down the iso version of the transfer, but rather the weaker one. This means that your mul_equiv_respects is most likely useless, as in practice you won't always have a group isomorphism at hand. Furthermore, your approach is more metatheoretical than it needs to be. Rather than reasoning about properties that transfer, you directly transfer the properties. This is justified because:

• You never talk about properties that don't transfer
• The amount of reasoning done at that level of generality is minimal, so it's innocuous redoing it in each concrete situation.

[Yaël Dillies]

But this last point might be wrong in your case. Maybe you do carry enough reasoning at the metatheoretical level that you wouldn't want to do it for each concrete property.

[Kevin Buzzard]

When I started with lean I was utterly convinced that this mul_equiv_respects thing would be crucial in algebra and algebraic geometry, but I was very surprised to find that it didn't seem to be at all.

[Junyan Xu]

Respecting isomorphisms isn't that interesting a predicate on properties, but there are other predicates that are useful in AG, and we are recently seeing #14944, #14966, and #15452 (these involve properties of morphisms not objects though). It appears that the predicates aren't made into classes yet, and in the case of the last PR the predicate doesn't get a separate definition.

[Yaël Dillies]

I am implementing the type synonyms approach now.

[Siddhartha Gadgil]

I will be giving a couple of lectures on something related, but am planning to start working on formalizing topological/geometric methods in Group theory. Is there any update on this. In particular, I did not see any formalization of

• Cayley Graph
• Graph's as normally used in Serre-Bass theory
• CW complexes
• Amalgamated free products and HNN extensions

Am I correct that none of this is in Mathlib? @Anand Rao Tadipatri @Antoine Labelle @Kyle Miller @Rémi Bottinelli

I plan to take as a target the Scott-Wall article "Topological methods in Group Theory". Of course collaboration is very welcome.

[Yaël Dillies]

Have you already checked branch#geometric-group-theory ?

[Siddhartha Gadgil]

Thanks. I did not know of this. Will look at it.

[Siddhartha Gadgil]

Looks like it is best to start with porting this.

[Rémi Bottinelli]

For graphs as used by Serre, there was some discussion about either going with plain quivers with an involutive inverse operation on edges, or defining a new type. I was in favour of the former, but it does involve plenty of hardship with index types (for me), which kind of makes me doubt whether it's the right way.
I made a start with Cayley graphs here: !3#18693, but I'm not sure there is much worth salvaging…
Finally, I had some hopes to develop combinatorial/geometric gt by leveraging groupoids, which could make things easier (most importantly Bass-Serre I thought) in the long term, and also allow some more topology more easily (pi₁ and covering spaces, van Kampen, etc).

[Siddhartha Gadgil]

Thanks @Rémi Bottinelli
If there is not much in that direction, it may be easiest for me to work with a clean slate and do Bass-Serre theory topologists style (and hopefully Grushko's theorem along the way). When something is ready for PR duplication can be reduced or bridge code written.

Concretely, I am starting with the following definitions:

structure Graph (V E : Type) where
  ι : E → V
  bar : E → E
  bar_involution: ∀ e, bar (bar e) = e
  bar_no_fp : ∀ e, e ≠ bar e

def Graph.τ {V E : Type} (G : Graph V E) (e : E) : V := G.ι (G.bar e)

inductive EdgePath {V E : Type} (G : Graph V E) : V → V → Type where
  | nil : ∀ v, EdgePath G v v
  | cons {v w u : V} : (e : E) →
        (EdgePath G w u) →  G.ι e = v → G.τ e = w  → EdgePath G v u

[Kevin Buzzard]

Is mathlib's definition of a graph no good for you? docs#SimpleGraph

[Siddhartha Gadgil]

Simple graphs are not good for topology. For instance we would want a circle to be a graph with 1 vertex and 1 edge, and for a free group have a single vertex and one edge for each generator.

[Siddhartha Gadgil]

But a variant of the above may be better: having a structure EdgeBetween which includes the proofs.

[David Wärn]

It looks like you can use docs#Quiver.HasInvolutiveReverse and docs#Quiver.Path

[Rémi Bottinelli]

Yeah, that's what I was refering to, and @Antoine Labelle added quite a few casting lemmas to facilitate working with those.
Note also that @Yaël Dillies has !3#16100 for multigraphs.

[Siddhartha Gadgil]

Thanks. @Anand Rao Tadipatri had also mentioned the definition with Quivers and I saw that EdgeBetween gives exactly that.
My first attempt will be for a demo so I will give self-contained definitions, but it seems eventually that the quiver approach is the best.

[Yaël Dillies]

#16100 is pending experimentation from Kyle in Lean 4.

[Scott Morrison]

I think it's good that we have multiple ab initio attempts at proving things using different graph formalisations. As long as everyone goes into ready to make compromises, and rip out their "favourite" definition to replace it with something mathlib compatible later, if necessary!

[Kyle Miller]

There's also something to be said about using the correct definition of a graph in each particular circumstance and then hope we can engineer bridges between all these graph theories. Let's not shoehorn things into simple graphs or quivers just because it seems like in the short term we'll have less code duplication!

[Kyle Miller]

I think Siddhartha's definition looks good for its purpose, and my only quibble is that E might be better as H or D (half-edge or dart)

[Antoine Chambert-Loir]

I don't think there's a better definition than the one used by Siddhartha (because it's basically the only one that allows for a functorial topological realization). However, it is useful to implement other versions of graphs (such as simple graphs, quivers, etc.) and natural coercions functions to standard graphs.

[Antoine Chambert-Loir]

For example, Serre's book (and Bourbaki's Topologie algébrique takes the same path) starts with quivers, defines graphs as above (quiver + fixed-point-free involution on edges), defines the graph associated with a quiver (add a reverse edge for each edge), an orientation of a graph (choose one edge between any two which are exchanged by the involution) and the associated quiver, proves that the corresponding graph is the initial one, etc.

[Kevin Buzzard]

It was remarked in 2019 that Lean had perfectoid spaces but not graphs, which was funny at the time; one reason for this was that people only mean one thing by perfectoid spaces but they seem to mean many things by a graph. It was argued that until the applications came along, we should hold off from committing to a definition of graph, and it was certainly remarked back then that probably more than one definition would be needed. It's great to see the applications finally coming along :D

[Siddhartha Gadgil]

Thanks all. Looks like the best approach is to go ahead and formalize for the next several weeks, and then reconcile if and when we have some non-trivial mathematical results. Grushko's theorem is one of my targets, small cancellation groups is another.

[Kyle Miller]

@Kevin Buzzard We committed to a definition of a simple graph a couple years ago and have various applications in mathlib. I'd say it's great having applications that force us to branch out to more than one kind of graph (this topological multigraph)

[Kyle Miller]

(We've had a need for simple digraphs for a while, but there's still an annoying dependent type issue that needs thought in that PR Yael mentioned in the interface to unify graphs and digraphs...)

[Alex J. Best]

I'd love to know what some of the lean graph theory people think about https://github.com/apnelson1/gen_graph/blob/master/graph.lean, a design that @Peter Nelson was experimenting with in Banff

[Yakov Pechersky]

Why should the Props about graphs be typeclases, as opposed to explicitly passed hypotheses?

[Peter Nelson]

No strong reason, but it is was more or less that I was thinking about simple graphs, multigraphs etc as 'settings' rather than hypotheses.

[Peter Nelson]

For instance, if proving a theorem about simple graphs with the subgraph order, you want simplicity to be invisibly preserved via typeclasses when passing to a subgraph, rather than providing an explicit proof. With something like the minor order, simplicity is something you'd need to prove.

[Peter Nelson]

Also, @Alexander Byard was looking at translating the design to lean 4 (and fixing an issue with the way I defined 'pair graphs')

[Yakov Pechersky]

That's absolutely valid. I was thinking about all of the various possible constructions that one does with graphs, like adjoining or deleting graphs, vertices, and edges, which might keep the simple/digraph/etc property. Composition of these constructions might create propeq but not defeq constructions, which might complicate TC search, even though they're all prop. I'm not sure.

[Kyle Miller]

I think typeclasses to organize the different kinds of graphs is going to be mathlib's future, but I'm not sure about everything being in terms of a single universal graph type constrained by typeclasses (though I'd like mathlib to be able to support everyone's personal favorite concrete graph type).

Basically, if there's a universal graph type that's being constrained, you may as well as take the next step and have typeclasses for the different fields of the different graph types, and then general theorems about graphs become theorems about types that have some collection of typeclasses (data and properties) -- all without there being any concrete graph type. The situation is somewhat similar to how homomorphisms are handled in the algebraic hierarchy.

[Kyle Miller]

I thought Yaël posted a different PR, so my previous comments about it make no sense; there's also mathlib4#4127 (and take a look at the Graph.Classes module). It's taking a first step implementing graph classes with a similar design to what Yaël had argued for, but starting with adding just digraphs since it's clearer how to modify the simple graph API for digraphs, and there are technical challenges that crop up even here.

I'll try to explain the problem better soon (or, better, solve it!) but right now this Adj function doesn't behave well on coercions of subgraphs to graphs, since simp is able to simplify subgraph expressions, which changes a type argument to a defeq but syntactically different type, and then some naturally formulated simp lemmas can't apply. Maybe the solution is no_index, which I just learned about from Zulip in the last week.

[Peter Nelson]

no_index seems hard to search for on zulip, because it gets too clever and removes the no_. Can you link to something for the curious?

[Scott Morrison]

https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/simp.20for.20ModelProd/near/363844421

[Peter Nelson]

And I'm happy to see this discussion. I don't have the time/energy to push mathlib graph to be exactly the way I want them, but I think the fact that there are truly multiple notions of 'graph' (and that even in informal mathematics, no single one of them is correct) is worth paying a lot of attention to; a solution that allows for all of them is quite important.

Formalizing the Robertson/Seymour graph minors structure theorem is one of the things on the horizon for me, and to do that at the right level of generality, one needs multigraphs (and probably ones with directions + decorations on the edges). But for stuff in the direct of Szemeredi's regularity lemma and the strong perfect graph theorem, multigraphs are pointless and cumbersome.

Even disregarding directions, the differences between multigraphs and simple graphs are maybe larger than one might imagine for the purposes of formalization. Multigraphs need a 'first-class' edge Type, to allow for the notion that an edge in a contracted graph is the same as the one as the one in the original graph, even when its ends are different. Thinking in a more CS way, a multigraph is basically a V x E zero-one matrix.

On the other hand, simple graphs are often best described with just a vertex type V, together with an adjacency Prop on its pairs, or equivalently a symmetric V x V zero-one matrix.

One thing to think about is where/how the complement of a graph should be defined. The complement of a multigraph is basically meaningless, but induced subgraph people take complements of simple graphs all the time.

This is not to mention hypergraphs, loops, half-edges, edge and vertex labels, etc etc. Possibly a good 'data structure' underlying all graphs is a V x E matrix with entries in a type with zero. Such a matrix can be used to encode all these things (simple graphs with support-two columns in Fin 2, directed graphs with support-two columns in {0,1,-1}, vertex labels with support-one columns, k-uniform hypergraphs with support-k columns, etc etc). Then typeclasses and interfaces can allow people to do 'normal' graph theory of whatever flavour they want.

[Peter Nelson]

While I'm on the topic...

One of the things that is obviously difficult type-theory-wise is treating subgraphs (or minors) as graphs. Analogous problems happen with the matroids I've been thinking about, and I've had quite some success by leaning much more into set theory, and having a Type of 'potential elements' and a Set of 'actual elements', together with an axiom that states that the structure outside this set is trivial. The analogue for graphs would be something like the following; here I define graphs and give an example subgraph-like definition and a lemma.

structure Graph (α β : Type _) :=
  (V : Set α)
  (E : Set β)
  (inc : α → β → Prop)
  (support_two : ∀ e u v w, inc e u → inc e v → inc e w → u = v ∨ u = w ∨ v = w)
    -- each edge is incident with at most two vertices
  (support_subset : ∀ v e, inc v e → v ∈ V ∧ e ∈ E)
    -- incidences only occur within the vertex and edge sets

-- Delete a set of vertices of a graph
def Graph.Delete (G : Graph α β) (D : Set α) : Graph α β where
  V := G.V \ D
  E := {e ∈ G.E | ∀ v, G.inc v e → v ∉ D}
  inc := (fun v e ↦ G.inc v e ∧ (∀ w, G.inc w e → w ∉ D) )
  support_two := sorry --easy
  support_subset := sorry --easy

theorem delete_delete (G : Graph α β) (D₁ D₂ : Set α) :
    (G.Delete D₁).Delete D₂ = G.Delete (D₁ ∪ D₂) := sorry
-- easy,  typechecks

The advantage is that theorems like delete_delete actually typecheck, without any hidden coercions or special subgraph type.

The disadvantage is that one has to explicitly keep track of the vertex and edge sets, getting proof obligations of the form v ∈ G.V all the time. But I've had some success handling things like this with aesop and autoparams.

See https://github.com/apnelson1/Matroid for an example of this in action. (You don't have to understand the details; the salient point is that a matroid is, mathematically, a structure on a set, but I've defined it as a structure on a type such that there is a particular Set where the structure 'happens', and then proofs deal with that set explicitly where needed).

[Peter Nelson]

Forgot to mention - thanks to @Johan Commelin for suggesting this approach for matroids; it's working quite well. (I have deviated from his original suggestion slightly by discharching the trivial goals using aesop/autoparams rather than the fact system).

[Chris Hughes]

Siddhartha Gadgil said:

I will be giving a couple of lectures on something related, but am planning to start working on formalizing topological/geometric methods in Group theory. Is there any update on this. In particular, I did not see any formalization of

• Cayley Graph
• Graph's as normally used in Serre-Bass theory
• CW complexes
• Amalgamated free products and HNN extensions

Am I correct that none of this is in Mathlib? Anand Rao Tadipatri Antoine Labelle Kyle Miller Rémi Bottinelli

I plan to take as a target the Scott-Wall article "Topological methods in Group Theory". Of course collaboration is very welcome.

I have a branch open for amalgamated products !4#6803

[Chris Hughes]

Also HNN extensions and Britton's lemma !4#6923