Agent Skills
› parcadei/Continuous-Claude-v3
› categories-functors
categories-functors
GitHub提供范畴论中函子的解题策略，涵盖范畴公理验证、函子性质检查及类型分类。指导使用Lean 4与Mathlib进行形式化证明和编译器验证，辅助数学理论研究与形式化方法实现。
Trigger Scenarios
需要验证范畴或函子的数学性质
使用Lean 4进行范畴论的形式化证明
Install
npx skills add parcadei/Continuous-Claude-v3 --skill categories-functors -g -y
SKILL.md
Frontmatter
{
"name": "categories-functors",
"description": "Problem-solving strategies for categories functors in category theory",
"allowed-tools": [
"Bash",
"Read"
]
}
Categories Functors
When to Use
Use this skill when working on categories-functors problems in category theory.
Decision Tree
-
Verify Category Axioms
- Objects and morphisms (arrows) defined?
- Identity morphism for each object: id_A: A -> A
- Composition associative: (f . g) . h = f . (g . h)
- Write Lean 4:
theorem assoc : (f ≫ g) ≫ h = f ≫ (g ≫ h) := Category.assoc
-
Check Functor Properties
- F: C -> D maps objects to objects, arrows to arrows
- Preserves identity: F(id_A) = id_{F(A)}
- Preserves composition: F(g . f) = F(g) . F(f)
- Write Lean 4:
theorem comp : F.map (g ≫ f) = F.map g ≫ F.map f := F.map_comp
-
Functor Types
- Covariant: preserves arrow direction
- Contravariant: reverses arrow direction
- Faithful/Full: injective/surjective on Hom-sets
- Equivalence: full, faithful, essentially surjective
-
Common Functors
- Forgetful functor: forgets structure (e.g., Grp -> Set)
- Free functor: left adjoint to forgetful
- Hom functor: Hom(A, -) or Hom(-, B)
- Power set functor: Set -> Set via X |-> P(X)
-
Verify with Lean 4
- Compiler-in-the-loop: write proof,
lake buildchecks - Mathlib has full category theory library
- See:
.claude/skills/lean4-functors/SKILL.mdfor exact syntax
- Compiler-in-the-loop: write proof,
Tool Commands
Lean4_Category
# Lean 4 with Mathlib: import CategoryTheory.Category.Basic
Lean4_Functor
# Lean 4: theorem map_comp (F : C ⥤ D) : F.map (g ≫ f) = F.map g ≫ F.map f := F.map_comp
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
