Adjunction.hs

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

Adjunctions are all over the place in mathematics.
-}

module Adjunction.Adjunction 
(
    leftAdjoint,
    rightAdjoint,
)
where
    import              FiniteCategory.FiniteCategory
    import              Diagram.Diagram
    import              CommaCategory.CommaCategory
    import              Data.Maybe                          (fromJust)
    import              Utils.AssociationList
    
    -- | 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 = [(y, indexTgt.head.universalMorphisms $ y) | y <- ob (tgt g), not (null (universalMorphisms y))],
                        mmap = [(m, head (binding m)) | m <- arrows (tgt g), not (null (binding m))]
                    }
        where
            universalMorphisms y = initialObjects (CommaCategory {rightDiag = g, leftDiag = fromJust (mkSelect1 (tgt g) y)})
            binding m = [a | a <- arrows (src g), (not (null (universalMorphisms (source m)))) && (not (null (universalMorphisms (target m)))) && ((target ((mmap g) !-! a)) == (source (arrow.head.universalMorphisms $ target m))) && (((arrow.head.universalMorphisms $ target m) @ m) == ((mmap g) !-! a) @ (arrow.head.universalMorphisms $ 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 = [(x, indexSrc.head.universalMorphisms $ x) | x <- ob (tgt f), not (null (universalMorphisms x))],
                        mmap = [(m, head (binding m)) | m <- arrows (tgt f), (not (null (universalMorphisms (source m)))) && (not (null (universalMorphisms (target m)))) && not (null (binding m))]
                    }
        where
            universalMorphisms x = terminalObjects (CommaCategory {leftDiag = f, rightDiag = fromJust (mkSelect1 (tgt f) x)})
            binding m = [a | a <- ar (src f) (indexSrc.head.universalMorphisms $ (source m)) (indexSrc.head.universalMorphisms $ (target m)), ((arrow.head.universalMorphisms $ target m) @ ((mmap f) !-! a)) == (m @ (arrow.head.universalMorphisms $ source m))]