Zulip Chat Archive

Stream: new members

Topic: Introducing myself + algebraic topology

Brian Thomas (Sep 19 2020 at 13:17):

Hello! Just introducing myself: I got a PhD in math last year (in algebraic topology) but now work in the software industry. I've been interested in theorem proving on and off for a while but never really dove into it. After reading a bit about Lean, and in particular the Xena Project and its goals around formalizing an undergrad math curriculum, I thought I'd give it a shot and contribute whenever I can.

I've played through the natural numbers game, and I'm not sure where to go next. Probably more tutorials. For what it's worth, I worked a lot on (un)stable homotopy theory & (co)homology operations, so I like homological algebra, spectral sequences, category theory, stuff like that. So I'd like to do something with algebraic topology eventually. Are classical theorems in algebraic topology feasible yet? If not, what needs to be done first? Does the Lean library (is that mathlib?) have a notion of (co)homology, (co)homotopy, etc?

Johan Commelin (Sep 19 2020 at 13:22):

Hi, and welcome!

Kevin Buzzard (Sep 19 2020 at 13:22):

The situation, as I understand, it this. I had a student who formalised group cohomology in Lean, so the system is certainly up to the job, but they have left mathematics now and so this work is unlikely to end up in Lean's maths library. However the library does have abelian categories and complexes, so all the machinery is there. No spectral sequences in Lean 3 yet. I will have an MSc student next year @Amelia Livingston who might do something related to the Auslander-Buchsbaum theorem (we're still not completely decided) so we will have to develop Ext and Tor in some generality. We have sheaves on topological spaces. I believe that @Johan Commelin and @Reid Barton have thought about simplicial homology but I'm unclear about its status with regards to mathlib. In short, we don't have pretty much any of the stuff you are mentioning, however within the last year we have managed to build the machinery which one would need to make it, so there is plenty to do; it would of course be helpful if we could arrange things so that nobody is treading on each other's toes. There is a chance that @Markus Himmel will also be working in this area in Lean for his Masters project in Cambridge this coming academic year.

Johan Commelin (Sep 19 2020 at 13:22):

branch#sset contains a definition of simplicial sets, simplicial homology, geometric realization of simplicial sets.

Johan Commelin (Sep 19 2020 at 13:23):

I want to PR that stuff somewhere in October.

Reid Barton (Sep 19 2020 at 13:31):

For simplicial homology the litmus test would be to prove homotopy invariance and excision.

Reid Barton (Sep 19 2020 at 13:32):

I have a repository https://github.com/rwbarton/lean-homotopy-theory which defines homotopy groups via a large detour involving cofibration categories, and whose crowning achievement is to prove that weak equivalences in Top satisfy two-out-of-three. I'm not sure I would recommend the approach for mathlib.

Reid Barton (Sep 19 2020 at 13:41):

Oh yes, one project I would like to recommend is the Dold-Kan correspondence, at least for modules but maybe even for an abelian category--we don't have this yet right?

Johan Commelin (Sep 19 2020 at 13:41):

Good suggestion! Indeed, I don't think we have this.

Reid Barton (Sep 19 2020 at 13:42):

I think this would be an easier way to stress test simplicial objects

Reid Barton (Sep 19 2020 at 13:51):

Johan has proposed indexing simplicial sets on the category of all finite nonempty linearly ordered sets and not just a skeleton. This has its advantages but I'm slightly concerned about the fact that nobody ever seems to do this. So it would be good to see how this plays out in a real theorem.

Johan Commelin (Sep 19 2020 at 13:54):

With "nobody", you mean other formal libraries?

Reid Barton (Sep 19 2020 at 13:56):

No I mean in informal math

Kevin Buzzard (Sep 19 2020 at 13:57):

Are there any other formal libraries doing homotopy theory? Is there a univalent one somewhere doing fundamental groups synthetically? Presumably this would be of limited use to us...

Reid Barton (Sep 19 2020 at 14:02):

HOL Light has a formalization of singular homology and applications like invariance of domain

Reid Barton (Sep 19 2020 at 14:03):

And right, HoTT systems can use a completely different synthetic approach

Johan Commelin (Sep 19 2020 at 14:03):

@Kevin Buzzard homotopy groups are one of the first things that HoTT libraries define. And like you guessed... we can't really mimic them.

Reid Barton (Sep 19 2020 at 14:06):

Well, I should say you could use some parts of the same approach once you define homotopy classes of maps and define $K(\pi, n)$

Reid Barton (Sep 19 2020 at 14:20):

Some more test theorems for simplicial sets are https://kerodon.net/tag/0077 and https://kerodon.net/tag/014D; I think these are roughly within reach but maybe Dold-Kan would be more appealing.

Brian Thomas (Sep 19 2020 at 14:31):

Wow, thanks for all comments. Some interesting things to think about here. I was thinking that the simplicial approach might be the formal way to go because of the combinatorial & categorical nature of it. These seem to be a better approach than geometric ones, but this is just my naive take, being new to this. Maybe they all require the same machinery at the "bottom".

Kevin Buzzard (Sep 19 2020 at 14:32):

If you're an experienced mathematician with a PhD, you might somehow feel like nobody could tell you anything new about the definition of basic stuff such as stable homotopy theory -- but you would be very surprised what shows up when you start digging.

Brian Thomas (Sep 19 2020 at 14:32):

@Reid Barton I will take a look at this homotopy theory repo. Very interesting that there is a theorem about weak equivs. Why do you say this might not be a good approach for mathlib?

Also, Dold-Kan would be cool!

Kevin Buzzard (Sep 19 2020 at 14:33):

I've been doing algebraic geometry for 30 years but was still blown away by some things I discovered when I tried to do the "simple" job of formalising the definition of a scheme.

Brian Thomas (Sep 19 2020 at 14:33):

@Kevin Buzzard Yes, that's something I'm actually really excited about.

Brian Thomas (Sep 19 2020 at 14:34):

Even just defining the fundamental group -- I'm sure that will be more involved than I'm imagining right now.

Kevin Buzzard (Sep 19 2020 at 14:34):

I got an undergraduate to do that in 2018 and yes, there were a couple of surprises.

Kevin Buzzard (Sep 19 2020 at 14:35):

At some point he embarked on a proof from first principles that if f : [0,1]-> X has f(1)=a, and g:[0,1] -> X has g(0)=a, then there's some new continuous function h which is scaled f on [0,1/2] and scaled g on [1/2,1], and it took him forever to prove continuity at 1/2 :-)

Kevin Buzzard (Sep 19 2020 at 14:36):

He should have been using general results from the topology library which he didn't know were there. Also writing the proof of associativity was interesting.

Reid Barton (Sep 19 2020 at 14:37):

I found that, while in principle I could prove all the basic facts about homotopies in the setting of cofibration categories (like if $f \sim g$ then $f \circ h \sim g \circ h$ , etc.), in practice it was pretty difficult to do so, and certainly a lot more difficult than if the definition of homotopy was "there exists $H : X \times [0, 1] \to Y$ such that ...". In particular, I think I got stuck proving that homotopic maps induce the same map on $\pi_i$ (though I also set aside the project for other reasons).

Kevin Buzzard (Sep 19 2020 at 14:38):

I think there is some general principle by which you have some "pseudo-associative" operation on functions [0,1] -> X, which really is not associative because f*(g*h) has f on [0,1/2] whereas (f*g)*h has f on [0,1/4]. However you get associativity on the nose when you pass to the appropriate quotient. Trying to figure out the correct generality to set things up is interesting.

Reid Barton (Sep 19 2020 at 14:38):

The one advantage of the cofibration category approach is that it avoids the exact point Kevin mentions, and it also avoids having to write down a formula for the associativity of path composition up to homotopy. (I guess that's two advantages.)

Brian Thomas (Sep 19 2020 at 14:39):

The associativity of path composition up to homotopy is exactly what came to mind when Kevin mentioned the point above, seems like a potential headache.

Brian Thomas (Sep 19 2020 at 14:39):

(Even doing that by hand can be annoying...)

Kevin Buzzard (Sep 19 2020 at 14:39):

@Brian Thomas if you are interested in learning this stuff, then I would choose something to work on and just start. You'll get stuck 10 times at the beginning, but people here will be able to unstick you. There are other mathematicians here who know the material you're talking about and also know Lean so they're in an excellent place to advise.

Reid Barton (Sep 19 2020 at 14:40):

So what I did is define a homotopy as a map out of any cylinder object, and then showed that gluing cylinder objects together is associative up to isomorphism

Reid Barton (Sep 19 2020 at 14:42):

ultimately the setup comes down to one calculation you have to do at some point anyways, that $[0, 1] \times \{0, 1\} \cup \{0\} \times [0, 1] \to [0, 1]^2$ is isomorphic as a map to $\{0\} \times [0,1] \to [0,1]^2$

Brian Thomas (Sep 19 2020 at 14:42):

I think I will download Lean and configure it today, and then try to pick a basic theorem or something to eventually work toward.

Brian Thomas (Sep 19 2020 at 14:43):

So are people often working with their own repos for projects, like this homotopy theory one? And then mathlib is the official one?

Johan Commelin (Sep 19 2020 at 14:44):

See https://leanprover-community.github.io/undergrad_todo.html for a list of stuff that we are interested in :grinning:

Brian Thomas (Sep 19 2020 at 14:44):

@Reid Barton That's cool, I'm curious to see what that looks like in Lean... once I'm at that level

Johan Commelin (Sep 19 2020 at 14:44):

Most people work in a fork of mathlib.

Brian Thomas (Sep 19 2020 at 14:44):

Oh that looks interesting

Kevin Buzzard (Sep 19 2020 at 14:44):

My advice is to try some "baby" projects in a test repo of your own, but if you want to do something serious then build it in a branch of mathlib.

Johan Commelin (Sep 19 2020 at 14:44):

But there are some projects that depend on mathlib, yes.

Johan Commelin (Sep 19 2020 at 14:45):

mathlib is not more official than the homotopy library.... it's just bigger and more central(?)

Brian Thomas (Sep 19 2020 at 14:45):

Alright, that sounds good.

Brian Thomas (Sep 19 2020 at 14:45):

Oh, I see. I was interpreting it as the "core".

Kevin Buzzard (Sep 19 2020 at 14:46):

It's where most of the mathematics is.

Johan Commelin (Sep 19 2020 at 14:46):

Right. Almost everything depends on mathlib

Brian Thomas (Sep 19 2020 at 14:46):

So all of the basic stuff, like say in the natural numbers game, is that just built in to Lean? Or did that import mathlib?

Brian Thomas (Sep 19 2020 at 14:46):

I see

Kevin Buzzard (Sep 19 2020 at 14:46):

But I have students who make random mathematical repos which depend on mathlib but are not part of mathlib

Kevin Buzzard (Sep 19 2020 at 14:46):

Yes, the natural number game imports mathlib.

Brian Thomas (Sep 19 2020 at 14:47):

Okay, that makes sense

Brian Thomas (Sep 19 2020 at 14:47):

Thanks all for info & suggestions

Kevin Buzzard (Sep 19 2020 at 14:47):

Here for example is a random MSc project which a student of mine just wrote -- they had a repo of their own and had mathlib as a dependency. They are now going to start on the very long job of moving parts of it over to mathlib though.

Reid Barton (Sep 19 2020 at 14:48):

There's plenty of other low-hanging fruit out there. For growing mathlib the trick is to find bits that won't need to be recast later in some broader framework, but for learning projects, it doesn't really matter.

Reid Barton (Sep 19 2020 at 14:49):

Another project which would be useful and largely independent of the rest of homotopy theory would be covering space theory

Kevin Buzzard (Sep 19 2020 at 14:49):

But just because it's maths doesn't mean it has to go into mathlib. With some undergraduates we developed group theory from scratch, just to see what it would teach us -- https://github.com/ImperialCollegeLondon/group-theory-game (it has its own definition of a group but uses other things from mathlib like the concept of finiteness). We don't intend on putting this stuff into mathlib though -- it already has groups (although we'll have Sylow's theorems soon :P; Lean only has Sylow 1)

Kevin Buzzard (Sep 19 2020 at 14:49):

That repo will probably turn into teaching material of some kind, e.g. a book or a game.

Brian Thomas (Sep 19 2020 at 14:55):

That's helpful. Yeah, I think I will fork mathlib and just play around in a sandbox for a bit. Maybe prove some very basic things before getting too excited and ahead of myself :)

Patrick Massot (Sep 19 2020 at 14:55):

Make sure to use https://leanprover-community.github.io/ as your entry point when looking for any kind of documentation (on installation for instance).

Kevin Buzzard (Sep 19 2020 at 14:56):

Oh that is a hugely important thing to say @Brian Thomas -- much as we'd love that website to be the number one hit if you start googling for Lean theorem prover, the old MS pages always beat it.

Brian Thomas (Sep 19 2020 at 14:59):

Ah, I didn't see the difference. Thanks for pointing that out

Kevin Buzzard (Sep 19 2020 at 15:00):

Microsoft don't formally have anything to do with mathlib, and mathlib is the thing which you as a mathematician will want to be using.

Kevin Buzzard (Sep 19 2020 at 15:01):

A lot of the chat here is about development of mathematics in Lean -- this is what separates it from the other provers.

Saul Glasman (Oct 18 2020 at 14:25):

@Brian Thomas , sorry to resurrect an oldish thread, but did you end up doing anything along these lines? I'd like to start doing some simplicial homotopy theory in Lean, and one milestone I have in mind is setting up the basic theory of model categories and the standard model structure on simplicial sets. I was also thinking about Dold-Kan.

Kevin Buzzard (Oct 18 2020 at 22:47):

You might want to mention this in #maths because people might have independently had a stab at some of this

Saul Glasman (Oct 20 2020 at 22:53):

Will do

Brian Thomas (Oct 21 2020 at 14:57):

@Saul Glasman Sorry for the late reply. The answer is that I haven't done much work on this since my last reply, unfortunately, because of other things that popped up. I am still quite interested in this but won't be able to dive deeper until next month. When I do that, I can send you a message and see where you're at -- maybe we can work on some stuff together.

Last updated: Dec 20 2023 at 11:08 UTC