Overview

This skill guides solving limits–colimits problems in category theory. It covers identifying the limit type (product, equalizer, pullback, terminal), verifying the universal property, dualizing for colimits, and performing concrete computations (e.g., in Set). It also notes Lean 4 tooling for formalization.

How This Skill Works

You classify the diagram into a limit or colimit, validate the universal property with a cone and a mediating morphism (often via IsLimit.lift in Lean 4), and then compute concrete representations or check preservation by adjoints. The approach emphasizes a small decision tree and practical checks.

When to Use It

• Identify the exact limit/colimit type for a given diagram (product, equalizer, pullback, etc.) or its dual (coproduct, coequalizer, pushout, initial).
• Prove the universal property by constructing the mediating morphism and showing uniqueness (use IsLimit.lift in Lean 4).
• Apply the dual perspective to handle colimits (coproduct, coequalizer, pushout, initial object).
• Compute explicit representations in Set to sanity-check (product as Cartesian product, equalizer as {x | f(x) = g(x)}, pullback as {(a,b) | f(a) = g(b)}; use a solver for equations when needed.
• Formalize or verify results using Lean 4 tooling (Lean4_Limit, Lean4_Universal) and understand preservation results.

Quick Start

1. Step 1: Identify the limit type for your diagram (Product, Equalizer, Pullback, Terminal).
2. Step 2: Verify the universal property by constructing the mediating morphism (IsLimit.lift in Lean 4) and check commutativity.
3. Step 3: If needed, compute concretely in Set or with Sympy to validate, then consider the dual colimit and preservation properties.

Best Practices

• Start by classifying the diagram into a limit type (Product, Equalizer, Pullback, Terminal) or its colimit dual.
• Always write down and reference the universal property before constructing a morphism.
• Use the dual perspective to avoid duplicating effort when working with Colimits.
• Compute concrete instances in Set to build intuition and catch mistakes.
• Check preservation facts (right adjoint preserves limits, left adjoint preserves colimits; representable functors preserve limits) and use Lean 4 syntax as needed.

Example Use Cases

• Compute a pullback in Sets for f: A -> C and g: B -> C, obtaining { (a,b) | f(a) = g(b) }.
• Compute the equalizer of two functions f, g: X -> Y in Sets, as { x in X | f(x) = g(x) }.
• Identify the product of objects in Sets as the limit of a discrete diagram with projections.
• Form the coproduct (disjoint union) as the colimit of a discrete diagram in Sets.
• Use Lean 4 to prove that right adjoints preserve limits or to construct the universal morphism via IsLimit.lift.

Frequently Asked Questions