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.
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.
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
@[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}
:
@[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}
:
@[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}
:
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]
:
Bundle a functorial function as a functor.
Equations
- CategoryTheory.Functor.of F = { toPrefunctor := { obj := F, map := fun {X Y : C} => CategoryTheory.map F }, map_id := ⋯, map_comp := ⋯ }
instance
CategoryTheory.instFunctorialObjToQuiverToCategoryStructToQuiverToCategoryStructToPrefunctor
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
(F : CategoryTheory.Functor C D)
:
Equations
- CategoryTheory.instFunctorialObjToQuiverToCategoryStructToQuiverToCategoryStructToPrefunctor 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
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
- One or more equations did not get rendered due to their size.