Seifert--van Kampen theorem

Stream: maths

[Kevin Buzzard]

I asked in a tweet about a formalised Seifert--van Kampen theorem. Here is something I am confused about. Hou and Shulman have "formalised the Seifert--van Kampen theorem". I want to have the Seifert--van Kampen theorem in Lean. Can I get it?

Which non-univalent theorem provers contain a proof of the Seifert--van Kampen theorem https://en.wikipedia.org/wiki/Seifert%E2%80%93van_Kampen_theorem ? #Coq #Isabelle #leanprover ? Note that Hou and Shulman gave a *synthetic* proof in a univalent theory; I am looking for a non-synthetic proof. I am not an expert.

- The Xena Project (@XenaProject)

[Reid Barton]

I thought a bit about how to do this--that's why I formalized the Lebesgue number theorem.

[Reid Barton]

I think the S-vK theorem is within reach for sure.

[Reid Barton]

(I assume you mean the theorem for topological spaces, though there are other versions which are also not synthetic, like for simplicial sets)

[Reid Barton]

It was the next big thing I wanted to add to lean-homotopy-theory before I decided to do model categories instead.

[Reid Barton]

Also, I realized that if you formalize the groupoid version, there is still a fair bit of other work needed to conclude that $\pi_1(S^1) = \mathbb{Z}$ from it.

[Sebastien Gouezel]

We don't even have the fundamental group, or the fundamental groupoid. If I recall correctly, there was a PR by @Kenny Lau doing it, but it was decided that it should instead be an instance of a more general object, and that we should first get the more general object in mathlib. I don't know anything about the general versions, but maybe we should try to get @Reid Barton 's homotopy theory library into mathlib.

[Patrick Massot]

I'd love to have Reid's stuff into mathlib. But, whatever the road, I wouldn't say we have the fundamental group if we don't derive the concrete statement about continuous maps frrom $\mathbb S^1$ to itself

[Reid Barton]

Now that we have $\exp$, especially, it would be nice to do covering space theory and compute $\pi_1(S^1)$ that way.

[Reid Barton]

However, the main obstruction I see is that no algebraic topologist actually uses the category of all topological spaces

[Reid Barton]

there are a number of different substitutes with slightly different technical properties

[Patrick Massot]

That's why I say: let's do a fancy version, but make sure we can derive the concrete stuff

[Reid Barton]

Now the next level problem: there are a number of different technical frameworks in which to organize things that are like categories of topological spaces...

[Sebastien Gouezel]

In my opinion, the fundamental groupoid is so fundamental that it should be defined in the most general situation, i.e., general topological spaces. If machinery to compute it only applies in more limited situations, I don't mind at all (but I definitely want to be able at some point to say interesting things on the $\pi_1$ of hawaiian earrings, or the complement of the horned sphere)

[Sebastien Gouezel]

And the universal cover should be defined for semi-locally simply connected spaces, of course!

[Patrick Massot]

You mean délaçables spaces, right?

[Kevin Buzzard]

OK I'm back thinking about van Kampen (a student has suggested trying it in Lean over the summer). Now we _do_ have fundamental groups and groupoids. The student (Chiyu Zhou) says that the proof in Hatcher looks terrifying to formalise but he's seen another proof which uses universal properties in some notes he's found on the internet (Peter May's "concise course in algebraic topology") which he thinks might be simpler. I don't know anything about this stuff -- does this sound feasible yet? Probably, because apparently Reid thought it was feasible in 2020 judging by the above comments.

[Adam Topaz]

Does mathlib know anything about the fundamental group? E.g. do we have a good theory of covers?

[Kyle Miller]

To add another reference, Ronald Brown's "Topology and Groupoids" explains how to construct the fundamental groupoid of a union of spaces as the pushout of the groupoids of each space. I don't know how feasible the proof is.

[Adam Topaz]

I would suspect that one could come up with a conceptual and simpler proof of Van-Kampen using the theory of covers.

[Adam Topaz]

For example, here is an argument in the etale case that one could mimic: https://mathoverflow.net/a/110638

[Kevin Buzzard]

I have this worry that we're going to run into this issue which IIRC @Reid Barton mentioned in his LT2020 talk -- the problem of some random path oscillating between the two open sets in an irritating way.

[Antoine Chambert-Loir]

One could try to formalize the proof of Bourbaki, Topologie algébrique.

The general theorem computes the fundamental groupoid of $X$ given a surjective map $f \colon Y\to X$ as the coequalizer of the morphism of groupoids $\varpi(Y\times_X Y)\Rightarrow\varpi(Y)$,
and then computes the fundamental group of a coequalizer.
For example, this theorem computes the fundamental group of the circle when it is written as a quotient of an interval $[0;1]$ by glueing the endpoints. There are no connectedness assumptions.

The first part is topological (descent of covers), and the other is a terrible groupoid computation.

The topological part is quite easy for an open covering. This is what Brown does, and May does it too, but in a very terse way.
But it works more generally if the map $f$ has local sections, but it also holds in some cases for locally finite coverings by closed subsets, or for a quotient of a space by a proper action of a discrete group.

The algebraic part is elementary (this is just algebra) but I find it really messy. Note that May or other references do not give the result of the computation even for two open connected subsets whose intersection has two connected components.

[Reid Barton]

Does this need some kind of local (simple?) connectedness hypothesis?

[Reid Barton]

May's proof is the one I would expect, using the Lebesgue number theorem

[Antoine Chambert-Loir]

The descent part may require locally (simply) connectedness properties, it depends on the situations, but not for the descent relative to an open covering.

However, there is a story that Bourbaki did not tell, that there are two groupoids under view: the Poincaré groupoid that corresponds to strict homotopy classes of paths, and the “Galois groupoid” $\gamma(X)$ that classifies the covers of $X$. There is a morphism from the Poincaré groupoid to the Galois groupoid which corresponds to lifting paths in a cover. If the space is nice (locally path connected, semi-locally simply connected, something that Bourbaki condenses as délaçable), then this morphism is an isomorphism.

When descent of covers holds for a map $f\colon Y \to X$, the Galois groupoid of $X$ is isomorphic to the coequalizer of a double arrow of Galois groupoids from $\gamma(Y\times_X Y)$ to $\gamma(Y)$.

If $f\colon Y\to X$ has local sections, for example if $Y$ is a disjoint union of open subsets of $X$, then the Poincaré groupoid of $X$ is isomorphic to the coequalizer of a double arrow of Poincaré groupoids from $\varpi(Y\times_X Y)$ to $\varpi(Y)$.