Documentation

Mathlib.CategoryTheory.Functor.Basic

Functors #

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

Introduces notation C ⥤ D⥤ D for the type of all functors from C to D. (Unfortunately the ⇒⇒ arrow (\functor) is taken by core, but in mathlib4 we should switch to this.)

structure CategoryTheory.Functor (C : Type u₁) [inst : CategoryTheory.Category C] (D : Type u₂) [inst : CategoryTheory.Category D] extends Prefunctor :
Type (maxv₁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

    This unexpander will pretty print F.obj X properly. Without this, we would have Prefunctor.obj F.toPrefunctor X.

    Equations
    • One or more equations did not get rendered due to their size.

    This unexpander will pretty print F.map f properly. Without this, we would have Prefunctor.map F.toPrefunctor f.

    Equations
    • One or more equations did not get rendered due to their size.

    Notation for a functor between categories.

    Equations
    theorem CategoryTheory.Functor.map_comp_assoc {C : Type u₁} [inst : CategoryTheory.Category C] {D : Type u₂} [inst : CategoryTheory.Category D] (self : C D) {X : C} {Y : C} {Z : C} (f : X Y) (g : Y Z) {Z : D} (h : self.obj Z Z) :
    self.map (f g) h = self.map f self.map g h

    𝟭 C is the identity functor on a category C.

    Equations

    Notation for the identity functor on a category.

    Equations
    @[simp]
    theorem CategoryTheory.Functor.id_obj {C : Type u₁} [inst : CategoryTheory.Category C] (X : C) :
    (𝟭 C).obj X = X
    @[simp]
    theorem CategoryTheory.Functor.id_map {C : Type u₁} [inst : CategoryTheory.Category C] {X : C} {Y : C} (f : X Y) :
    (𝟭 C).map f = f
    @[simp]
    theorem CategoryTheory.Functor.comp_obj {C : Type u₁} [inst : CategoryTheory.Category C] {D : Type u₂} [inst : CategoryTheory.Category D] {E : Type u₃} [inst : CategoryTheory.Category E] (F : C D) (G : D E) (X : C) :
    (F G).obj X = G.obj (F.obj X)
    def CategoryTheory.Functor.comp {C : Type u₁} [inst : CategoryTheory.Category C] {D : Type u₂} [inst : CategoryTheory.Category D] {E : Type u₃} [inst : CategoryTheory.Category E] (F : C D) (G : D E) :
    C E

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

    Equations

    Notation for composition of functors.

    Equations
    • One or more equations did not get rendered due to their size.
    @[simp]
    theorem CategoryTheory.Functor.comp_map {C : Type u₁} [inst : CategoryTheory.Category C] {D : Type u₂} [inst : CategoryTheory.Category D] {E : Type u₃} [inst : CategoryTheory.Category E] (F : C D) (G : D E) {X : C} {Y : C} (f : X Y) :
    (F G).map f = G.map (F.map f)
    theorem CategoryTheory.Functor.comp_id {C : Type u₁} [inst : CategoryTheory.Category C] {D : Type u₂} [inst : CategoryTheory.Category D] (F : C D) :
    F 𝟭 D = F
    theorem CategoryTheory.Functor.id_comp {C : Type u₁} [inst : CategoryTheory.Category C] {D : Type u₂} [inst : CategoryTheory.Category D] (F : C D) :
    𝟭 C F = F
    @[simp]
    theorem CategoryTheory.Functor.map_dite {C : Type u₁} [inst : CategoryTheory.Category C] {D : Type u₂} [inst : CategoryTheory.Category D] (F : C D) {X : C} {Y : C} {P : Prop} [inst : 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]
    theorem CategoryTheory.Functor.toPrefunctor_comp {C : Type u₁} [inst : CategoryTheory.Category C] {D : Type u₂} [inst : CategoryTheory.Category D] {E : Type u₃} [inst : CategoryTheory.Category E] (F : C D) (G : D E) :
    F.toPrefunctor ⋙q G.toPrefunctor = (F G).toPrefunctor