{-# LANGUAGE MultiParamTypeClasses #-}
{-| Module : FiniteCategories
Description : The lim functor which takes every diagram to its limit object. See also ConeCategory for the limit of a specific diagram.
Copyright : Guillaume Sabbagh 2021
License : GPL-3
Maintainer : guillaumesabbagh@protonmail.com
Stability : experimental
Portability : portable
The lim functor which takes every diagram to its limit object according to the global definition of limit. See also ConeCategory for the limit of a specific diagram.
-}
module Limit.Limit
(
limitFunctor,
colimitFunctor,
)
where
import FiniteCategory.FiniteCategory
import Diagram.Diagram
import Adjunction.Adjunction
import FunctorCategory.FunctorCategory
import DiagonalFunctor.DiagonalFunctor
import IO.PrettyPrint
-- | Returns the limit functor according to the global definition of limit (see https://ncatlab.org/nlab/show/limit#global_definition_in_terms_of_adjoint_of_the_constant_diagram_functor).
--
-- Given an indexing category @J@ and a category @C@, returns a functor which maps each diagram of form @J@ in @C@ to its limit object in @C@.
limitFunctor :: (FiniteCategory c1 m1 o1, Morphism m1 o1, Eq c1, Eq m1, Eq o1, PrettyPrintable c1, PrettyPrintable c2, PrettyPrintable o1, PrettyPrintable o2, PrettyPrintable m1, PrettyPrintable m2,
FiniteCategory c2 m2 o2, Morphism m2 o2, Eq c2, Eq m2, Eq o2) =>
c1 -> c2 -> Diagram (FunctorCategory c1 m1 o1 c2 m2 o2) (NaturalTransformation c1 m1 o1 c2 m2 o2) (Diagram c1 m1 o1 c2 m2 o2) c2 m2 o2
limitFunctor j c = rightAdjoint $ mkDiagonalFunctor j c
-- | Returns the colimit functor according to the global definition of colimit (see https://ncatlab.org/nlab/show/limit#global_definition_in_terms_of_adjoint_of_the_constant_diagram_functor).
--
-- Given an indexing category @J@ and a category @C@, returns a functor which maps each diagram of form @J@ in @C@ to its colimit object in @C@.
colimitFunctor :: (FiniteCategory c1 m1 o1, Morphism m1 o1, Eq c1, Eq m1, Eq o1,
FiniteCategory c2 m2 o2, Morphism m2 o2, Eq c2, Eq m2, Eq o2) =>
c1 -> c2 -> Diagram (FunctorCategory c1 m1 o1 c2 m2 o2) (NaturalTransformation c1 m1 o1 c2 m2 o2) (Diagram c1 m1 o1 c2 m2 o2) c2 m2 o2
colimitFunctor j c = leftAdjoint $ mkDiagonalFunctor j c