# Zulip Chat Archive

## Stream: maths

### Topic: Seifert--van Kampen theorem

#### Kevin Buzzard (May 15 2020 at 08:36):

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 (May 15 2020 at 08:45):

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

#### Reid Barton (May 15 2020 at 08:46):

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

#### Reid Barton (May 15 2020 at 08:47):

(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 (May 15 2020 at 08:54):

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

#### Reid Barton (May 15 2020 at 08:54):

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 (May 15 2020 at 09:13):

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 (May 15 2020 at 09:18):

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 (May 15 2020 at 09:19):

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 (May 15 2020 at 09:20):

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

#### Reid Barton (May 15 2020 at 09:20):

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

#### Patrick Massot (May 15 2020 at 09:22):

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

#### Reid Barton (May 15 2020 at 09:23):

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 (May 15 2020 at 10:29):

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 (May 15 2020 at 10:29):

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

#### Patrick Massot (May 15 2020 at 10:30):

You mean délaçables spaces, right?

Last updated: May 09 2021 at 10:11 UTC