category_theory.md

Maths in Lean : category theory

The category typeclass is defined in category_theory/category.lean. It depends on the type of the objects, so for example we might write category (Type u) if we're talking about a category whose objects are types (in universe u). Some care is needed with universes (see the section Universes), and end users may often prefer the abbreviations small_category and large_category.

Functors (which are a structure, not a typeclass) are defined in category_theory/functor.lean, along with identity functors and functor composition.

Natural transformations, and their compositions, are defined in category_theory/natural_transformation.lean.

The category of functors and natural transformations between fixed categories C and D is defined in category_theory/functor_category.lean.

Cartesian products of categories, functors, and natural transformations appear in category_theory/products.lean. (Product in the sense of limits will appear elsewhere soon!)

The category of types, and the hom pairing functor, are defined in category_theory/types.lean.

Universes

Unfortunately in a category theory library we have to deal with universes carefully. We have the following:

category.{u₁ v₁}     : Type (max (u₁+1) (v₁+1))
C                    : Type v₁
D                    : Type v₂
𝒞                    : category.{u₁ v₁} C
𝒟                    : category.{u₂ v₂} D
functor C D          : Type (max u₁ u₂ v₁ v₂)
F G                  : functor C D
nat_trans F G        : Type (max u₁ v₂)
functor.category C D : category.{(max u₁ v₂) (max u₁ u₂ v₁ v₂)}

In the above, category.{v₁ u₁} C is equivalently written as category.{v₁} C because u₁ can be inferred from C.

Note then that if we specialise to small categories, where uᵢ = vᵢ, then functor.category C D : category.{max u₁ u₂}, and so is again a small category. If C is a small category and D is a large category (i.e. u₂ = v₂+1), and v₂ = v₁ then we have functor.category C D : category.{v₁+1} so is again a large category.

Whenever you want to write code uniformly for small and large categories (which you do by talking about categories whose universe levels u and v are unrelated), you will find that Lean's variable mechanism doesn't always work, and the following trick is often helpful:

variables {C : Type u₁} [�� : category.{v₁} C]
variables {D : Type u₂} [�� : category.{v₂} D]
include �� ��

Some care with using section ... end can be required to make sure these included variables don't end up where they aren't wanted.

Notation

Categories

We use the ⟶ (\hom) arrow to denote sets of morphisms, as in X ⟶ Y. This leaves the actual category implicit; it is inferred from the type of X and Y by typeclass inference.

We use 𝟙 (\b1) to denote identity morphisms, as in 𝟙 X.

We use ≫ (\gg) to denote composition of morphisms, as in f ≫ g, which means "f followed by g". You may prefer write composition in the usual convention, using ⊚ (\oo or \circledcirc), as in f ⊚ g which means "g followed by f". To do so you'll need to add this notation locally, via

local notation f ` ⊚ `:80 g:80 := category.comp g f

Isomorphisms

We use ≅ for isomorphisms.

Functors

We use ⥤ (\func) to denote functors, as in C ⥤ D for the type of functors from C to D. (Unfortunately ⇒ is reserved in core: https://github.com/leanprover/lean/blob/master/library/init/relator.lean, so we can't use that here.)

We use F.obj X to denote the action of a functor on an object. We use F.map f to denote the action of a functor on a morphism`.

Functor composition can be written as F ⋙ G.

Natural transformations

We use τ.app X for the components of a natural transformation.

Otherwise, we mostly use the notation for morphisms in any category:

We use F ⟶ G (\hom or -->) to denote the type of natural transformations, between functors F and G. We use F ≅ G (\iso) to denote the type of natural isomorphisms.

For vertical composition of natural transformations we just use ≫. For horizontal composition, use hcomp.