Lean域

Lean域

Lean域（Field in Lean）是Lean定理证明器中用于表示数学域（Field）概念的抽象结构。在数学中，域是一种具备加法、乘法、减法、除法运算的代数结构，满足交换律、结合律、分配律等基本性质。在Lean中，域通过类型类（Type Class）实现，为程序员和数学家提供了形式化验证的基础。

定义与基本性质

数学上，域是一个集合$F$，配备两种二元运算（加法$+$和乘法$\cdot$），满足以下条件： 1. $(F,+)$构成一个交换群，其单位元记作$0$。 2. $(F\setminus \{0\},\cdot )$构成一个交换群，其单位元记作$1$。 3. 乘法对加法满足分配律：$a\cdot (b+c)=a\cdot b+a\cdot c$。

在Lean中，域的定义通过`Field`类型类实现，继承自`DivisionRing`（除环）和`CommRing`（交换环）。

class Field (α : Type u) extends DivisionRing α, CommRing α

基本示例

以下是Lean中定义和使用域的几个示例：

有理数域

Lean标准库中已经定义了有理数域ℚ（`Rat`类型），可以直接使用：

import Mathlib.Data.Rat.Basic

example : Field ℚ := by infer_instance

自定义有限域

定义一个有限域${\mathbb{𝔽}}_5$（模5的域）：

import Mathlib.Algebra.Field.Defs

def F5 := Fin 5

instance : Field F5 :=
  { Fin.instFieldFin 5 with }  -- 5是质数，因此Fin 5构成域

验证其性质：

#check Field F5  -- 输出: Field F5

运算与定理

域支持所有基本算术运算，并且可以验证域的性质。

基本运算

variable {F : Type} [Field F]

example (a b : F) : a + b = b + a := add_comm a b
example (a : F) : a * 1 = a := mul_one a
example (a : F) (ha : a ≠ 0) : a * a⁻¹ = 1 := mul_inv_cancel ha

域的特征

域的特征（characteristic）是指加法单位元$1$的阶。若$n\cdot 1=0$的最小正整数$n$存在，则称域的特征为$n$，否则为0。

import Mathlib.Algebra.CharP.Basic

example : CharZero ℚ := by infer_instance  -- ℚ的特征是0
example : CharP (ZMod 5) 5 := by infer_instance  -- 𝔽₅的特征是5

实际应用案例

线性代数

域是线性代数的基础，例如向量空间的定义依赖于域：

import Mathlib.LinearAlgebra.Basic

variable (F : Type) [Field F]
variable (V : Type) [AddCommGroup V] [Module F V]

-- V是F上的向量空间
example : Module F V := by infer_instance

多项式因式分解

在域上，多项式可以唯一分解为不可约多项式的乘积：

import Mathlib.Data.Polynomial.FieldDivision

variable {F : Type} [Field F] [DecidableEq F]

example (p : Polynomial F) : p ≠ 0 → ∃ (q : Polynomial F), Irreducible q ∧ q ∣ p :=
  Polynomial.exists_irreducible_factor

图表表示

域的继承关系可以用Mermaid图表示：

classDiagram Ring <|-- CommRing DivisionRing <|-- Field CommRing <|-- Field

总结

Lean中的域（`Field`）是形式化数学中重要的代数结构，广泛应用于线性代数、数论和代数几何等领域。通过类型类机制，Lean能够高效地处理域的性质，并用于定理证明和算法验证。