用途：当在范畴论中处理 categories-functors（范畴与函子）问题时使用该技能，按决策树逐步核对定义与性质。
主要能力：验证范畴公理，包括对象与态射是否定义、每个对象是否有恒等态射 id_A: A -> A、复合是否满足结合律 (f . g) . h = f . (g . h)。检查函子性质，包括 F: C -> D 对对象与箭头的映射、保持恒等 F(id_A) = id_{F(A)}、保持复合 F(g . f) = F(g) . F(f)。区分函子类型：协变、反变、忠实/满、等价（满、忠实、本质满）。列举常见函子：遗忘函子（如 Grp -> Set）、自由函子（遗忘函子的左伴随）、Hom 函子 Hom(A, -) 或 Hom(-, B)、幂集函子 Set -> Set，X |-> P(X)。
使用方式：用 Lean 4 与 Mathlib 编写并验证证明，编译器在环，通过 lake build 检查。示例写法：theorem assoc : (f ≫ g) ≫ h = f ≫ (g ≫ h) := Category.assoc；theorem comp : F.map (g ≫ f) = F.map g ≫ F.map f := F.map_comp；theorem map_comp (F : C ⥤ D) : F.map (g ≫ f) = F.map g ≫ F.map f := F.map_comp。导入方式为 import CategoryTheory.Category.Basic。
适用场景：范畴论学习、形式化证明、需要逐步核对范畴公理与函子性质的数学问题。
限制：具体语法细节需参考 .claude/skills/lean4-functors/SKILL.md，工具文档见 .claude/skills/math-mode/SKILL.md；资料未提供更多实现细节、依赖版本或运行环境要求。