Zulip Chat Archive

Stream: maths

Topic: why are manifolds difficult?


view this post on Zulip Kevin Buzzard (Feb 07 2021 at 10:20):

This is not a general question about why setting up the full theory of manifolds in Lean is so difficult -- I know part of the reasons why, and I've read some of the module docstrings, but perhaps I've not read the right one.

This is a specific question about formalising specifically the definition of a smooth (C^infty) manifold. Let's skip corners and C^n functions for now. My memory, which is possibly incorrect, is that Patrick once told me that there is some issue with atlases and that we sometimes cheat. Chris Hughes also made some comment about this which I didn't internalise at the time. I think the issue is something to do with the difference between an atlas and a maximal atlas. My memory is that Patrick claimed that sometimes the books say "obviously all this stuff works" but when he actually sat down to think about formalising the details he realised that there were subtleties.

What has prompted this question is that I've just got an email from Paolo Cascini, the person who teaches manifolds at Imperial right now, saying "don't you just need as data a bunch of open sets of R^n with some functions (the transition functions) which are known to be diffeomorphic?" We were talking about Heather's construction of a manifold structure on the n-sphere.

For a while now it has been on my job list to find out something about the details of what makes this stuff difficult in Lean. For algebraic geometry I now have this coherent story about R[1/fg] not being R[1/f][1/g] and how there is this implicit diagram-chase which is never done in the books, checking that some squares commute. Grothendieck's proof was "everything is canonical so it must work out", and it does, but his proof involves using = when comparing localisations in situations where what is really happening is that there is an isomorphism rather than an equality, so he doesn't even notice that there is something which needs to be checked -- he just applies the substitution principle (A = B -> f(A) = f(B)), but for a predicate which is canonical-isomorphism-invariant, something which should be checked but which is never checked in the literature. When I explained this subtlety to de Jong he seemed genuinely interested and he's been teching alg geom at Columbia, and before that at MIT, for a very long time. He made remarks about how some students never seem to get some arguments around this point and he wondered whether this was what was confusing them. It would be nice if I could understand a corresponding story for manifolds which indicated some subtlety which a generic manifolds lecturer might not even notice exists.

view this post on Zulip Sebastien Gouezel (Feb 07 2021 at 11:14):

The main difficulties are of technical nature, with implementation details and type-theoretic difficulties (especially with partially defined functions).

Let me still mention one mathematical subtlety related to this maximal atlas issue, with the example of the sphere. You can consider a maximal atlas when you consider the sphere as an analytic manifold, or as a smooth manifold. And you also have a functorial construction associating to a manifold its tangent bundle, so you get formally two tangent bundles, the one coming from the analytic structure and the other one coming from the smooth structure. Of course from the mathematical point of view they are the same thing, but from the formal point of view they are completely different stuff, and it should be a theorem that there is a canonical isomorphism between them. And the same goes if you consider a maximal C^1 structure, a maximal C^2 structure, and so on: each time, you get a new tangent bundle. But then, what is the derivative of a C^1 map? Do you want to see it as a map on the C^\infty tangent bundle, or just on the C^0 tangent bundle coming from the C^1 structure? But a C^\infty map is also a C^1 map, so you should have a theorem saying that the derivative of this map, seen as a map on the smooth tangent bundle, coincides with the derivative of the very same map seen as a map on the C^0 tangent bundle, under the canonical isomorphism I mentioned above. Of course, you will never see a theorem like that in books, because it is just "obvious" (is it really?).

If you want to formalize this in Lean, you can imagine how you run very quickly into trouble, if the definition of the derivative depends on the smoothness class you're considering. The design decision we have currently is to avoid all this by not using maximal atlases for a given smoothness class, but use one fixed (non-maximal) atlas on a manifold, and then use it to define one (and only one) tangent bundle, one (and only one) derivative, and so on. Depending on how nice the atlas is, the tangent bundle will automatically inherit a C^1 structure, a smooth structure, an analytic structure, and so on, and everything will be compatible by design.

view this post on Zulip Sebastien Gouezel (Feb 07 2021 at 12:50):

TLDR: there are a bunch of different objects that usual mathematical practice treats as equal, so using them properly would mean checking that a lot of diagrams commute, which is never done in practice. Does it ring a bell? :-)

view this post on Zulip Heather Macbeth (Feb 07 2021 at 16:39):

Kevin Buzzard said:

What has prompted this question is that I've just got an email from Paolo Cascini, the person who teaches manifolds at Imperial right now, saying "don't you just need as data a bunch of open sets of R^n with some functions (the transition functions) which are known to be diffeomorphic?" We were talking about Heather's construction of a manifold structure on the n-sphere.

To this point: Sébastien gave us two ways to make manifolds. One is the way that Paolo describes here, docs#charted_space_core. It is indeed just a bunch of open sets and smooth functions between fixed open subsets. The manifold (as, eg, a topological space) is then constructed as a quotient of the disjoint union of all the open sets by a certain equivalence relation.

But the preferred way to construct a manifold is directly from the definition, docs#charted_space. Here we have a pre-existing topological space, charts to it, and the smoothness of the transition functions. The advantage here is that we get a manifold instance on that pre-existing topological space, here docs#metric.sphere. We can pull in all topological facts (compactness, connectedness) from pre-existing theory.

It's just like how mathlib provides docs#uniform_space_of_dist, but it's not the preferred way to construct metric spaces; instead we use docs#metric_space which is built on top of a pre-existing uniform space.

view this post on Zulip Kevin Buzzard (Feb 07 2021 at 16:41):

Going back to schemes, there is probably something we can learn here. I remember Kenny struggling to make projective 1-space in an earlier incantation of schemes because it was two copies of affine 1-space glued together -- at least this is what it says in the books. Sounds like we should have made the topological space first (e.g. using Proj).

view this post on Zulip Heather Macbeth (Feb 07 2021 at 16:43):

Won't that give the Zariski topology? :)

view this post on Zulip Heather Macbeth (Feb 07 2021 at 16:43):

I think one should make projective space P(E)\mathbb{P}(E) as a set, provide the map E{0}P(E)E\setminus\{0\}\to \mathbb{P}(E), and then give it the coinduced topology.

view this post on Zulip Heather Macbeth (Feb 07 2021 at 16:44):

@Adam Topaz has been working on this ...

view this post on Zulip Kevin Buzzard (Feb 07 2021 at 16:44):

No we really were doing algebraic geometry, this was over some arbitrary commutative ring. I know you guys struggle with just C\mathbb{C} but...

view this post on Zulip Adam Topaz (Feb 07 2021 at 16:44):

Shameless plug: branch#proj-space-quot

view this post on Zulip Adam Topaz (Feb 07 2021 at 16:45):

And "working" is a strong word.

view this post on Zulip Adam Topaz (Feb 07 2021 at 16:45):

I want projective spaces because I want things like the fundamental theorem of projective geometry, which is one of the main useful things for anabelian geometry. And for that I really do need just the "classical" projective spaces.

view this post on Zulip Kevin Buzzard (Feb 07 2021 at 16:47):

One thing which we see in arithmetic geometry a lot is a place where mathematicians really do not write down the invisible maps in situations where they are actually highly non-trivial -- the analyticification of a complex algebraic variety, i.e. the functor which sends it to a complex analytic space (or complex manifold if the variety is smooth). Sometimes people even use the same notation for both, but people who are being careful use "X^an" for the manifold associated to the smooth scheme X of finite type over C.

view this post on Zulip Heather Macbeth (Feb 07 2021 at 16:52):

Heather Macbeth said:

I think one should make projective space P(E)\mathbb{P}(E) as a set, provide the map E{0}P(E)E\setminus\{0\}\to \mathbb{P}(E), and then give it the coinduced topology.

Now that I think about it, does this construction also work to transfer the Zariski topology from E{0}E\setminus\{0\} to P(E)\mathbb{P}(E)?

view this post on Zulip Adam Topaz (Feb 07 2021 at 16:53):

Yes, but the Zariski topology (in the classical sense) is only really useful over algebraically closed fields.

view this post on Zulip Justus Springer (Feb 07 2021 at 16:55):

Hey! I'm very new to this community so please forgive my naivety and maybe this is offtopic. But I'm getting the feeling that implicit isomorphisms like the ones you describe here are really a central hurdle in formalized mathematics. Mathematicians constantly use various identifications and natural isomorphisms without even thinking about them anymore. Making all of this explicit requires painful amount of care and attention to detail. I remember reading somewhere that in SGA, Grothendieck explicitly blurs the distinction between equality and isomorphism by using the symbol = to denote a "canonical isomorphism". Having a CS background, arguments like "everything is canonical so it must work out" always remind me of what functional programmers call "Theorems for free", which basically states that "parametricity implies naturality". This means that whenever you write a function which is parametrically polymorphic (as opposed to ad-hoc polymorphism), then it must automatically be a natural transformation. I've always wondered whether one can make this intuition precise in mathematics as well, stating that whenever a construction is canonical enough, it's automatically natural.

view this post on Zulip Adam Topaz (Feb 07 2021 at 16:57):

I would say that what Kevin described above is more like a coercion. You have the category of schemes over C\mathbb{C}, say, and some functor (Betti cohomology) which is defined on complex-analytic things, but there just so happens to be an invisible coercion from C\mathbb{C}-varieties to the complex-analytic category, which some people explicitly write as XXanX \mapsto X^{an}.

view this post on Zulip Adam Topaz (Feb 07 2021 at 16:58):

But humans are smart, and they can figure out that when I say "Consider the Betti cohomology Hi(X,Z)H^i(X,\mathbb{Z}) of the C\mathbb{C}-variety XX." that I really want to first pass through this invisible coercion, because Betti cohomology only makes sense after passing to this coercion.

view this post on Zulip Adam Topaz (Feb 07 2021 at 17:02):

A bigger sin IMO is when the author fixes some embedding of a number field into C\mathbb{C} and computes things like Betti cohomology by base-change along this embedding (I'm guilty of this sin), because such an embedding is not "canonical".

view this post on Zulip Kevin Buzzard (Feb 07 2021 at 17:03):

But in SGA (and EGA, and plenty of other books on the subject) there is this = trick (you might have read it in something I wrote, I tend to bang on about this in various places) and getting the theorems we wanted for schemes involved refactoring proofs which didn't use universal properties enough.

view this post on Zulip Kevin Buzzard (Feb 07 2021 at 17:03):

Adam Topaz said:

A bigger sin IMO is when the author fixes some embedding of a number field into C\mathbb{C} and computes things like Betti cohomology by base-change along this embedding (I'm guilty of this sin), because such an embedding is not "canonical".

The answers can be different, right? Some early theorem of Serre.

view this post on Zulip Kevin Buzzard (Feb 07 2021 at 17:04):

[I know this because I once started to read his collected works from the beginning :-) No, I didn't make it to the end...]

view this post on Zulip Heather Macbeth (Feb 07 2021 at 17:04):

Adam Topaz said:

A bigger sin IMO is when the author fixes some embedding of a number field into C\mathbb{C} and computes things like Betti cohomology by base-change along this embedding (I'm guilty of this sin), because such an embedding is not "canonical".

Or, God forbid, fixes an embedding of a Riemannian manifold into some RN\mathbb{R}^N (which exists by Nash's theorem), and defines some functional using this embedding and then checks that it's independent of the embedding. I have seen many people do this!

view this post on Zulip Kevin Buzzard (Feb 07 2021 at 17:05):

The sin is not checking, right?

view this post on Zulip Heather Macbeth (Feb 07 2021 at 17:05):

People generally check, I would just prefer to see an alternative construction that doesn't require such an embedding :)

view this post on Zulip Adam Topaz (Feb 07 2021 at 17:06):

The sin is "it is easy to see that this construction doesn't depend on the embedding [5]."

[5] J. Smith. Private communication (1983).

(I'm not guilty of this sin...)

view this post on Zulip Adam Topaz (Feb 07 2021 at 17:08):

Concerning the issue of schemes: It seems like the issue that came up here is the lack of API around gluing, right?

view this post on Zulip Kevin Buzzard (Feb 07 2021 at 17:10):

Right -- this was with a preliminary version anyway. This is just one of many things I want to get around to. But gluing in the category of schemes is not so simple! Pushouts of two morphisms don't exist in general, you have to be careful.

view this post on Zulip Kevin Buzzard (Feb 07 2021 at 17:11):

Brian Conrad once told me that he couldn't find a reference and sketched some general criteria for when things work. Private communication (1998 or so?)

view this post on Zulip Adam Topaz (Feb 07 2021 at 17:12):

Does it work if all the morphisms in the colimit diagram are open embeddings? I guess no, since you can have some crazy tower of open neighborhoods of something closed, etc.

view this post on Zulip Kevin Buzzard (Feb 07 2021 at 17:14):

you're saying you want me to find the email??

view this post on Zulip Adam Topaz (Feb 07 2021 at 17:14):

Actually maybe it does work?

view this post on Zulip Adam Topaz (Feb 07 2021 at 17:15):

I'm curious, because I've never seen such a criterion written down.

view this post on Zulip Kevin Buzzard (Feb 07 2021 at 17:15):

It would be easier to just email Brian again ;-)

view this post on Zulip Adam Topaz (Feb 07 2021 at 17:37):

Anyway, for gluing schemes, you would just want some descent datum in the Zariski topology... No need to really think about which colimits make sense.

view this post on Zulip Roman Bars (Feb 07 2021 at 18:01):

Kevin Buzzard said:

Adam Topaz said:

A bigger sin IMO is when the author fixes some embedding of a number field into C\mathbb{C} and computes things like Betti cohomology by base-change along this embedding (I'm guilty of this sin), because such an embedding is not "canonical".

The answers can be different, right? Some early theorem of Serre.

If you consider the intersection product on singular cohomology you can get different rings. I think an example is in F. Charles's "Conjugate varieties with distinct real cohomology algebras"

view this post on Zulip Damiano Testa (Feb 10 2021 at 07:34):

I am a little late for this discussion, but, with respect to gluing of schemes, this paper has some criteria:

https://www.math.utah.edu/~schwede/Papers/SchemeWithoutPoints.pdf


Last updated: May 18 2021 at 08:14 UTC