siddhartha-gadgil/leanaide/diagram-chase

Skill: Diagram Chase and Diagrammatic Reasoning

Pre-condition: Apply this skill when the problem contains commutative diagrams, exact sequences, maps between structured objects, or a geometric/graphical construction guiding the proof.

Goal: Track elements, maps, and commutativity relations through a diagram to construct the required object or prove equality.

Instructions:

1. Draw the Diagram Algebraically: List objects, maps, commutative squares, exact rows/columns, and known kernels/images.
2. Choose the Starting Element or Object: Identify the element, path, subobject, or diagram feature to chase.
3. Move Along Maps: Apply maps step by step, recording where commutativity lets two paths agree.
4. Use Exactness or Incidence: Convert membership in a kernel to existence in an image, or use the diagram's geometric constraints.
5. Construct the Target: Produce the required preimage, lift, factorization, equality, or contradiction.
6. Check Independence: If choices were made, prove the result is independent of those choices when required.

Common Failure Modes:

• Chasing through a square without proving it commutes.
• Using exactness in the wrong direction.
• Confusing equality of elements with equality of maps.