Fixing the definition of models with corners

Stream: mathlib4

[Michael Rothgang]

Background for the non-maintainers. Mathlib has a very general notion of "manifolds with boundary and corners". It allows boundaryless manifolds, manifolds with boundary, corners of any order (e.g., modelled on any Euclidean quadrant) and more. This is slightly different from most textbooks, in that mathlib's definition is just putting in "these are the minimal properties we need" (and extending this list as we realise more conditions are needed) as opposed to demanding a particular model.

Impetus. Specifically, mathlib's current definition of models with corners is wrong, in the sense of being too general. A complex manifold (of current mathlib) need not be a real manifold. (The reason is that the condition UniqueDiffOn C target does not imply UniqueDiffOn R target; unique differentiability over C is a weaker condition.) That is very undesirable, so we'd like to add another condition. This was discussed in #18403; @Sébastien Gouëzel proposed that we add the requirement "the interior of range I is convex". In #23657 (a pre-requisite to #23658 which makes that change), he proposed dropping the "interior" in that statement.

New discovery. However, since then Floris van Doorn and I realised that this condition is too strong. There is a notion of (finite-dimensional) complex manifolds with boundary (see Jack Lee's stackoverflow answer and a follow-up for a definition). In short, the proper definition is to allow models with range $${z\in U \colon\; f(z)\leq 0\}$, where $U\subset\mathbb{C}^n$ is open and $$f\colon U\to\mathbb{R}$ is a smooth submersion. This range, however, need not be convex.

What to do? Floris and I wondered if we can make this the general definition. To boot, this raises a few questions:

• how to define complex manifolds with corners? We certainly would like to have them in mathlib, so we can take finite products of manifolds.
  A first naive definition is "the model has range $$f^{-1}((-\infty,0])\cap g^{-1}((-\infty,0])$", where $f,g\colon U\to\mathbb{R}$ are two real submersions (and similarly for higher-order corners).
  This is not correct yet, as it would e.g. allow ${z: Im z = 0}$ as a complex manifold with corners (via the submersions $f(z):= Re z$ and $g = -f$). We need to add some non-degeneracy condition.

• what about Banach manifolds with corners? Many textbooks (e.g. Lang or Schmeding) do not speak about this. Roig-Dominguez define Banach manifolds with boundary and corners, in a similar way as above: you can take k linearly independent linear functionals $f_i$ on your model space, and consider models with range $\bigcap_{i=1}^k f_i^{-1}([0,\infty))$.

New proposal. Thus, here is a strawman proposal. We add a new constraint to the definition of models with corners modelled over an RCLike field, consisting of

• data: a finite set of maps $f_i\colon E\to\mathbb{R}$
• a proof that all these maps are submersions,
• a non-degeneracy condition: for each z in the range of the model, if precisely k of our submersions vanish at z, then their differentials at z are linearly independent (as vectors in the space of real linear maps $E\to\mathbb{R}$). (If all submersions are linear, this is precisely "all submersions are linearly independent.)
• the condition that our model with corners have range $\bigcap_{i=1}^k f_i^{-1}([0,\infty))$ (or perhaps, considering suitable restrictions of f_i instead)

This proposal

• allows for complex manifolds with boundary and also allows corners there
• is, over the real numbers, equivalent to the standard definition using Euclidean quadrants. (This requires a little work to prove, but follows since in suitable charts, submersions are just a coordinate projection.)
• implies the range is "large": its interior is dense in the range, and
• and implies the unique differentiability condition over R or C.

It also ensures complex manifolds are always real manifolds (as complex linearly independent vectors are also real linearly independent).

Tagging @Sébastien Gouëzel (whom else?)

[Sébastien Gouëzel]

If the issue is that complex manifolds are not always real manifolds, can't you just demand that, in the RCLike case, the range has UniqueDiffOn for R?

[Floris van Doorn]

I'd like to fix the definition of model spaces, instead of playing this game "let's work with the weakest definition of model spaces that can prove theorems $1, \ldots, N$ and if theorem $N+1$ requires an additional condition on model spaces, then we change its definition."

Michael mentioned the collar neighbourhood theorem recently, which probably also requires an additional condition on model spaces for real manifold with boundaries (without corners). Another example: I'm not sure if we can prove with the current definition that the boundary of a p-adic manifold is empty.

So Michael's proposal is a proposal to significantly restrict model spaces, while supporting all model spaces that I'm currently aware exist in the literature (which might not be exhaustive, of course).
In fact, maybe we should go one step further: if $\mathbb{k}$ is a field extension of $\mathbb{R}$ (or maybe if $\mathbb{k}$ is RC-like?) then we add the boundary data as in Michael's proposal, and otherwise we require that the model has range $E$, so that we also get nice model spaces for e.g. the p-adics.
If we do that, we can get rid of the unique differentiability condition and the condition that the interior is dense, since that follows from these conditions.

[Sébastien Gouëzel]

I'm definitely on par with enforcing that the range is univ when the field is not RCLike.

For RCLike fields, though, the definition proposed by Michael looks very specific. I'm not saying we should be general for the sake of being general, but rather for the sake of clarifying the picture and simplifying the proofs: Often, focusing on specific details hides the big picture of what is really going on, and tends to make proofs harder because you have too many things available and you don't know which tool to use.

For more specific theorems, of course, you will need more specific assumptions. For instance, the collar theorem only makes sense for manifolds with boundary, not manifolds with corners, because you need the boundary to be a manifold in itself.

[Sébastien Gouëzel]

This being said, we could change the definition to be whatever definition you like, prove from it the basic properties (the range is UniqueDiffOn, the interior of the range is dense, whatever) and then only use these properties when building the theory. I wouldn't mind at all. What I'm afraid of is that users of the library would try to come back to the initial very specific definition too often, and would get lost in it. But this could be avoided by a thorough docstring saying: "don't use this definition unless really necessary, use the API provided by such and such".

[Floris van Doorn]

If you're mostly worried about discovery of the important properties of model spaces, then I'm definitely happy to add in docstrings/module docs text of the form "these 2+ properties are often the only properties you need to do basic manifold theory" and prove these properties early.

[Sébastien Gouëzel]

(Note that the definition of complex manifold with boundary pointed by Michael can not be implemented in current Mathlib, as the model space would have to depend on the point you're looking at in the manifold, while we're working with a fixed model space all over the place).

[Joël Riou]

Sébastien Gouëzel said:

(Note that the definition of complex manifold with boundary pointed by Michael can not be implemented in current Mathlib, as the model space would have to depend on the point you're looking at in the manifold, while we're working with a fixed model space all over the place).

I have no idea how difficult implementing this generalization would be, but it would be very useful when we want to construct smooth manifolds attached to smooth schemes over the complex numbers (or over the reals). Otherwise, we would need equidimensional assumptions, which would be very annoying.

[Sébastien Gouëzel]

To be honest, I am not convinced yet that there is anything to be gained by changing the definition (apart from requiring that over C there is also real UniqueDiffOn for the range over the reals, but even for that it could even be better to have this as an additional typeclass over I added when needed, instead of being part of the definition). I think that to be convinced I just need to be shown a theorem where this is important.

[Sébastien Gouëzel]

Smooth manifolds in mathlib are indeed constant-dimensional globally, otherwise it's just a nightmare.

[Floris van Doorn]

Sébastien Gouëzel said:

(Note that the definition of complex manifold with boundary pointed by Michael can not be implemented in current Mathlib, as the model space would have to depend on the point you're looking at in the manifold, while we're working with a fixed model space all over the place).

True, although that design decision is orthogonal to this one.

[Sébastien Gouëzel]

In the same way, vector bundles have fixed dimension of the fiber.

[Floris van Doorn]

Sébastien Gouëzel said:

To be honest, I am not convinced yet that there is anything to be gained by changing the definition (apart from requiring that over C there is also real UniqueDiffOn for the range over the reals, but even for that it could even be better to have this as an additional typeclass over I added when needed, instead of being part of the definition). I think that to be convinced I just need to be shown a theorem where this is important.

That is another route we could take. Michael's definition does simplify the definition manifold with boundary without corner (or with n-corners but no (n+1)-corners): you can just say that any point is in at most n zero sets. But another option is to just have a type-class "this manifold has a nice smooth boundary and (therefore) no corners" and prove theorems that need that using that class.

[Sébastien Gouëzel]

We definitely need a class for model with corners with nice boundary, because they are needed to endow the boundary with a manifold structure, which should be available to typeclass inference.

[Floris van Doorn]

I guess using the current (general) definition the interior + boundary of the Koch snowflake is a manifold (I believe). Do we care about that?

[Sébastien Gouëzel]

It's not a smooth manifold, so no problem here as far as I can see.

[Floris van Doorn]

Is it not? It is a model space, and I can use 1 chart to model it.

[Sébastien Gouëzel]

Ah, for this weird model with corners yes, definitely. But the weird model with corners doesn't have a nice boundary.

[Kevin Buzzard]

@Joël Riou maybe for the analytic space associated to a scheme of finite type over $\mathbb{C}$ we need some new definition then? e.g. complex analytic spaces? And then maybe in the smooth case we show that their components are manifolds?

[Floris van Doorn]

If we're not uncomfortable with the fact that Mathlib has smooth manifolds with fractal boundary, then I can also live with adding Michael's conditions as a type-class on top of ModelWithCorners.
However, I would be happier to go in that direction if there is an actual use-case of the current ModelWithCorners besides being general for the sake of being general.

[Michael Rothgang]

Sébastien Gouëzel said:

We definitely need a class for model with corners with nice boundary, because they are needed to endow the boundary with a manifold structure, which should be available to typeclass inference.

By the way, #22059 is my current proposal in that area. It carries data (but that should be fine, given that we don't care about the particular choice of data, but merely about the existence of such data). The code is not maximally polished: it depends on a few not-yet-merged PRs, as a few sorries for unused PRs, and the last 200 lines can probably be ignored --- but this could give a first idea.
Before landing that in mathlib, we should probably merge a definition of smooth embeddings first (which I'm also working on).

Note that is a typeclass on the manifold, not the model with corners.

[Michael Rothgang]

I think a statement "if M is a real manifold modelled on the upper half space in R^n, then its boundary is a smooth real manifold" is false without additional assumptions. To start, note that M could be boundaryless (e.g., if M is in fact modelled on an open ball in the interior of the model's range). For an actual counterexample, let $n=2$ and let $M$ be the top right quadrant in R² (which has boundary and a corner). We embed M into the upper half space so the corner is on the real line. I believe that currently, this is allowed.

[Sébastien Gouëzel]

I don't get your example. To me, if you have a smooth real manifold modelled on the upper half space of dimension n+1, then its boundary is definitely a smooth real manifold (of dimension n, without boundary). Sketch of proof: at a point x of the boundary, the corresponding chart c of M sends a neighborhood of this point to some set in the upper half space, and a neighborhood of ∂M around x to a subset of ℝ^n. The restriction of c to ∂M is your chart, taking values in ℝ^n. The change of coordinates are smooth, everything looks fine to me. Am I overlooking something?

[Joël Riou]

Kevin Buzzard said:

Joël Riou maybe for the analytic space associated to a scheme of finite type over $\mathbb{C}$ we need some new definition then? e.g. complex analytic spaces? And then maybe in the smooth case we show that their components are manifolds?

Yes, anyways, we will have to introduce a new definition so as to include singularities.

[Sébastien Gouëzel]

But as far as I understand all this is blocked until we have invariance of domain, anyway.

[Antoine Chambert-Loir]

@Sébastien Gouëzel what is it specifically that makes the theory of manifolds a nightmare is the dimension, resp the local type, is not constant?

[Sébastien Gouëzel]

Honestly, I haven't even tried, since I avoid dependent type hell whenever I can. The issue is that, if the type of the model space, the charts, the model with corner, and so on, depend on the point of the manifold, then rewriting becomes impossible (well, not impossible, but a much more complicated dance).