3.3. Functors and natural transformations🔗

Assuming C and D are categories, the type Functor C D of functors from C to D is denoted C ⥤ D, where ⥤ is typed as \functor. The identity functor of the category C is 𝟭 C (where 𝟭 is typed as \sb1). The composition of two functors F : C₁ ⥤ C₂ and G : C₂ ⥤ C₃ is F ⋙ G : C₁ ⥤ C₃ where ⋙ is typed as \ggg. Similarly as for the composition of morphisms, this composition F ⋙ G is usually denoted GF is the mathematical literature.

For example, the identity functor is essentially defined as follows:

variable (C) in
-- the actual definition in mathlib is `Functor.id`
@[simps, implicit_reducible]
def Functor.id' : C ⥤ C where
  obj (X : C) := X
  map {X Y : C} (f : X ⟶ Y) := f

The action of a functor on objects is obj, and its action on morphisms is map. There are two axioms Functor.map_id and Functor.map_comp in the Functor structure, but they have by cat_disch as a default proof. cat_disch is a tactic that is based on aesop which closes many basic goals in category theory (in many cases, simp or ext <;> simp would also close goals). In this case, it was able to show that the identity functor preserves identity morphisms and the composition of morphisms. Many such goals for other structures in category theory are also automatically filled by this cat_disch tactic.

(The implicit_reducible attribute is required for definitions of essentially all functors. Otherwise, when trying to prove equalities of morphisms involving the action of functors, Lean may not be able to see through the obj fields of functors. Basically, any definiton of a structure that has a field which involves objects in a category should be declared implicit_reducible.)

The type C ⥤ D of functors is endowed with a category structure. A morphism f : F ⟶ G from F to G in the category of functors C ⥤ D is a natural transformation, i.e. a term in the type NatTrans F G.

Functor.category#synth Category (C ⥤ D)
variable {F G : C ⥤ D} (f : F ⟶ G)
example (X : C) : F.obj X ⟶ G.obj X := f.app X

/- the naturality of a natural transformation `f : F ⟶ G`
with respect to a morphism `g : X ⟶ Y` in `C` -/
example {X Y : C} (g : X ⟶ Y) :
    F.map g ≫ f.app Y = f.app X ≫ G.map g :=
  f.naturality g

Because Lean has a suitable hierarchy of universes, there is no "set-theoretical" issue regarding the "existence" of functor categories. Whatever the universe parameters for the categories C and D are (and they may be different for C and D!), the type of functors C ⥤ D and the types of natural transformations F ⟶ G between two functors in C ⥤ D live in suitable universes.