{"id":"categories-functors","name":"categories-functors","summary":"圏論における圏関手の問題解決戦略","body":"# Categories Functors\n\n## When to Use\n\nUse this skill when working on categories-functors problems in category theory.\n\n## Decision Tree\n\n\n1. **Verify Category Axioms**\n   - Objects and morphisms (arrows) defined?\n   - Identity morphism for each object: id_A: A -> A\n   - Composition associative: (f . g) . h = f . (g . h)\n   - Write Lean 4: `theorem assoc : (f ≫ g) ≫ h = f ≫ (g ≫ h) := Category.assoc`\n\n2. **Check Functor Properties**\n   - F: C -> D maps objects to objects, arrows to arrows\n   - Preserves identity: F(id_A) = id_{F(A)}\n   - Preserves composition: F(g . f) = F(g) . F(f)\n   - Write Lean 4: `theorem comp : F.map (g ≫ f) = F.map g ≫ F.map f := F.map_comp`\n\n3. **Functor Types**\n   - Covariant: preserves arrow direction\n   - Contravariant: reverses arrow direction\n   - Faithful/Full: injective/surjective on Hom-sets\n   - Equivalence: full, faithful, essentially surjective\n\n4. **Common Functors**\n   - Forgetful functor: forgets structure (e.g., Grp -> Set)\n   - Free functor: left adjoint to forgetful\n   - Hom functor: Hom(A, -) or Hom(-, B)\n   - Power set functor: Set -> Set via X |-> P(X)\n\n5. **Verify with Lean 4**\n   - Compiler-in-the-loop: write proof, `lake build` checks\n   - Mathlib has full category theory library\n   - See: `.claude/skills/lean4-functors/SKILL.md` for exact syntax\n\n\n## Tool Commands\n\n### Lean4_Category\n```bash\n# Lean 4 with Mathlib: import CategoryTheory.Category.Basic\n```\n\n### Lean4_Functor\n```bash\n# Lean 4: theorem map_comp (F : C ⥤ D) : F.map (g ≫ f) = F.map g ≫ F.map f := F.map_comp\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/categories-functors","license":"MIT","category":"writing","lang":"en","tokens":527,"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":[]}}