mathlib documentation

category_theory.functor

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

𝟭 C is the identity functor on a category C.

Equations
@[instance]

Equations
@[simp]
theorem category_theory.functor.id_obj {C : Type u₁} [category_theory.category C] (X : C) :
(𝟭 C).obj X = X

@[simp]
theorem category_theory.functor.id_map {C : Type u₁} [category_theory.category C] {X Y : C} (f : X Y) :
(𝟭 C).map f = f

def category_theory.functor.comp {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {E : Type u₃} [category_theory.category E] :
C DD EC 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₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {E : Type u₃} [category_theory.category E] (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₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {E : Type u₃} [category_theory.category E] (F : C D) (G : D E) {X Y : C} (f : X Y) :
(F G).map f = G.map (F.map f)

theorem category_theory.functor.comp_id {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (F : C D) :
F 𝟭 D = F

theorem category_theory.functor.id_comp {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (F : C D) :
𝟭 C F = F