经典李代数中的幂零轨道
本文讨论复数域上经典李代数中幂零轨道的分类，并建立其上的闭包偏序关系．据我们所知，目前文献中关于幂零轨道的闭包序和分拆的支配序之间的等价性证明较为分散，缺乏整洁的呈现．为此，我们建立了一种新的组合图示方法以构造连接不同 Jordan 型幂零轨道间的代数曲线．相对现有的处理，图示方法有效简化了现有方法的繁重记号，并为复杂的分类讨论提供了直观的引导．考虑到以往文献在刻画 B、C、D 型合法分拆支配序盖住关系的繁复讨论中出现遗漏的历史，我们在现代 LLM 和 coding agent 的辅助下对各型经典李代数合法分拆支配序的盖住关系进行了 Lean 4 形式化验证，为 AI 时代下数学家与人工智能协同工作、多快好省完成数学形式化验证提供了实践经验．
We study the classification of nilpotent orbits in the classical Lie algebras over \(\mathbb C\), the closure order on these orbits, and the corresponding dominance order on partitions. To the best of our knowledge, proofs in the literature of the equivalence between the dominance order on partitions and the closure order on nilpotent orbits are still scattered and lack a unified presentation. We develop a new diagrammatic method for constructing algebraic curves connecting nilpotent orbits of different Jordan types, which streamlines the cumbersome notation in existing approaches and offers a clearer guide to the constructive arguments. In addition, motivated by the historical difficulty of the case-by-case analysis, we formalize the cover relations in the dominance order of admissible partitions of classical types in Lean 4, providing a practical example of human-AI collaboration for modern mathematical formalization.
引言
李代数幂零轨道是几何表示论的经典研究对象，对其分类和闭包支配关系的研究是理解 Springer 纤维、Weyl 群表示等更深刻几何结构的必要基础．李代数的幂零轨道定义为适当代数群 \(G\) 在李代数 \(\mathfrak g\) 上作用得到的幂零元素的轨道，一般认为作用群应当选取适当表征共轭作用的连通代数群 [1, section 1.2]．本文讨论复数域 \(\mathbb C\) 上经典李代数的幂零轨道的分类和闭包支配关系．设 \(V\) 是域上 \(n\) 维线性空间，所谓经典李代数，即是单李代数中寄居在线性李代数 \(\mathfrak{gl}(V)\) 中的：
- A 型李代数：即特殊线性李代数 \(\mathfrak{sl}(V)\)，\(A_n\) 型对应 \(\dim V = n+1\)．
- C 型李代数：即辛李代数 \(\mathfrak{sp}(V)\)，\(C_n\) 型对应 \(\dim V = 2n\)．
- B 型和 D 型李代数：即正交李代数 \(\mathfrak{so}(V)\)，\(B_n\) 型对应 \(\dim V = 2n+1\)，\(D_n\) 型对应 \(\dim V = 2n\)．
在经典李代数的情形，一般并不严格要求定义幂零轨道的作用群作为代数群连通，习惯上有如下多种取法：所有经典李代数的作用群都可以取一般线性群 \(\mathrm{GL}(V)\)，此时幂零轨道的分类由 Jordan 标准型给出．特别地，\(\mathfrak{sl}(V)\) 的作用群还可以取特殊线性群 \(\mathrm{SL}(V)\)；\(\mathfrak{sp}(V)\) 的作用群可以取辛群 \(\operatorname{Sp}(V)\)；\(\mathfrak{so}(V)\) 的作用群可以取特殊正交群 \(\operatorname{SO}(V)\) 或正交群 \(O(V)\)．注意正交群 \(O(V)\) 并不连通，\(\operatorname{SO}(V)\) 是它的连通子群．不同作用群的选择可能导致粒度不同的轨道分类结果．例如在 \(D\) 型李代数中，正交群作用下的部分幂零轨道可能在特殊正交群作用下出现分支情况．在没有特殊说明的情况下，本文所指幂零轨道在 A 型李代数中均选取 \(\mathrm{GL}(V)\) 作为作用群，在 B、C、D 型李代数中均选取相应非退化双线性型的保距群作为作用群，即 C 型取辛群 \(\operatorname{Sp}(V)\)，B、D 型取正交群 \(O(V)\)．
本文的工作主要分为以下三部分．一是介绍复数域 \(\mathbb C\) 上经典李代数幂零轨道的 Jordan 型分类理论．这一部分主要跟随 [2, section 1] 的呈现，即先证明 Jordan 型是轨道分类的完全不变量，再给出合法分拆的构造和必要性证明．主要的不同是，我们在 经典李代数的 Jacobson–Morozov 定理 介绍了幂零轨道分类的结果和 Jacobson–Morozov 定理的联系，并借此在 表示论风格的分类重证 提供了幂零轨道分类的另一表示论风格的简明证明．我们注意到这一视角在 [3] 中曾被提及，与 [1, section 5.1] 给出的证明也有一定相似之处，但尚无文献对此做系统展开．
二是建立复数域 \(\mathbb C\) 上经典李代数幂零轨道上的支配序．关于幂零轨道支配序的研究历史，[2, section 13.16] 和 [1, theorem 6.2.5] 给出了一些评注．[4] 最早建立了经典李代数上幂零轨道闭包关系与分拆支配序的联系，但他在 [4, section 3.2, p. 567] 讨论 B、C、D 型合法分拆支配序的盖住关系时漏掉了几种情况．[5, proposition 3.9, theorem 3.10] 修补了这一漏洞．据我们所知，经典李代数上幂零轨道支配序的完整证明，尤其是对于 B、C、D 型李代数，尚未在文献中系统地呈现过．我们选取的路线独立于上述文献：对 A 型李代数，将基于盖住关系的路径构造和秩函数的下半连续性，给出支配序和分拆上的支配序的等价性证明；对于 B、C、D 型李代数，我们选取特定方便处理的非退化双线性型，仔细为其上的每一类盖住关系显式构建落在斜自伴李代数中的代数曲线．在此过程中，我们开发了一类组合图示为这些曲线的构造给出统一紧凑地描述，较大程度上为繁复的分类讨论提供了直观的指导．
三是完成了经典李代数中合法分拆支配序的盖住关系刻画的形式化验证．B、C、D 型合法分拆支配序的盖住关系的刻画需要大量分类讨论，每种情况的验证平凡而繁琐，而一旦遗漏便会导致不完整的结果．鉴于以往文献中已经出现过类似先例，我们认为除给出自然语言证明之外，对这一部分进行形式化验证亦具有一定必要性．形式化数学滥觞于 Hilbert 的符号化和形式主义哲学，其认为数学定理和数学证明的本质是将形式系统中按照固定规则进行的符号操作．计算机可以被用来执行这些符号操作，从而验证数学定理和证明的正确性．近年来，形式化验证工具的不断发展成熟，越来越多或经典、或前沿的数学研究成果正在接受形式化验证的检验 [6], [7]．与此同时，2022 年以来大语言模型（LLM）热潮方兴未艾，2025 年以来 agent 技术快速发展，函数式编程语言可验证性和强交互性的优势得以充分体现，AI 技术的进步为数学形式化验证工作提供了新的可能 [8]．为此，我们选取 Lean 4 证明助手 [9] 作为形式化验证的工具，使用 mathlib4 数学库 [10], [11] 作为形式化验证的基础，利用 OpenAI 的 GPT 5.5 模型 [12] 和 Codex coding agent [13] 辅助完成了各型合法分拆支配序盖住关系刻画的形式化验证．我们在 附录 B — 形式化验证 介绍形式化验证工作的细节，尤其是使用 AI 辅助完成形式化验证的实践经验．实验表明，对涉及大量繁琐分类讨论的数学结果，由人类给出证明思路、LLM 补全证明细节、coding agent 完成具体形式化验证的人机分工协作，或将成为多快好省完成数学形式化验证工作的新范式；而几何表示论领域丰富的组合对象和对构造性证明的需求，或将使其成为形式化数学和 AI4Math 的理想试验场．