{-# LANGUAGE MonadComprehensions  #-}
{-# LANGUAGE 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. Note that 'leftAdjoint' and 'rightAdjoint' are slow because we enumerate a lot of morphisms to find the universal morphisms. Prefer using your own construction of an adjoint if known.
-}

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.

    --

    -- Note that 'leftAdjoint' and 'rightAdjoint' are slow because we enumerate a lot of morphisms to find the universal morphisms. Prefer using your own construction of an adjoint if known.

    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 :: forall c1 m1 o1 c2 m2 o2.
(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 Diagram c1 m1 o1 c2 m2 o2
g = Diagram {
                        src :: c2
src = Diagram c1 m1 o1 c2 m2 o2 -> c2
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c2
tgt Diagram c1 m1 o1 c2 m2 o2
g,
                        tgt :: c1
tgt = Diagram c1 m1 o1 c2 m2 o2 -> c1
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c1
src Diagram c1 m1 o1 c2 m2 o2
g,
                        omap :: Map o2 o1
omap = Map o2 o1
om,
                        mmap :: Map m2 m1
mmap = Set (m2, m1) -> Map m2 m1
forall k v. Set (k, v) -> Map k v
weakMapFromSet [(m2
m, Set m1 -> m1
forall a. Set a -> a
anElement (m2 -> Set m1
binding m2
m)) | m2
m <- c2 -> Set m2
forall c m o. (FiniteCategory c m o, Morphism m o) => c -> Set m
arrows (Diagram c1 m1 o1 c2 m2 o2 -> c2
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c2
tgt Diagram c1 m1 o1 c2 m2 o2
g), o2 -> Map o2 o1 -> Bool
forall k a. Eq k => k -> Map k a -> Bool
Map.member (m2 -> o2
forall m o. Morphism m o => m -> o
source m2
m) Map o2 o1
om Bool -> Bool -> Bool
&& o2 -> Map o2 o1 -> Bool
forall k a. Eq k => k -> Map k a -> Bool
Map.member (m2 -> o2
forall m o. Morphism m o => m -> o
target m2
m) Map o2 o1
om Bool -> Bool -> Bool
&& Bool -> Bool
not (Set m1 -> Bool
forall a. Set a -> Bool
Set.null (m2 -> Set m1
binding m2
m))]
                    }
        where
            universalMorphisms :: o2 -> Set (CommaObject One o1 m2)
universalMorphisms o2
y = CommaCategory One One One c1 m1 o1 c2 m2 o2
-> Set (CommaObject One o1 m2)
forall c m o.
(FiniteCategory c m o, Morphism m o, Eq m, Eq o) =>
c -> Set o
initialObjects (CommaCategory {rightDiagram :: Diagram c1 m1 o1 c2 m2 o2
rightDiagram = Diagram c1 m1 o1 c2 m2 o2
g, leftDiagram :: Diagram One One One c2 m2 o2
leftDiagram = (c2 -> o2 -> Diagram One One One c2 m2 o2
forall c m o.
(Category c m o, Morphism m o, Eq o) =>
c -> o -> Diagram One One One c m o
selectObject (Diagram c1 m1 o1 c2 m2 o2 -> c2
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c2
tgt Diagram c1 m1 o1 c2 m2 o2
g) o2
y)})
            yToUniversalMorphism :: Map o2 (CommaObject One o1 m2)
yToUniversalMorphism = Set (o2, CommaObject One o1 m2) -> Map o2 (CommaObject One o1 m2)
forall k v. Set (k, v) -> Map k v
weakMapFromSet [(o2
y, Set (CommaObject One o1 m2) -> CommaObject One o1 m2
forall a. Set a -> a
anElement(Set (CommaObject One o1 m2) -> CommaObject One o1 m2)
-> (o2 -> Set (CommaObject One o1 m2))
-> o2
-> CommaObject One o1 m2
forall b c a. (b -> c) -> (a -> b) -> a -> c
.o2 -> Set (CommaObject One o1 m2)
universalMorphisms (o2 -> CommaObject One o1 m2) -> o2 -> CommaObject One o1 m2
forall a b. (a -> b) -> a -> b
$ o2
y) | o2
y <- c2 -> Set o2
forall c m o. FiniteCategory c m o => c -> Set o
ob (Diagram c1 m1 o1 c2 m2 o2 -> c2
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c2
tgt Diagram c1 m1 o1 c2 m2 o2
g), Bool -> Bool
not (Set (CommaObject One o1 m2) -> Bool
forall a. Set a -> Bool
Set.null (o2 -> Set (CommaObject One o1 m2)
universalMorphisms o2
y))]
            om :: Map o2 o1
om = (CommaObject One o1 m2 -> o1)
-> Map o2 (CommaObject One o1 m2) -> Map o2 o1
forall a b k. (a -> b) -> Map k a -> Map k b
Map.map CommaObject One o1 m2 -> o1
forall o1 o2 m3. CommaObject o1 o2 m3 -> o2
indexTarget Map o2 (CommaObject One o1 m2)
yToUniversalMorphism
            yToEta :: Map o2 m2
yToEta = (CommaObject One o1 m2 -> m2)
-> Map o2 (CommaObject One o1 m2) -> Map o2 m2
forall a b k. (a -> b) -> Map k a -> Map k b
Map.map CommaObject One o1 m2 -> m2
forall o1 o2 m3. CommaObject o1 o2 m3 -> m3
selectedArrow Map o2 (CommaObject One o1 m2)
yToUniversalMorphism 
            binding :: m2 -> Set m1
binding m2
m = [m1
a | m1
a <- c1 -> o1 -> o1 -> Set m1
forall c m o.
(Category c m o, Morphism m o) =>
c -> o -> o -> Set m
ar (Diagram c1 m1 o1 c2 m2 o2 -> c1
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c1
src Diagram c1 m1 o1 c2 m2 o2
g) (Map o2 o1
om Map o2 o1 -> o2 -> o1
forall k v. Eq k => Map k v -> k -> v
|!| (m2 -> o2
forall m o. Morphism m o => m -> o
source m2
m)) (Map o2 o1
om Map o2 o1 -> o2 -> o1
forall k v. Eq k => Map k v -> k -> v
|!| (m2 -> o2
forall m o. Morphism m o => m -> o
target m2
m)), ((Map o2 m2
yToEta Map o2 m2 -> o2 -> m2
forall k v. Eq k => Map k v -> k -> v
|!| m2 -> o2
forall m o. Morphism m o => m -> o
target m2
m) m2 -> m2 -> m2
forall m o. Morphism m o => m -> m -> m
@ m2
m) m2 -> m2 -> Bool
forall a. Eq a => a -> a -> Bool
== (Diagram c1 m1 o1 c2 m2 o2
g Diagram c1 m1 o1 c2 m2 o2 -> m1 -> m2
forall c1 m1 o1 m2 o2 c2.
(Category c1 m1 o1, Morphism m1 o1, Morphism m2 o2, Eq m1) =>
Diagram c1 m1 o1 c2 m2 o2 -> m1 -> m2
->£ m1
a) m2 -> m2 -> m2
forall m o. Morphism m o => m -> m -> m
@ (Map o2 m2
yToEta Map o2 m2 -> o2 -> m2
forall k v. Eq k => Map k v -> k -> v
|!| m2 -> o2
forall m o. Morphism m o => m -> o
source m2
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.

    --

    -- Note that 'leftAdjoint' and 'rightAdjoint' are slow because we enumerate a lot of morphisms to find the universal morphisms. Prefer using your own construction of an adjoint if known.

    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 :: forall c1 m1 o1 c2 m2 o2.
(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 Diagram c2 m2 o2 c1 m1 o1
f = Diagram {
                        src :: c1
src = Diagram c2 m2 o2 c1 m1 o1 -> c1
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c2
tgt Diagram c2 m2 o2 c1 m1 o1
f,
                        tgt :: c2
tgt = Diagram c2 m2 o2 c1 m1 o1 -> c2
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c1
src Diagram c2 m2 o2 c1 m1 o1
f,
                        omap :: Map o1 o2
omap = Map o1 o2
om,
                        mmap :: Map m1 m2
mmap = Set (m1, m2) -> Map m1 m2
forall k v. Set (k, v) -> Map k v
weakMapFromSet [(m1
m, Set m2 -> m2
forall a. Set a -> a
anElement  (m1 -> Set m2
binding m1
m)) | m1
m <- c1 -> Set m1
forall c m o. (FiniteCategory c m o, Morphism m o) => c -> Set m
arrows (Diagram c2 m2 o2 c1 m1 o1 -> c1
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c2
tgt Diagram c2 m2 o2 c1 m1 o1
f), (o1 -> Map o1 o2 -> Bool
forall k a. Eq k => k -> Map k a -> Bool
Map.member (m1 -> o1
forall m o. Morphism m o => m -> o
source m1
m) Map o1 o2
om) Bool -> Bool -> Bool
&& (o1 -> Map o1 o2 -> Bool
forall k a. Eq k => k -> Map k a -> Bool
Map.member (m1 -> o1
forall m o. Morphism m o => m -> o
target m1
m) Map o1 o2
om) Bool -> Bool -> Bool
&& Bool -> Bool
not (Set m2 -> Bool
forall a. Set a -> Bool
Set.null (m1 -> Set m2
binding m1
m))]
                    }
        where
            universalMorphisms :: o1 -> Set (CommaObject o2 One m1)
universalMorphisms o1
x = CommaCategory c2 m2 o2 One One One c1 m1 o1
-> Set (CommaObject o2 One m1)
forall c m o.
(FiniteCategory c m o, Morphism m o, Eq m, Eq o) =>
c -> Set o
terminalObjects (CommaCategory {leftDiagram :: Diagram c2 m2 o2 c1 m1 o1
leftDiagram = Diagram c2 m2 o2 c1 m1 o1
f, rightDiagram :: Diagram One One One c1 m1 o1
rightDiagram = (c1 -> o1 -> Diagram One One One c1 m1 o1
forall c m o.
(Category c m o, Morphism m o, Eq o) =>
c -> o -> Diagram One One One c m o
selectObject (Diagram c2 m2 o2 c1 m1 o1 -> c1
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c2
tgt Diagram c2 m2 o2 c1 m1 o1
f) o1
x)})
            xToUniversalMorphism :: Map o1 (CommaObject o2 One m1)
xToUniversalMorphism = Set (o1, CommaObject o2 One m1) -> Map o1 (CommaObject o2 One m1)
forall k v. Set (k, v) -> Map k v
weakMapFromSet [(o1
x, Set (CommaObject o2 One m1) -> CommaObject o2 One m1
forall a. Set a -> a
anElement(Set (CommaObject o2 One m1) -> CommaObject o2 One m1)
-> (o1 -> Set (CommaObject o2 One m1))
-> o1
-> CommaObject o2 One m1
forall b c a. (b -> c) -> (a -> b) -> a -> c
.o1 -> Set (CommaObject o2 One m1)
universalMorphisms (o1 -> CommaObject o2 One m1) -> o1 -> CommaObject o2 One m1
forall a b. (a -> b) -> a -> b
$ o1
x) | o1
x <- c1 -> Set o1
forall c m o. FiniteCategory c m o => c -> Set o
ob (Diagram c2 m2 o2 c1 m1 o1 -> c1
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c2
tgt Diagram c2 m2 o2 c1 m1 o1
f), Bool -> Bool
not (Set (CommaObject o2 One m1) -> Bool
forall a. Set a -> Bool
Set.null (o1 -> Set (CommaObject o2 One m1)
universalMorphisms o1
x))]
            om :: Map o1 o2
om = (CommaObject o2 One m1 -> o2)
-> Map o1 (CommaObject o2 One m1) -> Map o1 o2
forall a b k. (a -> b) -> Map k a -> Map k b
Map.map CommaObject o2 One m1 -> o2
forall o1 o2 m3. CommaObject o1 o2 m3 -> o1
indexSource Map o1 (CommaObject o2 One m1)
xToUniversalMorphism
            xToEps :: Map o1 m1
xToEps = (CommaObject o2 One m1 -> m1)
-> Map o1 (CommaObject o2 One m1) -> Map o1 m1
forall a b k. (a -> b) -> Map k a -> Map k b
Map.map CommaObject o2 One m1 -> m1
forall o1 o2 m3. CommaObject o1 o2 m3 -> m3
selectedArrow Map o1 (CommaObject o2 One m1)
xToUniversalMorphism
            binding :: m1 -> Set m2
binding m1
m = [m2
a | m2
a <- c2 -> o2 -> o2 -> Set m2
forall c m o.
(Category c m o, Morphism m o) =>
c -> o -> o -> Set m
ar (Diagram c2 m2 o2 c1 m1 o1 -> c2
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c1
src Diagram c2 m2 o2 c1 m1 o1
f) (Map o1 o2
om Map o1 o2 -> o1 -> o2
forall k v. Eq k => Map k v -> k -> v
|!| (m1 -> o1
forall m o. Morphism m o => m -> o
source m1
m)) (Map o1 o2
om Map o1 o2 -> o1 -> o2
forall k v. Eq k => Map k v -> k -> v
|!| (m1 -> o1
forall m o. Morphism m o => m -> o
target m1
m)), ((Map o1 m1
xToEps Map o1 m1 -> o1 -> m1
forall k v. Eq k => Map k v -> k -> v
|!| m1 -> o1
forall m o. Morphism m o => m -> o
target m1
m) m1 -> m1 -> m1
forall m o. Morphism m o => m -> m -> m
@ (Diagram c2 m2 o2 c1 m1 o1
f Diagram c2 m2 o2 c1 m1 o1 -> m2 -> m1
forall c1 m1 o1 m2 o2 c2.
(Category c1 m1 o1, Morphism m1 o1, Morphism m2 o2, Eq m1) =>
Diagram c1 m1 o1 c2 m2 o2 -> m1 -> m2
->£ m2
a)) m1 -> m1 -> Bool
forall a. Eq a => a -> a -> Bool
== (m1
m m1 -> m1 -> m1
forall m o. Morphism m o => m -> m -> m
@ (Map o1 m1
xToEps Map o1 m1 -> o1 -> m1
forall k v. Eq k => Map k v -> k -> v
|!| m1 -> o1
forall m o. Morphism m o => m -> o
source m1
m))]