Formalization in Lean of faithfully flat descent of projectivity

本文在 Lean 中形式化并验证了 Raynaud 和 Gruson 经典结论中 Perry 修正后的一个基础结果，即对于任意交换环 $R$ 到忠实平坦扩张 $S$ 的映射，$R$-模 $P$ 的投射性等价于 $S \otimes_R P$ 在 $S$ 上的投射性。

要点

这篇论文讲述了一个关于**“数学验证”**的故事。作者 Liran Shaul 使用了一种名为 Lean 的计算机编程语言，像给数学定理做“代码审计”一样，重新证明了一个非常古老且重要的数学结论。

为了让你轻松理解，我们可以把这篇论文的内容想象成**“修复一座古老桥梁的蓝图”**。

1. 背景：一座著名的“数学大桥”

在 20 世纪，数学家 Raynaud 和 Gruson 写了一篇著名的论文（就像一座宏伟的大桥），解决了代数领域的一个核心问题。这座桥的核心观点是：

如果你有一个复杂的结构（数学上的“模”），你想知道它是否“坚固”（数学上的“投射性”），你不需要亲自去检查它。你只需要把它“复制”到一个更广阔、更平坦的地方（数学上的“忠实平坦扩张”），如果那个副本是坚固的，那么原来的那个也是坚固的。

这就像你想检查一个木桶（原来的结构）是否漏水。你不需要把木桶拆了看，你只需要把它放进一个巨大的、绝对不漏水的透明水箱（新的环境）里。如果在水箱里它看起来滴水不漏，那么它原本就是不漏的。

2. 问题：蓝图里有个“隐形裂缝”

几十年后，另一位数学家 Gruson 发现，这座“大桥”的建造图纸（原始证明）里有一个细微的裂缝（逻辑漏洞）。虽然大家一直觉得这座桥很稳，但没人能 100% 确定那个裂缝到底补好了没有。

• 之前的尝试：后来有人试图修补这个裂缝，但修补方案从未经过严格的同行评审（就像有人口头说“我补好了”，但没拿出验收报告）。
• 作者的任务：Liran Shaul 决定用计算机语言 Lean 来重新建造并验收这座桥。他不仅要证明结论是对的，还要把修补裂缝的过程写得严丝合缝，让计算机也能一步步验证，确保没有任何逻辑漏洞。

3. 核心工具：数学界的“乐高积木”

为了完成这个任务，作者不能只用现有的工具，因为 Lean 库里缺很多关键零件。他不得不从零开始制造了四大类“乐高积木”：

• 积木一：无限分解术 (Kaplansky Devissage)

  • 比喻：想象你要检查一个巨大的、由无数小零件组成的乐高城堡。直接检查太累了。作者发明了一种方法，可以把这个城堡拆解成无数个**“小塔”**（可数生成的模块）。
  • 作用：只要证明每一个“小塔”是坚固的，整个城堡就是坚固的。这大大简化了问题。

• 积木二：Lazard 定理 (Lazard's Theorem)

  • 比喻：这就像是一个**“变形金刚”说明书**。它告诉你，任何“平坦”的结构（Flat Module），其实都是由一堆简单的、标准的“自由积木”（自由模）拼凑而成的。
  • 作用：这让我们能把复杂的结构还原成最简单的积木块来研究。

• 积木三：推积 (Pushout) 与“万能胶水”

  • 比喻：想象你有两块拼图，它们都连在同一块底板上。作者发明了一种**“万能胶水”**，能把这两块拼图完美地拼在一起，形成一个新的整体，同时保留它们原本的特性。
  • 作用：这是处理数学对象之间复杂关系的关键工具，就像把两个不同的世界连接起来。

• 积木四：Mittag-Leffler 条件 (Mittag-Leffler Condition)

  • 比喻：这就像是一个**“稳定器”**。想象你在观察一群不断变化的鸟群（逆系统）。Mittag-Leffler 条件保证了，虽然鸟在飞，但鸟群的“核心形状”最终会稳定下来，不会无限混乱。
  • 作用：这是连接“平坦”和“坚固”的桥梁。作者证明了，如果一个结构既“平坦”又“稳定”（满足 Mittag-Leffler），那它一定是“坚固”的。

4. 最终成果：完美的验收报告

作者把这些积木拼在一起，完成了一个超长的代码验证过程（超过 10,000 行代码）：

1. 第一步：利用“无限分解术”，把巨大的问题拆成无数个“小塔”。
2. 第二步：利用“稳定器”和“变形金刚”理论，证明每一个“小塔”如果是平坦的，那它就是坚固的。
3. 第三步：利用“万能胶水”和“忠实平坦”的特性，证明如果“小塔”在“透明水箱”里是坚固的，那它在原处也是坚固的。
4. 结论：通过计算机的严格逻辑检查，确认了 Raynaud 和 Gruson 当年的结论是正确的，并且那个“隐形裂缝”已经被完美修补了。

总结

这篇论文不仅仅是证明了一个数学定理，它更像是一次**“数学工程的数字化重建”**。

• 以前：数学家靠人脑和纸笔，可能漏掉细节。
• 现在：作者用计算机语言，把每一步逻辑都变成了可执行的代码，让计算机充当了最严格的“质检员”。

这不仅确认了 20 世纪代数几何的一块基石是稳固的，也为未来研究更复杂的数学问题（比如“有限维”问题）打下了坚实的基础。简单来说，作者说：“别担心，那座桥是安全的，我们刚刚用计算机把它彻底检查了一遍，连一颗螺丝都没松！”

技术摘要

论文技术总结：Lean 中忠实平坦下降与投射性的形式化

1. 研究背景与问题 (Problem)

本文旨在在 Lean 4 证明助手及其数学库 Mathlib 中形式化并验证交换代数中的一个基础且关键的结果：忠实平坦下降下的投射性（Faithfully Flat Descent of Projectivity）。

该问题的核心是解决 Raynaud 和 Gruson 在 1971 年的经典论文 [7] 中关于投射模下降定理的一个细微漏洞。该定理（文中称为定理 I）陈述如下：

设 $R \to S$ 是交换环的忠实平坦映射，$P$ 是任意 $R$-模。则 $P$ 在 $R$ 上是投射的，当且仅当 $S \otimes_R P$ 在 $S$ 上是投射的。

关键难点与背景：

• 非诺特情形与无限生成： 该定理不假设环是诺特的，且模 $P$ 可以是无限生成的。
• 经典证明的缺陷： Raynaud 和 Gruson 的原始证明被 Gruson 指出存在逻辑漏洞。虽然 Stacks Project [1] 和后续文献 [6] 提供了完整证明，但这些证明从未经过同行评审，且极其复杂。
• 形式化挑战： 该证明涉及高度非平凡的步骤，包括：
  1. 从完备诺特局部环到任意诺特局部环的过渡。
  2. 从局部到整体的论证。
  3. 处理无限生成模的超限分解（Transfinite Devissage）。
  4. Mittag-Leffler 条件在逆系统中的形式化。
  5. **普遍单射（Universally Injective）**映射的上升与下降性质。

2. 方法论 (Methodology)

作者 Liran Shaul 在 Lean 4 中从头构建了超过 10,000 行代码，系统性地开发了以下核心数学概念和工具，以填补 Mathlib 的空白并支撑主定理的证明：

2.1 基础架构开发

• Kaplansky 分解 (Kaplansky Devissage)： 形式化了将任意模分解为可数生成子模直和的结构。定义了基于序数（Ordinal）的过滤序列，确保每个商模是可数生成的，且每一步都是直和项。
• Mittag-Leffler 条件：
  • 逆系统： 形式化了 Mittag-Leffler 逆系统的定义（图像在指标增加时稳定），并证明了在可数定向集上，Mittag-Leffler 逆系统的逆极限非空。
  • Mittag-Leffler 模： 定义了 Mittag-Leffler 模（通过有限表现模的映射的支配性质），并建立了其与逆系统条件的等价性。
• 拉扎尔定理 (Lazard's Theorem)： 形式化了平坦模是有限表现自由模的直极限这一经典结论。
• 模的推出 (Pushout)： 在交换环上实现了模的推出构造，并证明了推出与张量积的交换性。
• 普遍单射 (Universally Injective)： 定义了普遍单射映射（对任意模张量后仍保持单射），并证明了其在忠实平坦映射下的下降性质。
• 支配关系 (Domination)： 形式化了线性映射之间的支配关系（核的包含关系），并建立了其与通过推出映射的普遍单射性之间的等价性。

2.2 证明策略

证明分为两个主要定理的构建：

1. 定理 II (特征刻画)： 证明一个模 $P$ 是投射的，当且仅当它满足三个条件：(1) 平坦；(2) Mittag-Leffler；(3) 是可数生成模的直和。
   • 利用 Kaplansky 分解将问题约化到可数生成情形。
   • 利用 Lazard 定理将平坦模表示为有限表现自由模的直极限。
   • 利用 Mittag-Leffler 条件和逆极限的满射性（Theorem 5.2）来构造提升映射，从而证明投射性。
2. 定理 I (忠实平坦下降)：
   • 可数生成情形： 利用定理 II，结合“忠实平坦反射 Mittag-Leffler 性质”和“忠实平坦反射可数生成性”两个引理，证明若 $S \otimes_R P$ 投射，则 $P$ 满足定理 II 的所有条件，从而 $P$ 投射。
   • 一般情形： 使用超限归纳法（Transfinite Induction）构建 Kaplansky 过滤，将任意模分解为可数生成投射模的直和，从而完成证明。

3. 关键贡献 (Key Contributions)

1. 首个形式化验证： 这是该定理及其完整证明（包括 Perry 对 Raynaud-Gruson 漏洞的修复）的首次形式化验证。
2. 填补 Mathlib 空白： 开发了大量此前 Lean 中不存在的基础设施，包括：
   • 基于序数的超限分解框架。
   • 完整的 Mittag-Leffler 模理论（包括多种等价定义和性质）。
   • 普遍单射映射及其在交换代数中的性质。
   • 模的推出及其与张量积的兼容性。
3. 修正与澄清： 在形式化过程中，作者发现并修正了文献 [6] 和 [1] 中关于 Mittag-Leffler 条件与直极限过渡映射之间等价性证明的细微不精确之处，提供了更严谨的 Lean 证明。
4. 大规模代码库： 生成了超过 10,000 行 Lean 代码，涵盖了从基础定义到复杂定理证明的完整链条。

4. 主要结果 (Results)

论文成功编译并验证了以下核心定理：

• 定理 I (Faithfully Flat Descent of Projectivity)：
  $$P \text{ is } R\text{-projective} \iff S \otimes_R P \text{ is } S\text{-projective}$$
  其中 $R \to S$ 是忠实平坦映射，$P$ 是任意 $R$-模。

• 定理 II (Characterization of Projective Modules)：
  对于任意环 $R$（不必交换）和左 $R$-模 $P$：
  $$P \text{ is projective} \iff \begin{cases} P \text{ is flat} \\ P \text{ is Mittag-Leffler} \\ P \text{ is a direct sum of countably generated modules} \end{cases}$$
  此结果统一了 Kaplansky 定理（投射模是可数生成投射模的直和）和 Lazard 定理。

• 辅助定理：

  • 证明了忠实平坦映射反射 Mittag-Leffler 性质。
  • 证明了忠实平坦映射反射可数生成性质。
  • 建立了支配关系、推出映射的普遍单射性以及因子分解之间的等价性。

5. 意义与影响 (Significance)

1. 数学严谨性的提升： 通过计算机辅助证明，彻底消除了 Raynaud-Gruson 经典工作中遗留的潜在逻辑漏洞，为交换代数中关于投射模和有限维度的研究提供了坚实的逻辑基础。
2. 对有限维度的贡献： 该定理是研究交换诺特环的**有限维数（finitistic dimension）**的关键工具。形式化该结果有助于未来在 Lean 中形式化 Bass 猜想及相关维度理论。
3. Lean 数学库的扩展： 本文极大地丰富了 Mathlib 在交换代数、同调代数（特别是 Mittag-Leffler 条件和逆极限）以及范畴论（推出、直极限）方面的能力，为后续更复杂的代数几何和数论形式化工作铺平了道路。
4. 方法论示范： 展示了如何利用形式化方法处理涉及超限归纳、复杂过滤结构和非诺特情形的现代代数问题，为其他高难度数学定理的形式化提供了范例。

综上所述，Liran Shaul 的这项工作不仅验证了一个具体的代数定理，更通过构建庞大的底层数学库，推动了计算机辅助数学在交换代数前沿领域的应用。