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.
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) → (c.obj X ⟶ c.obj Y)
- map_id' : (∀ (X : C), c.map (𝟙 X) = 𝟙 (c.obj X)) . "obviously"
- map_comp' : (∀ {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z), c.map (f ≫ g) = c.map f ≫ c.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.
@[simp]
theorem
category_theory.functor.map_id
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(c : C ⥤ D)
(X : C) :
@[simp]
theorem
category_theory.functor.map_comp
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(c : C ⥤ D)
{X Y Z : C}
(f : X ⟶ Y)
(g : Y ⟶ Z) :
@[protected, instance]
Equations
- category_theory.functor.inhabited C = {default := 𝟭 C _inst_1}
@[simp]
@[simp]
theorem
category_theory.functor.id_map
{C : Type u₁}
[category_theory.category C]
{X Y : C}
(f : X ⟶ Y) :
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).
@[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) :
@[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) :
@[protected]
theorem
category_theory.functor.comp_id
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(F : C ⥤ D) :
@[protected]
theorem
category_theory.functor.id_comp
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(F : C ⥤ D) :
@[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)) :