⚡

极限与余极限问题解决技能Skill limits-colimits

本技能用于解决范畴论中极限和余极限的问题，提供策略如识别极限类型、验证通用性质、具体计算和检查保持性。使用工具如Lean 4进行形式验证和Sympy进行符号计算，适用于数学研究、定理证明和形式化方法。关键词：范畴论，极限，余极限，问题解决，Lean 4，Sympy，数学验证，形式化方法。

数据分析 0 次安装 0 次浏览 更新于 3/14/2026

name: limits-colimits description: “范畴论中极限与余极限的问题解决策略” allowed-tools: [Bash, Read]

极限与余极限

何时使用

当处理范畴论中的极限-余极限问题时使用此技能。

决策树

  1. 识别极限类型

    • 积：离散图的极限
    • 等值子：平行对 f, g: A -> B 的极限
    • 拉回：A -> C <- B 的极限
    • 终对象：空图的极限
    • Lean 4: CategoryTheory.Limits 命名空间

  2. 验证通用性质

    • 来自 L 的锥，带有投影 pi_i: L -> D_i
    • 对于任何来自 X 的锥，唯一态射 u: X -> L
    • 三角形交换：pi_i . u = cone_i
    • Lean 4: IsLimit.lift 给出唯一态射

  3. 余极限（对偶）

    • 余积：离散图的余极限
    • 余等值子：平行对的余极限
    • 推出：A <- C -> B 的余极限
    • 始对象：空图的余极限

  4. 具体计算极限

    • 在集合中：积 = 笛卡尔积
    • 等值子 = {x | f(x) = g(x)}
    • 拉回 = {(a,b) | f(a) = g(b)}
    • sympy_compute.py solve "f(a) == g(b)"

  5. 保持性

    • 右伴随保持极限
    • 左伴随保持余极限
    • 可表示函子保持极限
    • Lean 4: Adjunction.rightAdjointPreservesLimits
    • 查看：.claude/skills/lean4-limits/SKILL.md 获取确切语法

工具命令

Lean4_Limit

# Lean 4: import CategoryTheory.Limits.Shapes.Products

Lean4_Universal

# Lean 4: IsLimit.lift cone -- 来自通用性质的唯一态射

Sympy_Pullback

uv run python -m runtime.harness scripts/sympy_compute.py solve "f(a) == g(b)"

Lean4_Build

lake build  # 编译器在环验证

认知工具参考

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