完全离散赋值环与局部场的形式化

局部场以及关于离散赋值完全的域是交换代数中的基本对象,在数论与代数几何中有应用。我们在 Lean 中形式化了离散赋值域的基本理论。特别地,我们证明了域上关于离散赋值的单位球是离散赋值环,反之,离散赋值环的分式域上的 adic 赋值是离散的。我们定义了赋值与离散赋值环的有限扩张,并证明了一些整体到局部的结果。基于这一一般理论,我们形式化了局部场的抽象定义与若干基本性质。作为一个应用,我们证明了 $p$-进数域 $\mathbb{Q}_p$ 与 $\mathbb{F}_p$ 上的 Laurent 级数域 $\mathbb{F}_p(\!(X)\!)$ 的有限扩张是局部场。