Documentation

Mathlib.CategoryTheory.Functor.Basic

Functors #

Defines a functor between categories, extending a Prefunctor between quivers.

Introduces, in the CategoryTheory scope, notations C ⥤ D for the type of all functors from C to D, 𝟭 for the identity functor and for functor composition.

TODO: Switch to using the arrow.

structure CategoryTheory.Functor (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] extends Prefunctor :
Type (max v₁ v₂ u₁ u₂)

Functor C D represents a functor between categories C and D.

To apply a functor F to an object use F.obj X, and to a morphism use F.map f.

The axiom map_id expresses preservation of identities, and map_comp expresses functoriality.

See https://stacks.math.columbia.edu/tag/001B.

Instances For
    @[simp]

    A functor preserves identity morphisms.

    @[simp]
    theorem CategoryTheory.Functor.map_comp {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (self : CategoryTheory.Functor C D) {X : C} {Y : C} {Z : C} (f : X Y) (g : Y Z) :

    A functor preserves composition.

    Notation for a functor between categories.

    Equations
    Instances For

      𝟭 C is the identity functor on a category C.

      Equations
      Instances For

        Notation for the identity functor on a category.

        Equations
        Instances For
          @[simp]
          theorem CategoryTheory.Functor.id_map {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {Y : C} (f : X Y) :

          F ⋙ G is the composition of a functor F and a functor G (F first, then G).

          Equations
          • F.comp G = { obj := fun (X : C) => G.obj (F.obj X), map := fun {X Y : C} (f : X Y) => G.map (F.map f), map_id := , map_comp := }
          Instances For

            Notation for composition of functors.

            Equations
            Instances For
              @[simp]
              theorem CategoryTheory.Functor.comp_map {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] (F : CategoryTheory.Functor C D) (G : CategoryTheory.Functor D E) {X : C} {Y : C} (f : X Y) :
              (F.comp G).map f = G.map (F.map f)
              @[simp]
              theorem CategoryTheory.Functor.map_dite {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) {X : C} {Y : C} {P : Prop} [Decidable P] (f : P(X Y)) (g : ¬P(X Y)) :
              F.map (if h : P then f h else g h) = if h : P then F.map (f h) else F.map (g h)
              @[simp]