Smooth varieties are smooth manifolds

Stream: new members

[Nicolò Cavalleri]

I've been away from Lean for a while but I am coming back now and besides working on my previous PRs I have a self contained project I would like to work on. The background is that, as part of my PhD, I need to do a computer science project and the two friends I am doing it with are very keen on trying Lean. One of the two is into algebraic geometry and the other into differential geometry, so I thought that formalizing the statement in the title could be a feasible cool project that interests everybody (by smooth variety I mean integral separated schemes of finite typer over a normed field).

My strategy would be to first proving it for affine varieties by using polynomials and the implicit function theorem and then extend the result to schemes by giving them a second topology through the "affine charts" for which the results follows from definitions. Does anybody have any specific suggestion / can foresee any big problem relating missing results in Mathlib that I am not seing now? @Heather Macbeth, since you implemented spheres I guess you might have something to say on this?

[Heather Macbeth]

@Nicolò Cavalleri Honestly, I'd try a smaller project first ... maybe projective space, or the Grassmannian (in either case as a quotient).

[Heather Macbeth]

Also, it'd be great to have smooth vector bundles ... you were working on this at some point, right?

[Heather Macbeth]

For defining submanifolds, maybe a first step would be to define the groupoid of smooth functions preserving a fixed linear subspace of the model space.

[Heather Macbeth]

Or from the algebraic side, I think there is a lot of algebraic geometry to be done before we can say "integral separated schemes of finite typer over a normed field" :)

[Nicolò Cavalleri]

Heather Macbeth said:

Also, it'd be great to have smooth vector bundles ... you were working on this at some point, right?

Yes I actually have a lot of stuff locally on my computer that I never PRed because I was waiting to merge the PRs on topological vector bundles! But in any case I don't think I can involve them in this!

[Nicolò Cavalleri]

Heather Macbeth said:

Nicolò Cavalleri Honestly, I'd try a smaller project first ... maybe projective space, or the Grassmannian (in either case as a quotient).

@Heather Macbeth How about the regular value theorem? I guess that could be a first step for the original project anyways

[Nicolò Cavalleri]

But without the submanifold part, just to prove that the preimage of a regular value is a manifold

[Kyle Miller]

Heather Macbeth said:

or the Grassmannian (in either case as a quotient).

I assume you mean where you take the quotient of GL(V) by the stabilizer of a subspace? Or maybe the quotient of $n\times k$ matrices of rank $k$ by the GL(k) action?

One thing I think would be nice (maybe not as the definition, but at least to show it's possible in Lean) would be to give the Grassmannian of $k$-dimensional subspaces its smooth topology in a way that doesn't depend on having to choose a subspace or a basis. Until recently, I thought you needed to choose an inner product for graph charts, but the following works (with a caveat): you can create a (non-maximal) atlas indexed by short exact sequences $1 \to U \to V \to W \to 1$ that come with a section $s:W\to V$, where $U$ is a $k$-dimensional subspace of $V$. Given $s$, you can define an injective map $\hom(U, W) \to \mathrm{Gr}_k(V)$ by $f\mapsto \{u+sfu\mid u\in U\}$.

The caveat is that we need to identify $\hom(U, W)$ with Euclidean space for all the charts to use the same model, so what also goes into indexing the charts would be a linear isomorphism $\hom(U,W)\to \mathbb{R}^{k(\dim V-k)}$ in addition to the short exact sequence and the section.

[Heather Macbeth]

Kyle Miller said:

Heather Macbeth said:

or the Grassmannian (in either case as a quotient).

Or maybe the quotient of $n\times k$ matrices of rank $k$ by the GL(k) action?

I was thinking this, but your way is nicer!

[Heather Macbeth]

Nicolò Cavalleri said:

Heather Macbeth How about the regular value theorem? I guess that could be a first step for the original project anyways

But without the submanifold part, just to prove that the preimage of a regular value is a manifold

That seems reasonable to me, but I'd check with @Sebastien Gouezel and @Patrick Massot too.

[Heather Macbeth]

@Kyle Miller I think another thing you can do for the Grassmannian is to define it as the quotient of $\{\text{rank-}k\text{ endomorphisms of }V\}$ by the conjugation action of $GL(V)$ edit : I don't think I mean that, the quotient by something else :).

[Heather Macbeth]

... maybe just the quotient by the left-multiplication action, since that ought to preserve the kernel.

[Nicolò Cavalleri]

Heather Macbeth said:

Nicolò Cavalleri said:

Heather Macbeth How about the regular value theorem? I guess that could be a first step for the original project anyways

But without the submanifold part, just to prove that the preimage of a regular value is a manifold

That seems reasonable to me, but I'd check with Sebastien Gouezel and Patrick Massot too.

For some reason I was convinced you wanted to work on this before... Am I getting confused? If not what stopped you if anything did?

[Heather Macbeth]

I started trying to define pullbacks of groupoids, morphisms of groupoids, etc, and got really confused :)
https://github.com/leanprover-community/mathlib/compare/submanifolds-1

[Heather Macbeth]

I would like to return to it at some point, or see someone else do it, but I think it needs a very clear head.

[Nicolò Cavalleri]

But this is for the submanifolds part right? If one only cares about the manifold structure things are much easier I guess

[Patrick Massot]

I think it's very important to prove that the preimage of a regular value is a manifold. We can't really claim we have a differential geometry library without this result. But it would be even nicer to do it more generally for the preimage of a submanifold under a map which is transverse to the submanifold.

[Patrick Massot]

If you want to state this more general version then you'll need submanifolds anyway.

[Patrick Massot]

The case of preimages of a point is easier only because by accident it's easier to prove that a point is a submanifold...

[Kevin Buzzard]

@Nicolò Cavalleri ?? You're on the LSGNT now?? Come to Xena on Thursdays at Imperial! Did you meet Amelia and Jujian? They're in your cohort and both Lean experts!

[Kevin Buzzard]

Jujian is working on GAGA for his thesis.

[Heather Macbeth]

@Kevin Buzzard which part??

[Kevin Buzzard]

I am in charge of admissions so I should have known you were in London, but I was on sabbatical last year and played no part in the admissions process. I've only just noticed you're on the list of newcomers!

[Kevin Buzzard]

@Heather Macbeth right now Jujian is defining projective varieties and learning the material. I don't know whether it's ridiculously optimistic to do GAGA but I thought we could give it a try, we have 4 years.

[Heather Macbeth]

Back to submanifolds: I'd like to know that a regular level set, equipped with the smooth manifold structure Nicolo is talking about, has inclusion function which is an immersion and a topological embedding. And in the other direction, to know that a topological embedding which is a smooth immersion has image which is locally the level set of of some submersion.

[Kevin Buzzard]

Nico who are the others interested in Lean who you mentioned above? Mel, Amelia, David, Sebastian and Jujian are all doing Lean mini-projects with me this year.

[Kevin Buzzard]

Back to submanifolds: do we have the implicit function theorem?

[Heather Macbeth]

Yup, thanks to Yury 18 months ago.

[Kevin Buzzard]

So is the submanifold thing a whole lot more difficult?

[Heather Macbeth]

(Back to GAGA: maybe Chow's theorem, that an analytic subvariety of $\mathbb{CP}^n$ is an algebraic subvariety? This doesn't require too much sheaf-y machinery.)

[Kevin Buzzard]

Right now Jujian is tempted to start thinking about cohomology theories. I wonder if I should just PR group cohomology, I have it sitting on a branch. We still don't have any cohomology theories other than derived_functor (for which I still don't think we have the long exact sequence!). I thought that the proof of Chow's theorem involved showing that the analytic sheaf corresponding to the zero locus of the analytic subvariety was algebraic?

[Heather Macbeth]

Indeed, it seems I was thinking of an easier theorem (which I suppose is also a form of GAGA): the space of holomorphic sections of $\mathcal{O}(d)$ over $\mathbb{CP}^n$ is isomorphic to the space of degree-$d$ polynomials in $n+1$ variables.

[Kevin Buzzard]

Yeah I think this is the initial target. In the algebraic category I think it's pretty easy. In the analytic category it will be more of a challenge.

[Heather Macbeth]

I was really excited to see someone talking about Hartogs's theorem the other day, but it turned out to be the wrong Hartogs's theorem :)

[Kevin Buzzard]

Heh, I once had the same experience in a conversation with Nick Katz!

[Nicolò Cavalleri]

Kevin Buzzard said:

Nicolò Cavalleri ?? You're on the LSGNT now?? Come to Xena on Thursdays at Imperial! Did you meet Amelia and Jujian? They're in your cohort and both Lean experts!

Yes!! Amelia told me but I did not speak with Jujian about Lean yet! I think I crossed you at Imperial but you were in a rush and I did not want to stop you!

[Nicolò Cavalleri]

Kevin Buzzard said:

Nico who are the others interested in Lean who you mentioned above? Mel, Amelia, David, Sebastian and Jujian are all doing Lean mini-projects with me this year.

One is @Sebastian Monnet and the other is Michela who is not on this chat yet!

[Sebastian Monnet]

Yeah, seems like a great opportunity to learn some Lean in preparation for the project

[Heather Macbeth]

@Nicolò Cavalleri Another project would be to define complex (analytic) spaces and then prove that both schemes over $\mathbb{C}$ and complex manifolds are special cases.

[Kevin Buzzard]

This would be an excellent project. I guess the schemes over $\mathbb{C}$ would need some finiteness assumptions. @Jujian Zhang do you know Nico? He's on the LSGNT.

[Nicolò Cavalleri]

Is the preimage theorem even true for manifolds with corners? If yes I believe we have a problem with the current implementation of model with corners cause to do things naturally in the proof at some point you'd need to show that the intersection of a subspace with a model with corners is again a model with corners and this is not true with the current implementation. @Sebastien Gouezel

[Sebastien Gouezel]

Most naive statements are not true for manifolds with boundary. The basic example to keep in mind is the following. Consider the graph $M$ of the function $x \mapsto e^{-1/x^2} \sin (1/x)$. It is a smooth submanifold of $\R^2$. Now consider the inclusion $i$ of the upper half plane (with boundary) into $\R^2$. Then its differential is everywhere invertible, but still $i^{-1}(M)$ is extremely nasty around $0$ (it has infinitely many connected components, for instance).

[Nicolò Cavalleri]

Ok thanks although I believe this can be a counterexample for the preimage of a manifold. As for the preimage of a point I believe that if the regular value is not on the boundary then the theorem holds for manifolds with boundary. However I am not sure if this extends to corners: I expect it does but the proof I had in mind requires that the intersection of a subspace with a model with corners is still a model with corners and this is not true with the current implementation

[Nicolò Cavalleri]

Would you suggest just proving the theorem in the boundaryless case?

[Sebastien Gouezel]

Yes, I'd just state and prove this in the boundaryless case.

[Nicolò Cavalleri]

Ok this is what we partially did in the end but this project made wonder: what are the advantages of having model with corners so general? I propose imposing some constraint on them such that they are closed under the operation of restricting them to a subspace, so that a theorem like this ones can be proved in such context. Something like adding a condition that 0 must be in the interior of the target?

[Nicolò Cavalleri]

Nicolò Cavalleri said:

Ok thanks although I believe this can be a counterexample for the preimage of a manifold. As for the preimage of a point I believe that if the regular value is not on the boundary then the theorem holds for manifolds with boundary. However I am not sure if this extends to corners: I expect it does but the proof I had in mind requires that the intersection of a subspace with a model with corners is still a model with corners and this is not true with the current implementation

By the way, this does extend to corners because apparently it is true for orbifolds...