PR #11604: Serre graphs, fundamental groups, covering spaces

Stream: mathlib4

[Siddhartha Gadgil]

I have made a (rather large) PR as first steps towards "topological methods in group theory" in Lean, bypassing Set topology. I am pasting details below. This is (most of) code @Anand Rao Tadipatri and I wrote a while back.

I realise that smaller PRs are preferred, but in this case I felt that this bigger PR has an advantage as there are many choices in how to formalise (even mathematical choices). So it is best to show that these choice "work" in the sense of letting us prove the theorems we want, and that alternatives can be discussed in the context of goals.

The summary of the PR is as follows:

Serre graphs for Topological methods in Group Theory

This is 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.

Some of the definitions and results in this PR:

• 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.
• Fundamental group of a graph.
• Covering maps of Graphs; path lifting, homotopy lifting.
• Universal cover; Cover corresponding to a subgroup.

The code in this PR is enough to give a topological proof of a non-trivial result: if two reduced paths are homotopic then they are equal.

Potential applications

@0art0 and I have proved the Nielsen-Schreier theorem: every subgroup of a free group is free but this PR is only part of the way for this.

Eventually this approach can be extended to 2-complexes following Lyndon-Schupp. The hope is to formalize Staling's topological proof of Grushko's theorem and also small cancellation theory.