Agent Skills
› parcadei/Continuous-Claude-v3
› limits-colimits
limits-colimits
GitHub提供范畴论中极限与余极限问题的解决策略，涵盖类型识别、泛性质验证及具体计算。
Trigger Scenarios
范畴论极限问题求解
使用Lean4证明极限性质
使用Sympy计算极限
Install
npx skills add parcadei/Continuous-Claude-v3 --skill limits-colimits -g -y
SKILL.md
Frontmatter
{
"name": "limits-colimits",
"description": "Problem-solving strategies for limits colimits in category theory",
"allowed-tools": [
"Bash",
"Read"
]
}
Limits Colimits
When to Use
Use this skill when working on limits-colimits problems in category theory.
Decision Tree
-
Identify Limit Type
- Product: limit of discrete diagram
- Equalizer: limit of parallel pair f, g: A -> B
- Pullback: limit of A -> C <- B
- Terminal object: limit of empty diagram
- Lean 4:
CategoryTheory.Limitsnamespace
-
Verify Universal Property
- Cone from L with projections pi_i: L -> D_i
- For any cone from X, unique morphism u: X -> L
- Triangles commute: pi_i . u = cone_i
- Lean 4:
IsLimit.liftgives the unique morphism
-
Colimit (Dual)
- Coproduct: colimit of discrete diagram
- Coequalizer: colimit of parallel pair
- Pushout: colimit of A <- C -> B
- Initial object: colimit of empty diagram
-
Compute Limits Concretely
- In Set: product = Cartesian product
- Equalizer = {x | f(x) = g(x)}
- Pullback = {(a,b) | f(a) = g(b)}
sympy_compute.py solve "f(a) == g(b)"
-
Preservation
- Right adjoint preserves limits
- Left adjoint preserves colimits
- Representable functors preserve limits
- Lean 4:
Adjunction.rightAdjointPreservesLimits - See:
.claude/skills/lean4-limits/SKILL.mdfor exact syntax
Tool Commands
Lean4_Limit
# Lean 4: import CategoryTheory.Limits.Shapes.Products
Lean4_Universal
# Lean 4: IsLimit.lift cone -- unique morphism from universal property
Sympy_Pullback
uv run python -m runtime.harness scripts/sympy_compute.py solve "f(a) == g(b)"
Lean4_Build
lake build # Compiler-in-the-loop verification
Cognitive Tools Reference
See .claude/skills/math-mode/SKILL.md for full tool documentation.
Version History
- d07ff4b Current 2026-08-20 12:47
