A formal proof of the projective Eisenbud-Evans-Storch theorem (Q444111)

Following \textit{T. Coquand} [Ann. Pure Appl. Logic 157, No. 2-3, 97--109 (2009; Zbl 1222.03072)], the general framework of this paper is a reformulation of Hilbert's programme in commutative algebra using formal topology. In formal topology, a topological space is not defined as a set of points, but as a logical theory which describes the lattice of open sets. Points are then infinite ideal objects, defined as particular filters of neighborhoods, while basic open sets are thought of as primitive, symbolic objects or observable facts. Hilbert's ideal objects are represented by points of suitable formal spaces. The use of ideal objects can often be directly replaced by working in the corresponding logical theory, which is here presented by a distributive lattice. As an example, the Zariski spectrum of a commutative ring \(R\) is described in a formal way through a distributive lattice, whose prime filters correspond to its prime ideals. A statement of existence of a prime ideal corresponds formally to the fact that the distributive lattice under consideration is non-trivial(that is, the underlying theory is non-contradictory). The Hilbert Nullstellensatz, which classically provides the link between the topology and the algebraic structure, is substituted by the effective existence of a proof certificate, in form of an algebraic identity. In 1972, Storch showed that each radical ideal \(R[X]\) is the radical of an ideal generated by at most \(d+1\) elements, provided that \(R\) has Krull dimension \(d\). Independently, in 1973, Eisenbud and Evans proved the same result and gave it also for the projective case. The constructive definition of Krull dimension for lattices and rings led to an elementary constructive proof of Kronecker's result and to a constructive rebuilding of the Storch proof. In this paper the author extend the latter proof to the projective case as stated by Eisenbud and Evans. He use the description of the projective spectrum as a distributive lattice and get a topological proof which follows the affine case \textit{T. Coquand, H. Lombardi} and \textit{P. Schuster} [Arch. Math. 85, No. 1, 49--54 (2005; Zbl 1093.03035)]. The central role played by lattice-theoretic techniques prompts to conjecture that these theorems, regarding the number of generators, could be stated more properly in the wider context of lattices. The Eisenbud-Evans-Storch theorem looks rather as a statement on the distributive lattices underlying the algebraic structure(respectively \(\mathrm{Zar}(R[X])\) for the affine case, \(\mathrm{Pro}^X(A)\) for the projective one). Further studies will be undertaken in order to clarify these similarities and to possibly find a common generalization in the context of distributive lattices.