{"id":"natural-transformations","name":"natural-transformations","summary":"圏論における自然変換の問題解決戦略","body":"# Natural Transformations\n\n## When to Use\n\nUse this skill when working on natural-transformations problems in category theory.\n\n## Decision Tree\n\n\n1. **Verify Naturality**\n   - eta: F => G is natural transformation between functors F, G: C -> D\n   - For each f: A -> B in C, diagram commutes:\n     G(f) . eta_A = eta_B . F(f)\n   - Write Lean 4: `theorem nat : η.app B ≫ G.map f = F.map f ≫ η.app A := η.naturality`\n\n2. **Component Analysis**\n   - eta_A: F(A) -> G(A) for each object A\n   - Each component is morphism in target category D\n   - Lean 4: `def η : F ⟶ G where app := fun X => ...`\n\n3. **Natural Isomorphism**\n   - Each component eta_A is isomorphism\n   - Functors F and G are naturally isomorphic\n   - Notation: F ≅ G (NatIso in Mathlib)\n\n4. **Functor Category**\n   - [C, D] has functors as objects\n   - Natural transformations as morphisms\n   - Vertical composition: Lean 4 `CategoryTheory.NatTrans.vcomp`\n   - Horizontal composition: `CategoryTheory.NatTrans.hcomp`\n\n5. **Yoneda Lemma Application**\n   - Nat(Hom(A, -), F) ~ F(A) naturally in A\n   - Lean 4: `CategoryTheory.yonedaEquiv`\n   - Fully embeds C into [C^op, Set]\n   - See: `.claude/skills/lean4-nat-trans/SKILL.md` for exact syntax\n\n\n## Tool Commands\n\n### Lean4_Naturality\n```bash\n# Lean 4: theorem nat : η.app B ≫ G.map f = F.map f ≫ η.app A := η.naturality\n```\n\n### Lean4_Nat_Trans\n```bash\n# Lean 4: def η : F ⟶ G where app := fun X => component_X\n```\n\n### Lean4_Yoneda\n```bash\n# Lean 4: CategoryTheory.yonedaEquiv -- Yoneda lemma\n```\n\n### Lean4_Build\n```bash\nlake build  # Compiler-in-the-loop verification\n```\n\n## Cognitive Tools Reference\n\nSee `.claude/skills/math-mode/SKILL.md` for full tool documentation.","author":"@parcadei","ownerProfile":null,"authorContacts":null,"sourceUrl":"https://github.com/parcadei/Continuous-Claude-v3/tree/main/.claude/skills/math/category-theory/natural-transformations","license":"MIT","category":"writing","lang":"en","tokens":519,"stars":0,"calls30d":2,"claimed":false,"visibility":"public","origin":"crawler","version":"0.1.0","createdAt":"2026-08-22","updatedAt":"2026-08-22","files":[],"requires":{"mcp":[],"tools":["Bash","Read"]},"safety":{"flags":[],"scannedAt":"2026-08-22","hasScripts":false,"networkEndpoints":[]}}