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] (F : 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} (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₁} [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