Limits Colimits

When to Use

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

Decision Tree

1. 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.Limits namespace

2. 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.lift gives the unique morphism

3. Colimit (Dual)

   • Coproduct: colimit of discrete diagram
   • Coequalizer: colimit of parallel pair
   • Pushout: colimit of A <- C -> B
   • Initial object: colimit of empty diagram