Daniel Busch

Stream: new members

[Daniel Busch]

Hi, I'm an undergrad from Germany new to Lean and interested in doing some topology -- specifically, proving the classification of surfaces. I have seen the proof using handle decompositions and the one by Conway. I'd consider myself at least decent at programming and have done a good chunk of the exercises in the "tutorials" project, but I don't have a clue yet as to how things are usually implemented in a maintainable way and what is already available in mathlib. Could someone give me a few hints to get me started? Specifically, it'd be useful to know where to start defining triangulations and how to explicitly construct the homeomorphisms. I realize that this is probably a huge amount of work, but I have time and motivation, and even if I didn't finish, something useful might come out of it anyways.

[Yaël Dillies]

Triangulations started being defined on branch#triangles for Goursat's lemma. I assume that's related?

[Johan Commelin]

@Daniel Busch A good way of getting started is to try to write the statement of your end goal in Lean.

[Johan Commelin]

Can you give a statement here that is precise and explicit? (You can write LaTeX on Zulip between double dollars: $$a^2 + b^2 = c^2$$)

[Daniel Busch]

@Yaël Dillies I don't think so, I would prefer working with real manifolds I think, and other people might be interested in higher dimensional triangulations anyway, so I would maybe opt for defining triangulations as generally as possible, if that seems reasonable.

[Yaël Dillies]

Are those triangulations simplicial complexes by any chance? If so, #9762 and branch#sperner-again are related.

[Johan Commelin]

@Daniel Busch For example, what exactly do you want to consider when you say "surface". Compact, or also certain non-compact cases? Etc...

[Daniel Busch]

@Johan Commelin Sure, I have made a sort of roadmap to the handle proof already, because that's the one i was taught in topology class. Anyway, our classification of surfaces reads: Let $X$ be a triangulable, compact real (probably smooth for my purposes, since these are already defined in mathlib) manifold without boundary, then X is homeomorphic to one of these:

• $S^2$
• $T^2 \# ... \# T^2$, a connected sum of a finite number of tori
• $\mathbb{RP}^2 \# ... \# \mathbb{RP}^2$, a connected sum of a finite number of real projective spaces.

[Johan Commelin]

I guess $X$ should also be connected?

[Daniel Busch]

@Yaël Dillies Yes, simplicial complexes seem about right, but I'm only guessing now because I'm not willing to look through a hundred commits yet :)

[Johan Commelin]

Note that mathlib has C^p manifolds for all p. But I don't know how general the statement works. It's even true for topological manifolds, right?

[Daniel Busch]

@Johan Commelin Yes, right.

[Yaël Dillies]

Sorry, this branch is huuuge :sweat_smile:

[Daniel Busch]

@Johan Commelin Yes, but that in turn relies on the fact that any 1, 2, or 3-dimensional topological manifold (maybe with some mild assumptions) can be triangulated and is thus smooth (i think).

[Daniel Busch]

@Yaël Dillies can you point me to your latest definition of a simplicial complex in it?

[Yaël Dillies]

It's here: https://github.com/leanprover-community/mathlib/pull/9762/files

[Daniel Busch]

@Yaël Dillies Oh i found it i think, never mind.

[Daniel Busch]

@Yaël Dillies Ah, thanks. :)

[Johan Commelin]

Daniel Busch said:

Johan Commelin Yes, but that in turn relies on the fact that any 1, 2, or 3-dimensional topological manifold (maybe with some mild assumptions) can be triangulated and is thus smooth (i think).

That might be. I'm not an expert on (topological) manifolds. Anyway, I think that aiming for smooth manifolds is a lofty first goal already.

[Daniel Busch]

Yes, if smooth manifolds are not defined yet then that's a significant amount of work too.

[Johan Commelin]

So, to write down the statement, a lot of stuff is already available in mathlib. What is missing is:

• triangulable
• torus
• projective plane
• connected sum

[Daniel Busch]

@Yaël Dillies Your simplicial complexes look pretty good, thanks for the hint!

[Johan Commelin]

Smooth manifolds are done. And mathlib knows that the sphere is a smooth manifold.

[Daniel Busch]

@Johan Commelin Okay, then I can probably use Yaëls definition of a simplicial complex for the triangulation and tick that off, the other three would need to be done by hand.

[Johan Commelin]

It probably makes sense to look at how the sphere is done, and then try to define tori and projective spaces?

[Johan Commelin]

Connected sum seems like the hardest ingredient to me.

[Daniel Busch]

Of these, the connected sum is probably going to be the most difficult by far since I would need to prove a lot of stuff for well-definedness that just gets handwaved in a regular lecture, for example that the resulting surface is independent of the two circles where you attach.

[Johan Commelin]

@Heather Macbeth might be the best to talk to. (She did spheres.)

[Heather Macbeth]

@Daniel Busch Do you want to work in the topological category or the smooth category?

[Daniel Busch]

@Johan Commelin Yeah, these two seem like a good point to start. In my opinion, these would be defined best by looking at some quotients of spaces, is that already in mathlib? Or better yet, how do i look it up?

[Reid Barton]

I think it might also be a good idea to start with 1-manifolds...

[Heather Macbeth]

Or even 0-manifolds!

[Daniel Busch]

@Heather Macbeth That's a question I'm trying to figure out too, seems smooth manifolds are already in mathlib but topological ones aren't.

[Heather Macbeth]

No, they both are.

[Daniel Busch]

Where can I find the topological ones?

[Heather Macbeth]

It's docs#charted_space / docs#has_groupoid for the docs#continuous_groupoid associated to docs#euclidean_space

[Heather Macbeth]

(the machinery is very general!!)

[Reid Barton]

Of course for topological manifolds you don't actually need any of that machinery (being a topological manifold is a property of a space) and maybe it would be useful to have a construction along these lines if there isn't one already... not sure

[Heather Macbeth]

@Adam Topaz and I were talking a while ago about how it would be nice to prove that a smooth manifold is triangulable. I believe there's a proof via Whitney's embedding theorem, which is in mathlib: docs#exists_embedding_euclidean_of_compact

[Daniel Busch]

Huh, the machinery seems to be general enough to throw me off there, thanks for the hint :)

[Daniel Busch]

@Reid Barton It might be convenient to define topological manifolds as a special case of the machinery there to make it easier to use and discover, right?

[Heather Macbeth]

But maybe it would be better for your purposes just to work throughout with simplicial complexes.

[Daniel Busch]

That would indeed make a few things easier -- on the other hand, the connected sum of two manifolds is probably something of a more general interest, should I aim to define it in the most general sense or something that's the most convenient to handle using simplicial complexes?

[Heather Macbeth]

I think we should have both constructions, eventually!

[Reid Barton]

What I was imagining was some sanity check theorem (hopefully easy) along the lines of: the category of topological n-manifolds is equivalent to the category of spaces that locally look like R^n

[Heather Macbeth]

Johan Commelin said:

So, to write down the statement, a lot of stuff is already available in mathlib. What is missing is:

• triangulable
• torus
• projective plane
• connected sum

Note that we have the torus already, as the product of two circles.

[Daniel Busch]

Do we already have the disjoint union of manifolds too if we have the product? That would be a good first step towards the connected sum.

[Heather Macbeth]

No, not yet. That could be a nice warm-up for you to get to know the library.

[Heather Macbeth]

Another task could be to define oriented manifolds. I'd have in mind to do this by defining the "oriented groupoid", like docs#times_cont_diff_groupoid with the extra condition that the Frechet derivative have everywhere positive determinant. @Sebastien Gouezel, does that seem like the right path to you?

[Daniel Busch]

I'll try to do that, from my current point of view, I'll probably need to define the disjoint union of groupoids and charted spaces and show that everything is an instance of every other relevant structure, right?

[Daniel Busch]

Or is the groupoid more of a local thing itself instead of the collection of all local homeos at all points?

[Heather Macbeth]

You don't need to define the disjoint union of groupoids, rather it would be something like

variables (H : Type*) [topological_space H]
variables {M₁ : Type*} [topological_space M₁] [charted_space H M₁]
variables {M₂ : Type*} [topological_space M₂] [charted_space H M₂]

instance : charted_space H (M₁ ⊕ M₂) := sorry

variables (G : structure_groupoid H)

variables [has_groupoid M₁ G] [has_groupoid M₂ G]

instance : has_groupoid (M₁ ⊕ M₂) G := sorry

[Sebastien Gouezel]

Yes, absolutely. Note that you can not define the connected sum before you define orientation (the result does depend on the choice of the orientation for gluing, cf. the example of $\mathbb{C}\mathbb{P}^2$).

[Patrick Massot]

The classification of surfaces is a very interesting formalization topic. I think it maximizes the amount of pain compared to the understanding you gain. I decided long ago that doing it would be both absolutely amazing and completely counter-productive when it comes to proving that formalized mathematics could be useful.

[Patrick Massot]

This is already true in ordinary mathematics when it comes to proving stuff vs drawing pictures.

[Patrick Massot]

I guess the "proof" by Conway mentioned by Daniel is the Zip proof explained in The shape of space. That's the wonderful example of a "proof" that gains nothing from being made rigorous. It's clear that making it rigorous would loose all its qualities and make it non-competitive against any other proof. This has nothing to do with Lean. You should simply try to state on paper what the different steps are claiming. That's a wonderful piece of math, but for a meaning of math that is completely different from what we are discussing here.

[Patrick Massot]

The classical Morse theory proof explained in Hirsch's differential topology book is much closer to being a proof, but it would still be a nightmare in Lean. And again I'm not even considering proving stuff. Stating what is meant and assembling all intermediate statements into a proof would already be very non trivial.

[Patrick Massot]

For people who don't know what we are talking about: Conway's "proof" can be found at https://www.maths.ed.ac.uk/~v1ranick/papers/francisweeks.pdf. That's a wonderful bedtime reading.