Generalized Smale conjecture

Stream: maths

[Patrick Massot]

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]

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

[Patrick Massot]

Yes, this is part of the preliminaries

[Sebastien Gouezel]

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

[Kevin Buzzard]

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

[Scott Morrison]

by well_known

[Kevin Buzzard]

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]

We already have well_known, it's called library_search

[Scott Morrison]

(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]

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]

no!

[Reid Barton]

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

[Reid Barton]

it's our "unique"

[Reid Barton]

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

[Sebastien Gouezel]

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

[Reid Barton]

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

[Patrick Massot]

I'd say yes unless Y is empty

[Patrick Massot]

:grinning:

[Kevin Buzzard]

My brain hurts

[Patrick Massot]

:smiling_devil:

[Kevin Buzzard]

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]

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

[Antoine Chambert-Loir]

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]

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 ;-)