vibecosystem

Limits Colimits

When to Use

Use this skill when working on limits-colimits problems in category theory.

Decision Tree

1. Identify Limit Type
2. Product: limit of discrete diagram
3. Equalizer: limit of parallel pair f, g: A -> B
4. Pullback: limit of A -> C <- B
5. Terminal object: limit of empty diagram
6. Lean 4: CategoryTheory.Limits namespace

1. Verify Universal Property
2. Cone from L with projections pi_i: L -> D_i
3. For any cone from X, unique morphism u: X -> L
4. Triangles commute: pi_i . u = cone_i
5. Lean 4: IsLimit.lift gives the unique morphism

1. Colimit (Dual)
2. Coproduct: colimit of discrete diagram
3. Coequalizer: colimit of parallel pair
4. Pushout: colimit of A <- C -> B
5. Initial object: colimit of empty diagram

1. Compute Limits Concretely
2. In Set: product = Cartesian product
3. Equalizer = {x | f(x) = g(x)}
4. Pullback = {(a,b) | f(a) = g(b)}
5. sympy_compute.py solve "f(a) == g(b)"

1. Preservation
2. Right adjoint preserves limits
3. Left adjoint preserves colimits
4. Representable functors preserve limits
5. Lean 4: Adjunction.rightAdjointPreservesLimits
6. See: .claude/skills/lean4-limits/SKILL.md for 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.