PR #11851 Multigraphs, Paths, Homotopy

Stream: PR reviews

[Siddhartha Gadgil]

I request a review of the following PR. This is the first in a series leading up to covering space theory for multigraphs enough to prove Nielsen-Schreier. This is already biggish, so I can split off the homotopy part to a separate file if that is better.

Multigraphs for Topological methods in Group Theory (a la Serre)

This is a start of basic theory for topological methods in group theory bypassing topology by working with graphs defined following Serre and directly developing fundamental group and covering space theory for this. Here we

• Graphs (a la Serre)
• Paths; reduced paths, reduction of paths
• Homotopy of paths in graphs (generated by cancellation); homotopy classes.
• Multiplication and inversion of paths and relations to homotopy. Induced operations on homotopy classes.

The corresponding covering space theory will follow in succeeding PRs

[Sébastien Gouëzel]

Can you explain how it relates to the proof we already have of Nielsen-Schreier in docs#subgroupIsFreeOfIsFree, which has the same kind of "topology but avoiding the topological definitions" flavor (if I understand correctly)?

[Siddhartha Gadgil]

The proof already there looks more efficient :smile: - it also avoid topology but in a different way, observing that graphs are free groupoids. Actually @Anand Rao Tadipatri had used this fact at one stage.

However my goal is to go beyond Fenchel-Nielsen to stuff requiring two-complexes: at least Stalling's topological proof of Grushko's theorem and ideally small cancellation theory. It seems to me at least that having explicit notions of covering, paths, homotopies etc will be easier to extend rather than the encoding of graphs as categorical objects.

[David Wärn]

I think there's a lot of overlap between this PR and existing stuff in mathlib that should be sorted out. At a glance, the difference between this and existing stuff seems mostly to come down to choice of terminology and questions about (un)directedness. For example this basic notion of Multigraph is a souped-up version of docs#Quiver (which is not a categorical object any more than Multigraph is). The difference is just about (un)directedness. Every Quiver determines a Multigraph via docs#Quiver.Symmetrify. Every Multigraph is (non-canonically) obtained in this way (if you pick an orientation of each edge), and more canonically you can always construct from a given Multigraph an equivalent Quiver by subdividing each edge.

The stuff on paths and PathClass and homotopyClass seems to be duplicating docs#CategoryTheory.FreeGroupoid and docs#Quiver.Path

The notion of covering space works very nicely in groupoidal language: a covering space of a groupoid is a functor to types, and the total space is the category of elements docs#CategoryTheory.Functor.Elements. I used this approach in formalising docs#subgroupIsFreeOfIsFree, but it's probably not very well-explained or documented, and it would probably be good to develop more theory around this.

[Siddhartha Gadgil]

Suppose one wanted to define two-complexes (for instance associated to group presentations) in such a way that graphs are 1-complexes. I would do this by taking a graph together with a family of loops. Would this be natural with quivers?

I see that Quiver.hasInvolutiveReverse is almost multi-graphs - we just need the involution to be free (for loops, where it is not automatic).

If the main difference is terminology, we can simply add documentation and perhaps some abbreviations/definitions. As I said, my goal is to formalize stuff like "binding ties" proof of Grushko's theorem and am happy to abandon the current PRs if the approach in Mathlib has all that is needed.

[David Wärn]

Sure, I guess you could also say a 2-complex is a quiver together with a family of loops (the type of loops is given by the free groupoid on the quiver). You can think of a Quiver as an oriented / directed Multigraph

[Siddhartha Gadgil]

Let me digest this. When I get to work on more formalization I will probably build on quivers.