The first-order theory of geometric points of schemes: Chevalley's theorem and quantifier elimination

TL;DR

This paper unifies Chevalley's theorem and quantifier elimination for algebraically closed fields by combining geometric and logical methods, providing a new logical interpretation of geometric points of schemes.

Contribution

It introduces a unified proof of Chevalley's theorem and quantifier elimination, giving a logical perspective on geometric points and finitely presented morphisms of schemes.

Findings

Unified proof of Chevalley's theorem and quantifier elimination

Logical interpretation of geometric points of schemes

Enhanced understanding of morphisms in algebraic geometry

Abstract

Chevalley's theorem on the images of morphisms of schemes and the principle of quantifier elimination for the theory of algebraically closed fields are widely understood to be two perspectives on the same theorem. In this paper, we demonstrate that both results can easily be proven simultaneously, using a mixture of geometric and logical techniques. In doing so, we give logical meaning to geometric points of schemes and to finitely presented morphisms thereof, in a manner reminiscent of Spencer Breiner's logical schemes.