Level set is a manifold

Stream: Is there code for X?

[Andrew Yang]

Do we know that the level set of a smooth function at a non critical point is a manifold?
Specifically I want the zero set of a family of polynomials on $\mathbb{R}^n$ to be a manifold under some nonsingularity conditions.

[Johan Commelin]

I don't think so, but I would be happy to learn that we now have it.

[Winston Yin (尹維晨)]

I would be excited to see this formalised!

[Antoine Chambert-Loir]

It doesn't seem that we have submanifolds of $\mathbf R^n$ or, better, of manifolds…

[Michael Rothgang]

This would be the regular value theorem: I would like to see it formalised as well, but AFAICT it's still missing.

[Michael Rothgang]

(You'll also want to have Sard's theorem, that almost every point is a regular value. That is work in progress.)

[Andrew Yang]

At least we do have the implicit value theorem. Do we have the definition of regular value?

[Junyan Xu]

Apparently regularity is simply expressed as surjectivity of the derivative in the Sard's theorem repo.
(But regular value requires quantifying over the preimage; maybe the repo isn't the correct place to look for that.)

[Winston Yin (尹維晨)]

Submanifolds generally are a tricky business and the subject of some past discussion here. For now, it’s sufficient to show level sets are manifolds without needing submanifolds

[Andrew Yang]

I started a sketch file and also noticed that it is not straightforward at all to define submanifolds. But I don't know how specializing to level sets can solve this problem though.

[Winston Yin (尹維晨)]

I was just suggesting that you can define a manifold structure on the level set via the implicit function theorem, without the need for a notion of submanifolds

[Andrew Yang]

I see. But I don't even know what a good choice of a "model" for the manifold structure on the subset would be.

And because ChartedSpace contains a lot of redundant data (junk values outside of domain of definition, inverses to functions instead of proofs that they are bijective etc), to construct such an instance directly would be very choice-y and hard to work with, and I think it would probably be easier to manipulate the chart later on if one first prove the existence of some structure which contains all the sufficient data and use choice once. And then it occurred to me that this "some structure which contains all the sufficient data" is probably just submanifolds.

[Winston Yin (尹維晨)]

I agree that the current formalisation of manifolds involves a lot of annoying structures like partial functions with junk values, and I think the community would appreciate alternative attempts just to explore the design space. (What do other formalised diff geo libraries do?)

[Winston Yin (尹維晨)]

On the question of choosiness, I think the intention of ChartedSpace is that each local chart (and its inverse) is explicitly given and is in principle computable. Coming from physics, I'm imagining that you can actually do explicit coordinate transformations using these charts. If you're proving something general about the existence of charts, then indeed it should be your job to Classical.choice a partial inverse function to satisfy ChartedSpace, rather than demanding that ChartedSpace become less computable. But you're right, we should be able to define an intermediate notion of manifolds that is less computable but whose proof obligations are simpler.

[Winston Yin (尹維晨)]

(my 2¢)