natural-transformations
npx machina-cli add skill parcadei/Continuous-Claude-v3/natural-transformations --openclawNatural Transformations
When to Use
Use this skill when working on natural-transformations problems in category theory.
Decision Tree
-
Verify Naturality
- eta: F => G is natural transformation between functors F, G: C -> D
- For each f: A -> B in C, diagram commutes: G(f) . eta_A = eta_B . F(f)
- Write Lean 4:
theorem nat : η.app B ≫ G.map f = F.map f ≫ η.app A := η.naturality
-
Component Analysis
- eta_A: F(A) -> G(A) for each object A
- Each component is morphism in target category D
- Lean 4:
def η : F ⟶ G where app := fun X => ...
-
Natural Isomorphism
- Each component eta_A is isomorphism
- Functors F and G are naturally isomorphic
- Notation: F ≅ G (NatIso in Mathlib)
-
Functor Category
- [C, D] has functors as objects
- Natural transformations as morphisms
- Vertical composition: Lean 4
CategoryTheory.NatTrans.vcomp - Horizontal composition:
CategoryTheory.NatTrans.hcomp
-
Yoneda Lemma Application
- Nat(Hom(A, -), F) ~ F(A) naturally in A
- Lean 4:
CategoryTheory.yonedaEquiv - Fully embeds C into [C^op, Set]
- See:
.claude/skills/lean4-nat-trans/SKILL.mdfor exact syntax
Tool Commands
Lean4_Naturality
# Lean 4: theorem nat : η.app B ≫ G.map f = F.map f ≫ η.app A := η.naturality
Lean4_Nat_Trans
# Lean 4: def η : F ⟶ G where app := fun X => component_X
Lean4_Yoneda
# Lean 4: CategoryTheory.yonedaEquiv -- Yoneda lemma
Lean4_Build
lake build # Compiler-in-the-loop verification
Cognitive Tools Reference
See .claude/skills/math-mode/SKILL.md for full tool documentation.
Source
git clone https://github.com/parcadei/Continuous-Claude-v3/blob/main/.claude/skills/math/category-theory/natural-transformations/SKILL.mdView on GitHub Overview
Natural transformations provide a structured way to compare functors F, G: C -> D via a family of morphisms η_A: F(A) -> G(A). This skill covers verifying naturaility diagrams, detailing components, and recognizing when a NatIso exists, using Yoneda and functor-category tools. It matters for rigorous proofs and for implementing Lean4 encodings of categorical structures.
How This Skill Works
Technically, you verify naturality for every f: A -> B by checking G.map f ∘ η_A = η_B ∘ F.map f. Then you specify each component η_A as a morphism F(A) -> G(A) in D, and you may show a natural isomorphism if each η_A is an isomorphism. In practice, you work in the functor category [C, D], use vertical and horizontal composition of natural transformations, and you may apply Yoneda to relate natural transformations to elements of F(A).
When to Use It
- You need to prove a given η is natural between F and G: C -> D by checking the commuting diagram for every f: A -> B.
- You want to construct a natural transformation from previously defined components η_A.
- You aim to establish a natural isomorphism F ≅ G by proving each η_A is an isomorphism.
- You are working inside the functor category [C, D], performing vcomp or hcomp of NatTrans to build complex transformations.
- You want to apply the Yoneda lemma to translate natural transformations into elements of F(A) and simplify proofs (as in YonedaEquiv).
Quick Start
- Step 1: Identify F, G: C -> D and propose components η_A: F(A) -> G(A).
- Step 2: Verify naturality: for every f: A -> B, check G.map f ∘ η_A = η_B ∘ F.map f.
- Step 3: (Optional) show each η_A is an isomorphism for a natural isomorphism, and implement in Lean 4 using yonedaEquiv or NatTrans.
Best Practices
- Check naturality for every morphism in C, not just a representative.
- State each component η_A explicitly: η_A: F(A) -> G(A).
- Keep Lean 4 expressions explicit: nat, η, vcomp, hcomp, map.
- Use the Yoneda lemma to reduce problems to using F(A) for each object A.
- Prove a NatIso by showing all components η_A are isomorphisms and using NatIso notation.
Example Use Cases
- Natural transformation between Hom-functors in Set, verifying naturality in the varying argument.
- Showing two functors from Grp to Grp are naturally isomorphic by giving an isomorphism on each object.
- Using the Yoneda embedding to realize a natural transformation as a canonical element of F(A).
- Constructing and composing natural transformations in a library (Lean 4 / mathlib) via vcomp and hcomp.
- Encoding NatTrans proofs in Lean 4: defining η := F ⟶ G with app := ... and verifying properties.
