# mathlibdocumentation

category_theory.functor

def category_theory.functor.to_prefunctor {C : Type u₁} {D : Type u₂} (self : C D) :
D

The prefunctor between the underlying quivers.

structure category_theory.functor (C : Type u₁) (D : Type u₂)  :
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.

@[simp]
theorem category_theory.functor.map_id {C : Type u₁} {D : Type u₂} (c : C D) (X : C) :
c.map (𝟙 X) = 𝟙 (c.obj X)
@[simp]
theorem category_theory.functor.map_comp {C : Type u₁} {D : Type u₂} (c : C D) {X Y Z : C} (f : X Y) (g : Y Z) :
c.map (f g) = c.map f c.map g
theorem category_theory.functor.map_comp_assoc {C : Type u₁} {D : Type u₂} (c : C D) {X Y Z : C} (f : X Y) (g : Y Z) {X' : D} (f' : c.obj Z X') :
c.map (f g) f' = c.map f c.map g f'
@[protected]
def category_theory.functor.id (C : Type u₁)  :
C C

𝟭 C is the identity functor on a category C.

Equations
@[protected, instance]
def category_theory.functor.inhabited (C : Type u₁)  :
Equations
@[simp]
theorem category_theory.functor.id_obj {C : Type u₁} (X : C) :
(𝟭 C).obj X = X
@[simp]
theorem category_theory.functor.id_map {C : Type u₁} {X Y : C} (f : X Y) :
(𝟭 C).map f = f
def category_theory.functor.comp {C : Type u₁} {D : Type u₂} {E : Type u₃} (F : C D) (G : D E) :
C E

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

Equations
@[simp]
theorem category_theory.functor.comp_obj {C : Type u₁} {D : Type u₂} {E : Type u₃} (F : C D) (G : D E) (X : C) :
(F G).obj X = G.obj (F.obj X)
@[simp]
theorem category_theory.functor.comp_map {C : Type u₁} {D : Type u₂} {E : Type u₃} (F : C D) (G : D E) {X Y : C} (f : X Y) :
(F G).map f = G.map (F.map f)
@[protected]
theorem category_theory.functor.comp_id {C : Type u₁} {D : Type u₂} (F : C D) :
F 𝟭 D = F
@[protected]
theorem category_theory.functor.id_comp {C : Type u₁} {D : Type u₂} (F : C D) :
𝟭 C F = F
@[simp]
theorem category_theory.functor.map_dite {C : Type u₁} {D : Type u₂} (F : C D) {X Y : C} {P : Prop} [decidable P] (f : P → (X Y)) (g : ¬P → (X Y)) :
F.map (dite P (λ (h : P), f h) (λ (h : ¬P), g h)) = dite P (λ (h : P), F.map (f h)) (λ (h : ¬P), F.map (g h))
theorem category_theory.functor.monotone {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] (F : α β) :