⚡

自然变换Skill natural-transformations

本技能专注于范畴论中自然变换的问题解决策略，提供决策树、Lean 4 工具命令和 Yoneda 引理应用，帮助用户验证自然性、分析分量、处理自然同构和函子范畴。关键词：范畴论、自然变换、Lean 4、Yoneda 引理、数学证明、问题解决、形式化验证。

实验设计 0 次安装 0 次浏览 更新于 3/14/2026

name: natural-transformations description: “范畴论中自然变换的问题解决策略” allowed-tools: [Bash, Read]

自然变换

何时使用

在范畴论中处理自然变换问题时使用此技能。

决策树

  1. 验证自然性

    • 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

  2. 分量分析

    • 对于每个对象 A，eta_A: F(A) -> G(A)
    • 每个分量是目标范畴 D 中的态射
    • Lean 4: def η : F ⟶ G where app := fun X => ...

  3. 自然同构

    • 每个分量 eta_A 是同构
    • 函子 F 和 G 是自然同构的
    • 记法：F ≅ G (在 Mathlib 中为 NatIso)

  4. 函子范畴

    • [C, D] 以函子为对象
    • 自然变换为态射
    • 垂直复合：Lean 4 CategoryTheory.NatTrans.vcomp
    • 水平复合：CategoryTheory.NatTrans.hcomp

  5. Yoneda 引理应用

    • 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 引理

Lean4_Build

lake build  # 编译器在环验证

认知工具参考

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