definition of algebraic variety

Stream: maths

[Kevin Buzzard]

This is a mess. At some point we certainly need to be able to start talking about algebraic varieties. But we need a definition and ideally we need to ensure that nobody will come along later and say "aargh why did you put in that hypothesis?"

I've done a brief literature search and of course the results are "different people have different definitions". Right now I'm envisaging some full subcategory of Over (Spec k)) where k is a...field. Here are some questions.

1) Should k be assumed to be algebraically closed? (my opinion: no)
2) Should k even be assumed to be a field, would a commutative ring be OK? (my opinion: unsure; we didn't do this with elliptic curves, we went with comm rings plus a warning)

Now we want to list the properties of the morphism.
3) Separated? (surely)
4) Integral (my opinion: not sure: this is reduced + irreducible, and I think some people like reducible varieties? But maybe reduced?)
5) finite type (surely, that's what makes them varieties, except that if we want an arbitrary base ring then actually we want finite presentation, except that finite presentation sounds stupid if the base is a field, the difference only kicks in if k is a non-Noetherian ring)

Hartshorne basically has "all of the above". I just looked in Qing Liu's book (p55/56) and their definition (to my surprise) is scheme of finite type over a field! (no separatedness, no reduced, no irreducible).

Yael is sitting here next to me with a formalized definition and these are the questions which arose.

[Michael Stoll]

Kevin Buzzard said:

1) Should k be assumed to be algebraically closed? (my opinion: no)

Certainly not! You'd toss out aithmetic geometry from the start...

[Damiano Testa]

I would go with "integral separated scheme of finite type over a field".

[Damiano Testa]

I view the fact that Hartshorne adds "algebraically closed" a mistake.

[Damiano Testa]

Everything else is a scheme.

[Damiano Testa]

Several people do not include the irreducible (but almost always include reduced). I personally prefer varieties to be irreducible (and also reduced, hence intergral).

[Yaël Dillies]

For context, we have a first definition in Toric

[Kevin Buzzard]

Damiano Testa said:

I would go with "integral separated scheme of finite type over a field".

"integral" or "geometically integral", if we're dropping "algebraically closed"?

[Damiano Testa]

Integral certainly!

[Kevin Buzzard]

I mean, geometrically integral implies integral, so I agree they need to be integral, I'm asking whether x^2=2 defines a variety over Q, because, after all, Q[x]/(x^2-2) is an integral domain...

[Damiano Testa]

In particular, being a variety is not stable under base-change.

[Kevin Buzzard]

Oh OK so you really mean "integral and not necessarily geometrically integral".

[Damiano Testa]

Yes, $x ^ 2 = 2$ is a variety over $\mathbb{Q}$, but not over $\mathbb{Q}(\sqrt{2})$.

[Kevin Buzzard]

@Michael Stoll are you happy with this? Does anyone else have an opinion?

[Damiano Testa]

Right, so "Integral certainly" meant "Definitely you do not need them to be geometrically integral. Just integral is enough".

[Michael Stoll]

That looks OK to me.
In the end it will be as usual: we have to try something, and if it turns out that it is inconvenient, change the definition. But this seems to converge to something that looks like a reasonable starting point.

[Damiano Testa]

I also think that quite a few results will be proved about schemes, regardless of which specialization of "schemes" we choose for "variety".

[Riccardo Brasca]

Yeah the point will be to prove anything in full generality.

[Riccardo Brasca]

Anyway for me it is an integral scheme of finite type over a field

[Thomas Browning]

Regarding the base being a field, does this actually need to be decided for the definition? I would have assumed that the definition of a variety would take in k with some typeclass assumptions, and theorems about varieties would also take in k with some typeclass assumptions, so the definition of a variety could assume CommRing, and theorems about varieties could assume Field as needed.

[Kevin Buzzard]

Riccardo Brasca said:

Anyway for me it is an integral scheme of finite type over a field

So no separated condition??

[Kevin Buzzard]

So with elliptic curves we do "definition works over a ring, all the theorems assume field". The only issue with allowing a commring is then I feel like "finite type" should actually be changed to "finite presentation" for a sensible theory, and then in all the applications we'll have this finite presentation proof obligation which will be slightly more annoying than having finite type proof obligations everywhere.

[Riccardo Brasca]

Kevin Buzzard said:

Riccardo Brasca said:

Anyway for me it is an integral scheme of finite type over a field

So no separated condition??

Sorry, separated.

[David Ang]

Imho separated should be included but integral can be relaxed; no opinion on finite type over either a field or a ring

[Kevin Buzzard]

"finite type" is almost never right if the base isn't Noetherian. Finite presentation enables you to reduce to the Noetherian case. If we really want to allow rings in the definition (which I am still dubious about) then we should surely have a definition which is useful in the non-Noetherian case as opposed to just "wrong".

[Damiano Testa]

My opinion is that allowing rings simply means "it's a scheme over an affine scheme". I would treat that as a scheme, not as a variety.

[Miguel Marco]

As a singularity theorist (or something along those lines), I think that nonreduced/reducible algebraic varieties are definitely a thing.

[Kevin Buzzard]

Oh-oh. So what do we do?

[Damiano Testa]

How about putting off defining variety and working with schemes instead?

[Patrick Massot]

I think we’re done proving Kevin’s claim that starts this thread. Now we only need to formalize it.

[Christian Merten]

1. As long as a statement does not talk about the category of $R$-varieties, I think it should never take IsVariety as an assumption and not work with Over X, but instead require (X : Scheme) [X.Over (Spec R)] (docs#AlgebraicGeometry.Scheme.Over) and the necessary assumptions on X ↘ Spec R.
2. When you need the category of $R$-varieties, I suggest developing as much as possible for P.Over ⊤ (Spec R) where P : MorphismProperty Scheme assuming whatever is necessary for P (IMO, then there is no reason to require S = Spec R anymore. Instead, it should be IsAffine S when needed). This discussion clearly shows that there is no consensus on what the category of varieties is.

Of course for downstream projects, there could very well be an abbreviation IsVariety picking the preferred set of assumptions the author likes.

[Kevin Buzzard]

My objection to this had been "but what about all the complex geometers who don't care about schemes at all but definitely want to talk about smooth projective complex varieties and then want to put manifold structures on the closed points" but your last sentence is perhaps the answer to what they should be doing in this case.

[Yaël Dillies]

Damiano Testa said:

How about putting off defining variety and working with schemes instead?

In Toric, we're trying to define toric varieties, and it seemed like defining the category of toric varieties was going to be the easiest route.

[Andrew Yang]

Do you really need the category of toric varieties?

[Andrew Yang]

but what about all the complex geometers who don't care about schemes at all but definitely want to talk about smooth projective complex varieties and then want to put manifold structures on the closed points

That could be solved by better documentation, giving a list of magic spells that they could just copy-paste.

[Junyan Xu]

Apparently there are toric schemes too:
https://www.zora.uzh.ch/id/eprint/40859/1/20111168.pdf
https://arxiv.org/abs/1107.2713
https://arxiv.org/abs/1207.0605

Have you started glueing the affine pieces yet?

[Antoine Chambert-Loir]

Illusie once told me that while everybody knows the definition of a scheme, nobody knows what an algebraic variety is. Certainly they're schemes of finite type over a field, imposing separated doesn't hurt, but whether they need to be integral, or reduced, or geometrically integral or geometrically reduced, is a mere convention.

[Antoine Chambert-Loir]

Regarding toric varieties, there is the question of the ground field (which should not be assumed to be algebraically closed), the normality assumption (sometimes annoying). The question of a base field is also a mess: surely fans define smooth schemes over Z, and it would be a mess not to have them. For me, a toric variety is an equivariant embedding of a torus over some base scheme.

[Damiano Testa]

This looks like the module vs vector space discussion.

[Kevin Buzzard]

It does doesn't it. And we gave up on VectorSpace in the end, but perhaps this was because lean 3 couldn't handle synonyms so well

[Kevin Buzzard]

I was far more pro vector spaces back then because I was far more engaged with trying to get undergraduates on board

[Damiano Testa]

I think that both vector space and varieties work well to help humans fix on a not-fixed collection of simplifying assumptions that help focus and figure out what is or is not true. Once that is done, when you formalise your results, you should pick the exact hypotheses that you need and then probably the correct approach is to use "module+assumptions on the ring" and "scheme+assumptions on the base scheme".

[Damiano Testa]

So, I view vector spaces and varieties as informally useful concepts that do not really have a formal counterpart.

[Damiano Testa]

They are unification hints for humans.

[Yaël Dillies]

Can we move this to #maths?

[tsuki]

So is there a definition of an algebraic variety in Lean4 now? Where can I find it?

[Yaël Dillies]

In mathlib, there is basically everything you could want a variety to be, but no def Variety := .... Tell us what a variety is to you and we can point you to what you're looking for :smile:

[Yaël Dillies]

Also note that this other thread exists: #Is there code for X? > ✔ definition of variety

[tsuki]

Let \( I \subseteq k[x_1, \ldots, x_n] \) be an ideal. We will denote by \( \mathbf{V}(I) \) the set
  \[
  \mathbf{V}(I) = \{(a_1, \ldots, a_n) \in k^n \mid f(a_1, \ldots, a_n) = 0 \text{ for all } f \in I\}.
  \]

[Johan Commelin]

Is that your definition of "variety"??

[Edward van de Meent]

Let $I \subseteq k[x_1, \ldots, x_n]$ be an ideal. We will denote by $\mathbf{V}(I)$ the set

$$\mathbf{V}(I) = \{(a_1, \ldots, a_n) \in k^n \mid f(a_1, \ldots, a_n) = 0 \text{ for all } f \in I\}.$$

:sparkles:

[Edward van de Meent]

now i can read it

[Kevin Buzzard]

That's an affine algebraic set and possibly an affine variety depending on whose definition you read.

[Michał Mrugała]

Importantly:

• this definition exists in the context of classical algebraic geometry (which afaik is not in mathlib because schemes supersede it)
• this is not the definition of a variety even in classical AG
• defining a variety in classical AG suffers from the same problems as defining a variety as a scheme (do we want irreducibility?)

[Antoine Chambert-Loir]

I slightly dissent. This definition definitely exists in the context of schemes. Then $\mathbf V(I)$ is a subscheme of the affine space $\mathbf A^n_k$, and what you wrote is its set of $k$-points, aka $\mathbf V(I)(k)$.

[Michał Mrugała]

Antoine Chambert-Loir said:

I slightly dissent. This definition definitely exists in the context of schemes. Then $V(I)$ is a subscheme of the affine space $A^n_k$, and what you wrote is its set of $k$-points, aka $V(I)(k)$.

What I meant is that this isn't the definition of a variety in the context of schemes in any reasonable sense of the word definition.