limits-colimits
starsforks
How to install limits-colimits?
parcadei/continuous-claude-v3/limits-colimits
$npx -y skills add parcadei/Continuous-Claude-v3 --skill limits-colimitsProblem-solving strategies for limits colimits in category theory
SKILL.md
| 1 | # Limits Colimits |
| 2 | |
| 3 | ## When to Use |
| 4 | |
| 5 | Use this skill when working on limits-colimits problems in category theory. |
| 6 | |
| 7 | ## Decision Tree |
| 8 | |
| 9 | |
| 10 | 1. **Identify Limit Type** |
| 11 | - Product: limit of discrete diagram |
| 12 | - Equalizer: limit of parallel pair f, g: A -> B |
| 13 | - Pullback: limit of A -> C <- B |
| 14 | - Terminal object: limit of empty diagram |
| 15 | - Lean 4: `CategoryTheory.Limits` namespace |
| 16 | |
| 17 | 2. **Verify Universal Property** |
| 18 | - Cone from L with projections pi_i: L -> D_i |
| 19 | - For any cone from X, unique morphism u: X -> L |
| 20 | - Triangles commute: pi_i . u = cone_i |
| 21 | - Lean 4: `IsLimit.lift` gives the unique morphism |
| 22 | |
| 23 | 3. **Colimit (Dual)** |
| 24 | - Coproduct: colimit of discrete diagram |
| 25 | - Coequalizer: colimit of parallel pair |
| 26 | - Pushout: colimit of A <- C -> B |
| 27 | - Initial object: colimit of empty diagram |
| 28 | |
| 29 | 4. **Compute Limits Concretely** |
| 30 | - In Set: product = Cartesian product |
| 31 | - Equalizer = {x | f(x) = g(x)} |
| 32 | - Pullback = {(a,b) | f(a) = g(b)} |
| 33 | - `sympy_compute.py solve "f(a) == g(b)"` |
| 34 | |
| 35 | 5. **Preservation** |
| 36 | - Right adjoint preserves limits |
| 37 | - Left adjoint preserves colimits |
| 38 | - Representable functors preserve limits |
| 39 | - Lean 4: `Adjunction.rightAdjointPreservesLimits` |
| 40 | - See: `.claude/skills/lean4-limits/SKILL.md` for exact syntax |
| 41 | |
| 42 | |
| 43 | ## Tool Commands |
| 44 | |
| 45 | ### Lean4_Limit |
| 46 | ```bash |
| 47 | # Lean 4: import CategoryTheory.Limits.Shapes.Products |
| 48 | ``` |
| 49 | |
| 50 | ### Lean4_Universal |
| 51 | ```bash |
| 52 | # Lean 4: IsLimit.lift cone -- unique morphism from universal property |
| 53 | ``` |
| 54 | |
| 55 | ### Sympy_Pullback |
| 56 | ```bash |
| 57 | uv run python -m runtime.harness scripts/sympy_compute.py solve "f(a) == g(b)" |
| 58 | ``` |
| 59 | |
| 60 | ### Lean4_Build |
| 61 | ```bash |
| 62 | lake build # Compiler-in-the-loop verification |
| 63 | ``` |
| 64 | |
| 65 | ## Cognitive Tools Reference |
| 66 | |
| 67 | See `.claude/skills/math-mode/SKILL.md` for full tool documentation. |
People who liked this also viewed
6 picksType
- find-skillsHelps users discover and install agent skills when they ask questions like "how do I do X", "find a skill for X", "is there a skill that can...", or express interest in extending capabilities. This skSkillsJul 2026
- grill-meA relentless interview to sharpen a plan or design.SkillsJul 2026
- vercel-react-best-practicesVercel's official collection of agent skillsSkillsJul 2026
- improve-codebase-architectureScan a codebase for deepening opportunities, present them as a visual HTML report, then grill through whichever one you pick.SkillsJul 2026
- setup-matt-pocock-skillsConfigure this repo for the engineering skills — set up its issue tracker, triage label vocabulary, and domain doc layout. Run once before first use of the other engineering skills.SkillsJul 2026
- triageMove issues and external PRs through a state machine of triage roles — categorise, verify, grill if needed, and write agent-ready briefs.SkillsJul 2026
