Seifert-VanKampen theorem

Stream: Is there code for X?

[Miguel Marco]

AFAIK we don't have Seifert-VanKampen theorem in Mathlib. I considered trying to formalize it (I did a first attempt, and then realized it would be considerably harder than I expected initially). Looking for resources, i found that Henning Basold, @Peter Bruin @Dominique Lawson did formalize a version of it for directed topological spaces.

I took a quick look and got the impression that the usual version would be a particular case of the directed version, so I wonder what is the reason why it wasn't included in Mathlib.

[Miguel Marco]

link to the repo and preprint

[Yaël Dillies]

I had no idea about this!

[Miguel Marco]

I just found it yesterday.

[Junyan Xu]

Apparently they only allow a cover by two open sets, which is probably easier and not as general as allowing an arbitrary open cover. I have an outline for the general case, which hopefully addresses most technical difficulties.
cc @Rob Lewis

[Miguel Marco]

The case with two open sets is the version that usually appears in the books (and also the one I was missing, so the one I tried to formalize).

I think that, even if we had a more general case covered, it would make sense to have the usual version with two sets (even if the proof is just apply general_case, since it would be what man people would expect to find in Mathlib.

[Antoine Chambert-Loir]

The groupoid version as given in May (or Brown, or Bourbaki) is the one to prove, but it needs to be complemented by an algebraic computation of the fundamental group from the presentation of the groupoid. May and Brown are insufficient there, Bourbaki gives a very general theorem but the proof is circonvoluted.

[Mauricio Collares]

Miguel Marco said:

link to the repo and preprint

Lean 4 version at https://github.com/Dominique-Lawson/Directed-Topology-Lean-4

[Peter Bruin]

Miguel Marco said:

AFAIK we don't have Seifert-VanKampen theorem in Mathlib. I considered trying to formalize it (I did a first attempt, and then realized it would be considerably harder than I expected initially). Looking for resources, i found that Henning Basold, Peter Bruin Dominique Lawson did formalize a version of it for directed topological spaces.

I took a quick look and got the impression that the usual version would be a particular case of the directed version, so I wonder what is the reason why it wasn't included in Mathlib.

Indeed, the directed version implies the groupoid version: a directed space is a topological space X together with a suitable collection D of paths, and to such a space one attaches a fundamental category. Taking D to consist of all paths in X gives the usual fundamental groupoid, and the directed Van Kampen theorem reduces to the usual one.

[Peter Bruin]

By the way, the formalisation is entirely due to @Dominique Lawson as part of his bachelor's project. The initial question, which came from Henning Basold, was about formalising constructions/theorems from directed topology. Once it was decided to use Lean for this and it turned out that even the undirected version had not been formalised yet, it quickly became clear that it would make most sense to prove the undirected version as a corollary of the directed one.

[Ben Eltschig]

Junyan Xu said:

Apparently they only allow a cover by two open sets, which is probably easier and not as general as allowing an arbitrary open cover. I have an outline for the general case, which hopefully addresses most technical difficulties.
cc Rob Lewis

I actually saw that one a few days ago and was also until just now thinking of formalising it - i.e., I've been doing a bit of reading and messing around in lean, but haven't gotten close to the core of the argument yet. Seeing this though, I suppose there's not much of a point in doing it if there's a more general version to be formalised, right?

[Peter Bruin]

Antoine Chambert-Loir said:

The groupoid version as given in May (or Brown, or Bourbaki) is the one to prove, but it needs to be complemented by an algebraic computation of the fundamental group from the presentation of the groupoid. May and Brown are insufficient there, Bourbaki gives a very general theorem but the proof is circonvoluted.

We did not formalise that part, but did notice that this is harder than one might expect. If I remember well, one difficulty is that one cannot naively work with categories up to equivalence here. Also, the directed version of the classical statement about fundamental groups (which would express the "fundamental monoid" at a point as a pushout) turns out to be false.

[Miguel Marco]

Just to be sure: the undirected version about fundamental grupoid implies the one for fundamental group, right?