{-# LANGUAGE FlexibleInstances, MultiParamTypeClasses #-}
{-| Module : FiniteCategories
Description : __FinCat__ is the category of finite categories, functors are the morphisms of __FinCat__.
Copyright : Guillaume Sabbagh 2021
License : GPL-3
Maintainer : guillaumesabbagh@protonmail.com
Stability : experimental
Portability : portable
The __FinCat__ category has as objects finite categories and as morphisms functors between them.
It is itself a large category (therefore not a finite one),
we only construct finite full subcategories of the mathematical infinite __FinCat__ category.
`FinCat` is the type of full finite subcategories of __FinCat__.
To instantiate it, use the `FinCat` constructor on a list of categories.
For example, see ExampleCat.ExampleCat
The `FinCat` type should not be confused with the `FiniteCategory` typeclass.
The `FiniteCategory` typeclass describes axioms a structure should follow to be considered a finite category.
The `FinCat` type is itself a `FiniteCategory` and contains finite categories as objects.
To convert a `FinFunctor` into any other kind of functor, see @Diagram.Conversion@.
-}
module Cat.FinCat
(
FinFunctor(..),
FinCat(..)
)
where
import FiniteCategory.FiniteCategory
import Utils.EnumerateMaps
import Utils.CartesianProduct
import IO.PrettyPrint
import IO.Show
import Utils.AssociationList
-- | A `FinFunctor` /F/ between two categories is a map between objects and a map between arrows of the two categories such that :
--
-- prop> F (srcF f) = srcF (F f)
-- prop> F (tgtF f) = tgtF (F f)
-- prop> F (f @ g) = F(f) @ F(g)
-- prop> F (identity a) = identity (F a)
--
-- It is meant to be a morphism between categories within `FinCat`, it is homogeneous, the type of the source category must be the same as the type of the target category.
--
-- See /Diagram/ for heterogeneous ones.
--
-- To convert a `FinFunctor` into any other kind of functor, see @Diagram.Conversion@.
data FinFunctor c m o = FinFunctor {srcF :: c, tgtF :: c, omapF :: AssociationList o o, mmapF :: AssociationList m m} deriving (Eq, Show)
instance (Eq c, Eq m, Eq o) => Morphism (FinFunctor c m o) c where
(@) FinFunctor{srcF=s2,tgtF=t2,omapF=om2,mmapF=fm2} FinFunctor{srcF=s1,tgtF=t1,omapF=om1,mmapF=fm1}
| t1 /= s2 = error "Illegal composition of FinFunctors."
| otherwise = FinFunctor{srcF=s1,tgtF=t2,omapF=om2!-.om1,mmapF=fm2!-.fm1}
source = srcF
target = tgtF
instance (FiniteCategory c m o, Morphism m o, PrettyPrintable c, PrettyPrintable m, PrettyPrintable o, Eq m, Eq o) =>
PrettyPrintable (FinFunctor c m o) where
pprint FinFunctor{srcF=s,tgtF=t,omapF=om,mmapF=fm} = "FinFunctor ("++pprint s++") -> ("++pprint t++")\n"++pprint om++"\n"++pprint fm
-- | Checks wether the properties of a FinFunctor are respected.
checkFinFunctoriality :: (FiniteCategory c m o, Morphism m o, Eq m, Eq o) => FinFunctor c m o -> Bool
checkFinFunctoriality FinFunctor {srcF=s,tgtF=t,omapF=om,mmapF=fm}
| not (and imIdNotId) = False
| not (and 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))]
-- | An instance of `FinCat` is a list of categories of interest.
--
-- Listing all arrows between two objects (i.e. listing FinFunctors between two categories) is slow (there are a lot of candidates).
newtype FinCat c m o = FinCat [c]
-- We are forced to use the language extension FlexibleInstances because of this instance declaration :
-- The category 'c' could be itself a `FinCat` category therefore not respecting the uniqueness rule of instanciation.
instance (FiniteCategory c m o, Morphism m o, Eq c, Eq m, Eq o) => FiniteCategory (FinCat c m o) (FinFunctor c m o) c where
ob (FinCat xs) = xs
identity finCat catObj = FinFunctor {srcF=catObj,tgtF=catObj,omapF=functToAssocList id (ob catObj),mmapF=functToAssocList id (arrows catObj)}
ar finCat cat1 cat2 = [FinFunctor{srcF=cat1,tgtF=cat2,mmapF=appF, omapF=appO} | appO <- appObj, appF <- concat <$> cartesianProduct [twoObjToMaps a b appO| a <- ob cat1, b <- ob cat1], checkFinFunctoriality FinFunctor{srcF=cat1,tgtF=cat2,mmapF=appF, omapF=appO}]
where
appObj = enumMaps (ob cat1) (ob cat2)
twoObjToMaps a b appO = enumMaps (ar cat1 a b) (ar cat2 (appO !-! a) (appO !-! b))
instance (FiniteCategory c m o, Morphism m o, Eq c, Eq m, Eq o) => GeneratedFiniteCategory (FinCat c m o) (FinFunctor c m o) c where
genAr = defaultGenAr
decompose = defaultDecompose