mathlib3 documentation

category_theory.limits.shapes.functor_category

If D has finite (co)limits, so do the functor categories C ⥤ D. #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

These are boiler-plate instances, in their own file as neither import otherwise needs the other.

source
@[protected, instance]
def category_theory.limits.functor_category_has_finite_limits {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] [category_theory.limits.has_finite_limits D] :
category_theory.limits.has_finite_limits (C ⥤ D)
source
@[protected, instance]
def category_theory.limits.functor_category_has_finite_colimits {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] [category_theory.limits.has_finite_colimits D] :
category_theory.limits.has_finite_colimits (C ⥤ D)