Agent Skills
› parcadei/Continuous-Claude-v3
› natural-transformations
natural-transformations
GitHub提供范畴论中自然变换问题的解决策略，涵盖验证自然性、分量分析、自然同构及Yoneda引理应用，并附带Lean 4代码生成与编译验证工具。
Trigger Scenarios
范畴论证明
自然变换验证
Lean 4数学定理开发
Install
npx skills add parcadei/Continuous-Claude-v3 --skill natural-transformations -g -y
SKILL.md
Frontmatter
{
"name": "natural-transformations",
"description": "Problem-solving strategies for natural transformations in category theory",
"allowed-tools": [
"Bash",
"Read"
]
}
Natural 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.
Version History
- d07ff4b Current 2026-08-20 12:47
