why are manifolds difficult?

Stream: maths

[Kevin Buzzard]

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.

[Sebastien Gouezel]

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.

[Sebastien Gouezel]

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

[Heather Macbeth]

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.

[Kevin Buzzard]

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

[Heather Macbeth]

Won't that give the Zariski topology? :)

[Heather Macbeth]

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

[Heather Macbeth]

@Adam Topaz has been working on this ...

[Kevin Buzzard]

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

[Adam Topaz]

Shameless plug: branch#proj-space-quot

[Adam Topaz]

And "working" is a strong word.

[Adam Topaz]

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.

[Kevin Buzzard]

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.

[Heather Macbeth]

Heather Macbeth said:

I think one should make projective space $\mathbb{P}(E)$ as a set, provide the map $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\setminus\{0\}$ to $\mathbb{P}(E)$?

[Adam Topaz]

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

[Justus Springer]

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.

[Adam Topaz]

I would say that what Kevin described above is more like a coercion. You have the category of schemes over $\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 $\mathbb{C}$-varieties to the complex-analytic category, which some people explicitly write as $X \mapsto X^{an}$.

[Adam Topaz]

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

[Adam Topaz]

A bigger sin IMO is when the author fixes some embedding of a number field into $\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".

[Kevin Buzzard]

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.

[Kevin Buzzard]

Adam Topaz said:

A bigger sin IMO is when the author fixes some embedding of a number field into $\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.

[Kevin Buzzard]

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

[Heather Macbeth]

Adam Topaz said:

A bigger sin IMO is when the author fixes some embedding of a number field into $\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 $\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!

[Kevin Buzzard]

The sin is not checking, right?

[Heather Macbeth]

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

[Adam Topaz]

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

[Adam Topaz]

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

[Kevin Buzzard]

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.

[Kevin Buzzard]

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

[Adam Topaz]

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.

[Kevin Buzzard]

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

[Adam Topaz]

Actually maybe it does work?

[Adam Topaz]

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

[Kevin Buzzard]

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

[Adam Topaz]

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.

[Roman Bars]

Kevin Buzzard said:

Adam Topaz said:

A bigger sin IMO is when the author fixes some embedding of a number field into $\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"

[Damiano Testa]

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