r-irbe Abstract Algebra & Category Theory
Algebraic and categorical foundations for type hierarchies, compositional structures, lattice-based orderings, and the deep connection between algebra and dependent type theory that makes Lean formalization possible.
Routing
- USE FOR: Abstract algebra, category theory, lattice theory, universal algebra, and algebraic structures relevant to Lean formalization. Use for reasoning about groups, rings, fields, modules, categories, functors, natural transformations, monads, adjunctions, lattices, and algebraic hierarchies. Covers both pure algebraic theory and categorical perspectives essential for type-theoretic formalization.
- DO NOT USE FOR: measure-theoretic reasoning (use @math-measure-probability); topology/analysis (use @math-topology-analysis); Lean proof (use @lean-math-foundations).
- TRIGGERS: abstract algebra, category theory, lattice theory, universal algebra, algebraic structure.
Workflow
- Classify the structure: group / ring / field / module / lattice / category / functor / monoidal.
- Pick the matching section of the body for the structure + its standard constructions.
- Produce the mathematical answer or the Mathlib pointer; surface any Mathlib namespacing convention.
- Hand off: to
@lean-math-foundationsfor the Lean encoding, to@lean-researchif pin-verification is needed, to@lean-zettelkasten.
Recovery & STOP
- STOP if the question is measure-theoretic — delegate to
@math-measure-probability. - STOP if topology/analysis dominates — delegate to
@math-topology-analysis. - STOP if the answer requires a pin-verified Mathlib lemma — escalate to
@lean-research.
Handoffs
- Predecessors:
agent:gateway,skill:lean-research. - Successors:
skill:lean-math-foundations,skill:lean-research,skill:lean-zettelkasten.
Detailed reference
Full content for math-algebra-category lives in
references/math-algebra-category-handbook.md.
Load that file when the skill is convened; the SKILL.md only carries
the dispatch contract and the parts index.
| Section | Topic |
|---|---|
| Part 1 | Algebraic Structures Hierarchy |
| Part 2 | Lattice Theory |
| Part 3 | Category Theory Foundations |
| Part 4 | Monads and Computational Effects |
| Part 5 | Topos Theory and Logic |
| Part 6 | Type Theory as Algebra |
| Part 7 | Homological Methods |
| Part 8 | Galois Theory Perspective |
| Part 9 | Formalization Connections |
See also
../../references/math-algebra-category-handbook.md— Full handbook (extracted from this skill)../lean-math-foundations/SKILL.md— Successor../lean-research/SKILL.md— Successor../lean-zettelkasten/SKILL.md— Successor