# mathlibdocumentation

category_theory.functorial

# Unbundled functors, as a typeclass decorating the object-level function. #

@[class]
structure category_theory.functorial {C : Type u₁} {D : Type u₂} (F : C → D) :
Type (max v₁ v₂ u₁ u₂)
• map : Π {X Y : C}, (X Y)(F X F Y)
• map_id' : (∀ (X : C), = 𝟙 (F X)) . "obviously"
• map_comp' : (∀ {X Y Z : C} (f : X Y) (g : Y Z), . "obviously"

A unbundled functor.

Instances
def category_theory.map {C : Type u₁} {D : Type u₂} (F : C → D) {X Y : C} (f : X Y) :
F X F Y

If F : C → D (just a function) has [functorial F], we can write map F f : F X ⟶ F Y for the action of F on a morphism f : X ⟶ Y.

Equations
@[simp]
theorem category_theory.map_as_map {C : Type u₁} {D : Type u₂} {F : C → D} {X Y : C} {f : X Y} :
@[simp]
theorem category_theory.functorial.map_id {C : Type u₁} {D : Type u₂} {F : C → D} {X : C} :
(𝟙 X) = 𝟙 (F X)
@[simp]
theorem category_theory.functorial.map_comp {C : Type u₁} {D : Type u₂} {F : C → D} {X Y Z : C} {f : X Y} {g : Y Z} :
(f g) =
def category_theory.functor.of {C : Type u₁} {D : Type u₂} (F : C → D)  :
C D

Bundle a functorial function as a functor.

Equations
@[protected, instance]
def category_theory.functor.obj.functorial {C : Type u₁} {D : Type u₂} (F : C D) :
Equations
@[simp]
theorem category_theory.map_functorial_obj {C : Type u₁} {D : Type u₂} (F : C D) {X Y : C} (f : X Y) :
= F.map f
@[protected, instance]
def category_theory.functorial_id {C : Type u₁}  :
Equations
def category_theory.functorial_comp {C : Type u₁} {D : Type u₂} {E : Type u₃} (F : C → D) (G : D → E)  :

G ∘ F is a functorial if both F and G are.

Equations