Natural Transformations

When to Use

Use this skill when working on natural-transformations problems in category theory.

Decision Tree

1. 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) . etaA = etaB . F(f) - Write Lean 4: theorem nat : η.app B ≫ G.map f = F.map f ≫ η.app A := η.naturality

1. 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 => ...

1. Natural Isomorphism

- Each component eta_A is isomorphism - Functors F and G are naturally isomorphic - Notation: F ≅ G (NatIso in Mathlib)

1. Functor Category

- [C, D] has functors as objects - Natural transformations as morphisms - Vertical composition: Lean 4 CategoryTheory.NatTrans.vcomp - Horizontal composition: CategoryTheory.NatTrans.hcomp

1. 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.md for exact syntax

Tool Commands

Lean4_Naturality

# Lean 4: theorem nat : η.app B ≫ G.map f = F.map f ≫ η.app A := η.naturality

Lean4NatTrans

# 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.