Lean范畴论库[编辑 | 编辑源代码]

介绍[编辑 | 编辑源代码]

Lean范畴论库是Lean定理证明器数学库（mathlib）中实现范畴论基础结构的核心模块。它为形式化数学提供了范畴、函子、自然变换等抽象概念的严格定义，并支持高阶数学结构的机器验证。该库的设计遵循数学惯例，同时充分利用Lean的类型系统和依赖类型特性。

范畴论作为"数学的数学"，在Lean中扮演着连接不同数学领域的桥梁角色。通过这个库，用户能够：

形式化抽象数学结构
验证范畴论命题的正确性
构建更复杂的数学理论框架
实现跨领域的数学概念转换

核心概念[编辑 | 编辑源代码]

基本定义[编辑 | 编辑源代码]

在Lean范畴论库中，核心概念被定义为类型类（typeclass）：

-- 范畴的基本结构
class Category (obj : Type u) (hom : obj → obj → Type v) :=
(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))

这个定义包含了范畴理论的五个基本公理： 1. 每个对象都有恒等态射（id） 2. 态射的可组合性（comp） 3. 恒等态射的左单位元律（id_comp） 4. 恒等态射的右单位元律（comp_id） 5. 态射组合的结合律（assoc）

函子与自然变换[编辑 | 编辑源代码]

函子（Functor）是保持范畴结构的映射：

structure Functor (C : Type u₁) [Category C] (D : Type u₂) [Category D] :=
(obj : C → D)
(map : ∀ {X Y : C}, (X ⟶ Y) → (obj X ⟶ obj Y))
(map_id' : ∀ (X : C), map (𝟙 X) = 𝟙 (obj X) . obviously)
(map_comp' : ∀ {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z), 
  map (f ≫ g) = (map f) ≫ (map g) . obviously)

自然变换（Natural Transformation）则是函子间的态射：

structure NatTrans (F G : C ⥤ D) :=
(app : ∀ X : C, F.obj X ⟶ G.obj X)
(naturality' : ∀ {X Y : C} (f : X ⟶ Y), 
  F.map f ≫ app Y = app X ≫ G.map f . obviously)

示例与应用[编辑 | 编辑源代码]

简单范畴示例[编辑 | 编辑源代码]

定义一个离散范畴（Discrete Category）：

instance discreteCategory (α : Type u) : Category α :=
{ hom := λ X Y, PLift (X = Y),
  id := λ X, PLift.up rfl,
  comp := λ X Y Z f g, PLift.up (Eq.trans f.down g.down) }

这个实例展示了如何构造一个对象间只有恒等态射的范畴。

极限与余极限[编辑 | 编辑源代码]

Lean范畴论库完整定义了极限（Limit）概念：

def limit {J C : Type u} [Category J] [Category C] (F : J ⥤ C) :=
{ cone := Cone F,
  is_limit := ∀ (s : Cone F), ∃! (f : s.X ⟶ cone.X), 
    ∀ j : J, f ≫ cone.π.app j = s.π.app j }

实际计算积（Product）的例子：

def product (X Y : C) [HasProduct X Y] := limit (pair X Y)

-- 使用示例
#check (prod.fst : X ⨯ Y ⟶ X)  -- 投影第一个分量
#check (prod.snd : X ⨯ Y ⟶ Y)  -- 投影第二个分量

高级主题[编辑 | 编辑源代码]

伴随函子[编辑 | 编辑源代码]

伴随（Adjunction）是范畴论中的重要概念：

在Lean中的形式化：

structure Adjunction (F : C ⥤ D) (G : D ⥤ C) :=
(unit : 𝟭 C ⟶ F ⋙ G)
(counit : G ⋙ F ⟶ 𝟭 D)
(adj1 : ∀ X : C, (unit.app X ≫ G.map (counit.app (F.obj X))) = 𝟙 (F.obj X))
(adj2 : ∀ Y : D, (F.map (unit.app (G.obj Y)) ≫ counit.app Y) = 𝟙 (G.obj Y))

幺半范畴[编辑 | 编辑源代码]

幺半范畴（Monoidal Category）的定义展示了库的表达能力：

class MonoidalCategory (C : Type u) [Category C] :=
(tensorObj : C → C → C)
(tensorHom : ∀ {X₁ Y₁ X₂ Y₂}, (X₁ ⟶ Y₁) → (X₂ ⟶ Y₂) → (tensorObj X₁ X₂ ⟶ tensorObj Y₁ Y₂))
(tensorUnit : C)
-- 省略结合子、单位子等公理...

应用案例[编辑 | 编辑源代码]

代数拓扑中的应用[编辑 | 编辑源代码]

使用范畴论库定义基本群：

def FundamentalGroup (X : Top) (x : X) : Group :=
{ carrier := pathComponent x ⥤ pathComponent x,
  mul := λ f g, f ≫ g,
  one := 𝟭 _,
  inv := λ f, leftQuasiInverse f }

程序语言语义[编辑 | 编辑源代码]

用范畴论建模程序语言的指称语义：

对应Lean形式化：

def DenotationalSemantics : Syntax ⥤ Denotation :=
{ obj := λ P, ⟦P⟧,
  map := λ P Q f, ⟦f⟧,
  map_id' := by /- 证明恒等映射 -/,
  map_comp' := by /- 证明组合律 -/ }

学习建议[编辑 | 编辑源代码]

对于初学者，建议按照以下路径学习： 1. 先掌握Lean基础语法和类型论 2. 理解范畴论的基本概念（范畴、函子、自然变换） 3. 通过简单实例熟悉库的基本用法 4. 逐步探索高级概念如极限、伴随等 5. 尝试形式化经典数学定理

对于高级用户，可以：

研究库的底层实现技巧
为数学库贡献新定义和定理
开发特定领域的范畴论扩展
探索高阶范畴论的形式化

参见[编辑 | 编辑源代码]