构造性仿射方案的单价化形式
摘要：建构性仿射概念的形式化在Cubical Agda证明辅助程序中进行。这个发展不仅是完全建构性和预测性的，还关键地使用了同构性。到目前为止，已经在各种证明辅助程序中对概念进行了形式化。然而，大多数现有的形式化遵循Hartshorne经典教材《代数几何》中内在的非构造性方法，对于所谓的结构层的构建而言，其形式化相当直接，并且无论是否使用同构性都能有效。我们采取了一种另类的方法，使用点无关描述构造性对应物Zariski谱的Zariski格，并通过在形式的基本开放集上定义结构层，然后将其扩展到整个格上进行。这种一般策略在众多教材中都有使用，但对其进行形式化却是有一些困难的。本文的主要结果是，借助同构性原则，我们可以将这种“从基础上提升”的策略形式化，并得到一个完全形式化的建构性仿射概念叙述。
作者：Max Zeuner and Anders M"ortberg
论文ID：2212.02902
分类：Logic
分类简称：math.LO
提交时间：2023-05-15