用途
该技能用于处理范畴论中的自然变换（natural transformations）问题。当你在范畴论中遇到 natural-transformations 相关问题时，可使用本技能。
主要能力
技能以决策树形式组织，覆盖以下内容：
验证自然性
eta: F => G 是函子 F, G: C -> D 之间的自然变换。对 C 中每个 f: A -> B，下图交换：
G(f) . eta_A = eta_B . F(f)
Lean 4 写法：
theorem nat : η.app B ≫ G.map f = F.map f ≫ η.app A := η.naturality
分量分析
eta_A: F(A) -> G(A) 对每个对象 A 成立。每个分量是目标范畴 D 中的态射。
Lean 4 写法：
def η : F ⟶ G where app := fun X => ...
自然同构
每个分量 eta_A 都是同构，则函子 F 与 G 自然同构。记号：F ≅ G（Mathlib 中为 NatIso）。
函子范畴
[C, D] 以函子为对象，以自然变换为态射。
垂直复合：Lean 4 CategoryTheory.NatTrans.vcomp
水平复合：CategoryTheory.NatTrans.hcomp
米田引理应用
Nat(Hom(A, -), F) ~ F(A) 关于 A 自然。
Lean 4：CategoryTheory.yonedaEquiv
将 C 完全嵌入 [C^op, Set]。
精确语法参见：.claude/skills/lean4-nat-trans/SKILL.md
使用方式
技能提供以下工具命令：
-
Lean4_Naturality
Lean 4: theorem nat : η.app B ≫ G.map f = F.map f ≫ η.app A := η.naturality
-
Lean4_Nat_Trans
Lean 4: def η : F ⟶ G where app := fun X => component_X
-
Lean4_Yoneda
Lean 4: CategoryTheory.yonedaEquiv -- Yoneda lemma
-
Lean4_Build
lake build # Compiler-in-the-loop verification
完整工具文档参见：.claude/skills/math-mode/SKILL.md
适用场景
适用于在 Lean 4 与 Mathlib 环境下进行范畴论中自然变换相关的证明、构造与验证工作，包括自然性证明、自然变换定义、自然同构判定、函子范畴中的复合操作以及米田引理的应用。
限制
关于该技能的具体收费、价格、支持平台、实际效果等事实，资料中暂未提供。