mathlib documentation

category_theory.functor.basic

Functors #

Defines a functor between categories, extending a prefunctor between quivers.

Introduces notation C ⥤ D for the type of all functors from C to D. (Unfortunately the ⇒ arrow (\functor) is taken by core, but in mathlib4 we should switch to this.)

source
def category_theory.functor.to_prefunctor {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (self : C ⥤ D) :
prefunctor C D

The prefunctor between the underlying quivers.

source
structure category_theory.functor (C : Type u₁) [category_theory.category C] (D : Type u₂) [category_theory.category D] :
Type (max v₁ v₂ u₁ u₂)
  • obj : C → D
  • map : Π {X Y : C}, (X ⟶ Y) → (self.obj X ⟶ self.obj Y)
  • map_id' : (∀ (X : C), self.map (𝟙 X) = 𝟙 (self.obj X)) . "obviously"
  • map_comp' : (∀ {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z), self.map (f ≫ g) = self.map f ≫ self.map g) . "obviously"

functor C D represents a functor between categories C and D.

To apply a functor F to an object use F.obj X, and to a morphism use F.map f.

The axiom map_id expresses preservation of identities, and map_comp expresses functoriality.

See https://stacks.math.columbia.edu/tag/001B.

source
@[simp]
theorem category_theory.functor.map_id {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (self : C ⥤ D) (X : C) :
self.map (𝟙 X) = 𝟙 (self.obj X)
source
@[simp]
theorem category_theory.functor.map_comp {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (self : C ⥤ D) {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) :
self.map (f ≫ g) = self.map f ≫ self.map g
source
theorem category_theory.functor.map_comp_assoc {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (self : C ⥤ D) {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) {X' : D} (f' : self.obj Z ⟶ X') :
self.map (f ≫ g) ≫ f' = self.map f ≫ self.map g ≫ f'
source
@[protected]
def category_theory.functor.id (C : Type u₁) [category_theory.category C] :
C ⥤ C

𝟭 C is the identity functor on a category C.

Equations
source
@[protected, instance]
def category_theory.functor.inhabited (C : Type u₁) [category_theory.category C] :
inhabited (C ⥤ C)
Equations
source
@[simp]
theorem category_theory.functor.id_obj {C : Type u₁} [category_theory.category C] (X : C) :
(𝟭 C).obj X = X
source
@[simp]
theorem category_theory.functor.id_map {C : Type u₁} [category_theory.category C] {X Y : C} (f : X ⟶ Y) :
(𝟭 C).map f = f
source
def category_theory.functor.comp {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {E : Type u₃} [category_theory.category E] (F : C ⥤ D) (G : D ⥤ E) :
C ⥤ E

F ⋙ G is the composition of a functor F and a functor G (F first, then G).

Equations
source
@[simp]
theorem category_theory.functor.comp_obj {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {E : Type u₃} [category_theory.category E] (F : C ⥤ D) (G : D ⥤ E) (X : C) :
(F ⋙ G).obj X = G.obj (F.obj X)
source
@[simp]
theorem category_theory.functor.comp_map {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {E : Type u₃} [category_theory.category E] (F : C ⥤ D) (G : D ⥤ E) {X Y : C} (f : X ⟶ Y) :
(F ⋙ G).map f = G.map (F.map f)
source
@[protected]
theorem category_theory.functor.comp_id {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (F : C ⥤ D) :
F ⋙ 𝟭 D = F
source
@[protected]
theorem category_theory.functor.id_comp {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (F : C ⥤ D) :
𝟭 C ⋙ F = F
source
@[simp]
theorem category_theory.functor.map_dite {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (F : C ⥤ D) {X Y : C} {P : Prop} [decidable P] (f : P → (X ⟶ Y)) (g : ¬P → (X ⟶ Y)) :
F.map (dite P (λ (h : P), f h) (λ (h : ¬P), g h)) = dite P (λ (h : P), F.map (f h)) (λ (h : ¬P), F.map (g h))