Documentation

Mathlib.CategoryTheory.Limits.FunctorCategory.Finite

Functor categories have finite limits when the target category does #

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

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