Zulip Chat Archive

Stream: maths

Topic: Generalized Smale conjecture


view this post on Zulip Patrick Massot (Sep 20 2019 at 08:25):

I'm not sure this stream can be used for general math news, but we have a new high point of mathematics we can dream to formalize in Lean 42.0 after we'll have a couple of thousands pages or preliminaries covered: https://arxiv.org/abs/1909.08710

view this post on Zulip Sebastien Gouezel (Sep 20 2019 at 08:46):

We'd better start with something easy like Perelman's geometrization theorem.

view this post on Zulip Patrick Massot (Sep 20 2019 at 08:46):

Yes, this is part of the preliminaries

view this post on Zulip Sebastien Gouezel (Sep 20 2019 at 08:47):

I think your "a couple of thousands pages of preliminaries" is underestimated by a factor of 10 (at least :).

view this post on Zulip Kevin Buzzard (Sep 20 2019 at 10:25):

The computer scientists will like the deduction of Theorem 1.3 from Theorem 1.2 in the intro.

view this post on Zulip Scott Morrison (Sep 20 2019 at 10:27):

by well_known

view this post on Zulip Kevin Buzzard (Sep 20 2019 at 10:28):

Later on in the paper they assume all manifolds are 3-dimensional. This is well-known to be false, so it's not surprising that they can prove so much.

view this post on Zulip Patrick Massot (Sep 20 2019 at 11:16):

We already have well_known, it's called library_search

view this post on Zulip Scott Morrison (Sep 20 2019 at 11:23):

(I'm wishing that I called library_search instead help. I've got a soon-to-be-PR that adds a "try harder please" mode as library_search!, but help! would have been so much more fun.)

view this post on Zulip Sebastien Gouezel (Sep 20 2019 at 13:12):

In the paper, Theorem 1.2 says that some set is either empty or contractible. I don't want to start a flame war, but isn't the empty set contractible? (Of course, this depends on the precise definition of contractible you use, but I guess there is maybe a definition of contractible in @Reid Barton Lean homotopy library, and then the question makes sense).

view this post on Zulip Reid Barton (Sep 20 2019 at 13:19):

no!

view this post on Zulip Reid Barton (Sep 20 2019 at 13:20):

At least in homotopy theory, I've only seen it used to mean "has the homotopy type of a point"

view this post on Zulip Reid Barton (Sep 20 2019 at 13:21):

it's our "unique"

view this post on Zulip Reid Barton (Sep 20 2019 at 13:21):

Well, unique + exists if you don't consider that to be part of "unique"

view this post on Zulip Sebastien Gouezel (Sep 20 2019 at 13:22):

Yes, I agree it's hard to argue for the contractibility of the empty space. Connectedness is a better question :)

view this post on Zulip Reid Barton (Sep 20 2019 at 13:26):

Here is another one I like. If f:XYf : X \to Y and XX is empty, is ff constant?

view this post on Zulip Patrick Massot (Sep 20 2019 at 13:27):

I'd say yes unless Y is empty

view this post on Zulip Patrick Massot (Sep 20 2019 at 13:27):

:grinning:

view this post on Zulip Kevin Buzzard (Sep 20 2019 at 13:27):

My brain hurts

view this post on Zulip Patrick Massot (Sep 20 2019 at 13:27):

:smiling_devil:

view this post on Zulip Kevin Buzzard (Sep 20 2019 at 13:45):

I'd never seen that one before. There are two natural definitions of constant and Patrick's answer is what you get with one of them

view this post on Zulip Keeley Hoek (Sep 20 2019 at 14:41):

3) Image is a singleton :D, different answer again!

view this post on Zulip Antoine Chambert-Loir (Sep 29 2019 at 22:40):

Bourbaki's definition (E, II, p. 15) of a constant function is : for all x,x'∈X, f(x)=f(x').
With this definition, if X is empty, any function f:X →Y is constant. However, a constant function f:X →Y has a value iff X is nonempty.

view this post on Zulip Kevin Buzzard (Sep 29 2019 at 22:52):

On the other hand if you asked a mathematician for a definition, surely some would say "there exists c in Y such that for all x in X, f(x)=c". And of course if you showed those people bourbaki, many would say that the definitions were obviously the same ;-)


Last updated: May 10 2021 at 07:15 UTC