跳到主要内容

Lean 同态与同构

在代数结构中，**同态（Homomorphism）和同构（Isomorphism）**是两个非常重要的概念。它们描述了不同代数结构之间的映射关系，帮助我们理解这些结构之间的相似性和差异性。本文将详细介绍这两个概念，并通过Lean代码示例和实际案例帮助你更好地理解它们。

1. 什么是同态？​

同态是一种保持结构的映射。具体来说，如果我们在两个代数结构之间有一个映射，并且这个映射保持了结构中的运算，那么这个映射就是一个同态。

1.1 同态的定义​

假设我们有两个代数结构 (A, *) 和 (B, ·)，其中 * 和 · 分别是 A 和 B 上的二元运算。一个映射 f: A → B 被称为同态，如果对于所有的 a₁, a₂ ∈ A，都有：

f(a₁ * a₂) = f(a₁) · f(a₂)

这意味着，f 将 A 中的运算结果映射到 B 中相应的运算结果。

1.2 Lean中的同态示例​

让我们通过一个简单的例子来理解同态。假设我们有两个集合 A 和 B，分别定义了加法运算。我们可以定义一个同态映射 f，将 A 中的元素映射到 B 中。

lean
structure AdditiveGroup where
  carrier : Type
  add : carrier → carrier → carrier
  zero : carrier
  neg : carrier → carrier

def homomorphism (A B : AdditiveGroup) (f : A.carrier → B.carrier) : Prop :=
  ∀ a₁ a₂ : A.carrier, f (A.add a₁ a₂) = B.add (f a₁) (f a₂)

在这个例子中，homomorphism 函数检查映射 f 是否是一个同态。如果 f 满足 f(a₁ + a₂) = f(a₁) + f(a₂)，那么 f 就是一个同态。

2. 什么是同构？​

同构是一种特殊的同态，它不仅保持结构，而且是一个双射（即既单射又满射）。这意味着两个代数结构在某种意义上“完全相同”。

2.1 同构的定义​

假设我们有两个代数结构 (A, *) 和 (B, ·)，一个映射 f: A → B 被称为同构，如果：

  1. f 是一个同态。
  2. f 是一个双射。

如果存在一个同构映射 f，那么我们说 A 和 B 是同构的，记作 A ≅ B。

2.2 Lean中的同构示例​

让我们继续使用前面的 AdditiveGroup 结构，定义一个同构映射。

lean
def isomorphism (A B : AdditiveGroup) (f : A.carrier → B.carrier) : Prop :=
  homomorphism A B f ∧ bijective f

在这个例子中，isomorphism 函数检查映射 f 是否是一个同构。如果 f 是一个同态并且是双射的，那么 f 就是一个同构。

3. 实际案例​

3.1 整数加法群与偶数加法群​

考虑整数加法群 (ℤ, +) 和偶数加法群 (2ℤ, +)。我们可以定义一个映射 f: ℤ → 2ℤ，其中 f(n) = 2n。这个映射是一个同态，因为：

f(n + m) = 2(n + m) = 2n + 2m = f(n) + f(m)

此外，f 是一个双射，因此 f 是一个同构。这意味着 ℤ 和 2ℤ 是同构的。

3.2 Lean中的实现​

lean
def int_to_even (n : ℤ) : ℤ := 2 * n

theorem int_even_isomorphism :
  isomorphism (AdditiveGroup.mk ℤ int.add 0 int.neg) (AdditiveGroup.mk ℤ int.add 0 int.neg) int_to_even :=
begin
  -- 证明 int_to_even 是一个同构
  sorry
end

在这个例子中，我们定义了 int_to_even 映射，并尝试证明它是一个同构。

4. 总结​

同态和同构是代数结构中非常重要的概念。同态描述了代数结构之间的映射关系，而同构则进一步描述了这些结构之间的“相同性”。通过Lean代码示例和实际案例，我们展示了如何定义和验证同态与同构。

5. 附加资源与练习​

  • 练习1：定义一个从 (ℤ, +) 到 (ℤ, ×) 的映射，并验证它是否是一个同态。
  • 练习2：证明 (ℤ, +) 和 (ℚ, +) 不是同构的。
提示

如果你对Lean中的代数结构感兴趣，可以进一步学习群论、环论和域论等内容，这些内容在Lean中都有丰富的支持。