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/Basic.lean because that file shouldn't import Mathlib/CategoryTheory/Limits/Shapes/FiniteProducts.lean.

source
instance CategoryTheory.Limits.instHasFiniteLimitsFunctor {C : Type u_1} [Category.{v_1, u_1} C] {K : Type u_2} [Category.{v_2, u_2} K] [HasFiniteLimits C] :
HasFiniteLimits (Functor K C)
source
instance CategoryTheory.Limits.instHasFiniteProductsFunctor {C : Type u_1} [Category.{v_1, u_1} C] {K : Type u_2} [Category.{v_2, u_2} K] [HasFiniteProducts C] :
HasFiniteProducts (Functor K C)
source
instance CategoryTheory.Limits.instHasFiniteColimitsFunctor {C : Type u_1} [Category.{v_1, u_1} C] {K : Type u_2} [Category.{v_2, u_2} K] [HasFiniteColimits C] :
HasFiniteColimits (Functor K C)
source
instance CategoryTheory.Limits.instHasFiniteCoproductsFunctor {C : Type u_1} [Category.{v_1, u_1} C] {K : Type u_2} [Category.{v_2, u_2} K] [HasFiniteCoproducts C] :
HasFiniteCoproducts (Functor K C)
source
instance CategoryTheory.Limits.instPreservesFiniteLimitsFunctorObjEvaluationOfHasFiniteLimits {C : Type u_1} [Category.{v_1, u_1} C] {K : Type u_2} [Category.{v_2, u_2} K] [HasFiniteLimits C] (k : K) :
PreservesFiniteLimits ((evaluation K C).obj k)
source
instance CategoryTheory.Limits.instPreservesFiniteColimitsFunctorObjEvaluationOfHasFiniteColimits {C : Type u_1} [Category.{v_1, u_1} C] {K : Type u_2} [Category.{v_2, u_2} K] [HasFiniteColimits C] (k : K) :
PreservesFiniteColimits ((evaluation K C).obj k)