DiagonalFunctor.hs

{-# LANGUAGE MonadComprehensions  #-}
{-# LANGUAGE MultiParamTypeClasses  #-}
{-| Module  : FiniteCategories
Description : Diagonal functor.
Copyright   : Guillaume Sabbagh 2022
License     : GPL-3
Maintainer  : guillaumesabbagh@protonmail.com
Stability   : experimental
Portability : portable

The diagonal functor sends each object to the constant functor on this object.
-}

module Math.Functors.DiagonalFunctor 
(
    diagonalFunctor,
)
where
    import              Data.WeakSet        (Set)
    import qualified    Data.WeakSet    as  Set
    import              Data.WeakSet.Safe
    import              Data.WeakMap        (Map)
    import qualified    Data.WeakMap    as  Map
    import              Data.WeakMap.Safe

    import              Math.FiniteCategory
    import              Math.Categories.FunctorCategory
    
    -- | Given two categories /J/ and /C/, return the diagonal functor /C/ -> /C/^/J/.
    --
    -- 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.
    diagonalFunctor :: (FiniteCategory c1 m1 o1, Morphism m1 o1,
                        FiniteCategory c2 m2 o2, Morphism m2 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/
    diagonalFunctor j c = Diagram{src=c
                                , tgt=FunctorCategory j c
                                , omap=memorizeFunction (constantDiagram j c) (ob c)
                                , mmap=memorizeFunction (\f -> unsafeNaturalTransformation (constantDiagram j c (source f)) (constantDiagram j c (target f)) (memorizeFunction (\x->f) (ob j))) (arrows c)}