跳到主要内容

Lean 范畴论基础

引言​

范畴论是现代数学中的一个重要分支，它研究的是数学结构之间的关系。在编程语言中，范畴论的概念被广泛应用于函数式编程、类型系统设计等领域。Lean作为一种交互式定理证明器，支持范畴论的形式化定义和推理。本文将带你了解Lean中范畴论的基础知识，并通过代码示例和实际案例帮助你掌握这些概念。

什么是范畴？​

范畴（Category）是范畴论中的基本概念。一个范畴由以下两部分组成：

  1. 对象（Objects）：范畴中的元素，可以是任何数学结构，如集合、群、拓扑空间等。
  2. 态射（Morphisms）：对象之间的箭头，表示对象之间的关系。态射需要满足结合律和单位律。

在Lean中，我们可以定义一个范畴如下：

lean
import category_theory.category

open category_theory

structure Category :=
  (Obj : Type)
  (Hom : Obj → Obj → Type)
  (id : Π (X : Obj), Hom X X)
  (comp : Π {X Y Z : Obj}, Hom X Y → Hom Y Z → Hom X Z)
  (id_comp : ∀ {X Y : Obj} (f : Hom X Y), comp (id X) f = f)
  (comp_id : ∀ {X Y : Obj} (f : Hom X Y), comp f (id Y) = f)
  (assoc : ∀ {W X Y Z : Obj} (f : Hom W X) (g : Hom X Y) (h : Hom Y Z),
    comp (comp f g) h = comp f (comp g h))

解释​

  • Obj 表示范畴中的对象类型。
  • Hom X Y 表示从对象 X 到对象 Y 的态射集合。
  • id X 是对象 X 的恒等态射。
  • comp f g 是态射 f 和 g 的复合。
  • id_comp 和 comp_id 保证了恒等态射的性质。
  • assoc 保证了态射的复合满足结合律。

函子​

函子（Functor）是范畴之间的映射。它由两部分组成：

  1. 对象映射：将一个范畴的对象映射到另一个范畴的对象。
  2. 态射映射：将一个范畴的态射映射到另一个范畴的态射，并保持复合和恒等态射的性质。

在Lean中，函子可以定义如下：

lean
structure Functor (C D : Category) :=
  (obj : C.Obj → D.Obj)
  (map : Π {X Y : C.Obj}, C.Hom X Y → D.Hom (obj X) (obj Y))
  (map_id : ∀ (X : C.Obj), map (C.id X) = D.id (obj X))
  (map_comp : ∀ {X Y Z : C.Obj} (f : C.Hom X Y) (g : C.Hom Y Z),
    map (C.comp f g) = D.comp (map f) (map g))

解释​

  • obj 是对象映射函数。
  • map 是态射映射函数。
  • map_id 保证了恒等态射的映射性质。
  • map_comp 保证了态射复合的映射性质。

自然变换​

自然变换（Natural Transformation）是函子之间的映射。给定两个函子 F 和 G，自然变换 η 将 F 的每个对象映射到 G 的对应对象，并且满足自然性条件。

在Lean中，自然变换可以定义如下：

lean
structure NaturalTransformation {C D : Category} (F G : Functor C D) :=
  (app : Π (X : C.Obj), D.Hom (F.obj X) (G.obj X))
  (naturality : ∀ {X Y : C.Obj} (f : C.Hom X Y),
    D.comp (F.map f) (app Y) = D.comp (app X) (G.map f))

解释​

  • app X 是自然变换在对象 X 上的分量。
  • naturality 保证了自然变换的自然性条件。

实际案例：集合范畴​

集合范畴（Category of Sets）是一个常见的范畴，其对象是所有集合，态射是集合之间的函数。我们可以用Lean来定义集合范畴：

lean
def Set : Category :=
{ Obj := Type,
  Hom := λ X Y, X → Y,
  id := λ X x, x,
  comp := λ X Y Z f g, g ∘ f,
  id_comp := by intros; refl,
  comp_id := by intros; refl,
  assoc := by intros; refl }

解释​

  • Obj 是 Type，表示所有集合。
  • Hom X Y 是 X → Y，表示集合 X 到集合 Y 的函数。
  • id 是恒等函数。
  • comp 是函数的复合。
  • id_comp、comp_id 和 assoc 保证了函数的性质。

总结​

本文介绍了Lean中范畴论的基础知识，包括范畴、函子和自然变换的定义，并通过集合范畴的实际案例展示了这些概念的应用。范畴论是一个强大的工具，它在数学和计算机科学中有着广泛的应用。

附加资源​

练习​

  1. 定义一个群范畴（Category of Groups），其对象是群，态射是群同态。
  2. 定义一个函子，将集合范畴映射到群范畴。
  3. 定义一个自然变换，将两个函子之间的映射关系表示出来。

通过完成这些练习，你将更深入地理解Lean中的范畴论概念。