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

class CategoryTheory.Functorial {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.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), CategoryTheory.Functorial.map' (CategoryTheory.CategoryStruct.id X) = CategoryTheory.CategoryStruct.id (F X)

  A functorial map preserves identities.

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

  A functorial map preserves composition of morphisms.

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

A functorial map preserves identities.

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

A functorial map preserves composition of morphisms.

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

@[simp]

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

@[simp]

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

def CategoryTheory.Functor.of {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : C → D) [I : CategoryTheory.Functorial F] : CategoryTheory.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₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) : CategoryTheory.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₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) {X : C} {Y : C} (f : X ⟶ Y) : CategoryTheory.map F.obj f = F.map f

instance CategoryTheory.functorial_id {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] : CategoryTheory.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₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] (F : C → D) [CategoryTheory.Functorial F] (G : D → E) [CategoryTheory.Functorial G] : CategoryTheory.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' := ⋯ }