If D has finite (co)limits, so do the functor categories C ⥤ D. #
These are boiler-plate instances, in their own file as neither import otherwise needs the other.
instance
CategoryTheory.Limits.functor_category_hasFiniteLimits
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
[CategoryTheory.Limits.HasFiniteLimits D]
:
Equations
- ⋯ = ⋯
instance
CategoryTheory.Limits.functor_category_hasFiniteColimits
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
[CategoryTheory.Limits.HasFiniteColimits D]
:
Equations
- ⋯ = ⋯