{"id":"limits-colimits","name":"limits-colimits","summary":"圏論における極限余極限の問題解決戦略","body":"# Limits Colimits\n\n## When to Use\n\nUse this skill when working on limits-colimits problems in category theory.\n\n## Decision Tree\n\n\n1. **Identify Limit Type**\n   - Product: limit of discrete diagram\n   - Equalizer: limit of parallel pair f, g: A -> B\n   - Pullback: limit of A -> C <- B\n   - Terminal object: limit of empty diagram\n   - Lean 4: `CategoryTheory.Limits` namespace\n\n2. **Verify Universal Property**\n   - Cone from L with projections pi_i: L -> D_i\n   - For any cone from X, unique morphism u: X -> L\n   - Triangles commute: pi_i . u = cone_i\n   - Lean 4: `IsLimit.lift` gives the unique morphism\n\n3. **Colimit (Dual)**\n   - Coproduct: colimit of discrete diagram\n   - Coequalizer: colimit of parallel pair\n   - Pushout: colimit of A <- C -> B\n   - Initial object: colimit of empty diagram\n\n4. **Compute Limits Concretely**\n   - In Set: product = Cartesian product\n   - Equalizer = {x | f(x) = g(x)}\n   - Pullback = {(a,b) | f(a) = g(b)}\n   - `sympy_compute.py solve \"f(a) == g(b)\"`\n\n5. **Preservation**\n   - Right adjoint preserves limits\n   - Left adjoint preserves colimits\n   - Representable functors preserve limits\n   - Lean 4: `Adjunction.rightAdjointPreservesLimits`\n   - See: `.claude/skills/lean4-limits/SKILL.md` for exact syntax\n\n\n## Tool Commands\n\n### Lean4_Limit\n```bash\n# Lean 4: import CategoryTheory.Limits.Shapes.Products\n```\n\n### Lean4_Universal\n```bash\n# Lean 4: IsLimit.lift cone -- unique morphism from universal property\n```\n\n### Sympy_Pullback\n```bash\nuv run python -m runtime.harness scripts/sympy_compute.py solve \"f(a) == g(b)\"\n```\n\n### Lean4_Build\n```bash\nlake build  # Compiler-in-the-loop verification\n```\n\n## Cognitive Tools Reference\n\nSee `.claude/skills/math-mode/SKILL.md` for full tool documentation.","author":"@parcadei","ownerProfile":null,"authorContacts":null,"sourceUrl":"https://github.com/parcadei/Continuous-Claude-v3/tree/main/.claude/skills/math/category-theory/limits-colimits","license":"MIT","category":null,"lang":"en","tokens":502,"stars":0,"calls30d":1,"claimed":false,"visibility":"public","origin":"crawler","version":"0.1.0","createdAt":"2026-08-22","updatedAt":"2026-08-22","files":[],"requires":{"mcp":[],"tools":["Bash","Read"]},"safety":{"flags":[],"scannedAt":"2026-08-22","hasScripts":false,"networkEndpoints":[]}}