Zulip Chat Archive

Stream: new members

Topic: the projective space

Hoang Le Truong (May 19 2019 at 08:02):

I'd like to work with the projective space. Can you help me understand how close or far we are from being able to represent the projective space in Lean

Kevin Buzzard (May 19 2019 at 08:02):

That very much depends on what you mean by projective space.

Kevin Buzzard (May 19 2019 at 08:03):

To various people this means: the set k^{n+1} - 0 / equivalence relation

Kevin Buzzard (May 19 2019 at 08:03):

some combinatorial structure involving points and lines

Kevin Buzzard (May 19 2019 at 08:03):

or a scheme

Kevin Buzzard (May 19 2019 at 08:03):

or a variety

Mario Carneiro (May 19 2019 at 08:04):

I want to second this request, I need mathematician help to untangle what projective space means

Hoang Le Truong (May 19 2019 at 08:04):

a projective space can be thought of as the set of lines through the origin of a vector space V

Kevin Buzzard (May 19 2019 at 08:05):

Well that's a 5th option yes ;-)

Kevin Buzzard (May 19 2019 at 08:05):

If you just want the set, then go ahead and make it as the quotient by an equivalence relation.

Mario Carneiro (May 19 2019 at 08:05):

the question isn't what is it but what do people want to do with it

Mario Carneiro (May 19 2019 at 08:06):

what are the ways it is used

Kevin Buzzard (May 19 2019 at 08:06):

Different mathematicians want to do different things with their different (and sometimes incompatible) notions of a projective space

Kevin Buzzard (May 19 2019 at 08:06):

Some computer people want to prove that there is no projective plane of size 14 or whatever (or whatever number they're up to)

Kevin Buzzard (May 19 2019 at 08:06):

other people think this is a trivial consequence of the fact that there's no solution to q^2+q+1=14

Kevin Buzzard (May 19 2019 at 08:07):

Algebraic geometers want to show that the main theorem of elimination theory is equivalent to the statement that projective morphisms are proper

Kevin Buzzard (May 19 2019 at 08:08):

Elliptic curve over finite fields people want to define group laws on subsets of some version of projective space using cubic equations

Kevin Buzzard (May 19 2019 at 08:08):

but other people think that projective space over a finite field is infinite

Kevin Buzzard (May 19 2019 at 08:08):

because they're counting homogeneous prime ideals of some graded ring

Kevin Buzzard (May 19 2019 at 08:09):

"projective space" is a fabulous example of notation overloading in mathematics.

Mario Carneiro (May 19 2019 at 08:09):

oof

Kevin Buzzard (May 19 2019 at 08:09):

Even geometers have different ideas about projective space.

Kevin Buzzard (May 19 2019 at 08:09):

In my corridor alone there is more than one opinion on what the topology on $\mathbb{P}^1(\mathbb{C})$ is.

Hoang Le Truong (May 19 2019 at 08:10):

I need with the projective space in algebraic geometry and analytic variety

Kevin Buzzard (May 19 2019 at 08:10):

The complex geometers would give it the complex analytic topology, the algebraic geometers the Zariski topology.

Kevin Buzzard (May 19 2019 at 08:10):

Well first you need to give us a definition of what a complex variety is.

Kevin Buzzard (May 19 2019 at 08:11):

because there are three categories in mathematics which contain things called "complex variety"

Kevin Buzzard (May 19 2019 at 08:11):

There is the category of complex manifolds

Kevin Buzzard (May 19 2019 at 08:11):

the category of algebraic varieties over the complexes

Kevin Buzzard (May 19 2019 at 08:11):

and the category of schemes

Mario Carneiro (May 19 2019 at 08:11):

Would the Zariski topology be a reasonable near term project?

Mario Carneiro (May 19 2019 at 08:12):

I think we have everything we need for defining a variety

Kevin Buzzard (May 19 2019 at 08:12):

Even then you have to decide whether you are using maximal ideals or prime ideals.

Kevin Buzzard (May 19 2019 at 08:12):

There is a functor from (what people used to mean by variety pre Grothendieck) to (what people mean by variety post Grothendieck)

Kevin Buzzard (May 19 2019 at 08:12):

and one the other way too

Kevin Buzzard (May 19 2019 at 08:12):

and it changes the underlying topological space

Mario Carneiro (May 19 2019 at 08:13):

oh dear

Kevin Buzzard (May 19 2019 at 08:13):

This is a serious issue for formalisers.

Mario Carneiro (May 19 2019 at 08:13):

I don't even know which one I mean

Kevin Buzzard (May 19 2019 at 08:13):

Even post Grothendieck many many people still use the pre Grothendieck notion.

Hoang Le Truong (May 19 2019 at 08:13):

There is the category of complex manifolds and the category of algebraic varieties over the complexes. It is connect both

Kevin Buzzard (May 19 2019 at 08:13):

What do you mean by an algebraic variety? There are two definitions in the literature, both in common usage.

Kevin Buzzard (May 19 2019 at 08:14):

Let me spell out the problem, even for affine 1-space over the complexes.

Kevin Buzzard (May 19 2019 at 08:14):

Classically, complex geometers thought that affine 1-space over the complex numbers was the set $\mathbb{C}$ equipped with the usual topology on the complex numbers.

Kevin Buzzard (May 19 2019 at 08:14):

Then algebraic geometers came along and wanted to work with affine 1-space over any algebraically closed field

Kevin Buzzard (May 19 2019 at 08:15):

because they wanted to do number theory using geometry so they needed to be able to work in characteristic $p$

Kevin Buzzard (May 19 2019 at 08:15):

So they had to reject the usual topology on the complexes

Kevin Buzzard (May 19 2019 at 08:15):

so they went with the Zariski topology,

Kevin Buzzard (May 19 2019 at 08:16):

so now we have affine 1-space over any algebraically closed field $k$ , and the underlying set is $k$ and the topology is the one where the closed sets are just $k$ and the finite subsets

Kevin Buzzard (May 19 2019 at 08:16):

and by the Nullstellensatz this is just the maximal ideals of the polynomial ring $k[x]$

Kevin Buzzard (May 19 2019 at 08:16):

and then in the 1960s people got more ambitious and wanted affine 1-space over any field, and indeed any commutative ring

Kevin Buzzard (May 19 2019 at 08:17):

but "maximal ideal" isn't functorial; if $R\to S$ is a map of rings then the pre-image of a maximal ideal of $S$ might not be a maximal ideal of $R$ .

Kevin Buzzard (May 19 2019 at 08:17):

However, "prime ideal" is functorial, even in this generality

Kevin Buzzard (May 19 2019 at 08:18):

so affine 1-space was redefined as the set of prime ideals of $k[x]$

Kevin Buzzard (May 19 2019 at 08:18):

and that's what an arithmetic geometer like me thinks that affine 1-space is nowadays

Kevin Buzzard (May 19 2019 at 08:18):

but even if $k$ is the complex numbers, that set is not $\mathbb{C}$ any more

Kevin Buzzard (May 19 2019 at 08:19):

because we have added an extra "generic point" corresponding to the non-maximal prime ideal $(0)$

Kevin Buzzard (May 19 2019 at 08:19):

This point is essential for people like me

Kevin Buzzard (May 19 2019 at 08:19):

but the complex geometers don't need it, because in the only situations they care about, the maximal ideals of their rings "determine the ring" in a sense that can be made precise.

Kevin Buzzard (May 19 2019 at 08:20):

So even for a ring finitely generated over the complexes, like $\mathbb{C}[x]$

Kevin Buzzard (May 19 2019 at 08:20):

some people talk about "the associated variety" as being the set of maximal ideals, and others mean the set of prime ideals.

Kevin Buzzard (May 19 2019 at 08:21):

And there's an equivalence of categories between the two notions, which is just applied where necessary, without anyone even noticing

Kevin Buzzard (May 19 2019 at 08:21):

We developed a theory of schemes, so we have all the prime ideals.

Kevin Buzzard (May 19 2019 at 08:22):

But to develop a theory of varieties over an algebraically closed field one has to make a decision about whether to keep carrying around the non-maximal prime ideals or just to let them drop.

Kevin Buzzard (May 19 2019 at 08:22):

And of course the best answer depends on what you are actually doing.

Kevin Buzzard (May 19 2019 at 08:23):

So the answer to your original question @Hoang Le Truong is that as far as I know, we still haven't even decided what the definition of projective space in algebraic geometry is

Kevin Buzzard (May 19 2019 at 08:24):

However, it is perhaps not unreasonable to conjecture that if you think projective space is the set of lines in a vector space, then all you care about is maximal ideals.

Kevin Buzzard (May 19 2019 at 08:25):

So the answer is that the schemes repo in its current form is useless to you and we have nothing.

Kevin Buzzard (May 19 2019 at 08:25):

Coincidentally, in Jan-Mar 2020 I will be teaching an alg geom course at Imperial using the classical language of varieties, so I will no doubt try and formalise something by then.

Kevin Buzzard (May 19 2019 at 08:26):

Of course, there's nothing stopping you defining projective space as lines through the origin, and even giving it a topology coming from a topology on the underlying field.

Mario Carneiro (May 19 2019 at 08:27):

Oh right you have Spec already

Kevin Buzzard (May 19 2019 at 08:27):

But the moment you need the Nullstellensatz (NSS) someone will have to formalise some commutative algebra. From what I have seen this would be a very feasible and interesting project in Lean, and most definitely attainable. There are some very slick and short proofs of NSS nowadays.

Kevin Buzzard (May 19 2019 at 08:28):

We have Spec (not in mathlib though) but we don't have Proj.

Kevin Buzzard (May 19 2019 at 08:28):

Proj takes as input a graded ring and spits out a scheme.

Mario Carneiro (May 19 2019 at 08:28):

is Spec the same as the zariski topology?

Kevin Buzzard (May 19 2019 at 08:28):

Yes

Kevin Buzzard (May 19 2019 at 08:28):

and it's all the prime ideals.

Mario Carneiro (May 19 2019 at 08:29):

But you can do the same trick with maximal ideals, is that what you are saying?

Kevin Buzzard (May 19 2019 at 08:29):

So Spec of $\mathbb{C}[x]$ would be $\mathbb{C}$ union some other point

Kevin Buzzard (May 19 2019 at 08:29):

Some people call the set of maximal ideals $Max(R)$ or $Specm(R)$

Mario Carneiro (May 19 2019 at 08:30):

wow, so CS

Kevin Buzzard (May 19 2019 at 08:30):

and applying that to $\mathbb{C}[x]$ would spit out $\mathbb{C}$

Kevin Buzzard (May 19 2019 at 08:30):

But this is not a functor on the category of all commutative rings

Kevin Buzzard (May 19 2019 at 08:30):

you have to restrict to some full subcategory, for example rings finitely generated over the complex numbers

Kevin Buzzard (May 19 2019 at 08:31):

and then proving it's a functor involves some MSc level maths, the Nullstellensatz.

Kevin Buzzard (May 19 2019 at 08:32):

Because mathematicians mean three things by "projective $n$ -space over $\mathbb{C}$ " I suspect that ultimately this means that Lean needs three different definitions.

Kevin Buzzard (May 19 2019 at 08:32):

This will make notation an issue.

Mario Carneiro (May 19 2019 at 08:33):

the notation problem is solved by not having one

Kevin Buzzard (May 19 2019 at 08:33):

I guess!

Mario Carneiro (May 19 2019 at 08:33):

no notation => no notation problem

Hoang Le Truong (May 19 2019 at 08:34):

Yes, we need three different definitions. I see that now we do not have it. is it true?

Kevin Buzzard (May 19 2019 at 08:34):

Yes, we don't have any of the three things.

Kevin Buzzard (May 19 2019 at 08:34):

Before you start on projective space I think it's important to decide the scope of what you want.

Mario Carneiro (May 19 2019 at 08:35):

We have the lattice of submodules, which in this context is called the Grassmannian

Mario Carneiro (May 19 2019 at 08:35):

you can define the subset of one-dimensional submodules and that's projective space

Kevin Buzzard (May 19 2019 at 08:35):

The lattice of submodules of $k^2$ has two random extra points.

Mario Carneiro (May 19 2019 at 08:35):

but what structure are people expecting on it?

Kevin Buzzard (May 19 2019 at 08:36):

This is what @Hoang Le Truong needs to tell us

Mario Carneiro (May 19 2019 at 08:36):

a topology, I guess... anything else?

Mario Carneiro (May 19 2019 at 08:36):

(and the topology has at least two options, maybe three, based on what you said)

Kevin Buzzard (May 19 2019 at 08:36):

You can inherit a topology from a topology on the underlying field

Kevin Buzzard (May 19 2019 at 08:37):

or you can put the Zariski topology on the space, which works for all fields.

Kevin Buzzard (May 19 2019 at 08:37):

Those are the two options.

Kevin Buzzard (May 19 2019 at 08:37):

For non-algebraically closed fields the situation is even worse.

Kevin Buzzard (May 19 2019 at 08:38):

Topologists would define "projective 2-space over the reals" as the lines in $\mathbb{R}^3$ , equipped with a topology coming from the topology on the reals.

Kevin Buzzard (May 19 2019 at 08:39):

Algebraic geometers would consider maximal or prime ideals in some ring, so would see more points.

Mario Carneiro (May 19 2019 at 08:39):

you can also draw lines in projective space, by using planes in the vector space

Mario Carneiro (May 19 2019 at 08:39):

is that an operation?

Kevin Buzzard (May 19 2019 at 08:39):

You can draw curves in projective space by using homogeneous equations on the vector space.

Kevin Buzzard (May 19 2019 at 08:40):

I can draw the graph of $x^n+y^n=z^n$ in projective 2-space.

Kevin Buzzard (May 19 2019 at 08:40):

If $(x,y,z)\in k^3$ then I can consider $x^n+y^n-z^n$ .

Mario Carneiro (May 19 2019 at 08:40):

so we need homogeneous polynomials then

Kevin Buzzard (May 19 2019 at 08:41):

If I take two points $(x,y,z)$ and $(x', y', z')$ in the same line, then unfortunately this function is not constant -- it can take different values at those two points.

Kevin Buzzard (May 19 2019 at 08:41):

However, asking "is the value of this function zero" is constant on lines.

Kevin Buzzard (May 19 2019 at 08:41):

So one can still make sense of the subspace where $x^n+y^n-z^n=0$

Kevin Buzzard (May 19 2019 at 08:42):

This is because the equation is homogeneous.

Mario Carneiro (May 19 2019 at 08:42):

I guess rings are out at this point?

Mario Carneiro (May 19 2019 at 08:42):

since zero divisors would mess that up

Kevin Buzzard (May 19 2019 at 08:43):

It all works for rings, because in algebraic geometry projective n-space of a ring is not the lines in $R^{n+1}$ , it's some clever set of prime ideals.

Kevin Buzzard (May 19 2019 at 08:43):

So amazingly it can all be made to work.

Mario Carneiro (May 19 2019 at 08:43):

how bad would it be if that was the definition and we had some API for the lines through the origin approach?

Kevin Buzzard (May 19 2019 at 08:44):

Lines through the origin works fine for algebraically closed fields.

Hoang Le Truong (May 19 2019 at 08:44):

it is the set of homogeneous prime ideals

Kevin Buzzard (May 19 2019 at 08:44):

And it most definitely has its uses for some other fields, like the reals.

Kevin Buzzard (May 19 2019 at 08:44):

it is the set of homogeneous prime ideals

That is not what you said earlier.

Kevin Buzzard (May 19 2019 at 08:44):

You said lines through the origin of a vector space.

Hoang Le Truong (May 19 2019 at 08:45):

ah ok

Kevin Buzzard (May 19 2019 at 08:45):

When I was learning this stuff I found the literature extremely confusing.

Mario Carneiro (May 19 2019 at 08:45):

what about infinite dimensions? Is that just not done?

Kevin Buzzard (May 19 2019 at 08:45):

In abstract algebraic geometry you can do anything

Kevin Buzzard (May 19 2019 at 08:46):

but the moment you're in infinite dimensions you have even more questions about topology

Kevin Buzzard (May 19 2019 at 08:46):

$Spec(R)$ makes sense for any commutative ring at all, no finiteness conditions needed.

Kevin Buzzard (May 19 2019 at 08:47):

However mathematicians cannot actually work with general hugely infinite objects, they always need extra structure to make things manageable, like some topology or some countability assumption

Kevin Buzzard (May 19 2019 at 08:47):

or some other finiteness assumption like Noetherian or whatever

Mario Carneiro (May 19 2019 at 08:47):

My goal is to avoid restrictions that serve no purpose. I am always confused when mathematicians start their analysis on some very specific kind of thing like algebraically closed fields when they don't use the structure, but when I ask about generalization it usually seems like the mathematician has to context switch completely. I don't quite understand why math is done this way

Kevin Buzzard (May 19 2019 at 08:48):

Right. We saw this a long time ago when I insisted that taking the square root of a negative number made no sense.

Kevin Buzzard (May 19 2019 at 08:48):

The concept of "making no sense" is something that mathematicians and computer scientists interpret very differently.

Kevin Buzzard (May 19 2019 at 08:49):

For example, one can define affine 1-space over a general field $k$ just to be $k$ .

Kevin Buzzard (May 19 2019 at 08:49):

If $k$ is not algebraically closed, this is a really bad idea.

Kevin Buzzard (May 19 2019 at 08:49):

because it is not telling the correct story.

Kevin Buzzard (May 19 2019 at 08:49):

Affine 1-space over $k$ should be defined to be the set of prime ideals, or maximal ideals, of $k[x]$ .

Kevin Buzzard (May 19 2019 at 08:50):

But it makes perfect sense from a formalising point of view

Kevin Buzzard (May 19 2019 at 08:50):

and if you stick to algebraically closed fields when proving your theorems about affine space, nobody will notice that your definition is "wrong for mathematicians"

Kevin Buzzard (May 19 2019 at 08:51):

But the equation $x^2+y^2=-1$ is much simpler than the equation $x^{100}+y^{100}=-1$

Kevin Buzzard (May 19 2019 at 08:51):

even if you are considering this equation over the rationals

Kevin Buzzard (May 19 2019 at 08:51):

because sure, neither equation has solutions (squares are non-negative)

Kevin Buzzard (May 19 2019 at 08:52):

but both equations "have geometry"

Kevin Buzzard (May 19 2019 at 08:52):

e.g. you can consider the functor on $\mathbb{Q}$ -algebras sending $R$ to the set of solutions over $R$

Kevin Buzzard (May 19 2019 at 08:52):

and now the equations are behaving very differently.

Kevin Buzzard (May 19 2019 at 08:53):

Grothendieck observed that one can capture this by looking at $Spec(\mathbb{Q}[x,y]/(x^2+y^2+1))$ and $Spec(\mathbb{Q}[x,y]/(x^{100}+y^{100}+1)$

Kevin Buzzard (May 19 2019 at 08:53):

and noting that these schemes behave very differently.

Kevin Buzzard (May 19 2019 at 08:54):

But before Grothendieck, when we were more naive about these things, people associated the polynomial with its set of solutions.

Kevin Buzzard (May 19 2019 at 08:54):

This works great for irreducible polynomials over algebraically closed fields

Kevin Buzzard (May 19 2019 at 08:54):

and is a terrible idea in general.

Kevin Buzzard (May 19 2019 at 08:55):

But you see there are already so many interesting questions about irreducible polynomials over algebraically closed fields

Kevin Buzzard (May 19 2019 at 08:55):

for example the Hodge conjecture

Kevin Buzzard (May 19 2019 at 08:56):

that you now get two schools of thought -- people who just don't care about these subtleties regarding prime ideals or non-algebraically closed fields, because they just care about projective varieties over the complex numbers in the traditional sense

Kevin Buzzard (May 19 2019 at 08:56):

and people like me who use algebraic geometry in a completely different way because we care more about fields like the rational numbers where the traditional approach of identifying affine 1-space over $k$ with $k$ simply doesn't work.

Kevin Buzzard (May 19 2019 at 08:58):

For me, affine 1-space over $\mathbb{Q}$ is the set of prime ideals in $\mathbb{Q}[x]$ and this is a really complicated set.

Mario Carneiro (May 19 2019 at 09:00):

If there is evidence that one definition is "wrong" when generalized, then it seems best to avoid it in favor of one that generalizes

Kevin Buzzard (May 19 2019 at 09:00):

Summary then: before we leap into projective space I think we need to think about the ultimate goals of what we are trying to formalise. This would entail, for example: (a) deciding which base fields we're interested in, (b) whether or not we want generic points, (c) which topology we want on projective space.

Mario Carneiro (May 19 2019 at 09:02):

As was pointed out, we can have all the topologies, although there will probably be some battle for the default

Kevin Buzzard (May 19 2019 at 09:02):

The problem with "wrong" is that complex geometers do not need the generalizations which arithmetic geometers think about, because their base field is always the complexes with its usual topology. So they can forge ahead being blissfully ignorant of modern arithmetic geometry, and if occasionally they do need a result which uses Grothendieck style stuff then they just quickly apply the equivalence of categories, steal it, and get out again.

Mario Carneiro (May 19 2019 at 09:03):

sure, but we can support such use with the right API, if the definitions are equivalent in the arena where the complex geometer works

Hoang Le Truong (May 19 2019 at 09:09):

For me, (a) base fields is complex number (b) I want generic points, (c) usual topology from complex number. What will I begin?

Kevin Buzzard (May 19 2019 at 09:26):

I really need to get back to my marking so I should try and wind up here (there's no point me sitting in my office doing stuff I could be doing at home). But I think (b) and (c) are incompatible, aren't they? Let's consider projective 2-space over the complexes. Arithmetic geometers would have the Zariski topology, and a generic point for each curve such as $x^n+y^n=z^n$ . However if you want the usual topology, then you can now restrict to affine 2-space in projective 2-space, and now you have a whole bunch of closed sets like the graph of $x^n+y^n=1$ which have a generic point because they are defined by equations which happen to be polynomials. and also a whole bunch of closed sets like the graph of $y=e^x$ which have no generic point because they are truly analytic subspaces. So now one can do things like restrict to small open balls and get closed subsets with generic points such as the zeros of $y=\sum_{n=0}^Mx^n/n!$ whose limits as $M\to\infty$ are closed subsets with no generic point. Generic points are an algebro-geometric phenomenon which surely only work with algebro-geometric topologies such as the Zariski topology. Or am I wrong?

Kevin Buzzard (May 19 2019 at 09:33):

If you're interested in the Hodge conjecture then I guess one might want to keep in mind the fact that this was made in the 1930s, when the concept of a generic point was something completely different. For the Hodge conjecture I think the natural structure you want for projective $n$ -space is that of a complex manifold, so now I have to bow out and defer to the people currently working on manifolds. It seems to me that, just like in the schemes project, when the manifold project has finished with its definitions and needs examples, projective $n$ -space will be one of the first things it goes for. We have spectrum of a ring but I think we need projective $n$ -space in the arithmetic geometry sense (over any commutative ring, with Zariski topology) to prove that we got the right definition of scheme. Of course this does not stop you from defining the set and putting a topology on it, but there will be work involved with the topology. You will want to cover projective $n$ -space with $n+1$ copies of affine $n$ -space, identify affine $n$ -space with $\mathbb{C}^n$ with its usual product topology, and then you'll have to check that the topologies glue together. This would be the "correct" way to do it I guess. There might be cheap tricks which get you to the goal sooner. It all goes back to the question of why you want it. If you spend hours making it like this, it doesn't mean you'll be able to do the next thing you want from it.

Johan Commelin (May 19 2019 at 10:39):

Tangent: Didn't Grothendieck teach us that points of projective space are the 1-dimensional quotients of a vector space, instead of the lines in it?

Johan Commelin (May 19 2019 at 10:39):

So we also have to choose between the space and its dual.

Johan Commelin (May 19 2019 at 10:40):

And if we are trying to determine what we're interested in: I'm interested in projective schemes over number fields.

Kevin Buzzard (May 19 2019 at 17:39):

So you'll want the version which will ultimately end up in the schemes repo Johan

Last updated: Dec 20 2023 at 11:08 UTC