多项式律的形式化化构及普遍除法代数

本文旨在 Lean/Mathlib 数学库框架下，对 Roby (1965) 对普遍除法代数构造的形式化化作品进行展示。该构造是除法理论中类似于经典多项式代数的类比对象。它是晶体上同调理论发展中的关键工具，也用于 p 初等Hodge理论中定义晶体周期环。作为代数结构，此普遍除法代数拥有相当简单的定义，表明其为分级代数。Roby 定理的主要难点在于在其共轭理想上构建除法结构。为此，Roby 将其分级部分识别为另一种普遍结构：齐次多项式律。我们对多项式律理论的前期步骤进行形式化化，并展示了如何通过后续工作完成上述除法结构的形式化化。我们报告了在该形式化化过程中出现的各种困难：处理宇宙问题、将某些 Mathlib 库方面扩展至半环、以及应对若干“看不见的数学”。