# 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₁) [] (D : Type u₂) [] extends :
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 .

Instances For

Notation for a functor between categories.

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem CategoryTheory.Functor.map_comp_assoc {C : Type u₁} {D : Type u₂} (F : ) {X : C} {Y : C} {Z : C} (f : X Y) (g : Y Z) {W : D} (h : F.obj Z W) :
def CategoryTheory.Functor.id (C : Type u₁) [] :

𝟭 C is the identity functor on a category C.

Equations
Instances For

Notation for the identity functor on a category.

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

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

Equations
Instances For

Notation for composition of functors.

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