siddhartha-gadgil/leanaide/universal-property

Skill: Universal Property Arguments

Pre-condition: Apply this skill when objects are defined by maps into or out of them, or when a canonical isomorphism should follow from products, coproducts, quotients, tensor products, free objects, adjunctions, limits, or colimits.

Goal: Prove the desired object or map exists and is unique by verifying a universal mapping property.

Instructions:

1. Name the Universal Property: Identify the source/target category, test object, and required bijection or unique factorization.
2. Construct the Mediating Map: Given arbitrary compatible data, define the unique map promised by the property.
3. Verify Compatibility: Check projections, inclusions, quotient relations, bilinearity, commutative diagrams, or naturality conditions.
4. Prove Uniqueness: Show any map satisfying the same compatibility must equal the constructed map.
5. Conclude Canonical Isomorphism: If comparing two universal objects, build maps in both directions and use uniqueness to prove they are inverses.

Common Failure Modes:

• Verifying existence without uniqueness.
• Using an object-specific construction when the universal property would give a canonical map.
• Omitting naturality or compatibility conditions.