论文标题
建设性仿射方案的单一形式化
A Univalent Formalization of Constructive Affine Schemes
论文作者
论文摘要
我们提出了立方AGDA证明助手中建设性仿射方案的形式化。这种发展不仅是完全建设性的和谓词，而且还至关重要的是使用一致性。到现在为止，计划已经在各种证明助手中正式化。但是，大多数现有的形式化遵循Hartshorne经典的“代数几何”教科书的固有非构造方法，为此，所谓的结构的构造相当简单地正式化，并且在无与伦比的情况下起作用。我们遵循一种替代方法，该方法使用了称为Zariski晶格的Zariski Spectrum的建设性对应物的无点描述，并通过在正式基本打开上定义结构，然后将其提升到整个晶格中。这种一般策略用于大量教科书中，但正式化它已被证明是棘手的。本文的主要结果是，借助单位原则，我们可以正式制定“基础”策略的“提升”，并获得对建设性仿射方案的完全正式化的说明。
We present a formalization of constructive affine schemes in the Cubical Agda proof assistant. This development is not only fully constructive and predicative, it also makes crucial use of univalence. By now schemes have been formalized in various proof assistants. However, most existing formalizations follow the inherently non-constructive approach of Hartshorne's classic "Algebraic Geometry" textbook, for which the construction of the so-called structure sheaf is rather straightforwardly formalizable and works the same with or without univalence. We follow an alternative approach that uses a point-free description of the constructive counterpart of the Zariski spectrum called the Zariski lattice and proceeds by defining the structure sheaf on formal basic opens and then lift it to the whole lattice. This general strategy is used in a plethora of textbooks, but formalizing it has proved tricky. The main result of this paper is that with the help of the univalence principle we can make this "lift from basis" strategy formal and obtain a fully formalized account of constructive affine schemes.
