哈德-纳拉辛汉理论的形式化
代数几何
2026-02-17 v3 形式语言与自动机理论
计算机科学中的逻辑
数论
摘要
哈德-纳拉辛汉理论为射影曲线上的向量丛提供了一个规范滤过，其逐次商是斜率严格递减的半稳定丛。在本文中，我们展示了在证明助手Lean 4及其数学库Mathlib中对哈德-纳拉辛汉理论的形式化。该形式化基于Chen和Jeannin最近提出的哈德-纳拉辛汉理论方法，该方法以序理论术语重新解释该理论，并避免了经典上对代数几何的依赖。作为一个应用，我们形式化了诺特环上有限生成模的余准素滤过的唯一性，以及半稳定哈德-纳拉辛汉博弈的若尔当-赫尔德滤过的存在性。代码可在以下地址获取：https://github.com/YijunYuan/HarderNarasimhan
引用
@article{arxiv.2509.19632,
title = {Formalization of Harder-Narasimhan theory},
author = {Yijun Yuan},
journal= {arXiv preprint arXiv:2509.19632},
year = {2026}
}
备注
31 pages