split AlgebraicGeometry

Stream: mathlib4

[Heather Macbeth]

I propose to split the AlgebraicGeometry folder into two parts, one about (locally) ringed spaces and one about Spec, Proj, schemes, etc. I argue that this will make the structure clearer (especially for casual users and for people doing refactors), and it will also reduce the apparent oddity when we start to import locally ringed spaces into Manifold if the locally ringed spaces are not nominally in a folder marked AlgebraicGeometry.

I tried the split at https://github.com/leanprover-community/mathlib4/tree/reorg-sheafed-space but wanted to get a quorum before opening a PR. For now I called the new folder Geometry/RingedSpace, but I am open to changing this (e.g. it could alternatively live in Topology/Sheaves).

[Heather Macbeth]

@Riccardo Brasca @Kevin Buzzard @Johan Commelin @Junyan Xu @Andrew Yang

[Riccardo Brasca]

I agree. We can move the folder about locally ringed space outside algebraic geometry.

[Kevin Buzzard]

We should develop the theory of complex analytic spaces at some point and they are ringed spaces.

[Junyan Xu]

Antoine Chambert-Loir said:

Kevin Buzzard said:

I think another nice (and even harder) project would be to put a complex manifold structure on the complex points of a smooth scheme of finite type over the complexes.

Well, while you wish to push in this direction, do it over any complete normed field. And that could be a good test of what has to be known about smooth schemes.

Yeah I think the reorg is good. I've been thinking that analytic spaces should be an intermediate step between Scheme and ChartedSpace after I saw your recent proposal above. (Aren't there some students working on GAGA?) I guess the perfectoid stuff also belong to analytic geometry rather than algebraic. Should we have folders Geometry/Algebraic and Geometry/Analytic rather than AlgebraicGeometry and AnalyticGeometry?

[Heather Macbeth]

OK, the PR for the split is #7330.

[Heather Macbeth]

Junyan Xu said:

Should we have folders Geometry/Algebraic and Geometry/Analytic rather than AlgebraicGeometry and AnalyticGeometry?

I don't think we need to go this far -- too much nesting makes it hard to reach things. (I would actually like to move Geometry.Manifold up to the top level as DifferentialGeometry before it gets too much bigger. But this can wait until we have a few things which are unequivocally "geometry" rather than just smooth manifold theory.)

[Riccardo Brasca]

Not sure I will have time to have a look during the weekend, but I will try.

[Antoine Chambert-Loir]

I do agree, ringed spaces are prevalent in geometry, and are not (should not!) be confined to algebraic geometry.

[Heather Macbeth]

As of #7423 we will have some non-algebro-geometric locally ringed spaces ;-)

[Kevin Buzzard]

So when is this coming?

[Heather Macbeth]

This being mathlib, I suppose we should actually work with Banach analytic spaces.

[Heather Macbeth]

Anyway, it should definitely be done, but this would be a different project from developing the sheaf theory of our existing manifold definition.

[Kevin Buzzard]

Heather Macbeth said:

This being mathlib, I suppose we should actually work with Banach analytic spaces.

Screenshot-from-2023-09-29-08-37-35.png

:laughing:

But yeah, touch\'e, I'd never heard of these infinite-dimensional versions before.

[Johan Commelin]

I really think that we should just go for (liquid) analytic spaces.