⚡

范畴函子技能Skill categories-functors

这个技能用于在范畴论中处理和验证函子相关问题，提供问题解决策略，利用Lean 4编程语言进行数学证明和编译器验证。它覆盖范畴公理检查、函子性质验证、常见函子类型以及使用Lean 4工具进行高效验证。关键词：范畴论，函子，Lean 4，数学证明，编译器验证，问题解决策略。

无 0 次安装 0 次浏览 更新于 3/14/2026

name: categories-functors description: “范畴论中范畴函子的问题解决策略” allowed-tools: [Bash, Read]

范畴函子

何时使用

当在范畴论中处理范畴-函子问题时使用此技能。

决策树

  1. 验证范畴公理

    • 对象和态射（箭头）是否已定义？
    • 每个对象的恒等态射：id_A: A -> A
    • 复合结合律：(f . g) . h = f . (g . h)
    • 编写 Lean 4：theorem assoc : (f ≫ g) ≫ h = f ≫ (g ≫ h) := Category.assoc

  2. 检查函子性质

    • F: C -> D 映射对象到对象，箭头到箭头
    • 保持恒等：F(id_A) = id_{F(A)}
    • 保持复合：F(g . f) = F(g) . F(f)
    • 编写 Lean 4：theorem comp : F.map (g ≫ f) = F.map g ≫ F.map f := F.map_comp

  3. 函子类型

    • 协变：保持箭头方向
    • 逆变：反转箭头方向
    • 忠实/满：在 Hom-集上单射/满射
    • 等价：满、忠实、本质满射

  4. 常见函子

    • 遗忘函子：忘记结构（例如，Grp -> Set）
    • 自由函子：遗忘函子的左伴随
    • Hom 函子：Hom(A, -) 或 Hom(-, B)
    • 幂集函子：Set -> Set 通过 X |-> P(X)

  5. 使用 Lean 4 验证

    • 编译器在循环中：编写证明，lake build 检查
    • Mathlib 拥有完整的范畴论库
    • 参见：.claude/skills/lean4-functors/SKILL.md 获取确切语法

工具命令

Lean4_Category

# Lean 4 with Mathlib: import CategoryTheory.Category.Basic

Lean4_Functor

# Lean 4: theorem map_comp (F : C ⥤ D) : F.map (g ≫ f) = F.map g ≫ F.map f := F.map_comp

Lean4_Build

lake build  # 编译器在循环中验证

认知工具参考

参见 .claude/skills/math-mode/SKILL.md 获取完整工具文档。