{-# 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 :: 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 :: forall c1 m1 o1 c2 m2 o2.
c1
-> c2
-> AssociationList o1 o2
-> AssociationList m1 m2
-> Diagram c1 m1 o1 c2 m2 o2
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 :: AssociationList o2 o1
omap = [(o2
y, CommaObject One o1 m2 -> o1
forall o1 o2 m3. CommaObject o1 o2 m3 -> o2
indexTgt(CommaObject One o1 m2 -> o1)
-> (o2 -> CommaObject One o1 m2) -> o2 -> o1
forall b c a. (b -> c) -> (a -> b) -> a -> c
.[CommaObject One o1 m2] -> CommaObject One o1 m2
forall a. [a] -> a
head([CommaObject One o1 m2] -> CommaObject One o1 m2)
-> (o2 -> [CommaObject One o1 m2]) -> o2 -> CommaObject One o1 m2
forall b c a. (b -> c) -> (a -> b) -> a -> c
.o2 -> [CommaObject One o1 m2]
universalMorphisms (o2 -> o1) -> o2 -> o1
forall a b. (a -> b) -> a -> b
$ o2
y) | o2
y <- c2 -> [o2]
forall c m o. FiniteCategory c m o => c -> [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 ([CommaObject One o1 m2] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null (o2 -> [CommaObject One o1 m2]
universalMorphisms o2
y))],
                        mmap :: AssociationList m2 m1
mmap = [(m2
m, [m1] -> m1
forall a. [a] -> a
head (m2 -> [m1]
forall {o}. (Morphism m1 o, FiniteCategory c1 m1 o) => m2 -> [m1]
binding m2
m)) | m2
m <- c2 -> [m2]
forall c m o.
(FiniteCategory c m o, FiniteCategory c m o, Morphism m o) =>
c -> [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), Bool -> Bool
not ([m1] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null (m2 -> [m1]
forall {o}. (Morphism m1 o, FiniteCategory c1 m1 o) => m2 -> [m1]
binding m2
m))]
                    }
        where
            universalMorphisms :: o2 -> [CommaObject One o1 m2]
universalMorphisms o2
y = CommaCategory One One One c1 m1 o1 c2 m2 o2
-> [CommaObject One o1 m2]
forall c m o. (FiniteCategory c m o, Morphism m o) => c -> [o]
initialObjects (CommaCategory :: forall c1 m1 o1 c2 m2 o2 c3 m3 o3.
Diagram c1 m1 o1 c3 m3 o3
-> Diagram c2 m2 o2 c3 m3 o3
-> CommaCategory c1 m1 o1 c2 m2 o2 c3 m3 o3
CommaCategory {rightDiag :: Diagram c1 m1 o1 c2 m2 o2
rightDiag = Diagram c1 m1 o1 c2 m2 o2
g, leftDiag :: Diagram One One One c2 m2 o2
leftDiag = Maybe (Diagram One One One c2 m2 o2)
-> Diagram One One One c2 m2 o2
forall a. HasCallStack => Maybe a -> a
fromJust (c2 -> o2 -> Maybe (Diagram One One One c2 m2 o2)
forall c m o.
(FiniteCategory c m o, Morphism m o, Eq o) =>
c -> o -> Maybe (Diagram One One One c m o)
mkSelect1 (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)})
            binding :: m2 -> [m1]
binding m2
m = [m1
a | m1
a <- c1 -> [m1]
forall c m o.
(FiniteCategory c m o, FiniteCategory c m o, Morphism m o) =>
c -> [m]
arrows (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), (Bool -> Bool
not ([CommaObject One o1 m2] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null (o2 -> [CommaObject One o1 m2]
universalMorphisms (m2 -> o2
forall m o. Morphism m o => m -> o
source m2
m)))) Bool -> Bool -> Bool
&& (Bool -> Bool
not ([CommaObject One o1 m2] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null (o2 -> [CommaObject One o1 m2]
universalMorphisms (m2 -> o2
forall m o. Morphism m o => m -> o
target m2
m)))) Bool -> Bool -> Bool
&& ((m2 -> o2
forall m o. Morphism m o => m -> o
target ((Diagram c1 m1 o1 c2 m2 o2 -> AssociationList m1 m2
forall c1 m1 o1 c2 m2 o2.
Diagram c1 m1 o1 c2 m2 o2 -> AssociationList m1 m2
mmap Diagram c1 m1 o1 c2 m2 o2
g) AssociationList m1 m2 -> m1 -> m2
forall a b. Eq a => AssociationList a b -> a -> b
!-! m1
a)) o2 -> o2 -> Bool
forall a. Eq a => a -> a -> Bool
== (m2 -> o2
forall m o. Morphism m o => m -> o
source (CommaObject One o1 m2 -> m2
forall o1 o2 m3. CommaObject o1 o2 m3 -> m3
arrow(CommaObject One o1 m2 -> m2)
-> (o2 -> CommaObject One o1 m2) -> o2 -> m2
forall b c a. (b -> c) -> (a -> b) -> a -> c
.[CommaObject One o1 m2] -> CommaObject One o1 m2
forall a. [a] -> a
head([CommaObject One o1 m2] -> CommaObject One o1 m2)
-> (o2 -> [CommaObject One o1 m2]) -> o2 -> CommaObject One o1 m2
forall b c a. (b -> c) -> (a -> b) -> a -> c
.o2 -> [CommaObject One o1 m2]
universalMorphisms (o2 -> m2) -> o2 -> m2
forall a b. (a -> b) -> a -> b
$ m2 -> o2
forall m o. Morphism m o => m -> o
target m2
m))) Bool -> Bool -> Bool
&& (((CommaObject One o1 m2 -> m2
forall o1 o2 m3. CommaObject o1 o2 m3 -> m3
arrow(CommaObject One o1 m2 -> m2)
-> (o2 -> CommaObject One o1 m2) -> o2 -> m2
forall b c a. (b -> c) -> (a -> b) -> a -> c
.[CommaObject One o1 m2] -> CommaObject One o1 m2
forall a. [a] -> a
head([CommaObject One o1 m2] -> CommaObject One o1 m2)
-> (o2 -> [CommaObject One o1 m2]) -> o2 -> CommaObject One o1 m2
forall b c a. (b -> c) -> (a -> b) -> a -> c
.o2 -> [CommaObject One o1 m2]
universalMorphisms (o2 -> m2) -> o2 -> m2
forall a b. (a -> b) -> a -> b
$ 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 -> AssociationList m1 m2
forall c1 m1 o1 c2 m2 o2.
Diagram c1 m1 o1 c2 m2 o2 -> AssociationList m1 m2
mmap Diagram c1 m1 o1 c2 m2 o2
g) AssociationList m1 m2 -> m1 -> m2
forall a b. Eq a => AssociationList a b -> a -> b
!-! m1
a) m2 -> m2 -> m2
forall m o. Morphism m o => m -> m -> m
@ (CommaObject One o1 m2 -> m2
forall o1 o2 m3. CommaObject o1 o2 m3 -> m3
arrow(CommaObject One o1 m2 -> m2)
-> (o2 -> CommaObject One o1 m2) -> o2 -> m2
forall b c a. (b -> c) -> (a -> b) -> a -> c
.[CommaObject One o1 m2] -> CommaObject One o1 m2
forall a. [a] -> a
head([CommaObject One o1 m2] -> CommaObject One o1 m2)
-> (o2 -> [CommaObject One o1 m2]) -> o2 -> CommaObject One o1 m2
forall b c a. (b -> c) -> (a -> b) -> a -> c
.o2 -> [CommaObject One o1 m2]
universalMorphisms (o2 -> m2) -> o2 -> m2
forall a b. (a -> b) -> a -> b
$ 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.

    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 :: forall c1 m1 o1 c2 m2 o2.
c1
-> c2
-> AssociationList o1 o2
-> AssociationList m1 m2
-> Diagram c1 m1 o1 c2 m2 o2
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 :: AssociationList o1 o2
omap = [(o1
x, CommaObject o2 One m1 -> o2
forall o1 o2 m3. CommaObject o1 o2 m3 -> o1
indexSrc(CommaObject o2 One m1 -> o2)
-> (o1 -> CommaObject o2 One m1) -> o1 -> o2
forall b c a. (b -> c) -> (a -> b) -> a -> c
.[CommaObject o2 One m1] -> CommaObject o2 One m1
forall a. [a] -> a
head([CommaObject o2 One m1] -> CommaObject o2 One m1)
-> (o1 -> [CommaObject o2 One m1]) -> o1 -> CommaObject o2 One m1
forall b c a. (b -> c) -> (a -> b) -> a -> c
.o1 -> [CommaObject o2 One m1]
universalMorphisms (o1 -> o2) -> o1 -> o2
forall a b. (a -> b) -> a -> b
$ o1
x) | o1
x <- c1 -> [o1]
forall c m o. FiniteCategory c m o => c -> [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 ([CommaObject o2 One m1] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null (o1 -> [CommaObject o2 One m1]
universalMorphisms o1
x))],
                        mmap :: AssociationList m1 m2
mmap = [(m1
m, [m2] -> m2
forall a. [a] -> a
head (m1 -> [m2]
binding m1
m)) | m1
m <- c1 -> [m1]
forall c m o.
(FiniteCategory c m o, FiniteCategory c m o, Morphism m o) =>
c -> [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), (Bool -> Bool
not ([CommaObject o2 One m1] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null (o1 -> [CommaObject o2 One m1]
universalMorphisms (m1 -> o1
forall m o. Morphism m o => m -> o
source m1
m)))) Bool -> Bool -> Bool
&& (Bool -> Bool
not ([CommaObject o2 One m1] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null (o1 -> [CommaObject o2 One m1]
universalMorphisms (m1 -> o1
forall m o. Morphism m o => m -> o
target m1
m)))) Bool -> Bool -> Bool
&& Bool -> Bool
not ([m2] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null (m1 -> [m2]
binding m1
m))]
                    }
        where
            universalMorphisms :: o1 -> [CommaObject o2 One m1]
universalMorphisms o1
x = CommaCategory c2 m2 o2 One One One c1 m1 o1
-> [CommaObject o2 One m1]
forall c m o. (FiniteCategory c m o, Morphism m o) => c -> [o]
terminalObjects (CommaCategory :: forall c1 m1 o1 c2 m2 o2 c3 m3 o3.
Diagram c1 m1 o1 c3 m3 o3
-> Diagram c2 m2 o2 c3 m3 o3
-> CommaCategory c1 m1 o1 c2 m2 o2 c3 m3 o3
CommaCategory {leftDiag :: Diagram c2 m2 o2 c1 m1 o1
leftDiag = Diagram c2 m2 o2 c1 m1 o1
f, rightDiag :: Diagram One One One c1 m1 o1
rightDiag = Maybe (Diagram One One One c1 m1 o1)
-> Diagram One One One c1 m1 o1
forall a. HasCallStack => Maybe a -> a
fromJust (c1 -> o1 -> Maybe (Diagram One One One c1 m1 o1)
forall c m o.
(FiniteCategory c m o, Morphism m o, Eq o) =>
c -> o -> Maybe (Diagram One One One c m o)
mkSelect1 (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)})
            binding :: m1 -> [m2]
binding m1
m = [m2
a | m2
a <- c2 -> o2 -> o2 -> [m2]
forall c m o.
(FiniteCategory c m o, Morphism m o) =>
c -> o -> o -> [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) (CommaObject o2 One m1 -> o2
forall o1 o2 m3. CommaObject o1 o2 m3 -> o1
indexSrc(CommaObject o2 One m1 -> o2)
-> (o1 -> CommaObject o2 One m1) -> o1 -> o2
forall b c a. (b -> c) -> (a -> b) -> a -> c
.[CommaObject o2 One m1] -> CommaObject o2 One m1
forall a. [a] -> a
head([CommaObject o2 One m1] -> CommaObject o2 One m1)
-> (o1 -> [CommaObject o2 One m1]) -> o1 -> CommaObject o2 One m1
forall b c a. (b -> c) -> (a -> b) -> a -> c
.o1 -> [CommaObject o2 One m1]
universalMorphisms (o1 -> o2) -> o1 -> o2
forall a b. (a -> b) -> a -> b
$ (m1 -> o1
forall m o. Morphism m o => m -> o
source m1
m)) (CommaObject o2 One m1 -> o2
forall o1 o2 m3. CommaObject o1 o2 m3 -> o1
indexSrc(CommaObject o2 One m1 -> o2)
-> (o1 -> CommaObject o2 One m1) -> o1 -> o2
forall b c a. (b -> c) -> (a -> b) -> a -> c
.[CommaObject o2 One m1] -> CommaObject o2 One m1
forall a. [a] -> a
head([CommaObject o2 One m1] -> CommaObject o2 One m1)
-> (o1 -> [CommaObject o2 One m1]) -> o1 -> CommaObject o2 One m1
forall b c a. (b -> c) -> (a -> b) -> a -> c
.o1 -> [CommaObject o2 One m1]
universalMorphisms (o1 -> o2) -> o1 -> o2
forall a b. (a -> b) -> a -> b
$ (m1 -> o1
forall m o. Morphism m o => m -> o
target m1
m)), ((CommaObject o2 One m1 -> m1
forall o1 o2 m3. CommaObject o1 o2 m3 -> m3
arrow(CommaObject o2 One m1 -> m1)
-> (o1 -> CommaObject o2 One m1) -> o1 -> m1
forall b c a. (b -> c) -> (a -> b) -> a -> c
.[CommaObject o2 One m1] -> CommaObject o2 One m1
forall a. [a] -> a
head([CommaObject o2 One m1] -> CommaObject o2 One m1)
-> (o1 -> [CommaObject o2 One m1]) -> o1 -> CommaObject o2 One m1
forall b c a. (b -> c) -> (a -> b) -> a -> c
.o1 -> [CommaObject o2 One m1]
universalMorphisms (o1 -> m1) -> o1 -> m1
forall a b. (a -> b) -> a -> b
$ 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 -> AssociationList m2 m1
forall c1 m1 o1 c2 m2 o2.
Diagram c1 m1 o1 c2 m2 o2 -> AssociationList m1 m2
mmap Diagram c2 m2 o2 c1 m1 o1
f) AssociationList m2 m1 -> m2 -> m1
forall a b. Eq a => AssociationList a b -> a -> b
!-! 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
@ (CommaObject o2 One m1 -> m1
forall o1 o2 m3. CommaObject o1 o2 m3 -> m3
arrow(CommaObject o2 One m1 -> m1)
-> (o1 -> CommaObject o2 One m1) -> o1 -> m1
forall b c a. (b -> c) -> (a -> b) -> a -> c
.[CommaObject o2 One m1] -> CommaObject o2 One m1
forall a. [a] -> a
head([CommaObject o2 One m1] -> CommaObject o2 One m1)
-> (o1 -> [CommaObject o2 One m1]) -> o1 -> CommaObject o2 One m1
forall b c a. (b -> c) -> (a -> b) -> a -> c
.o1 -> [CommaObject o2 One m1]
universalMorphisms (o1 -> m1) -> o1 -> m1
forall a b. (a -> b) -> a -> b
$ m1 -> o1
forall m o. Morphism m o => m -> o
source m1
m))]