编辑“︁Lean范畴论库”︁（章节）

= Lean范畴论库 =

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

范畴论作为"数学的数学"，在Lean中扮演着连接不同数学领域的桥梁角色。通过这个库，用户能够：
* 形式化抽象数学结构
* 验证范畴论命题的正确性
* 构建更复杂的数学理论框架
* 实现跨领域的数学概念转换

== 核心概念 ==

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

<syntaxhighlight lang="lean">
-- 范畴的基本结构
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))
</syntaxhighlight>

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

=== 函子与自然变换 ===
函子（Functor）是保持范畴结构的映射：

<syntaxhighlight lang="lean">
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)
</syntaxhighlight>

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

<syntaxhighlight lang="lean">
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)
</syntaxhighlight>

== 示例与应用 ==

=== 简单范畴示例 ===
定义一个离散范畴（Discrete Category）：

<syntaxhighlight lang="lean">
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) }
</syntaxhighlight>

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

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

<syntaxhighlight lang="lean">
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 }
</syntaxhighlight>

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

<syntaxhighlight lang="lean">
def product (X Y : C) [HasProduct X Y] := limit (pair X Y)

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

== 高级主题 ==

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

<mermaid>
graph LR
  C[范畴C] -->|左伴随F| D[范畴D]
  D -->|右伴随G| C
  F -.-|伴随同构| G
</mermaid>

在Lean中的形式化：

<syntaxhighlight lang="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))
</syntaxhighlight>

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

<syntaxhighlight lang="lean">
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)
-- 省略结合子、单位子等公理...
</syntaxhighlight>

== 应用案例 ==

=== 代数拓扑中的应用 ===
使用范畴论库定义基本群：

<syntaxhighlight lang="lean">
def FundamentalGroup (X : Top) (x : X) : Group :=
{ carrier := pathComponent x ⥤ pathComponent x,
  mul := λ f g, f ≫ g,
  one := 𝟭 _,
  inv := λ f, leftQuasiInverse f }
</syntaxhighlight>

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

<mermaid>
graph TB
  Syntax[语法范畴] -->|[[_]]| Denotation[指称范畴]
  Equations[程序方程] -->|通过函子| SemanticEq[语义等式]
</mermaid>

对应Lean形式化：

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

== 学习建议 ==

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

对于高级用户，可以：
* 研究库的底层实现技巧
* 为数学库贡献新定义和定理
* 开发特定领域的范畴论扩展
* 探索高阶范畴论的形式化

== 参见 ==
* [[Lean定理证明器]]
* [[形式化数学]]
* [[依赖类型理论]]
* [[范畴论基础]]

[[Category:Lean数学库]]
[[Category:形式化数学]]
[[Category:范畴论]]

[[Category:计算机科学]]
[[Category:Lean]]
[[Category:Lean与数学库]]