Zulip Chat Archive

Stream: maths

Topic: Seifert--van Kampen theorem


view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip Reid Barton (May 15 2020 at 08:46):

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

view this post on Zulip 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)

view this post on Zulip 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.

view this post on Zulip 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 π1(S1)=Z\pi_1(S^1) = \mathbb{Z} from it.

view this post on Zulip 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.

view this post on Zulip 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 S1\mathbb S^1 to itself

view this post on Zulip Reid Barton (May 15 2020 at 09:19):

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

view this post on Zulip 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

view this post on Zulip Reid Barton (May 15 2020 at 09:20):

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

view this post on Zulip 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

view this post on Zulip 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...

view this post on Zulip 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 π1\pi_1 of hawaiian earrings, or the complement of the horned sphere)

view this post on Zulip Sebastien Gouezel (May 15 2020 at 10:29):

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

view this post on Zulip Patrick Massot (May 15 2020 at 10:30):

You mean délaçables spaces, right?


Last updated: May 09 2021 at 10:11 UTC