General statement of Ax-Grothendieck

Stream: maths

[Chris Hughes]

Wikipedia and Terry Tao say that the general statement of the Ax-Grothendieck is that it's true for any map from an algebraic variety to itself. I understand how to use model theory to prove the statement for the zero-set of a finite set of polynomials, but I don't understand straight away how to do it for infinite sets of polynomials? Does this follow from the finite case?

[Matthew Ballard]

Variety usually means finite type

[Antoine Chambert-Loir]

The zero set of an infinite set of polynomials (in finitely many variables) is the zero set of a finite subset of these polynomials, because the ring of polynomials (over a field) is noetherian.

[Junyan Xu]

"Finite type" means in finitely many variables, finite presentation means finite type + defined by finitely many polynomials. Over a noetherian ring (e.g. a field) they are equivalent stacks#00FP, because the ring of polynomials over a noetherian ring is also noetherian (docs#MvPolynomial.isNoetherianRing, docs#Polynomial.isNoetherianRing).

[Chris Hughes]

Okay, Thanks everyone. The statement I went for was this.

variable {K ι : Type*} [Field K] [IsAlgClosed K] [Finite ι]

theorem ax_grothendieck_zeroLocus
    (I : Ideal (MvPolynomial ι K))
    (p : ι → MvPolynomial ι K) :
    let S := zeroLocus I
    S.MapsTo (fun v i => MvPolynomial.eval v (p i)) S →
    S.InjOn (fun v i => MvPolynomial.eval v (p i)) →
    S.SurjOn (fun v i => MvPolynomial.eval v (p i)) S := by

[Junyan Xu]

I tried several spellings using Lean 4's succinct function notation and not all them work:

(fun v => (MvPolynomial.eval v <| p ·)) : works
(fun v => (MvPolynomial.eval v (p ·))) : doesn't work
(MvPolynomial.eval · <| p ·) : works, preferred spelling?
(MvPolynomial.eval · (p ·)) : doesn't work
(fun i => MvPolynomial.eval · <| p i) : works
(fun i => MvPolynomial.eval · (p i)) : works
replacing <| by $ also works

By the way, is it easy to make a pretty printer for such function notation? Not that it help much in this case, but it would make the co(ntra)variance assumptions in docs#add_eq_add_iff_eq_and_eq etc. much more readable.

[Eric Rodriguez]

(MvPolynomial.eval · <| p ·) seems absolutely unreadable

[Chris Hughes]

I think Ax-Grothendieck is fairly easily generalizable to rational functions, or even I guess functions definable in the language of fields. I don't know if people are interested in these generalizations

[Kevin Buzzard]

What is the version of injectivity you want to allow if you're allowing infinity as a value?

[Maarten Derickx]

Grothendieck himself already formulated a very general statement in EGA, see 10.4.11 in http://www.numdam.org/article/PMIHES_1966__28__5_0.pdf . Note that preschemes there are nowadays just called schemes.
Translation into modern english that statement reads:

Let S be a scheme, and X be a scheme over S of finite type. Then every S endomorphism of X that is radical is surjective (and hence bijective).

It think it would be awesome if you could prove it in this generality just because it means we have enough scheme theory in Mathlib to reduce the statement for arbitrary $S$ to the case where $S$ is itself of finite type over $\mathbb Z$.

[Chris Hughes]

I'm not really very good at algebraic geometry. Can it be proven with similar methods in model theory, or is it completely different?

[Maarten Derickx]

It is a completely different proof. Theorem 3.1 of https://arxiv.org/pdf/0903.0517.pdf has a good short overview of how Grothendiecks proof goes, in a slightly less general setting that proof sketch is really short and understandable.

[Chris Hughes]

I'm not sure we do have enough scheme theory and it would take me quite a bit of time to understand that stuff. I guess realistically I won't be doing the general version unless someone writes me a clear explanation of how and it turns out to be easier than it sounds. I think it might have to wait.

[Kevin Buzzard]

Chris you could just restrict to the affine case over an alg closed field (which covers C^n but also all Zariski-closed subspaces of C^n, i.e. subspaces defined by polynomial equations). Then it really is just ring theory and at the end of the day the proof in Lean would be much simpler than the model theory one.

[Chris Hughes]

Isn't that what I did prove?

theorem ax_grothendieck_zeroLocus
    (I : Ideal (MvPolynomial ι K))
    (p : ι → MvPolynomial ι K) :
    let S := zeroLocus I
    S.MapsTo (fun v i => MvPolynomial.eval v (p i)) S →
    S.InjOn (fun v i => MvPolynomial.eval v (p i)) →
    S.SurjOn (fun v i => MvPolynomial.eval v (p i)) S := by

[Chris Hughes]

Or maybe you need the slightly more general one

theorem ax_grothendieck_of_definable [CompatibleRing K] {c : Set K}
    (S : Set (ι → K)) (hS : c.Definable Language.ring S)
    (ps : ι → MvPolynomial ι K) :
    S.MapsTo (fun v i => eval v (ps i)) S →
    S.InjOn (fun v i => eval v (ps i)) →
    S.SurjOn (fun v i => eval v (ps i)) S :=

CompatibleRing just means that it's a mode-theoretic ring structure and a ring in a way that's compatible.

[Chris Hughes]

My initial impression is that these non-model theoretic proofs are more or less the same as the model-theoretic proof. The model theoretic proof works basically by exhibiting an alg-closed field of char zero as an ultraproduct of $$\overline{\mathbb{F}_p$$, and it seems maybe these other proofs do the same thing, and then more or less prove a special case of Łoś's Ultraproduct theorem, by proving for a simple formula what Łoś proved for all formulas. I'm just guessing about what's going on here, I could be completely wrong.

[Kevin Buzzard]

Isn't that what I did prove?

Probably. I don't think I understand the statement. docs#MvPolynomial.zeroLocus

[Kevin Buzzard]

Yes, you've already done the affine case over an alg closed base. My understanding is that Grothendieck generalised this in three ways: he weakens the alg closed field base first to an arbitrary commutative ring (where now you have to look at prime ideals rather than just closed points) and then to a scheme, and he generalised the variety over the base from an affine one to a general one, so all the next steps are schemey except that you could change K to a commring and use PrimeSpectrum instead of iota -> K.

[Chris Hughes]

Is that easy?

[Chris Hughes]

And I guess I'm just curious, is what I've proved useful for proving the most general case, or do you have to start over and do something totally different?

[Kevin Buzzard]

I should imagine that what you have is already useful. I haven't looked at the Grothendieck proof but results in algebraic geometry are often proved by reducing them to simpler cases such as the one you've already proved.

[Kevin Buzzard]

Yes, Grothendieck reduces from a general base to a field, although unfortunately he doesn't reduce to the affine case.

[Chris Hughes]

A field or an Algebrically Closed field?

[Chris Hughes]

I'm seeing the French word "Or" which has no translation in English so I'm told.

[Chris Hughes]

So I guess we're using the fact that any subfield of C is an ultraproduct of subfields of $\overline{\mathbb{F}_p}$ or something like that. Which is a little more general than what the model theory stuff uses.

[Kevin Buzzard]

Yeah he reduces to a field and then to a finitely generated ring and then he appeals to a general result about the image being constructible. You have to understand "injective" in terms of the scheme points though. I wonder if the HoTT people can prove it? The hard part might be stating it.

[Chris Hughes]

What is HoTTy about this theorem? I don't understand why HoTT is relevant. It should be constructively provable if you can constructively prove completeness of ACF_p, by doing the quantifier elimination algorithm

[Chris Hughes]

The image being constructible sound a bit like quantifier elimination

[Kevin Buzzard]

Grothendieck's version of the theorem states that a map is surjective, by which he means "surjective on scheme-theoretic points". At least one HoTT construction of schemes which I have seen did not have an API for the scheme-theoretic points with its topological space structure, but "surjective" is a statement about this structure.

[Kevin Buzzard]

"scheme-theoretic points" is different to "functor of points".

[Chris Hughes]

I kind of think this discussion is useless unless I know exactly what's going on. You say reduce to a field, but clearly x^3 : Q->Q is injective and not surjective. I don't think it can be explained by halves.

[Kevin Buzzard]

Q is not the scheme-theoretic points of affine 1-space over Q. The scheme-theoretic points biject with the monic irreducible polynomials and there are a lot more of these than those of the form X - q. The point X^2+X+1 gets mapped to X - 1 by cubing, as does X - 1.

[Kevin Buzzard]

Over an alg closed field, the field bijects with the monic irreducible polynomials over the field because they're all degree 1. But for a general field they become different concepts. It's really important to use this more abstract one rather than the "solutions to the equation over the field" one (the one used by Weil and all the classical people) because for a field like the rationals most equations have no solutions at all, so how are you going to tell x^7+y^7=z^7 and x^11+y^11=z^11 apart -- their solution set is the same. But the prime ideals of Q[x,y,z] containing x^7+y^7-z^7 are very different to those containing x^11+y^11-z^11.

[Yaël Dillies]

Chris Hughes said:

I'm seeing the French word "Or" which has no translation in English so I'm told.

I would usually translate it by "but indeed". If you give me more context, I can be more precise.

[Maarten Derickx]

I'm a little bit late in replying here, but there is at least no obvious use of ultraproducts in Grothendieks proof. The key idea from Grothendieck restricted to $\mathbb C^n$ for simplicity is that if you have a map $f: \mathbb C^n \to \mathbb C^n$ described by multivariate polynomials $f_1, \ldots, f_n$ then there is a finite set $S \subset \mathbb C$ that contains all coefficients of these polynomials. So in fact f can be defined over the finitely generated subring $\mathbb Z[S] \subset \mathbb C$, and now suddenly you know that since $S$ is finite there will be infinitely many primes $p$ for which $\mathbb Z[S]/ p \mathbb Z[S]$ is not the zero ring. So suddenly you can relate geoemetry in characteristic 0 to geometry in characteristic $p$.

[Maarten Derickx]

Although I wouldn't be surprised if some parts of the proof would be translatable. For example Grothendieck uses the fact that being radical is a constructible property and being surjecitive is one as well. Which allows him to deduce that f is radical if an only if there is a finite subset $$S\subset \C$$ such that f "restricted" to $\mathbb Z[S]$ is radical. And the same for surjectiveness (however for surjectiveness it is the scheme theoretic sense of surjectiveness meaning $f : \mathbb A^n_{\matbb Z[S]} \to \mathbb A^n_{\matbb Z[S]}$ is surjective. And a lot of the reduction steps in the proof that reduce it to finitely generated rings $\mathbb Z[S]$ feel like a kind of compactness theorem from model theory. However it is not clear to me if this is just something that looks the same on first sight or wether there is a deeper connection.

[Kevin Buzzard]

@Maarten Derickx note that we have a ton of stuff about Jacobson rings in mathlib, but I don't think we have that the image of a constructible set is construcible

[Johan Commelin]

Does mathlib even have the definition of constructible sets?

[Kevin Buzzard]

This is all topology rather than alg geom but not as far as I know.

[Damiano Testa]

A proof of Chevalley's theorem was my first dream when I started with mathlib. I think that I got to formalizing that the map ${\textrm{Spec}} \, k[t] \to {\textrm{Spec}} \, k$ is open: docs#AlgebraicGeometry.Polynomial.isOpenMap_comap_C.