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

[Michael Rothgang]

This zulip discussion seems to have reached a steady state. Let me summarize what was discussed after the initial proposal.

• to make e.g. an ellipsoid in R^2k a complex manifold with boundary, the model with corners would have to depend on the base point. (Perhaps this can be avoided by working harder to construct a model. I haven't tried very hard.)
• Currently, mathlib assumes the model space is constant. Changing this could be involved (e.g., the identification of tangent spaces with the model space would break; one cannot rw by this any more) --- but also orthogonal to the other changes proposed. In other words, this could be a change independent of this one. Assuming a constant model space also means a manifold has constant dimension (which some applications may wish to not assume... but that is another discussion for the future).
• Note that with the current definition of models with corners, the interior and boundary of the Koch snowflake are a smooth manifold (for this very particular model).
• p-adic manifolds are funny objects; often p-adic spaces are the much more interesting objects to study. But p-adic Lie groups are studied, so we should keep manifolds for this reason.

Overall, there are (at least) two options forward.

Option 1: "minimal changes"

Add a condition that complex manifolds also have unique derivatives over R. Prove that complex manifolds are also real manifolds. If the future need arises, add a type class "has nice boundary" which could state the quadrant condition above.

Option 1b: "almost minimal changes"

Like Option 1, but also demand that p-adic manifolds have no boundary. (Perhaps with a TODO to remove this condition, if it can be deduced from the others. In paper mathematics, it can --- I haven't investigated if this is also true in mathlib. Whoever uses p-adic manifolds can look into this.)

Option 1c: also require convexity

Require that the range of the model with corners is convex in the real or complex case, and univ otherwise. (This implies the conditions in option 1b and 1c.) This condition is important to define Riemannian manifolds: if you want to say that, locally, the distance in the manifold is comparable to the distance in the model space, then you need (some form of) convexity in the model space. And you need this comparability to say that the distance induced by a Riemannian metric defines the same topology as the preexisting one.

Option 2. require Euclidean quadrants

Change the definition of models with corners substantially: demand that it be defined using finitely many linearly independent functionals, and that the range of the model with corners is the simultaneous non-negativity set of all of these. This nicely yields a definition of "boundary without corners". Deduce the current properties from this definition. Augment the doc-string to emphasize that usually, we only use these properties of models.
This is stronger than option 1c.
Biggest downside: this excludes e.g. the ellipsoid, or complex manifolds with boundary (like option 1c).

Option 2b: require "curved quadrants"

Weaker than option 2: instead of linear functionals, take real submersions (as detailed above). This is now a non-standard definition, but is general enough to include complex manifolds with boundary.

Option 3: add a ConvexModel typeclass instead

This would be assumed for a theorem "complex manifolds are real manifolds", or for studying manifolds with a Riemannian metric.

[Michael Rothgang]

Is this a fair summary? Is something missing? Please let me know and I can edit it.

[Michael Rothgang]

All this considered, I propose going ahead with option 1 (and optionally also option 1b) --- for now.

[Sébastien Gouëzel]

There is also Option 1c: require that the range of the model with corners is convex in the real or complex case, and univ otherwise.

[Sébastien Gouëzel]

That would be important to define Riemannian manifolds: if you want to say that, locally, the distance in the manifold is comparable to the distance in the model space, then you need (some form of) convexity in the model space. And you need this comparability to say that the distance induced by a Riemannian metric defines the same topology as the preexisting one.

[Michael Rothgang]

Option 1c will exclude complex manifolds with boundary, right?

[Michael Rothgang]

Added to the summary above

[Sébastien Gouëzel]

option 1c is weaker than option 2, right? Because a Euclidean quadrant is always convex. So if you're happy with 2, you should also be happy with 1c?

[Michael Rothgang]

... right. I added option 2b to use "curved quadrants" (as Floris and I originally proposed).

[Michael Rothgang]

I guess, at this point I'm happy to postpone discussions about complex manifolds with boundary a bit further, and revisit that decision if/when somebody would like to formalise them.

[Michael Rothgang]

In other words: I'm also happy to go with option 1c.

[Sébastien Gouëzel]

I'm happy with 1c. I can have a go at it if you like (and if nobody objects)

[Michael Rothgang]

I can have a go at it if you like

Given #23658 exists, how about we split this: you can fix Instances/Real.lean(feel free to ask for my review), and then I'll re-base #23658 on top of your PR?

(Assuming there are no further objections.)

[Michael Rothgang]

I just remembered that all convexity results needed (if one talks about the range of the model, as opposed to its interior) are already in mathlib, hence #23658 just needs a touch-up. I just did most of it, but am stuck with two sorries. @Sébastien Gouëzel Would you like to have a go at fixing those? This would be most welcome.

[Sébastien Gouëzel]

In this PR, it would also make sense to deduce unique differentiability and the fact it's the closure of the interior from the convexity. Can I try to do that in the branch?

[Michael Rothgang]

Sure! (In fact, Floris and I stumbled across the fact that we wanted convexity of the whole range to do some of this --- so having it proven would be great to have.)

[Michael Rothgang]

Adding an instance "a complex model with corners is a real model with corners" could also be nice to have (but I can also do that, if you prefer).

[Michael Rothgang]

I just tried to do so, and pushed what I have to the branch.

[Floris van Doorn]

Oh, I didn't expect we would now go with excluding certain complex manifold with boundaries... Probably not my preferred option, but I can live with it, especially if it's also useful for Riemannian manifolds.

Michael, I don't understand why your ellipsoid example needs a point-dependent model space (or why an ellipsoid would have a boundary), but let's discuss that live.

[Sébastien Gouëzel]

I have a working branch in SG_test3 (compiles, no sorry). @Michael Rothgang, so you want to merge it into #23658?

[Michael Rothgang]

Thanks a lot! Looking over the diff, my impression is that this does several unrelated clean-ups also. Can you split these out, please? (I'll be happy to approve quickly... it certainly LGTM now.)

• one for renaming ModelWithCorners.transDiffeomorph and Diffeomorph.toTransDiffeomorph
• perhaps one for turning symm_toLinearEquiv around
  Merging the remainder into my branch sounds good.

[Sébastien Gouëzel]

The transDiffeomorph change is directly related to the branch: currently, it's for composing with a diffeomorphism, but once one switches to convex sets one can only compose with linear equivs, hence the change of name from transDiffeomorph to transContinuousLinearEquiv.

For the turning around of symm_toLinearEquiv (which I need to fix a proof), I'll wait until there is a conclusion in the other discussion.

[Notification Bot]

8 messages were moved from this topic to #mathlib4 > Invariant of domain by Michael Rothgang.

[Michael Rothgang]

Discussing with @Heather Macbeth and @Patrick Massot at Big Proof turned up two further options. If I understand correctly, Heather was nervous of using typeclass synthesis for the definition of models with corners. (I didn't catch why precisely --- perhaps you can articulate that?) Hence, two further options emerged:

• keep the current definition of models with corners: with the understanding that it is "too general" in some sense, but serving as a minimal common ground for surprisingly many theorems. Add a ConvexModel typeclass, stating that the model with corners has convex range. Then the relation between real and complex manifolds becomes "a complex manifold with a ConvexModel is a real manifold (with a ConvexModel). Many theorems will just assume a convex model, just like a number of results assume Hausdorff or second countable results.
• remove the talk about p-adic manifolds, and restrict to the real or complex numbers. This is much more radical, but means we don't get to deal with any case distinctions any more: the base field of a manifold is always RCLike, and this is baked into the definition. This certainly surprised me on first glance; the argument in favour is that p-adic manifolds are very weird objects to begin with. Generally, you'd want to work with adic spaces instead. (That's what I hear, I don't know myself.)

[Michael Rothgang]

On Github, Sebastién wrote the following:

My idea is to include in model with corners whatever we need to cover the standard examples in the literature, while being able to prove the maximum number of theorems we can, and minimize the pain for users.

We need to include something like convexity of the range of model with corners, for Riemannian geometry: otherwise, if you have norms on tangent spaces, and you define the distance between two points as the inf of lenghts of C^1 paths between these points, this may not define the same topology as the original one (think of a comb-like model with corners, with branches of height 1 accumulating at a branch at 0: then the geodesic distance between (0,0) and (1/n, 0) is of the order of 2 (because you need to get up the branches to link these two points) while for the topology they are very close).

One could have a class [ConvexRange I] for good model with corners, registering that the range is convex, but this would be one more typeclass that the user would need to type. Since it is satisfied in all standard examples, it seems simpler to me to include it directly in the definition of model with corners. It is a little painful to state, but the good news is that this will only show up when defining model with corners, not when using them. Hopefully we already have all the standard examples of models with corners in mathlib, so I expect users will never have to deal with this weird definition with case distinction -- they will only use the API saying that the range is convex, if their field happens to be R or C.

It's a little bit like minSmoothness , defined using a case disjunction and making it possible to talk about a C^3 Lie group over R or C, and an analytic Lie group over other fields. Once the API is in place, users never need to unfold the definition.

[Michael Rothgang]

Personally: I don't really care which decision we pick --- but this thread has been drawing out for long enough.
I'd be very interested in a quick resolution here: I'm visiting Patrick right now (for a month), and working on Riemannian manifolds would be a very nice topic. But this is only possible if such blockers get resolved in some way.

[Sébastien Gouëzel]

I think we should absolutely keep p-adic manifolds, not for p-adic manifolds by themselves, but for p-adic Lie groups which are definitely a thing.

[Michael Rothgang]

If there is a need for discussion, I can accomodate this. But I would rather prefer not stalling this for "no good reason".

[Sébastien Gouëzel]

Michael Rothgang said:

If I understand correctly, Heather was nervous of using typeclass synthesis for the definition of models with corners.

typeclass synthesis is not used when defining models with corners with the convexity condition: it's of the form "if some prop holds then foo else bar" (and it's again a prop), so there is no data involved, and no typeclass synthesis involved.

[Michael Rothgang]

@Heather Macbeth Do you mind weighing in here? At this point, I'd rather not debug my faulty memory what you said, but let you speak directly.

[Filippo A. E. Nuccio]

Sébastien Gouëzel said:

I think we should absolutely keep p-adic manifolds, not for p-adic manifolds by themselves, but for p-adic Lie groups which are definitely a thing.

They certainly are a thing, but they are basically only the $p$-adic points of the corresponding algebraic group with the induced topology from $\mathbb{Q}_p^n$ (unlike true $p$-adic manifolds) so I don't know if it is worth it to be bothered by them.

[Jeremy Ravenel]

In the proof of the cobordism hypothesis, boundaries of manifolds with cirners are considered. Sorry if it interrupts some.

But it could he good to take a glance because of how ordinary cobordism and bordism theory do not cover the patterns that the theory there does.

[Michael Rothgang]

Thanks for trying to help. I'm not quite sure, though - can you clarify how what you're saying relates to this thread? My reading is that everybody agrees that having manifolds with corners is good, and that talking about the boundary of a manifold with corners (as a manifold with boundary) is useful.
Do you want to say "this particular reference has an interesting use of manifolds with corners"?

[Sébastien Gouëzel]

For p-adic Lie groups, the point is you want to talk about their Lie algebra, and relate properties of the Lie algebra to the Lie group. This should be done in a single framework, not separately over $\R$, $\mathbb{C}$ and $\mathbb{Q}_p$.

[Kevin Buzzard]

But is there a single example in the p-adic setting when you're not using algebraic groups? In algebraic geometry if G is a group variety over an arbitrary field k then the k-points G(k) are a group, the identity element corresponds via the usual algebraic geometry yoga to a maximal ideal $m$ of a $k$-algebra $A$ and then you can define the Lie algebra of G to be the dual of $m/m^2.$ If furthermore $k$ has a topology then $G(k)$ inherits a topology and if $H$ is an open subgroup of $G(k)$ then you can just define the Lie algebra of $H$ to be the dual of $m/m^2$ as well. All functoriality for algebraic maps exists in the algebraic world and you don't need any of the manifold framework or any assumptions on $k$ at all. For example what I've said above all works for a power series field $F((t))$ over a finite field $F$.

I am quite conflicted by this. I've seen the claim that "Serre once used $p$-adic Lie groups" but I don't know the details. I've had to deal a lot with $p$-adic geometry in my work and I've always used totally different foundations to those of the manifold library (adic spaces etc). We don't want to design $\mathbb{Q}_p$ out of the manifold system if someone can actually point to a place where it would be useful but if it's causing more problems than it's solving then I would not personally care at all if it went. I definitely want the open mapping theorem for $p$-adic Banach spaces and a $p$-adic logarithm but I'm not at all clear yet on whether I want $p$-adic manifolds with the classical definition.

[Filippo A. E. Nuccio]

I have also been using the Lie group / Lie algebra yoga when the former were showing up as Galois groups of big non abelian extensions, but the algebraic approach was enough. I agree with @Sébastien Gouëzel that things should be done uniformly whenever possible but if that makes life too hard for serious differential geometry, it might not be worth the effort.

[Jeremy Ravenel]

I think the difference with ordinary cobordism (just boundaries) and manifolds with corners as it arises in the tangle hypothesis (which later got renamed) arises in situations where one considers boundaries between boundaries, boundaries between those, etc. (edit: Inrealized this could be kind of unclear, since I meant bordisms!)

I mentioned it since it was suggested to build in a condition as to when the boundary is itself one of a number oc things, such as a manifold or manifold with corners.

Possibly that (edit: what it "cobords") is not possible without extra information about the manifold, such as is already the case with a cobordism, that it consists of a designated two manifolds even though one could consider an empty one along with the disjoint union of the others. So, more would be built on top of it to get bordisms.

[Sébastien Gouëzel]

Filippo A. E. Nuccio said:

if that makes life too hard for serious differential geometry, it might not be worth the effort.

It doesn't make life hard, as far as I can tell.

[Floris van Doorn]

I'm happy with #25824. I think that approach is almost perfect.

There is a small risk in that it might exclude some (complex) manifolds with boundaries, but it is not clear if it actually does (or whether the separate design decision of having the model being independent of the point in the manifold already excludes some of these). If we later decide that this is actually a problem, we can then decide to refactor and put the convexity in a separate mixin class on the model with corners.

[pro-Lie stabilizer]

I would say the existence of an atlas of corners (with partitions of unity) by which one can demonstrate Stoke's theorem using the case for corners is important.

[pro-Lie stabilizer]

P.S. Consider an effective epimorphism f : X → Y such that prop₁(X) and such that the maps out of the pullback π₁, π₂ : pullback (f, f) → X have special property prop₂(π₁, dom(π₁), cod(π₁)), prop₂(π₂, dom(π₂), cod(π₂)), in addition to being effective epimorphisms satisfying prop₁(X). (surjective local homeomorphisms are particular effective epimorphisms locally compact spaces).

e.g.

prop₁(X) of "X is a corner", and prop₂(πᵢ,dom(πᵢ), cod(πᵢ)) of "πᵢ is a local diffeomorphism between open subsets of corners".

It's typical not to count disjoint unions (it's either the regular or strict ones that don't lose generality), so this is actually consistent with the approach here:

e.g.
prop₁(X) is the convexity assumption used here, which seems to imply connected, and prop₂(πᵢ,dom(πᵢ), cod(πᵢ)) varies subsequently.

[pro-Lie stabilizer]

Sorry, I wasn't following closely enough I think.

[Michael Rothgang]

Status update: This question is slowly but surely becoming the bottleneck for landing Sébastien's work on Riemannian manifolds, which is on the path towards upstreaming Patrick's and mine. If there's no further comment (from Heather or anybody else) by Sunday, I suggest we merge #25824. If follow-up discussions yield a better alternative, we can always switch to that, going forward.

[Patrick Massot]

I think we can even go ahead earlier than Sunday.

[Michael Rothgang]

Sure, let me add this clause: if all other PRs are reviewed and merged before, than we should also go ahead.

[Antoine Chambert-Loir]

Kevin Buzzard said:

I am quite conflicted by this. I've seen the claim that "Serre once used $p$-adic Lie groups" but I don't know the details. I've had to deal a lot with $p$-adic geometry in my work and I've always used totally different foundations to those of the manifold library (adic spaces etc). We don't want to design $\mathbb{Q}_p$ out of the manifold system if someone can actually point to a place where it would be useful but if it's causing more problems than it's solving then I would not personally care at all if it went. I definitely want the open mapping theorem for $p$-adic Banach spaces and a $p$-adic logarithm but I'm not at all clear yet on whether I want $p$-adic manifolds with the classical definition.

Well, Bourbaki's Lie groups requires $p$-adic manifolds, and in fact, manifolds over any field which is complete for a nontrivial ultrametric absolute value. In characteristic $p$, this is used to state the correct version of the correspondence between Lie algebras and a local version of Lie subgroups (“groupuscules”). They are not at all extremely terrible objects and it would be a pity that they disappear from mathlib.

[Antoine Chambert-Loir]

On the other hand, I don't know of any objects with corners in this setting.

[Michael Rothgang]

Rest assured: p-adic manifolds will stay in mathlib; this thread has convinced me thoroughly.

[Michael Rothgang]

p-adic manifolds never have boundary: somebody explained that on zulip, a while ago.

[Michael Rothgang]

This thread seems to have converged. Assuming there is no further discussion until tomorrow morning, I think we should get this merged. Since both Sébastien and I authored significant parts of the code, and we discussed this a lot --- would you like to do the honours, @Floris van Doorn?

[CylindricalTransportInvariantExistence&UniquenessofPreimagesforHomotopynFunctorsofaWeakEquivalence]

@Michael Rothgang @Antoine Chambert-Loir @Floris van Doorn @Kevin Buzzard

Yesterday I left a comment questioning how this was said to converge. I'm leaving this comment here publicly since it is apparent that the objection I made to that has been deleted.

[CylindricalTransportInvariantExistence&UniquenessofPreimagesforHomotopynFunctorsofaWeakEquivalence]

In that post, I asked whether a complex model with curved corners is a real model with ordinary corners when regarded as a real model.

[Mr Proof]

So basically any theorem that people made in Lean which was proved is "not true for all Complex Manifolds" is now not correct because the definition was too general and could have had something being a complex manifold without also being a real manifold? :scream:

This reinforces my stance that only proofs whose propositions can be stated in simple terms can be trusted to be what they pretend to be(e.g. FLT). All other propositions fall into the category of "useful" but may not prove what you think they prove on the surface. :thinking:

[Patrick Massot]

No, we wouldn’t have taken such a non-sensical result in Mathlib. That’s part of the maintainer team job.

[CylindricalTransportInvariantExistence&UniquenessofPreimagesforHomotopynFunctorsofaWeakEquivalence]

According to what you have said, there must be a complex model with curved corners which, when regarded as a smooth real model, is not a real model with ordinary real corners.

[CylindricalTransportInvariantExistence&UniquenessofPreimagesforHomotopynFunctorsofaWeakEquivalence]

I suggest you first accept some kind of result about smooth real coordinate changes on analytic real charts combined with the implicit function theorem and straightening for transversely intersecting submanifolds, later proceeding with an example about curved complex cornered manifolds which do not induce smooth real manifolds with ordinary real corners.

[Kevin Buzzard]

Please stop posting AI-generated rubbish or you will be banned; it is against the rules of the site. Please take this as your last warning. If you think there is a problem with manifolds with corners, it's your job to post an explicit problem, not just keep on posting nonsense and asking other people to do something.

[CylindricalTransportInvariantExistence&UniquenessofPreimagesforHomotopynFunctorsofaWeakEquivalence]

Screenshot 2025-09-08 at 9.57.59 AM.png

[Kevin Buzzard]

I'm well aware that previous nonsense you posted was deleted.

[CylindricalTransportInvariantExistence&UniquenessofPreimagesforHomotopynFunctorsofaWeakEquivalence]

(1553) #mathlib4 > Fixing the definition of models with corners - Lean - Zulip.pdf

[Michael Rothgang]

To be fair, the hint of such an issue is contained in the backscroll here:

• requiring the range of a model with corners to be convex excludes certain complex manifolds with corners. Unless, perhaps they also admit such a presentation. It is not obvious to me which ones, if any, do --- let alone if all manifolds do.)
• At the same time, it was not obvious to anybody in the thread what a good definition of complex manifolds with corners and boundaries is. (I am not a complex geometer, and neither are Floris van Doorn or Sébastien Gouezel.) The previous definition was also wrong; that was the impetus of this entire thread. (A definition in terms of Euclidean quadrants is an option, but also has its downsides.)
• If needed, the convexity requirement can be dropped.

Ultimately, the decision was to change the definition as proposed here --- and revisit this when the need arises (and somebody who is actually well familiar with complex manifolds with boundary has time to engage here). This was a conscious decision.

[Michael Rothgang]

To summarise: the current definition is not perfect (but better than the previous version), everybody knew this, and this was a conscious decision

[Michael Rothgang]

I do not expect you to read all of zulip. But looking at this previous thread is a reasonable bar (and if you haven't, please say so clearly and be prepared to retract your message). Much of what you said has been discussed previously. Also: you're proposing a sweeping change, hence should convince us why this is useful. Not the other way around.

[K768]

Just tuning in here. @Michael Rothgang @Kevin Buzzard @Patrick Massot I don't wish to make things more difficult or to suggest it has to be perfect, but it seems like the atlas used in John Lee's answer is consistent with the following lemma:

Let $f$ be a $C^{k}$ submersion from $\mathbb{R}^{\text{n}}$ to $\mathbb{R}$. Then $\{ x \in \mathbb{R}^{n} // f(x) \leq 0 \}$ is a smooth real manifold with corners.

The surprise-factor is that it's a real manifold with boundary, so the corner is of the form $[0,\infty) \times \mathbb{R}^{dimension- 1}$.

[Mr Proof]

[I decided to delete this message but I couldn't find the delete button :sob:]

[K768]

I am surprised and have not seen this kind of indifference towards a question before. I think it's safe to conclude with respect to John Lee's example that real manifolds with corners, later referred to as "a definition in terms of Euclidian quadrants" (is that the same thing or not?) but after reading a code heavy thread with no examples and an awful lot of entitlement I am really surprised at how unclear this is, especially in terms of presentation.

[K768]

...that complex manifolds with curved corners are, when regarded as a real manifold, a smooth real manifold with corners, but it was suggested that this is a sweeping change... wouldn't it be more reasonable to have first solved this mathematical problem and only then decided to encode it?

[K768]

... and the same for complex manifolds with boundary of the kind that Lee defines in that post.

[Patrick Massot]

Indifference towards which question? There is no problem at all working with complex manifolds having a real boundary in current mathlib, and no plan to change that.

[Patrick Massot]

And don’t know what “Lee defines in that post” refers to. Which post are you talking about?

[Michael Rothgang]

I don't understand what question you're asking here. Presuming this lemma is true (I haven't thought about it much yet), what would we use it for?

[Michael Rothgang]

(There are lots of potentially useful lemmas missing from mathlib, but we all only have so much time. I wouldn't mind a PR adding it. I don't see yet if this is just a single lemma or fits into some broader context.)

[Michael Rothgang]

Zaytsev Vasil Innokentievich said:

wouldn't it be more reasonable to have first solved this mathematical problem and only then decided to encode it?

In the abstract, I would agree with you here. I'm not convinced this applies here, though:

There was a mathematical problem solved: what is the right abstraction of manifolds to cover finite and infinite-dimensional manifolds, potentially with boundary and corners, over the reals, complexes or p-adics? (That question is not fully answered in the literature, AFAICT. And I did search.) The definition prior to this thread was approximating the answer, the current definition is a better approximation (and enables progress). Deciding "we have to solve this other mathematical problem first before we can make any progress" would have been worse.

I do want to find the perfect definition, everybody here does. But there is a trade-off of "get things perfect" and "get things done".

[Michael Rothgang]

(That trade-off comes up a lot in software engineering. Here's a blog post I like which discusses it.)

[Patrick Massot]

Maybe we need to be clearer: as far as we know, the definition currently in Mathlib covers all cases that appear in the real world. It is already much more general that what you would find in any standard graduate level differential geometry textbook.

[CylindricalTransportInvariantExistence&UniquenessofPreimagesforHomotopynFunctorsofaWeakEquivalence]

How about, simply, the new option:
Screenshot 2025-09-09 at 2.47.56 PM.png

[CylindricalTransportInvariantExistence&UniquenessofPreimagesforHomotopynFunctorsofaWeakEquivalence]

This seems like a great idea, so sorry I didn't appreciate it at first. I must have been worrying that there is some kind of "inherently complex" corner.

[Michael Rothgang]

Well, that was discussed in the thread above: If I recall correctly,

• it's not clear what generality it would enable
• at the same time, it runs the risk of making proofs less conceptual (by relying on a specific model with quadrants, as opposed to some properties of its range

Why would you prefer making this change? (Bear in mind that change has a cost --- it is possible, but it needs to have a good reason.)

[CylindricalTransportInvariantExistence&UniquenessofPreimagesforHomotopynFunctorsofaWeakEquivalence]

I think two reasons are:

Firstly, Stoke's theorem for a corner is very simple, and so is Stoke's theorem for a cube. The prospects for making an API for calculus are interesting, but for one thing the boundary needs to be one on which one can make sense of the integral of a differential form dω.

Secondly, in cobordism one can consider the product of manifolds as having a boundary. This was remarked earlier in the thread and I definitely agree with it.

[Sébastien Gouëzel]

All this is perfectly fine with the current definition we have in mathlib. It is even designed for these applications.

[Michael Rothgang]

#23138 defines bordism groups, and things work out fine. (That branch has not been updated to current mathlib, because it is still blocked on other work, but I'm pretty confident things will work.)