Formalizing multi-graded Brenner-Schröer Proj schemes and dilatations of rings in Lean4

技术摘要：在 Lean4 中形式化多分次 Brenner–Schröer Proj 方案与环的扩张（Dilatations）

问题陈述
本文探讨了在 Lean4 定理证明器中对高级代数几何构造的形式化实现。虽然经典的代数几何通常依赖于由自然数 ($\mathbb{N}$) 或整数 ($\mathbb{Z}$) 分次的环，但现代发展——例如在李理论、几何表示论以及极小模型纲领中的应用——需要由更一般的单群或群分次的环。具体而言，作者专注于 Brenner–Schröer Proj 构造，该构造将经典的 Proj 构造推广到了多分次情形，以及与局部化和吹胀（blowups）相关的环扩张（dilatations）理论。其挑战在于如何在类型论框架（Lean4）中实现这些结构，同时必须严谨地处理分次环 $A$ 与其直和分解 $\bigoplus_{i \in \iota} A_i$ 之间的区别，且不牺牲易用性。

方法论
作者采用了一种与现有文献（特别是遵循 [9] 中的处理方式）一致的代数方法，在 Lean4 中形式化这些概念。其方法论包括：

1. 分次结构的通用设置： 该形式化定义了分次环和分次模，其中分次单群 $\iota$ 是一个任意的交换群。为了处理类型论中的约束，作者区分了环 $A$ 及其分次分量 $A_i$，利用 SetLike 结构将分量视为子群，同时保持在环与其直和分解之间切换的能力。
2. 齐次局部化与“药剂”（Potions）： 一个核心的技术创新是“药剂”（$\vartheta(S)$）的定义，它被定义为齐次局部化 $A(S)$ 的零次部分。与标准的局部化不同，药剂并非定义为局部化环的子环，而是定义为三元组 $(i, a, b)$ 的商，其中 $a, b$ 是相同次数的齐次元素且 $b \in S$。这种结构有助于简化归纳过程并便于访问分子与分母。
3. 相关性与良好的药剂成分： 作者形式化了“相关”齐次子单群的概念，即该子单群中元素的次数所生成的子群在分次群中具有有限指数（或挠商）。他们将“良好的药剂成分”定义为既是相关的又是有限生成的子单群。
4. 粘合与 Proj 构造： Proj 方案通过将与一系列良好药剂成分相关的仿射方案 $\text{Spec}(\vartheta(S_i))$ 进行粘合来构建。粘合数据依赖于药剂张量积之间的同构关系（例如 $\vartheta(ST) \otimes_{\vartheta(S)} \vartheta(SR) \cong \vartheta(RST)$），这些同构是通过“药剂生成元”建立的。
5. 扩张（Dilatations）： 本文形式化了关于多中心（一组理想与元素的集合）的环的扩张。这涉及定义符号分数 $m/a^\nu$ 的等价类，并证明刻画扩张的普遍性质。

主要贡献与结果
本文在 Lean4 中呈现了一个完整的定义、引理和定理库：

• 多分次 Proj 的形式化： 作者提供了 Brenner–Schröer Proj 构造的完整实现。这包括齐次局部化的定义、药剂理论以及通过粘合仿射方案来形成 Proj 方案。
• 药剂生成元与同构： 一个重要的贡献是形式化了“药剂生成元”，这使得作者能够证明对于相关的 $S$ 和有限生成的 $T$，态射 $\text{Spec}(\vartheta(ST)) \to \text{Spec}(\vartheta(S))$ 是一个开浸入。他们还建立了用于粘合构造所需的循环条件（cocycle conditions）。
• 函子性： Proj 构造被证明是从分次环范畴到方案范畴的反变函子。作者仔细处理了类型论中的微妙之处，即一个族在环同态下的像并不在定义上等于目标族，因此需要使用特定的态射（projHomOfLE）来建立函子性。
• 扩张： 本文形式化了环扩张的定义，并证明了其普遍性质：对于任何环同态 $\chi: A \to B$，其中中心元素的像是非零因子且生成了对应理想的像，则存在从扩张到 $B$ 的唯一态射。
• 扩大族之同构： 作者证明了通过扩大（包含现有成分的乘积）一个良好药剂成分族，会得到一个同构的 Proj 方案，从而确保了构造对于生成族的鲁棒性。

意义
本文声称其意义主要在于作为高级代数几何形式化的基础性步骤。它作为：

1. 文档： 对支撑形式化的定义、设计选择及主要结果的详细说明，旨在指导未来的开发者。
2. 基础： 一个可重用的库，用于未来扩展代数几何中的形式化工作，特别是对于需要多分次结构或扩张的项目。
3. 验证： 一个完全形式化的实现，在证明助手中验证了 Brenner–Schröer 构造和扩张理论的正确性，确保了对文献中代数定义的严谨遵循。

作者明确指出，相应的代码已公开，以支持进一步开发高级几何结构的形式化工作。他们并非声称解决了代数几何中的开放问题，而是成功地将现有的复杂理论转化为机器可检查的形式。