categories-functors
npx machina-cli add skill parcadei/Continuous-Claude-v3/categories-functors --openclawCategories 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.
Source
git clone https://github.com/parcadei/Continuous-Claude-v3/blob/main/.claude/skills/math/category-theory/categories-functors/SKILL.mdView on GitHub Overview
This skill explains how to solve category theory problems involving functors. It covers verifying category axioms, checking functor preservation of identities and composition, and recognizing common functor types, with Lean 4 verification guidance to ensure correctness.
How This Skill Works
First, verify the source and target categories C and D with their objects and morphisms. Then ensure the functor F preserves identities and composition, using F.map id_A = id_{F(A)} and F.map (g ≫ f) = F.map g ≫ F.map f. Identify the functor type (covariant, contravariant, faithful/full, or equivalence) and apply relevant examples like forgetful, free, Hom, or power set functors. Finally, use Lean 4 (Mathlib) and lake build for compiler-verified proofs.
When to Use It
- Verifying category axioms (objects, morphisms, identities, and associative composition)
- Checking that a functor preserves identities and composition
- Determining whether a functor is covariant, contravariant, faithful, full, or an equivalence
- Reviewing common functors such as forgetful, free, Hom, and power set functors
- Using Lean 4 with Mathlib to verify functor properties via compiler-in-the-loop
Quick Start
- Step 1: Identify C and D and list their objects and morphisms
- Step 2: Check Axioms and Functor properties: id preservation and composition preservation
- Step 3: If needed, implement and verify in Lean 4 with lake build using Mathlib
Best Practices
- Explicitly state objects and morphisms when defining a functor F: C -> D
- Verify identity preservation: F(id_A) = id_{F(A)}
- Verify composition preservation: F(g . f) = F(g) . F(f)
- Differentiate between covariant vs contravariant behavior and note Hom-sets for faithful/full analysis
- Leverage Lean 4 proofs (e.g., theorem map_comp, theorem comp) and run lake build for verification
Example Use Cases
- Forgetful functor: from Grp to Set, forgetting algebraic structure while preserving underlying functions
- Free functor: left adjoint to forgetful functor, constructing free objects on a set
- Hom functor: Hom(A, -) or Hom(-, B) producing representable functors
- Power set functor: Set -> Set given by X ↦ P(X), mapping functions to inverse image maps
- Equivalence as a goal: full, faithful, and essentially surjective to establish category equivalence
