manifolds without corners

Stream: maths

[Kevin Buzzard]

So I finally had a proper look at @Nicolò Cavalleri 's paper with @Anthony Bordg on Lie groups etc in Lean https://arxiv.org/abs/2108.00484 . They talk about the problems they had using manifolds with corners, e.g. when proving the product of two Lie groups is a Lie group. Johan reminds me of Patrick's observation that locally ringed spaces can't be used as a foundation for the theory of manifolds with corners, because e.g. the closed quarter disc and closed half disc are isomorphic as locally ringed spaces but not isomorphic as manifolds with corners. However I personally had never heard of a manifold with corner before this development and I'm not sure that they come up at all in the kinds of manifolds I'm interested in as a Langlands philosophy person, namely the quotients of symmetric spaces like the upper half plane by discrete subgroups like SL_2(Z). We do see manifolds with boundary as part of a differential-geometric compactification sometimes, but we will not need such things for a very long time.

I am wondering if there is a case for developing a theory of smooth manifolds using the locally ringed space machinery we have, to see if it makes applications like Lie groups or vector bundles any easier -- I think that exterior powers of the cotangent bundle are something which we will need sooner rather than later but it still seems to me that we're struggling to do this. With locally ringed spaces I should think linear algebra on bundles becomes as easy as linear algebra on modules.

Or is making a new definition a disastrous idea and we should instead make a better API for what we have?

[Patrick Massot]

The corner thing is true, but that's not the main point. The main point is that the ring space point of view doesn't fix anything, because you need charts anyway. The discussion is analogous to saying you don't need Spec to define schemes because schemes are locally ringed spaces.

[Patrick Massot]

This whole discussion is an algebraic geometer fantasy, but no one ever took it seriously.

[Kevin Buzzard]

But this paper points out some problems with how we have things set up, and some of them seem to be because we're keeping track of corners too hard

[Kevin Buzzard]

I guess I'm trying to work out why doing linear algebra with the tangent bundle is hard

[Adam Topaz]

Kevin, in what sense is the quarter disc isomorphic to the half disc as locally ringed spaces? What are the sheaves? This probably just means you're considering a context with too many functions in your sheaves.

[Kevin Buzzard]

I just figured that the "complex squaring map" was an isomorphism from a closed quarter-disc to a closed half-disc. Is there something funny going on at 0?

Patrick's point is I think that even if we had no corners we'd still have the issue that if G is locally R^a and H is locally R^b then G x H is probably locally R^a x R^b instead of R^{a+b}.

[Kyle Miller]

Squaring doesn't induce an isomorphism of 1-jets at $0$. If $s:Q\to H$ is the squaring map from the closed quarter disk to the closed half disk, the induced ring homomorphism $\hom(C^\infty_0(H)/\mathfrak{m}_0^2,C^\infty_0(Q)/\mathfrak{m}_0^2)$ is $[f]\mapsto [f(0)]$, where $\mathfrak{m}_0$ denotes the maximal ideal in the relevant local ring. (At least, I'm pretty sure that these quotients are both isomorphic to $\R[x_1,x_2]/(x_1,x_2)^2$ even in the presence of corners. It seems everything carries over just fine.)

The angle doubling function doesn't seem to work, either, since nothing maps to the germ of $f(x,y)=x$ on $Q$ at $0$.

[Sebastien Gouezel]

The difficulty has nothing to do with corners, it is already there for manifolds without boundary. Let's say that a manifold is a space with the data of a bunch of charts. For instance, a vector space is naturally a manifold, with a single chart, the identity. Then, if E and F are two vector spaces, then E × F is a vector space, so it has the manifold structure with the identity as single chart. But it is also a product of manifolds, so it has a manifold structure, with a single chart equal to the product of the charts of the single components, i.e., the product of the identities, which is not defeq to the identity. If you're not careful, you get two non-defeq manifold structures on E × F, which is bad as we know. This just means that you have to be a little bit careful when defining product manifolds, by introducing a suitable type synonym somewhere. But this is not hard at all, it's just one of these little things that you notice when you formalize properly.

By the way, I have no interest for manifolds with corners. What I really care about are manifolds, and manifolds with boundary (these show up everywhere, for instance to formulate Stokes formula). Manifolds with corners as defined in mathlib are just one way to cover in one go manifolds and manifolds with boundary.

[Eric Wieser]

Could you elaborate on exactly what ends up nondefeq? (Specifically what type the offending equality is between)

[Patrick Massot]

Kevin gave the main example two messages above.

[Eric Wieser]

Perhaps I should have also asked "are they even propositionally equal"?

[Patrick Massot]

They are only isomorphic.

[Eric Wieser]

I'm probably getting only a fraction of the picture here; but it sounds like the typeclass being hypothesized here has a field like (chart_type : Type u) meaning that typeclass diamonds end up needing to show equality of types. That problem goes away if you change chart_type to an out_param, although I'm sure that introduces a different sort of issue.

[Sebastien Gouezel]

My example is not this one. And in this example, they are propositionally equal, but not defeq. Let me state it again.

Say that a manifold structure on a space M with model E (a real vector space) is a bunch of charts on open subsets of M, with target open subsets of E. The first instance of a manifold structure is on E itself, with one single chart equal to the identity.

[Sebastien Gouezel]

If M is a manifold modelled on E, and N is a manifold modelled on F, then you can define a manifold structure on M x N, with model E x F, by taking the direct products of all charts on M and on N.

[Sebastien Gouezel]

Then, on E x F, you get two manifold structures with target space E x F. The first one comes from the fact that E x F is a vector space, so it has a single chart, equal to the identity. The second one comes from the product structure. It has a single chart, which is the product of the single charts on E and on F, i.e., the direct product of the identities. It is propositionally the identity (so the two manifold structures are the same) but not definitionally.

[Sebastien Gouezel]

The way this is solved currently in the library is by saying that the model space for a product of manifolds is not E x F, but a type synonym called model_prod E F. This means that E x F has a manifold structure with model space E x F (coming from the fact that it is a vector space), and another one coming from the fact that it is a product (with model space model_prod E F).

By the way, this example shows that the model space can not be an out_param, because we get a natural example with two different model spaces.

[Eric Wieser]

Does lean actually require that out_params have a unique solution?

[Eric Wieser]

(I think my confusion arises from now knowing what lean type "the identity" and "the direct product of identities" have in your example)

[Eric Wieser]

(is the problem just that prod.map id id = id is not true definitionally?)

[Sebastien Gouezel]

Yes

[Nicolò Cavalleri]

Sorry if I never answered to this post: I was already on holiday and then I forgot. Just to clarify, when we underlined some difficulties with manifolds with corners it was more meant to say that for a mathematician who never used Lean before there will be some new formalism to digest that they might not be used to. As for whether or not the current is a good implementation I actually think the current implementation is great and that we do really need manifold with corners: since for sure one wants manifold with boundary let them have corners since the beginning (the product of two manifolds with boundary is not a manifold with boundary and to me this is a good reason to want corners in the picture).

However I have a remark I want to share here about manifolds without boundary: the current implementation is done with the property model_with_corners.boundaryless for which, however, there is no API yet. I think another possible implementation could be to define them separately from manifold with corners and then register an instance of them as manifolds with corners, so to have that the theorems for the latter are automatically valid for manifold without boundary. In the project I just undertook I realized that when you need to use properties of manifolds without boundary (namely that charts are local diffeos on the vector spaces) the corners setting adds extra complication that can be avoided. I have the following impression: in the case of the current implementation one has to write a new API for boundaryless manifolds by rewriting ext_charts as local homeos instead of local equivs and restate only the lemmas for them (I guess for sure one would want to have them recognized as local homeos to take advantage of the great local homeo library). In my implementation one has the extra effort of having to restate all lemmas for manifolds but all the proofs can be recovered from the current ones and I have the impression that being able to avoid the extra complicacy of corners in lemmas that need boundaryless manifolds still wins over this extra effort. Is there anything else I am not considering for which my proposed implementation of boundaryless manifolds could be problematic?

[Sebastien Gouezel]

I don't know for sure what the best implementation of manifolds without boundary is -- only experimenting can tell us. What I know, though, is that I want only one construction of the tangent bundle, and one notion of differentiability. This means that whatever the definition of boundaryless manifold you use, the definition of the derivative in charts will have to go through ext_chart, and the very notion of derivative will need to mention some model with corner I. It would probably make sense to provide an API to hide this a little bit, and then the details of the implementation should not matter.

[Nicolò Cavalleri]

Sebastien Gouezel said:

I don't know for sure what the best implementation of manifolds without boundary is -- only experimenting can tell us. What I know, though, is that I want only one construction of the tangent bundle, and one notion of differentiability. This means that whatever the definition of boundaryless manifold you use, the definition of the derivative in charts will have to go through ext_chart, and the very notion of derivative will need to mention some model with corner I. It would probably make sense to provide an API to hide this a little bit, and then the details of the implementation should not matter.

Yes sure I 100% agree on this although my idea would not require rewriting any definition right? As for ext_chart one would want to rewrite a version for boundaryless manifolds that local homeos and that a posteriori one proves to be equal to ext_charts as functions. The point here is that I realize that in the proof where the boundaryless property is necessary, it is probably because you want very badly that ext_chart_atbe recognized as a local homeo and hence you'd need to rewrite it anyways (you can do something like ext_chart_at.to_local_homeo which is what you'd do in my case as well)

[Sebastien Gouezel]

Defining something like

ext_chart_at_lh [...] [I.boundaryless] (x : M) : local_homeomorph M E :=
{ continuous_to_fun := sorry,

  .. ext_chart_at I x }

definitely sounds like a good idea (where lh stands for local homeo).