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

Adjunctions are all over the place in mathematics.
-}

module Math.Functors.Adjunction 
(
    leftAdjoint,
    rightAdjoint,
)
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
    import              Math.Categories.CommaCategory
    
    -- | Returns the left adjoint of a functor, if the left adjoint does not exist, returns a partial Diagram being the best ajoint we could construct.
    leftAdjoint :: (FiniteCategory c1 m1 o1, Morphism m1 o1, Eq m1, Eq o1,
                     FiniteCategory c2 m2 o2, Morphism m2 o2, Eq m2, Eq o2) =>
                     Diagram c1 m1 o1 c2 m2 o2 -> Diagram c2 m2 o2 c1 m1 o1
    leftAdjoint g = Diagram {
                        src = tgt g,
                        tgt = src g,
                        omap = om,
                        mmap = weakMapFromSet [(m, anElement (binding m)) | m <- arrows (tgt g), Map.member (source m) om && Map.member (target m) om && not (Set.null (binding m))]
                    }
        where
            universalMorphisms y = initialObjects (CommaCategory {rightDiagram = g, leftDiagram = (selectObject (tgt g) y)})
            yToUniversalMorphism = weakMapFromSet [(y, anElement.universalMorphisms $ y) | y <- ob (tgt g), not (Set.null (universalMorphisms y))]
            om = Map.map indexTarget yToUniversalMorphism
            yToEta = Map.map selectedArrow yToUniversalMorphism 
            binding m = [a | a <- ar (src g) (om |!| (source m)) (om |!| (target m)), ((yToEta |!| target m) @ m) == (g ->£ a) @ (yToEta |!| source m)]
    
    -- | Returns the right adjoint of a functor, if the right adjoint does not exist, returns a partial Diagram being the best ajoint we could construct.
    rightAdjoint :: (FiniteCategory c1 m1 o1, Morphism m1 o1, Eq m1, Eq o1,
                     FiniteCategory c2 m2 o2, Morphism m2 o2, Eq m2, Eq o2) =>
                     Diagram c2 m2 o2 c1 m1 o1 -> Diagram c1 m1 o1 c2 m2 o2
    rightAdjoint f = Diagram {
                        src = tgt f,
                        tgt = src f,
                        omap = om,
                        mmap = weakMapFromSet [(m, anElement  (binding m)) | m <- arrows (tgt f), (Map.member (source m) om) && (Map.member (target m) om) && not (Set.null (binding m))]
                    }
        where
            universalMorphisms x = terminalObjects (CommaCategory {leftDiagram = f, rightDiagram = (selectObject (tgt f) x)})
            xToUniversalMorphism = weakMapFromSet [(x, anElement.universalMorphisms $ x) | x <- ob (tgt f), not (Set.null (universalMorphisms x))]
            om = Map.map indexSource xToUniversalMorphism
            xToEps = Map.map selectedArrow xToUniversalMorphism
            binding m = [a | a <- ar (src f) (om |!| (source m)) (om |!| (target m)), ((xToEps |!| target m) @ (f ->£ a)) == (m @ (xToEps |!| source m))]