Definition. Functor [002v]

  • November 29, 2025

1. The data

  • November 29, 2025

For categories \(C\) and \(D\), a functor \(F : C \to D\) consists of:

  • An assignment on objects \[ \text {Ob}(C) \to \text {Ob}(D) \quad X \mapsto F(X) \]
  • An assignment on morphisms \[ C(X, Y) \to D(F(X), F(Y)) \quad f \mapsto F(f) \] equivalently we can denote this explicitly as \[ F_{X, Y} : \text {Hom}_C(X, Y) \to \text {Hom}_D(F(X), F(Y)) \]

2. The axioms

  • November 29, 2025

The data must satisfy composition and identity axioms:

  • The equality \[ F(g \circ f) = F(g) \circ F(f) \]
  • For each object \(X \in \text {Ob}(C)\) the equality \[ F(\text {id}_X) = \text {id}_{F(X)} \in D(F(X), F(X)) \]

3. Commutative diagram

  • November 29, 2025

If we wish to represent the composition axiom diagrammatically we can do so as follows:

4. Lean definition

  • November 29, 2025
 

        structure Functor 
      (C : Type u₁) [Category.{v₁} C] 
      (D : Type u₂) [Category.{v₂} D] :
          Type max v₁ v₂ u₁ u₂ where

        /-- The action of a functor on objects. -/
        obj : C → D
        
        /-- The action of a functor on morphisms. -/
        map : ∀ {X Y : C}, (X ⟶ Y) → ((obj X) ⟶ (obj Y))
        
        /-- A functor preserves identity morphisms. -/
        map_id : ∀ X : C, map (𝟙 X) = 𝟙 (obj X) := by cat_disch
        
        /-- A functor preserves composition. -/
        map_comp : ∀ {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z), 
          map (f ≫ g) = map f ≫ map g := by cat_disch

    /-- Notation for a functor between categories. -/
    scoped [CategoryTheory] infixr:26 " ⥤ " => Functor -- type as \func

Backlinks

    Definition. Full and faithful functors [002w]

    • November 30, 2025

    We consider a functor between two (locally small) categories \(F : C \to D\). For each pair of objects \(X, Y \in \mathrm {Ob}(C)\) the functor induces a function between hom-sets:

    \[ F_{X, Y} : C(X, Y) \to D(F(X), F(Y)) \]

    We can describe functors based on the properties of these induced functions as follows:

    • The functor \(F\) is called faithful if for every pair of objects \(X, Y \in \mathrm {Ob}(C)\) the function \(F_{X, Y}\) is injective. We can also denote this as: \[ (x \xrightarrow {f} y) \mapsto (F(x) \xrightarrow {F(f)} F(y)) \] or using the notation of an embedding as: \[ C(X, Y) \hookrightarrow D(F(X), F(Y)) \] An important note to make here is that a faithful functor only presereves distinctness of morphisms, so what this means is that:
      no two different arrows with the same domain and codomain in \(C\) are mapped to (or get identified by) the same arrow in \(D\)
      It does not say
      • different objects in \(C\) are mapped to different objects in \(D\).
      • two morphisms with different domains/codomains in \(C\) are mapped to different morphisms in \(D\).
      So in a diagrammatic sense a faithful functor essentially guarantees this:
    • The functor \(F\) is called full if for every pair of objects \(X, Y \in \mathrm {Ob}(C)\) the function \(F_{X, Y}\) is surjective. Likewise here its important to note that
      a full functor only guarantees that any morphism between two objects in the image of \(F\) comes from a morphism in \(C\)
      It does not say
      • every object in \(D\) is in the image of \(F\). In other words objects in \(D\) outside the image of \(F\) may not have any preimage in \(C\).
      • every morphism with a domain/codomain outside the image of \(F\) comes from a morphism in \(C\). Similarly morphisms between objects in the image of \(F\) may not have a preimage in \(C\).
      We can again demonstrate this diagrammatically as follows:
      The main idea being that a full functor only guarantees that if we have some arrow between two objects in the image (application) of \(F\) then there exists some preimage arrow in \(C\) that maps to it. But we can have objects and morphisms outside the image of \(F\) that do not have any preimage in \(C\).
      • In other words it does not mean the functor is surjective on objects or morphisms in general.
    • The functor \(F\) is called fully faithful if for every pair of objects \(X, Y \in \mathrm {Ob}(C)\) the function \(F_{X, Y}\) is bijective. We say that a fully faithful functor is necessarily injective on objects up to isomorphism, that is assuming \(F\) is fully faithful then we have: \[ F(X) \cong F(Y) \implies X \cong Y \] This means that if two objects in the image of \(F\) are isomorphic then their preimages in \(C\) must also be isomorphic. In other words what this means is that a fully faithful functor preserves distinctness of objects up to the point of being the same for all practical purposes (i.e. isomorphism).