mathlib documentation

category_theory.functor.functorial

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

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

@[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 of this typeclass
Instances of other typeclasses for category_theory.functorial
  • category_theory.functorial.has_sizeof_inst
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

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) :
@[protected, instance]
Equations