# Zulip Chat Archive

## Stream: maths

### Topic: Generalized Smale conjecture

#### 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

#### Sebastien Gouezel (Sep 20 2019 at 08:46):

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

#### Patrick Massot (Sep 20 2019 at 08:46):

Yes, this is part of the preliminaries

#### 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 :).

#### 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.

#### Scott Morrison (Sep 20 2019 at 10:27):

`by well_known`

#### 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.

#### Patrick Massot (Sep 20 2019 at 11:16):

We already have `well_known`

, it's called `library_search`

#### 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.)

#### 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).

#### Reid Barton (Sep 20 2019 at 13:19):

no!

#### 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"

#### Reid Barton (Sep 20 2019 at 13:21):

it's our "unique"

#### Reid Barton (Sep 20 2019 at 13:21):

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

#### 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 :)

#### Reid Barton (Sep 20 2019 at 13:26):

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

#### Patrick Massot (Sep 20 2019 at 13:27):

I'd say yes unless Y is empty

#### Patrick Massot (Sep 20 2019 at 13:27):

:grinning:

#### Kevin Buzzard (Sep 20 2019 at 13:27):

My brain hurts

#### Patrick Massot (Sep 20 2019 at 13:27):

:smiling_devil:

#### 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

#### Keeley Hoek (Sep 20 2019 at 14:41):

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

#### 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.

#### 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