Unbundled functors, as a typeclass decorating the object-level function.
@[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₂)
- map : Π {X Y : C}, (X ⟶ Y) → (F X ⟶ F Y)
- map_id' : (∀ (X : C), category_theory.functorial.map (𝟙 X) = 𝟙 (F X)) . "obviously"
- map_comp' : (∀ {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z), category_theory.functorial.map (f ≫ g) = category_theory.functorial.map f ≫ category_theory.functorial.map g) . "obviously"
A unbundled functor.
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
@[simp]
theorem
category_theory.map_as_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} :
@[simp]
theorem
category_theory.functorial.map_id
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{F : C → D}
[category_theory.functorial F]
{X : C} :
category_theory.map F (𝟙 X) = 𝟙 (F X)
@[simp]
theorem
category_theory.functorial.map_comp
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{F : C → D}
[category_theory.functorial F]
{X Y Z : C}
{f : X ⟶ Y}
{g : Y ⟶ Z} :
category_theory.map F (f ≫ g) = category_theory.map F f ≫ category_theory.map F g
def
category_theory.functor.of
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(F : C → D)
[I : category_theory.functorial F] :
C ⥤ D
Bundle a functorial function as a functor.
Equations
- category_theory.functor.of F = {obj := F, map := category_theory.functorial.map I, map_id' := _, map_comp' := _}
@[instance]
def
category_theory.category_theory.functorial
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(F : C ⥤ D) :
@[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) :
category_theory.map F.obj f = F.map f
@[instance]
def
category_theory.functorial_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)
[category_theory.functorial F]
(G : D → E)
[category_theory.functorial G] :
category_theory.functorial (G ∘ F)
G ∘ F is a functorial if both F and G are.
Equations
- category_theory.functorial_comp F G = {map := (category_theory.functor.of F ⋙ category_theory.functor.of G).map, map_id' := _, map_comp' := _}