YonedaEmbedding.hs

-- {-# LANGUAGE FlexibleContexts, MultiParamTypeClasses #-}

{-| Module  : FiniteCategories
Description : The Yoneda embedding of a category.
Copyright   : Guillaume Sabbagh 2021
License     : GPL-3
Maintainer  : guillaumesabbagh@protonmail.com
Stability   : experimental
Portability : portable

The Yoneda embedding of a category.
-}

module YonedaEmbedding.YonedaEmbedding where
    import FiniteCategory.FiniteCategory
    import FunctorCategory.FunctorCategory
    import Diagram.Diagram
    import OppositeCategory.OppositeCategory
    import Set.FinSet
    import Utils.AssociationList
    import Subcategories.Subcategory
    import Currying.Currying
    import OppositeCategory.OppositeCategory
    import Limit.Limit
    import ConeCategory.ConeCategory
    import DiagonalFunctor.DiagonalFunctor
    import Utils.Tuple
    
    import IO.PrettyPrint
    
    -- | A presheaf on a category @C@ is a diagram from @C^op@ to __Set__.
    type PreSheaf c m o = Diagram (OppositeCategory c m o) (OppositeMorphism m o) o (FinSetCat m) (FinMap m) (FinSet m)
    
    -- | Natural transformation between presheaves.
    type PreSheavesNatTransfo c m o = NaturalTransformation (OppositeCategory c m o) (OppositeMorphism m o) o (FinSetCat m) (FinMap m) (FinSet m)
    
    -- | The type of the category of presheaves.
    type PreSheavesCategory c m o = FunctorCategory (OppositeCategory c m o) (OppositeMorphism m o) o (FinSetCat m) (FinMap m) (FinSet m)
    
    -- | Returns the presheaf category generated by a Yoneda embedding and an insertion functor full and faithful.
    yonedaEmbedding :: (FiniteCategory c m o, Morphism m o, Eq m, Eq o) => c -> (PreSheavesCategory c m o, Diagram c m o (PreSheavesCategory c m o) (PreSheavesNatTransfo c m o) (PreSheaf c m o))
    yonedaEmbedding cat = (presheavesCat, functor)
        where
            hom x = fromList $ fromList <$> (\s -> Elem <$> ar cat s x) <$> (ob cat)
            omapPresheaf x s = fromList $ Elem <$> ar cat s x
            mmapPresheaf x m = FinMap{codomain = omapPresheaf x (target m)
                                    , finMap = zip (toList (omapPresheaf x (source m))) ((\f -> fmap (@ (opOpMorph m)) f) <$> (toList (omapPresheaf x (source m))))}
            presheaf x = Diagram {    src = Op cat
                                    , tgt = FinSetCat $ toList $ union $ hom <$> ob cat
                                    , omap = functToAssocList (omapPresheaf x) (ob (Op cat))
                                    , mmap = functToAssocList (mmapPresheaf x) (arrows (Op cat))}
                                        
            ntFromMorph m o = FinMap {codomain = (omap $ presheaf (target m)) !-! o
                                    , finMap = zip (toList domain) (toList postcom) }
                where
                    domain = (omap $ presheaf (source m)) !-! o
                    postcom = (m @) `fmap` domain
            mmapFunctor m = NaturalTransformation {   srcNT = presheaf (source m)
                                                    , tgtNT = presheaf (target m)
                                                    , component = ntFromMorph m}
                                                        
            presheavesCat = FunctorCategory { sourceCat = Op cat
                                            , targetCat = FinSetCat $ concat (toList <$> (hom <$> ob cat))}
            functor = Diagram {   src = cat
                                , tgt = presheavesCat
                                , omap = functToAssocList presheaf (ob cat)
                                , mmap = functToAssocList mmapFunctor (arrows cat)
                              }