Map · 18
category theory
MSC 18 · Category theory; homological algebra
65,252 declarations (44,435 theorems, 20,817 definitions) across 1,576 files. 2 of the 3 famous theorems listed for this area are in Mathlib (67%). 1 open conjectures here are stated in Lean.
Files are assigned to areas by a language model reading each file's documentation. Report a file that is in the wrong area.
Subareas8
- 18A General theory of categories and functors 32,155
- 18D Categorical structures 8,904
- 18E Categorical algebra 7,704
- 18B Special categories 7,406
- 18G Homological algebra in category theory, derived categories and functors 3,809
- 18F Categories in geometry and topology 2,101
- 18C Categories and theories 1,659
- 18N Higher categories and homotopical algebra 1,514
Famous theorems2 of 3
From the 1000+ theorems project, which classifies each theorem by MSC area.
Not yet in Mathlib · 1
In Mathlib · 2
- Beck's monadicity theoremCategoryTheory.Monad.monadicOfCreatesGSplitCoequalizers
- Mitchell's embedding theoremCategoryTheory.Abelian.freyd_mitchell
Open conjectures stated in Lean1
Statements without proofs, collected by the Formal Conjectures project.
- Mathoverflow31809.mathoverflow_31809MathOverflow
Structures defined here24
Typeclasses defined in this area's files, most assumed first.
- CategoryTheory.Category 71,336
- CategoryTheory.Preadditive 5,367
- CategoryTheory.Limits.HasZeroMorphisms 5,306
- CategoryTheory.MonoidalCategory 4,886
- CategoryTheory.Bicategory 2,887
- CategoryTheory.Abelian 2,703
- CategoryTheory.HasShift 2,551
- CategoryTheory.Limits.HasZeroObject 1,978
- CategoryTheory.Functor.Additive 1,858
- CategoryTheory.CartesianMonoidalCategory 1,555
- CategoryTheory.BraidedCategory 1,209
- CategoryTheory.Pretriangulated 974
- CategoryTheory.Functor.PreservesZeroMorphisms 924
- CategoryTheory.IsIso 921
- CategoryTheory.Functor.IsLocalization 727
- CategoryTheory.Mono 684
- CategoryTheory.MorphismProperty.IsMultiplicative 620
- CategoryTheory.ConcreteCategory 593
- CategoryTheory.Limits.HasColimitsOfShape 560
- CategoryTheory.Functor.CommShift 517
- CategoryTheory.Functor.Monoidal 510
- TotalComplexShape 510
- CategoryTheory.Functor.Full 507
- CategoryTheory.Functor.Faithful 483
Files1,576
Largest first. The code after each file is its assigned subarea.
- Mathlib.CategoryTheory.Monoidal.Mon
The category of monoids in a monoidal category.
18D · 547
- Mathlib.CategoryTheory.Limits.Cones
Cones and cocones
18A · 459
- Mathlib.CategoryTheory.Comma.Over.Basic
Over and under categories
18A · 411
- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
The category of "structured arrows"
18A · 406
- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
Multi-(co)equalizers
18A · 397
- Mathlib.CategoryTheory.Monoidal.Grp
The category of groups in a Cartesian monoidal category
18D · 391
- Mathlib.Algebra.Homology.ShortComplex.RightHomology
Right Homology of short complexes
18E · 367
- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Binary (co)products
18A · 357
- Mathlib.CategoryTheory.Monoidal.Functor
(Lax) monoidal functors
18D · 349
- Mathlib.Algebra.Homology.ShortComplex.Homology
Homology of short complexes
18E · 320
- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
Binary biproducts
18A · 318
- Mathlib.CategoryTheory.Sites.Sieves
Theory of sieves
18A · 314