Documentation

Mathlib.CategoryTheory.Limits.FunctorCategory.Finite

Functor categories have finite limits when the target category does #

These declarations cannot be in Mathlib/CategoryTheory/Limits/FunctorCategory.lean because that file shouldn't import Mathlib/CategoryTheory/Limits/Shapes/FiniteProducts.lean.

source
instance CategoryTheory.Limits.instHasFiniteLimitsFunctor {C : Type u_1} [Category.{u_3, u_1} C] {K : Type u_2} [Category.{u_4, u_2} K] [HasFiniteLimits C] :
HasFiniteLimits (Functor K C)
source
instance CategoryTheory.Limits.instHasFiniteProductsFunctor {C : Type u_1} [Category.{u_3, u_1} C] {K : Type u_2} [Category.{u_4, u_2} K] [HasFiniteProducts C] :
HasFiniteProducts (Functor K C)
source
instance CategoryTheory.Limits.instHasFiniteColimitsFunctor {C : Type u_1} [Category.{u_3, u_1} C] {K : Type u_2} [Category.{u_4, u_2} K] [HasFiniteColimits C] :
HasFiniteColimits (Functor K C)
source
instance CategoryTheory.Limits.instHasFiniteCoproductsFunctor {C : Type u_1} [Category.{u_3, u_1} C] {K : Type u_2} [Category.{u_4, u_2} K] [HasFiniteCoproducts C] :
HasFiniteCoproducts (Functor K C)