{-# LANGUAGE UndecidableInstances, FlexibleInstances, MultiParamTypeClasses  #-}

{-| Module  : FiniteCategories
Description : A subcategory is the image of a faithful functor.
Copyright   : Guillaume Sabbagh 2021
License     : GPL-3
Maintainer  : guillaumesabbagh@protonmail.com
Stability   : experimental
Portability : portable

A subcategory is the image of a faithful functor.
-}

module Subcategories.Subcategory where
    import FiniteCategory.FiniteCategory
    import Diagram.Diagram
    import Utils.AssociationList
    import Data.List (nub)
    import Subcategories.FullSubcategory
    
    -- | The type to view a faithful diagram as a subcategory.

    --

    -- It is your responsability to check that the diagram is faithful.

    data Subcategory c1 m1 o1 c2 m2 o2 = Subcategory (Diagram c1 m1 o1 c2 m2 o2)
    
    instance (FiniteCategory c1 m1 o1, Morphism m1 o1, Eq m1, Eq o1
            , FiniteCategory c2 m2 o2, Morphism m2 o2, Eq m2, Eq o2) => 
            FiniteCategory (Subcategory c1 m1 o1 c2 m2 o2) m2 o2 where
        ob :: Subcategory c1 m1 o1 c2 m2 o2 -> [o2]
ob (Subcategory Diagram c1 m1 o1 c2 m2 o2
diag) = [o2] -> [o2]
forall a. Eq a => [a] -> [a]
nub ([o2] -> [o2]) -> [o2] -> [o2]
forall a b. (a -> b) -> a -> b
$ ((Diagram c1 m1 o1 c2 m2 o2 -> AssociationList o1 o2
forall c1 m1 o1 c2 m2 o2.
Diagram c1 m1 o1 c2 m2 o2 -> AssociationList o1 o2
omap Diagram c1 m1 o1 c2 m2 o2
diag) AssociationList o1 o2 -> o1 -> o2
forall a b. Eq a => AssociationList a b -> a -> b
!-!) (o1 -> o2) -> [o1] -> [o2]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (c1 -> [o1]
forall c m o. FiniteCategory c m o => c -> [o]
ob (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
diag))
        identity :: Morphism m2 o2 => Subcategory c1 m1 o1 c2 m2 o2 -> o2 -> m2
identity (Subcategory Diagram c1 m1 o1 c2 m2 o2
diag) o2
o = c2 -> o2 -> m2
forall c m o. (FiniteCategory c m o, Morphism m o) => c -> o -> m
identity (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
diag) o2
o
        ar :: Morphism m2 o2 => Subcategory c1 m1 o1 c2 m2 o2 -> o2 -> o2 -> [m2]
ar (Subcategory Diagram c1 m1 o1 c2 m2 o2
diag) o2
s o2
t = [m2] -> [m2]
forall a. Eq a => [a] -> [a]
nub ([m2] -> [m2]) -> [m2] -> [m2]
forall a b. (a -> b) -> a -> b
$ ((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
diag) AssociationList m1 m2 -> m1 -> m2
forall a b. Eq a => AssociationList a b -> a -> b
!-!) (m1 -> m2) -> [m1] -> [m2]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> c1 -> o1 -> o1 -> [m1]
forall c m o.
(FiniteCategory c m o, Morphism m o) =>
c -> o -> o -> [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
diag) ((AssociationList o1 o2 -> AssociationList o2 o1
forall a b. AssociationList a b -> AssociationList b a
inverse(AssociationList o1 o2 -> AssociationList o2 o1)
-> (Diagram c1 m1 o1 c2 m2 o2 -> AssociationList o1 o2)
-> Diagram c1 m1 o1 c2 m2 o2
-> AssociationList o2 o1
forall b c a. (b -> c) -> (a -> b) -> a -> c
.Diagram c1 m1 o1 c2 m2 o2 -> AssociationList o1 o2
forall c1 m1 o1 c2 m2 o2.
Diagram c1 m1 o1 c2 m2 o2 -> AssociationList o1 o2
omap (Diagram c1 m1 o1 c2 m2 o2 -> AssociationList o2 o1)
-> Diagram c1 m1 o1 c2 m2 o2 -> AssociationList o2 o1
forall a b. (a -> b) -> a -> b
$ Diagram c1 m1 o1 c2 m2 o2
diag) AssociationList o2 o1 -> o2 -> o1
forall a b. Eq a => AssociationList a b -> a -> b
!-! o2
s) ((AssociationList o1 o2 -> AssociationList o2 o1
forall a b. AssociationList a b -> AssociationList b a
inverse(AssociationList o1 o2 -> AssociationList o2 o1)
-> (Diagram c1 m1 o1 c2 m2 o2 -> AssociationList o1 o2)
-> Diagram c1 m1 o1 c2 m2 o2
-> AssociationList o2 o1
forall b c a. (b -> c) -> (a -> b) -> a -> c
.Diagram c1 m1 o1 c2 m2 o2 -> AssociationList o1 o2
forall c1 m1 o1 c2 m2 o2.
Diagram c1 m1 o1 c2 m2 o2 -> AssociationList o1 o2
omap (Diagram c1 m1 o1 c2 m2 o2 -> AssociationList o2 o1)
-> Diagram c1 m1 o1 c2 m2 o2 -> AssociationList o2 o1
forall a b. (a -> b) -> a -> b
$ Diagram c1 m1 o1 c2 m2 o2
diag) AssociationList o2 o1 -> o2 -> o1
forall a b. Eq a => AssociationList a b -> a -> b
!-! o2
t)
        
    instance (GeneratedFiniteCategory c1 m1 o1, Morphism m1 o1, Eq m1, Eq o1
            , GeneratedFiniteCategory c2 m2 o2, Morphism m2 o2, Eq m2, Eq o2) => 
              GeneratedFiniteCategory (Subcategory c1 m1 o1 c2 m2 o2) m2 o2 where
        genAr :: Morphism m2 o2 => Subcategory c1 m1 o1 c2 m2 o2 -> o2 -> o2 -> [m2]
genAr (Subcategory Diagram c1 m1 o1 c2 m2 o2
diag) o2
s o2
t = [m2] -> [m2]
forall a. Eq a => [a] -> [a]
nub ([m2] -> [m2]) -> [m2] -> [m2]
forall a b. (a -> b) -> a -> b
$ ((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
diag) AssociationList m1 m2 -> m1 -> m2
forall a b. Eq a => AssociationList a b -> a -> b
!-!) (m1 -> m2) -> [m1] -> [m2]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> c1 -> o1 -> o1 -> [m1]
forall c m o.
(GeneratedFiniteCategory c m o, Morphism m o) =>
c -> o -> o -> [m]
genAr (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
diag) ((AssociationList o1 o2 -> AssociationList o2 o1
forall a b. AssociationList a b -> AssociationList b a
inverse(AssociationList o1 o2 -> AssociationList o2 o1)
-> (Diagram c1 m1 o1 c2 m2 o2 -> AssociationList o1 o2)
-> Diagram c1 m1 o1 c2 m2 o2
-> AssociationList o2 o1
forall b c a. (b -> c) -> (a -> b) -> a -> c
.Diagram c1 m1 o1 c2 m2 o2 -> AssociationList o1 o2
forall c1 m1 o1 c2 m2 o2.
Diagram c1 m1 o1 c2 m2 o2 -> AssociationList o1 o2
omap (Diagram c1 m1 o1 c2 m2 o2 -> AssociationList o2 o1)
-> Diagram c1 m1 o1 c2 m2 o2 -> AssociationList o2 o1
forall a b. (a -> b) -> a -> b
$ Diagram c1 m1 o1 c2 m2 o2
diag) AssociationList o2 o1 -> o2 -> o1
forall a b. Eq a => AssociationList a b -> a -> b
!-! o2
s) ((AssociationList o1 o2 -> AssociationList o2 o1
forall a b. AssociationList a b -> AssociationList b a
inverse(AssociationList o1 o2 -> AssociationList o2 o1)
-> (Diagram c1 m1 o1 c2 m2 o2 -> AssociationList o1 o2)
-> Diagram c1 m1 o1 c2 m2 o2
-> AssociationList o2 o1
forall b c a. (b -> c) -> (a -> b) -> a -> c
.Diagram c1 m1 o1 c2 m2 o2 -> AssociationList o1 o2
forall c1 m1 o1 c2 m2 o2.
Diagram c1 m1 o1 c2 m2 o2 -> AssociationList o1 o2
omap (Diagram c1 m1 o1 c2 m2 o2 -> AssociationList o2 o1)
-> Diagram c1 m1 o1 c2 m2 o2 -> AssociationList o2 o1
forall a b. (a -> b) -> a -> b
$ Diagram c1 m1 o1 c2 m2 o2
diag) AssociationList o2 o1 -> o2 -> o1
forall a b. Eq a => AssociationList a b -> a -> b
!-! o2
t)
        decompose :: Morphism m2 o2 => Subcategory c1 m1 o1 c2 m2 o2 -> m2 -> [m2]
decompose (Subcategory Diagram c1 m1 o1 c2 m2 o2
diag) m2
m = [m2] -> [m2]
forall a. Eq a => [a] -> [a]
nub ([m2] -> [m2]) -> [m2] -> [m2]
forall a b. (a -> b) -> a -> b
$ ((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
diag) AssociationList m1 m2 -> m1 -> m2
forall a b. Eq a => AssociationList a b -> a -> b
!-!) (m1 -> m2) -> [m1] -> [m2]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> c1 -> m1 -> [m1]
forall c m o.
(GeneratedFiniteCategory c m o, Morphism m o) =>
c -> m -> [m]
decompose (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
diag) ((AssociationList m1 m2 -> AssociationList m2 m1
forall a b. AssociationList a b -> AssociationList b a
inverse(AssociationList m1 m2 -> AssociationList m2 m1)
-> (Diagram c1 m1 o1 c2 m2 o2 -> AssociationList m1 m2)
-> Diagram c1 m1 o1 c2 m2 o2
-> AssociationList m2 m1
forall b c a. (b -> c) -> (a -> b) -> a -> c
.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 -> AssociationList m2 m1)
-> Diagram c1 m1 o1 c2 m2 o2 -> AssociationList m2 m1
forall a b. (a -> b) -> a -> b
$ Diagram c1 m1 o1 c2 m2 o2
diag) AssociationList m2 m1 -> m2 -> m1
forall a b. Eq a => AssociationList a b -> a -> b
!-! m2
m)
        
    -- | Extracts a full and faithful diagram out of a faithful diagram.

    fullDiagram :: (  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 c1 m1 o1 (Subcategory c1 m1 o1 c2 m2 o2) m2 o2
    fullDiagram :: 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 c1 m1 o1 (Subcategory c1 m1 o1 c2 m2 o2) m2 o2
fullDiagram Diagram c1 m1 o1 c2 m2 o2
diag = 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 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
diag, tgt :: Subcategory c1 m1 o1 c2 m2 o2
tgt = Diagram c1 m1 o1 c2 m2 o2 -> Subcategory c1 m1 o1 c2 m2 o2
forall c1 m1 o1 c2 m2 o2.
Diagram c1 m1 o1 c2 m2 o2 -> Subcategory c1 m1 o1 c2 m2 o2
Subcategory Diagram c1 m1 o1 c2 m2 o2
diag, omap :: AssociationList o1 o2
omap = Diagram c1 m1 o1 c2 m2 o2 -> AssociationList o1 o2
forall c1 m1 o1 c2 m2 o2.
Diagram c1 m1 o1 c2 m2 o2 -> AssociationList o1 o2
omap Diagram c1 m1 o1 c2 m2 o2
diag, mmap :: AssociationList m1 m2
mmap = 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
diag}
    
    -- | Strips the target of a diagram so that only given objects remain.

    stripDiagram :: ( 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 -> [o2] -> Diagram c1 m1 o1 (FullSubcategory c2 m2 o2) m2 o2
    stripDiagram :: 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
-> [o2] -> Diagram c1 m1 o1 (FullSubcategory c2 m2 o2) m2 o2
stripDiagram Diagram c1 m1 o1 c2 m2 o2
diag [o2]
keep = 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 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
diag,
                            tgt :: FullSubcategory c2 m2 o2
tgt = c2 -> [o2] -> FullSubcategory c2 m2 o2
forall c m o. c -> [o] -> FullSubcategory c m o
FullSubcategory (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
diag) [o2]
keep,
                            omap :: AssociationList o1 o2
omap = Diagram c1 m1 o1 c2 m2 o2 -> AssociationList o1 o2
forall c1 m1 o1 c2 m2 o2.
Diagram c1 m1 o1 c2 m2 o2 -> AssociationList o1 o2
omap Diagram c1 m1 o1 c2 m2 o2
diag,
                            mmap :: AssociationList m1 m2
mmap = 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
diag
                                }