编辑“︁Lean代数学基础”︁

{{DISPLAYTITLE:Lean代数学基础}}

'''Lean代数学基础'''是使用[[Lean定理证明器]]进行形式化数学研究时所需的核心代数概念集合。本条目将系统介绍如何在Lean中表示和操作基本代数结构，包括群、环、域等抽象代数对象，并提供实际的形式化证明示例。

== 基本概念 ==

在Lean中，代数学结构通过'''类型类(type class)'''机制实现。这种设计允许数学家以高度抽象的方式定义代数结构，同时保持严格的类型安全性。

=== 主要代数结构 ===
Lean数学库<code>mathlib</code>定义了以下基础结构（按层级排序）：
* '''半群(Semigroup)'''：具有封闭的二元运算
* '''幺半群(Monoid)'''：含单位元的半群
* '''群(Group)'''：含逆元的幺半群
* '''环(Ring)'''：具有加法群和乘法幺半群结构
* '''域(Field)'''：非零元构成乘法群的交换环

== 形式化示例 ==

=== 群的定义 ===
以下是Lean中群的定义简化表示：

<syntaxhighlight lang="lean">
class Group (G : Type u) where
  mul : G → G → G
  one : G
  inv : G → G
  mul_assoc : ∀ (x y z : G), mul (mul x y) z = mul x (mul y z)
  mul_one : ∀ (x : G), mul x one = x
  one_mul : ∀ (x : G), mul one x = x
  mul_left_inv : ∀ (x : G), mul (inv x) x = one
</syntaxhighlight>

=== 实际证明示例 ===
证明群中单位元唯一：

<syntaxhighlight lang="lean">
theorem group_unit_unique (G : Type) [Group G] : 
  ∀ (e : G), (∀ x : G, mul e x = x) → e = one :=
begin
  intros e h,
  specialize h one,
  rw [←one_mul e, h],
end
</syntaxhighlight>

'''输出'''：Lean成功验证此证明，确认在任何群中满足"∀ x, e * x = x"的元素e必定等于群的单位元<code>one</code>。

== 图表表示 ==
代数结构继承关系可通过以下图表展示：

<mermaid>
graph TD
    A[Semigroup] --> B[Monoid]
    B --> C[Group]
    C --> D[CommGroup]
    B --> E[CommMonoid]
    A --> F[AddSemigroup]
    F --> G[AddMonoid]
    G --> H[AddGroup]
</mermaid>

== 高级主题 ==

=== 商群构造 ===
Lean中可以使用<code>quotient_group</code>构造商群：

<syntaxhighlight lang="lean">
import group_theory.quotient_group

variables {G : Type} [group G] (N : subgroup G) [normal_subgroup N]

example : group (quotient_group.quotient N) := 
by apply_instance
</syntaxhighlight>

=== 多项式环 ===
定义多项式环并证明基本性质：

<syntaxhighlight lang="lean">
import data.polynomial

variables (R : Type) [comm_ring R]

example : comm_ring (polynomial R) := 
by apply_instance
</syntaxhighlight>

== 实际应用案例 ==

'''案例'''：验证对称群S₃的非交换性

<syntaxhighlight lang="lean">
import group_theory.perm_group

def σ : equiv.perm (fin 3) := ![1, 2, 0]
def τ : equiv.perm (fin 3) := ![1, 0, 2]

example : σ * τ ≠ τ * σ :=
begin
  rw [equiv.perm.ext_iff],
  intro h,
  have h0 := h 0,
  simp [σ, τ] at h0,
  contradiction,
end
</syntaxhighlight>

'''解释'''：这个例子构造了S₃中的两个置换σ和τ，通过具体计算证明它们的乘积顺序不可交换。

== 数学公式 ==

在Lean中，代数结构的公理可以表示为：
* 结合律：<math>\forall x y z, (x * y) * z = x * (y * z)</math>
* 单位元：<math>\exists e, \forall x, e * x = x * e = x</math>
* 逆元：<math>\forall x, \exists y, x * y = y * x = e</math>

== 学习建议 ==

1. 从<code>mathlib</code>中的基础结构开始研究
2. 使用<code>#check</code>命令查看已有定理
3. 通过<code>example</code>块尝试简单证明
4. 逐步构建自己的代数结构形式化项目

通过系统学习Lean代数学基础，程序员可以将抽象的数学概念转化为可验证的代码实现，为形式化验证和数学研究奠定坚实基础。

[[Category:计算机科学]]
[[Category:Lean]]
[[Category:Lean数学基础]]