DiagonalFunctor.hs

{-| Module  : FiniteCategories
Description : Diagonal functor of an index category.
Copyright   : Guillaume Sabbagh 2021
License     : GPL-3
Maintainer  : guillaumesabbagh@protonmail.com
Stability   : experimental
Portability : portable

Let /J/ and /C/ be two categories, we consider the functor category /C/^/J/.
The diagonal functor /D/ : /C/ -> /C/^/J/ maps each object /x/ of /C/ to the constant diagram /D_x/ from /J/ to /C/.
It maps each morphism to the natural transformation between the two constant diagrams associated to the source and the target of the morphism.
-}

module DiagonalFunctor.DiagonalFunctor
(
mkDiagonalFunctor
)
where
    import Diagram.Diagram
    import FiniteCategory.FiniteCategory
    import FunctorCategory.FunctorCategory
    import Data.Maybe                              (fromJust)
    import Utils.AssociationList
    
    -- | Given two categories /J/ and /C/, returns the diagonal functor /C/ -> /C/^/J/.
    mkDiagonalFunctor :: (FiniteCategory c1 m1 o1, Morphism m1 o1,
                         FiniteCategory c2 m2 o2, Morphism m2 o2, Eq o2) =>
                        c1 -- ^ /J/
                     -> c2 -- ^ /C/
                     -> Diagram c2 m2 o2 (FunctorCategory c1 m1 o1 c2 m2 o2) (NaturalTransformation c1 m1 o1 c2 m2 o2) (Diagram c1 m1 o1 c2 m2 o2) -- ^ /D/ : /C/ -> /C/^/J/
    mkDiagonalFunctor j c = Diagram{src=c
                                  , tgt=FunctorCategory{sourceCat=j, targetCat=c}
                                  , omap=functToAssocList (\o ->  constDiag o) (ob c)
                                  , mmap=functToAssocList (\f -> NaturalTransformation{srcNT=constDiag (source f),tgtNT=constDiag (target f),component=(\x->f)}) (arrows c)}
                            where
                                constDiag obj = fromJust $ mkConstantDiagram j c obj