Cubical Agda 中概形的函子点方法

我们在 Cubical Agda 证明助手中对拟紧拟分离概形（qcqs-schemes）进行了形式化。我们遵循 Grothendieck 的函子点方法，将作为现代代数几何核心概念的概形定义为从交换环到集合的某些具有良好性质的函子。该方法通常被认为在概念上比将概形定义为局部环化空间的标准方法更简单，但据我们所知，它在代数几何的形式化中尚未被采用。我们基于先前对与交换环相关联的所谓 Zariski 格的形式化，定义了紧开子函子的概念。这使得 qcqs-schemes 的定义更加简洁，简化了通常的表述，例如 Demazure 和 Gabriel 的标准教科书中的表述。它还使我们能够获得仿射概形的紧开子函子是 qcqs-schemes 的完全构造性证明。