Lean4 中 Auslander--Buchsbaum--Serre 准则的形式化

我们在 Lean4 定理证明器中对 Auslander--Buchsbaum--Serre 准则进行了完整的形式化。该准则刻画了正则局部环为那些具有有限全局维数的 Noether 局部环。我们的方法不同于经典论证：经典论证通过商以正则序列的方式计算剩余域的射影维数，并利用 Koszul 复合将余切空间维数限制在全局维数之内。相反，我们的方法基于通过 Ext 函数组合消失来定义深度的形式化，系统性地构建而成。我们建立了包括 Rees 定理、Auslander--Buchsbaum 公式和 Ischebeck 定理在内的关键同伦结果，并进一步发展了 Cohen--Macaulay 模块与环的理论，包括对 Cohen--Macaulay 环上 unmixed 定理的完整形式化。为证明 Auslander--Buchsbaum--Serre 准则，我们证明了正则局部环上的最大 Cohen--Macaulay 模块为自由模块，并建立了针对唯一最大理想的弱化形式的 Ferrand--Vasconcelos 定理。作为推论，我们推导出正则性可在最大理想处检查，并形式化了 Hilbert 齐次定理。本工作表明同伦代数在交换代数形式化中能够有效应用，为该领域的未来发展提供了广泛的基础设施。