mathlib documentation

category_theory.functorial

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

@[class]
structure category_theory.functorial {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] :
(C → D)Type (max v₁ v₂ u₁ u₂)

A unbundled functor.

Instances
def category_theory.map {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (F : C → D) [category_theory.functorial F] {X Y : C} :
(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₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {F : C → D} [category_theory.functorial F] {X Y : C} {f : X Y} :

@[simp]
theorem category_theory.functorial.map_id {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {F : C → D} [category_theory.functorial F] {X : C} :

@[simp]
theorem category_theory.functorial.map_comp {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {F : C → D} [category_theory.functorial F] {X Y Z : C} {f : X Y} {g : Y Z} :

def category_theory.functor.of {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (F : C → D) [I : category_theory.functorial F] :
C D

Bundle a functorial function as a functor.

Equations
@[simp]
theorem category_theory.map_functorial_obj {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (F : C D) {X Y : C} (f : X Y) :

@[instance]

Equations

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

Equations