Zariski topology on an affine/projective space

Stream: mathlib4

[Yury G. Kudryashov]

Some theorems in dynamical systems say that a certain property holds for coefficients from a set that contains a nonempty Zariski open set. I want to formalize some of these theorems (not right now, but in a few months), so I want to have a filter for this. What's the best way to link it to the existing theory? I think, all I need for my goals is a bunch of inequalities between filters (nonempty Zariski open > countable intersection of nonempty Zariski open sets > residual $\sqcup$ ae volume).

[Yury G. Kudryashov]

Also, I may want to add complements to sets given by analytic functions to this graph of inequalities.

[Kevin Buzzard]

Is $\R^n$ an example of a space on which you would like to talk about nonempty Zariski opens?

[Yury G. Kudryashov]

The result I had in mind is about $\mathbb C^n$. I'm not sure if I need $\mathbb R^n$.

[Yury G. Kudryashov]

There is a bunch of results about polynomial foliations on $\mathbb C^2$ (e.g., the leaves are usually dense in $\mathbb C^2$) with different "genericity" conditions for each result. I need to refresh my memory to see which of them use Zariski.

[Kevin Buzzard]

I guess the thing I was going to raise even applies to $\mathbb{C}^n$, which is that modern algebraic geometry works with schemes, which are unions of affine schemes, and affine schemes are built from all prime ideals of a ring. Historically, pre-Grothendieck, people would work with all maximal ideals of a ring (the theory of algebraic varieties, which is less functorial) and the Nullstellensatz says that the maximal ideals of $\mathbb{C}[X_1,X_2,\ldots,X_n]$ are in natural bijection with $\mathbb{C}^n$, with $(a_1,a_2,\ldots,a_n)\in\mathbb{C}^n$ corresponding to the ideal generated by $X_i-a_i$. However AFAIK we have no theory of varieties in mathlib, and even if we do build a theory of varieties we will probably keep all the schemey points, so I'm not sure that any occurrence of the word Zariski in mathlib will be of any use to you, unless you want to make new objects corresponding to closed points of schemes (and even this trick wouldn't work for $\mathbb{R}^n$, which was why I asked).

[Yury G. Kudryashov]

I think that it makes sense to specialize some definitions and/or results to the usual affine spaces, because they are sometimes useful in other parts of mathematics, but we can discuss it when we actually need one of them.

[Kevin Buzzard]

What I'm saying is that it's not a specialisation. There is no scheme whose underlying topological space is naturally identified with the one you want. What you want is a new thing, not a specialisation.

[Kevin Buzzard]

Well, historically it's an old thing, which we now cover in a different way. Affine n-space in mathlib has a ton of non-closed points. Do you want to take these on?

[Joël Riou]

It seems you are looking for something like this:

import Mathlib.AlgebraicGeometry.AffineSpace

open AlgebraicGeometry

universe u

variable (K : Type u) [Field K] (ι : Type u)

noncomputable def point (x : ι → K) :
    Spec (.of (MvPolynomial ι K)) :=
  Spec.map (CommRingCat.ofHom ((MvPolynomial.aeval (R := K) x).toRingHom)) default

#check TopologicalSpace.induced (point K ι)