Lean同态与同构

Lean同态与同构

介绍

在抽象代数和形式化数学中，同态（Homomorphism）和同构（Isomorphism）是描述代数结构之间关系的重要概念。在Lean中，这些概念通过类型类和函数形式化，用于证明结构之间的映射性质。

• 同态：指两个代数结构之间的映射，保持结构的运算或关系。例如，群同态保持群运算，环同态同时保持加法和乘法。
• 同构：是一种特殊的同态，要求映射是双射（即一一对应），且其逆映射也是同态。同构的结构在代数意义上是“相同的”。

数学定义

设 $(G,*)$ 和 $(H,\cdot )$ 是两个群，函数 $f:G\to H$ 是群同态当且仅当： $\mathrm{\forall }a,b\in G,f(a*b)=f(a)\cdot f(b)$

若 $f$ 是双射，则称 $f$ 为群同构，记作 $G\cong H$。

Lean中的实现

在Lean的数学库Mathlib中，同态和同构通过类型类定义。以下是群同态和同构的示例：

群同态示例

import Mathlib.Algebra.Group.Defs

-- 定义两个群G和H
variables (G H : Type*) [Group G] [Group H]

-- 群同态的结构
structure GroupHomomorphism (f : G → H) : Prop where
  map_mul : ∀ a b : G, f (a * b) = f a * f b

-- 示例：恒等同态
def id_hom : GroupHomomorphism (id : G → G) where
  map_mul := λ a b => rfl

群同构示例

import Mathlib.Algebra.Group.Defs

-- 群同构的结构
structure GroupIsomorphism (f : G → H) extends GroupHomomorphism f where
  bijective : Function.Bijective f

-- 示例：逆映射也是同态
def inv_iso {f : G → H} (iso : GroupIsomorphism f) : GroupIsomorphism (Function.invFun f) :=
  ⟨⟨λ a b => ?_⟩, iso.bijective.2⟩  -- 省略具体证明

实际案例

整数加法群与偶数加法群

考虑整数加法群 $(\mathbb{\mathbb{Z}},+)$ 和偶数加法群 $(2\mathbb{\mathbb{Z}},+)$。映射 $f(n)=2n$ 是一个群同构：

• 同态性：$f(a+b)=2(a+b)=2a+2b=f(a)+f(b)$
• 双射性：存在逆映射 $f^{-1}(x)=x/2$。

在Lean中可形式化为：

def Z_to_2Z : ℤ → ℤ := λ n => 2 * n

lemma Z_iso_2Z : GroupIsomorphism Z_to_2Z := by
  constructor
  · intro a b  -- 证明同态性
    simp [Z_to_2Z, mul_add]
  · apply Function.bijective_iff_has_inverse.2  -- 证明双射性
    exact ⟨λ x => x / 2, by simp, by intro x; exact Int.emod_two_eq_zero_or_one x⟩

图表展示

graph LR G[群 G] -- 同态 f --> H[群 H] H -- 同构 f⁻¹ --> G

高级主题

范畴论视角

在范畴论中，同态和同构是态射的一种。例如：

• 在群范畴（Grp）中，态射是群同态，同构是群同构。
• 在环范畴（Ring）中，态射需同时保持加法和乘法。

自动生成同构

Lean的Mathlib提供了工具（如`@[simps]`）自动生成同构的对称性和传递性：

@[simps]
def mulAut : GroupIsomorphism G G :=
  { toFun := λ g => g * h
    invFun := λ g => g * h⁻¹
    map_mul := by simp [mul_assoc] }

总结

• 同态是保持结构的映射，同构是双向的同态。
• 在Lean中，通过类型类和结构体实现严格的形式化。
• 实际应用包括对称性分析、结构等价性证明等。

通过理解同态与同构，程序员可以更高效地形式化代数问题，并利用Lean的自动化工具简化证明过程。