{-| Module : FiniteCategories
Description : Functions to create usual and arbitrary diagrams.
Copyright : Guillaume Sabbagh 2021
License : GPL-3
Maintainer : guillaumesabbagh@protonmail.com
Stability : experimental
Portability : portable
A diagram is a heterogeneous FinFunctor, it is a shift of perspective : we view the functor not as a morphism of categories but as a selection in a category.
By heterogeneous, we mean that the type of the source category may be different from the target category.
To convert a `Diagram` into any other kind of functor, see @Diagram.Conversion@.
To enumerate all diagrams between two categories, see the `ob` function of /FunctorCategory/.
-}
module Diagram.Diagram
(
-- * Diagram typeclass and useful functions
Diagram(..),
checkFunctoriality,
completeMmap,
composeDiag,
objectImage,
-- * Constructors of diagrams
mkDiagram,
mkIdentityDiagram,
mkConstantDiagram,
mkDiscreteDiagram,
mkSelect0,
mkSelect1,
mkSelect2,
mkSelect3,
mkTriangle,
mkParallel,
mkV,
mkHat,
)
where
import Prelude hiding ((@))
import FiniteCategory.FiniteCategory
import Cat.FinCat
import Cat.PartialFinCat
import UsualCategories.DiscreteCategory
import UsualCategories.Zero
import UsualCategories.One
import qualified UsualCategories.Two as Two
import qualified UsualCategories.Three as Three
import qualified UsualCategories.Parallel as Par
import qualified UsualCategories.V as V
import qualified UsualCategories.Hat as Hat
import Data.List (intercalate, nub)
import Utils.SetList
import Utils.AssociationList
import IO.PrettyPrint
import IO.Show
-- | A diagram is a heterogeneous FinFunctor /F/, it is a shift of perspective : we view the FinFunctor not as a morphism of categories but as a selection in a category. It must obey the following rules :
--
-- prop> F (src f) = src (F f)
-- prop> F (tgt f) = tgt (F f)
-- prop> F (f @ g) = F(f) @ F(g)
-- prop> F (identity a) = identity (F a)
--
-- Unlike /FinFunctor/, a `Diagram` can have a source category and a target category with different types.
--
-- Using constructor functions `mkDiagram`, `mkConstantDiagram`, `mkDiscreteDiagram`, `mkSelect0`, `mkSelect1`, `mkSelect2`, `mkSelect3`, `mkTriangle` and `mkParallel`
-- is the safe way to instantiate a `Diagram` (FinFunctoriality is checked during construction).
--
-- Therefore, if you want to construct an arbitrary diagram, use the constructor function `mkDiagram` unless it is too long to check FinFunctoriality in which case
-- you should use the `Diagram` constructor. It is then your responsability to ensure the FinFunctoriality property is verified.
data Diagram c1 m1 o1 c2 m2 o2 = Diagram {src :: c1 -- ^ The source category of the `Diagram`
, tgt :: c2 -- ^ The target category of the `Diagram`
, omap :: AssociationList o1 o2 -- ^ The object map
, mmap :: AssociationList m1 m2} -- ^ The morphism map
deriving (Eq, Show)
-- | Checks wether the properties of a Diagram are respected. Returns True if the diagram is well formed, else False.
checkFunctoriality :: (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 -> Bool
checkFunctoriality Diagram{src=s,tgt=t,omap=om,mmap=fm}
| not (foldr (&&) True imIdNotId) = False
| not (foldr (&&) True errFunct) = False
| otherwise = True
where
imIdNotId = [fm !-! (identity s a) == identity t (om !-! a) | a <- ob s]
errFunct = [fm !-! (g @ f) == (fm !-! g) @ (fm !-! f) | f <- (arrows s), g <- (arFrom s (target f))]
instance (FiniteCategory c1 m1 o1, Morphism m1 o1, PrettyPrintable m1, PrettyPrintable o1, Eq m1, Eq o1, PrettyPrintable c1,
FiniteCategory c2 m2 o2, Morphism m2 o2, PrettyPrintable m2, PrettyPrintable o2, PrettyPrintable c2) =>
PrettyPrintable (Diagram c1 m1 o1 c2 m2 o2) where
pprint Diagram{src=s,tgt=t,omap=om,mmap=fm} = "Diagram "++pprint s++" -> "++pprint t++"\n"++pprint om++"\n"++pprint fm
-- | Constructor of an arbitrary `Diagram` that checks functoriality.
--
-- Use the `Diagram` constructor if the functoriality check is too slow. It is then your responsability to ensure the functoriality property is verified.
mkDiagram :: (FiniteCategory c1 m1 o1, Morphism m1 o1, Eq m1, Eq o1,
FiniteCategory c2 m2 o2, Morphism m2 o2, Eq m2, Eq o2) =>
c1 -- ^ The source category of the diagram.
-> c2 -- ^ The target category of the diagram.
-> AssociationList o1 o2 -- ^ The object map of the diagram.
-> AssociationList m1 m2 -- ^ The morphism map of the diagram.
-> Maybe (Diagram c1 m1 o1 c2 m2 o2) -- ^ The constructor returns Nothing if the FinFunctoriality check failed.
mkDiagram c1 c2 om fm = if checkFunctoriality diag then Just diag else Nothing
where diag = Diagram {src=c1, tgt=c2, omap=om, mmap=fm}
-- | Completes the function map `mmap` of a diagram so that you do not have to specify images of identites and composite arrows.
completeMmap :: (GeneratedFiniteCategory c1 m1 o1, Morphism m1 o1, Eq o1, Eq m1,
FiniteCategory c2 m2 o2, Morphism m2 o2, Eq o2, Eq m2) =>
c1 -- ^ The source category, it must be a generated category.
-> c2 -- ^ The target category.
-> AssociationList o1 o2 -- ^ The omap.
-> AssociationList m1 m2 -- ^ The mmap to complete.
-> AssociationList m1 m2 -- ^ The completed mmap.
completeMmap c1 c2 om fm = nub fm2
where
fm1 = [(identity c1 o, identity c2 (om !-! o)) | o <- ob c1]++fm
fm2 = [(a,compose $ (fm1 !-!) <$> decompose c1 a) | a <- arrows c1]++fm1
-- | Compose two diagrams.
composeDiag :: (FiniteCategory c1 m1 o1, Morphism m1 o1
,FiniteCategory c2 m2 o2, Morphism m2 o2
,FiniteCategory c3 m3 o3, Morphism m3 o3
,Eq m1, Eq o1, Eq m2, Eq o2) =>
Diagram c2 m2 o2 c3 m3 o3 -> Diagram c1 m1 o1 c2 m2 o2 -> Diagram c1 m1 o1 c3 m3 o3
diag2 `composeDiag` diag1 = Diagram {src=(src diag1), tgt=(tgt diag2), omap=((omap diag2)!-.(omap diag1)), mmap=((mmap diag2)!-.(mmap diag1))}
-- | Returns the objects image of the diagram.
objectImage :: (FiniteCategory c1 m1 o1, Morphism m1 o1
,FiniteCategory c2 m2 o2, Morphism m2 o2) =>
Diagram c1 m1 o1 c2 m2 o2 -> [o2]
objectImage diag = snd <$> (omap diag)
-- | Constructs a diagram which maps a category to itself to that each object is mapped to itself and each morphism is mapped to itself too.
mkIdentityDiagram :: (FiniteCategory c m o, Morphism m o) => c -> (Diagram c m o c m o)
mkIdentityDiagram c = Diagram {src=c, tgt=c, omap=functToAssocList id (ob c),mmap=functToAssocList id (arrows c)}
-- | Constructs a diagram where every object is mapped to a single object and every morphism is mapped to the identity of this single object.
mkConstantDiagram :: (FiniteCategory c1 m1 o1, Morphism m1 o1,
FiniteCategory c2 m2 o2, Morphism m2 o2, Eq o2) => c1 -> c2 -> o2 -> Maybe (Diagram c1 m1 o1 c2 m2 o2)
mkConstantDiagram c1 c2 o2
| elem o2 (ob c2) = Just Diagram {src=c1, tgt=c2, omap=functToAssocList (\x -> o2) (ob c1),mmap=functToAssocList (\x -> (identity c2 o2)) (arrows c1)}
| otherwise = Nothing
-- | Constructs a diagram that selects a list of objects of a category.
mkDiscreteDiagram :: (FiniteCategory c m o, Morphism m o, Eq o) =>
c -> [o] -> Maybe (Diagram (DiscreteCategory o) (DiscreteIdentity o) (DiscreteObject o) c m o)
mkDiscreteDiagram c objs
| objs `isIncludedIn` (ob c) = Just Diagram {src=DiscreteCategory objs, tgt=c, omap=functToAssocList (\(DiscreteObject o) -> o) (ob (DiscreteCategory objs)),mmap=functToAssocList (\(DiscreteIdentity o) -> (identity c o)) (arrows (DiscreteCategory objs))}
| otherwise = Nothing
-- | Constructs a diagram that selects no object and no morphism.
mkSelect0 :: (FiniteCategory c m o, Morphism m o) => c -> Diagram Zero Zero Zero c m o
mkSelect0 c = Diagram {src=Zero, tgt=c, omap=[],mmap=[]}
-- | Constructs a diagram that selects a single object and its identity.
mkSelect1 :: (FiniteCategory c m o, Morphism m o, Eq o) => c -> o -> Maybe (Diagram One One One c m o)
mkSelect1 c o
| elem o (ob c) = Just Diagram {src=One, tgt=c, omap=[(One,o)],mmap=[(One,(identity c o))]}
| otherwise = Nothing
-- | Constructs a diagram that selects a single arrow.
mkSelect2 :: (FiniteCategory c m o, Morphism m o, Eq m, Eq o) => c -> m -> Maybe (Diagram Two.Two Two.TwoAr Two.TwoOb c m o)
mkSelect2 c m
| condition = Just Diagram {src=Two.Two, tgt=c, omap=om,mmap=(completeMmap Two.Two c om [(Two.F,m)])}
| otherwise = Nothing
where
condition = elem (source m) (ob c) && elem (target m) (ob c) && elem m (ar c (source m) (target m))
om = [(Two.A,source m),(Two.B,target m)]
-- | Constructs a diagram that selects a triangle.
--
-- > B <-f- A
-- > | /
-- > g g\@f
-- > | /
-- > v v
-- > C
mkSelect3 :: (FiniteCategory c m o, Morphism m o, Eq o, Eq m) => c -- ^ The target category.
-> m -- ^ /f/
-> m -- ^ /g/
-> Maybe (Diagram Three.Three Three.ThreeAr Three.ThreeOb c m o)
mkSelect3 c f g
| condition = Just Diagram {src=Three.Three, tgt=c, omap=om,mmap=(completeMmap Three.Three c om [(Three.F,f),(Three.G,g)])}
| otherwise = Nothing
where
condition = obInCat && arInCat && (source g) == (target f)
obInCat = elem (source f) (ob c) && elem (target f) (ob c) && elem (target g) (ob c)
arInCat = elem f (ar c (source f) (target f)) && elem g (ar c (source g) (target g))
om = [(Three.A,source f),(Three.B,target f),(Three.C,target g)]
-- | Constructs a diagram that selects a triangle. (Alias for `mkSelect3`).
mkTriangle :: (FiniteCategory c m o, Morphism m o, Eq o, Eq m) => c -> m -> m -> Maybe (Diagram Three.Three Three.ThreeAr Three.ThreeOb c m o)
mkTriangle = mkSelect3
-- | Constructs a diagram that selects two parallel arrows.
mkParallel :: (FiniteCategory c m o, Morphism m o, Eq o, Eq m) => c -> m -> m -> Maybe (Diagram Par.Parallel Par.ParallelAr Par.ParallelOb c m o)
mkParallel c f g
| condition = Just Diagram {src=Par.Parallel, tgt=c, omap=om,mmap=(completeMmap Par.Parallel c om [(Par.F,f),(Par.G,g)])}
| otherwise = Nothing
where
condition = obInCat && arInCat && (source f) == (source g) && (target f) == (target g)
obInCat = elem (source f) (ob c) && elem (target f) (ob c)
arInCat = elem f (ar c (source f) (target f)) && elem g (ar c (source g) (target g))
om = [(Par.A,source f), (Par.B, target f)]
-- | Constructs a diagram that selects a V.
mkV :: (FiniteCategory c m o, Morphism m o, Eq o, Eq m) => c -> m -> m -> Maybe (Diagram V.V V.VAr V.VOb c m o)
mkV c f g
| condition = Just Diagram {src=V.V, tgt=c, omap=om,mmap=(completeMmap V.V c om [(V.F,f),(V.G,g)])}
| otherwise = Nothing
where
condition = obInCat && arInCat && (target f) == (target g)
obInCat = elem (source f) (ob c) && elem (target f) (ob c)
arInCat = elem f (ar c (source f) (target f)) && elem g (ar c (source g) (target g))
om = [(V.A,source f), (V.B, source g), (V.C, target g)]
-- | Constructs a diagram that selects a Hat.
mkHat :: (FiniteCategory c m o, Morphism m o, Eq o, Eq m) => c -> m -> m -> Maybe (Diagram Hat.Hat Hat.HatAr Hat.HatOb c m o)
mkHat c f g
| condition = Just Diagram {src=Hat.Hat, tgt=c, omap=om,mmap=(completeMmap Hat.Hat c om [(Hat.F,f),(Hat.G,g)])}
| otherwise = Nothing
where
condition = obInCat && arInCat && (source f) == (source g)
obInCat = elem (source f) (ob c) && elem (target f) (ob c)
arInCat = elem f (ar c (source f) (target f)) && elem g (ar c (source g) (target g))
om = [(Hat.A,source f), (Hat.B, target f), (Hat.C, target g)]