Mathlib Phrasebook

3. Category theory🔗

This page explains how to express common concepts in category theory using the definitions in Mathlib. We assume basic knowledge of both Lean and category theory.

Most of the definitions regarding general category theory are in the CategoryTheory namespace. In order to use limits or colimits, we often need to open the CategoryTheory.Limits sub-namespace. A typical file using category theory may contain:

open CategoryTheory Limits

The exposition is split in the following subsections:

  1. 3.1. Categories
  2. 3.2. Associativity of the composition
  3. 3.3. Functors and natural transformations
  4. 3.4. Isomorphisms
  5. 3.5. The category of types
  6. 3.6. Yoneda's lemma
  7. 3.7. Concrete categories
  8. 3.8. Full subcategories
  9. 3.9. Equivalences of categories
  10. 3.10. Limits