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

class CategoryTheory.Functorial {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : C → D) : Type (max v₁ v₂ u₁ u₂)

An unbundled functor.

• map' {X Y : C} : (X ⟶ Y) → (F X ⟶ F Y)

  A functorial map extends to an action on morphisms.

• map_id' (X : C) : map' (CategoryStruct.id X) = CategoryStruct.id (F X)

  A functorial map preserves identities.

• map_comp' {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) : map' (CategoryStruct.comp f g) = CategoryStruct.comp (map' f) (map' g)

  A functorial map preserves composition of morphisms.

def CategoryTheory.map {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : C → D) [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

• CategoryTheory.map F f = CategoryTheory.Functorial.map' f

@[simp]

theorem CategoryTheory.map'_as_map {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F : C → D} [Functorial F] {X Y : C} {f : X ⟶ Y} : Functorial.map' f = map F f

@[simp]

theorem CategoryTheory.Functorial.map_id {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F : C → D} [Functorial F] {X : C} : map F (CategoryStruct.id X) = CategoryStruct.id (F X)

@[simp]

theorem CategoryTheory.Functorial.map_comp {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F : C → D} [Functorial F] {X Y Z : C} {f : X ⟶ Y} {g : Y ⟶ Z} : map F (CategoryStruct.comp f g) = CategoryStruct.comp (map F f) (map F g)

def CategoryTheory.Functor.of {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : C → D) [I : Functorial F] : Functor C D

Bundle a functorial function as a functor.

Equations

• CategoryTheory.Functor.of F = { obj := F, map := fun {X Y : C} => CategoryTheory.map F, map_id := ⋯, map_comp := ⋯ }

instance CategoryTheory.instFunctorialObj {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) : Functorial F.obj

Equations

• CategoryTheory.instFunctorialObj F = { map' := fun {X Y : C} => F.map, map_id' := ⋯, map_comp' := ⋯ }

@[simp]

theorem CategoryTheory.map_functorial_obj {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) {X Y : C} (f : X ⟶ Y) : map F.obj f = F.map f

instance CategoryTheory.functorial_id {C : Type u₁} [Category.{v₁, u₁} C] : Functorial id

Equations

• CategoryTheory.functorial_id = { map' := fun {X Y : C} (f : X ⟶ Y) => f, map_id' := ⋯, map_comp' := ⋯ }

def CategoryTheory.functorial_comp {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] (F : C → D) [Functorial F] (G : D → E) [Functorial G] : Functorial (G ∘ F)

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

Equations

• CategoryTheory.functorial_comp F G = { map' := fun {X Y : C} (f : X ⟶ Y) => CategoryTheory.map G (CategoryTheory.map F f), map_id' := ⋯, map_comp' := ⋯ }