natural-transformations
Provides a decision tree to verify naturality and diagram commutativity in category theory using Lean 4 syntax.
Install
mkdir -p .claude/skills/natural-transformations && curl -L -o skill.zip "https://agentskills.codes/api/skills/download/2323" && unzip -o skill.zip -d .claude/skills/natural-transformations && rm skill.zipInstalls to .claude/skills/natural-transformations
Activation
This is the description your AI agent reads to decide when to run this skill — the better it matches your request, the more reliably it fires.
Problem-solving strategies for natural transformations in category theoryKey capabilities
- →Verify naturality of transformations between functors
- →Define natural transformations using Lean 4 syntax
- →Perform vertical and horizontal composition of transformations
- →Apply the Yoneda lemma for functor embedding
- →Check for natural isomorphisms
How it works
The skill provides a decision tree for verifying naturality diagrams and maps these concepts to Lean 4 syntax and Mathlib library functions.
Inputs & outputs
When to use natural-transformations
- →Verify naturality diagrams
- →Define natural transformations in Lean
- →Apply Yoneda lemma
- →Perform component analysis
About this skill
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.
When not to use it
- →Tasks unrelated to category theory
- →General programming logic not involving functor mappings
Prerequisites
Limitations
- →Requires Lean 4 environment for verification
- →Limited to the scope of category theory natural transformations
How it compares
It translates abstract category theory proofs into verifiable Lean 4 code rather than relying on manual diagrammatic reasoning.
Compared to similar skills
natural-transformations side by side with the closest alternatives in the catalog.
| Skill | Installs | Updated | Safety | Difficulty |
|---|---|---|---|---|
| natural-transformations (this skill) | 2 | 7mo | Review | Advanced |
| literature-review | 559 | 2mo | Review | Advanced |
| openalex-database | 48 | 7mo | Review | Intermediate |
| annas-archive-ebooks | 22 | 7mo | Review | Beginner |
Try saying
Example prompts that trigger this skill in your AI assistant.
More by parcadei
View all by parcadei →You might also like
literature-review
K-Dense-AI
Conduct comprehensive, systematic literature reviews using multiple academic databases (PubMed, arXiv, bioRxiv, Semantic Scholar, etc.). This skill should be used when conducting systematic literature reviews, meta-analyses, research synthesis, or comprehensive literature searches across biomedical, scientific, and technical domains. Creates professionally formatted markdown documents and PDFs with verified citations in multiple citation styles (APA, Nature, Vancouver, etc.).
openalex-database
davila7
Query and analyze scholarly literature using the OpenAlex database. This skill should be used when searching for academic papers, analyzing research trends, finding works by authors or institutions, tracking citations, discovering open access publications, or conducting bibliometric analysis across 240M+ scholarly works. Use for literature searches, research output analysis, citation analysis, and academic database queries.
annas-archive-ebooks
ratacat
Use when needing to look up book content, find a book by title/author, download an ebook, or reference material from a published book. Triggers on book lookups, ebook downloads, "find the book", "get the PDF/EPUB of". Downloads produce PDF/EPUB/MOBI files - use ebook-extractor skill to convert to text.
scientific-critical-thinking
davila7
Evaluate research rigor. Assess methodology, experimental design, statistical validity, biases, confounding, evidence quality (GRADE, Cochrane ROB), for critical analysis of scientific claims.
biorxiv-database
lifangda
Efficient database search tool for bioRxiv preprint server. Use this skill when searching for life sciences preprints by keywords, authors, date ranges, or categories, retrieving paper metadata, downloading PDFs, or conducting literature reviews.
gpt-researcher
assafelovic
GPT Researcher is an autonomous deep research agent that conducts web and local research, producing detailed reports with citations. Use this skill when helping developers understand, extend, debug, or integrate with GPT Researcher - including adding features, understanding the architecture, working with the API, customizing research workflows, adding new retrievers, integrating MCP data sources, or troubleshooting research pipelines.