{-# LANGUAGE MultiParamTypeClasses #-}
module Math.Categories.PresheafCategory
(
Presheaf(..),
PresheafMorphism(..),
PresheafCategory(..),
yonedaEmbedding
)
where
import Math.Category
import Math.FiniteCategory
import Math.Categories.FunctorCategory
import Math.Categories.Opposite
import Math.Categories.FinSet
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 Data.Simplifiable
type Presheaf c m o = Diagram (Op c) (OpMorphism m) o (FinSet m) (Function m) (Set m)
type PresheafMorphism c m o = NaturalTransformation (Op c) (OpMorphism m) o (FinSet m) (Function m) (Set m)
type PresheafCategory c m o = FunctorCategory (Op c) (OpMorphism m) o (FinSet m) (Function m) (Set m)
yonedaEmbedding :: (FiniteCategory c m o, Morphism m o, Eq m, Eq o) => c -> Diagram c m o (PresheafCategory c m o) (PresheafMorphism c m o) (Presheaf c m o)
yonedaEmbedding :: forall c m o.
(FiniteCategory c m o, Morphism m o, Eq m, Eq o) =>
c
-> Diagram
c
m
o
(PresheafCategory c m o)
(PresheafMorphism c m o)
(Presheaf c m o)
yonedaEmbedding c
cat = Diagram
c
m
o
(FunctorCategory
(Op c) (OpMorphism m) o (FinSet m) (Function m) (Set m))
(NaturalTransformation
(Op c) (OpMorphism m) o (FinSet m) (Function m) (Set m))
(Diagram (Op c) (OpMorphism m) o (FinSet m) (Function m) (Set m))
forall {m1} {o1} {a} {m2} {o2} {a} {a}.
Diagram
c
m
o
(FunctorCategory (Op c) m1 o1 (FinSet a) m2 o2)
(NaturalTransformation
(Op c) (OpMorphism m) o (FinSet a) (Function m) (Set m))
(Diagram (Op c) (OpMorphism m) o (FinSet a) (Function m) (Set m))
functor
where
hom :: o -> Set (Set m)
hom o
x = (\o
s -> c -> o -> o -> Set m
forall c m o.
(Category c m o, Morphism m o) =>
c -> o -> o -> Set m
ar c
cat o
s o
x) (o -> Set m) -> Set o -> Set (Set m)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (c -> Set o
forall c m o. FiniteCategory c m o => c -> Set o
ob c
cat)
omapPresheaf :: o -> o -> Set m
omapPresheaf o
x o
s = c -> o -> o -> Set m
forall c m o.
(Category c m o, Morphism m o) =>
c -> o -> o -> Set m
ar c
cat o
s o
x
mmapPresheaf :: o -> OpMorphism m -> Function m
mmapPresheaf o
x OpMorphism m
m = Function{codomain :: Set m
codomain = o -> o -> Set m
omapPresheaf o
x (OpMorphism m -> o
forall m o. Morphism m o => m -> o
target OpMorphism m
m)
, function :: Map m m
function = AssociationList m m -> Map m m
forall k v. AssociationList k v -> Map k v
weakMap (AssociationList m m -> Map m m) -> AssociationList m m -> Map m m
forall a b. (a -> b) -> a -> b
$ [m] -> [m] -> AssociationList m m
forall a b. [a] -> [b] -> [(a, b)]
zip (Set m -> [m]
forall a. Eq a => Set a -> [a]
Set.toList (o -> o -> Set m
omapPresheaf o
x (OpMorphism m -> o
forall m o. Morphism m o => m -> o
source OpMorphism m
m))) ((\m
f -> (m
f m -> m -> m
forall m o. Morphism m o => m -> m -> m
@ (OpMorphism m -> m
forall m. OpMorphism m -> m
opOpMorphism OpMorphism m
m))) (m -> m) -> [m] -> [m]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Set m -> [m]
forall a. Eq a => Set a -> [a]
Set.toList (o -> o -> Set m
omapPresheaf o
x (OpMorphism m -> o
forall m o. Morphism m o => m -> o
source OpMorphism m
m))))}
presheaf :: o
-> Diagram (Op c) (OpMorphism m) o (FinSet a) (Function m) (Set m)
presheaf o
x = Diagram { src :: Op c
src = c -> Op c
forall c. c -> Op c
Op c
cat
, tgt :: FinSet a
tgt = FinSet a
forall a. FinSet a
FinSet
, omap :: Map o (Set m)
omap = (o -> Set m) -> Set o -> Map o (Set m)
forall k v. (k -> v) -> Set k -> Map k v
memorizeFunction (o -> o -> Set m
omapPresheaf o
x) (Op c -> Set o
forall c m o. FiniteCategory c m o => c -> Set o
ob (c -> Op c
forall c. c -> Op c
Op c
cat))
, mmap :: Map (OpMorphism m) (Function m)
mmap = (OpMorphism m -> Function m)
-> Set (OpMorphism m) -> Map (OpMorphism m) (Function m)
forall k v. (k -> v) -> Set k -> Map k v
memorizeFunction (o -> OpMorphism m -> Function m
mmapPresheaf o
x) (Op c -> Set (OpMorphism m)
forall c m o. (FiniteCategory c m o, Morphism m o) => c -> Set m
arrows (c -> Op c
forall c. c -> Op c
Op c
cat))}
ntFromMorph :: m -> o -> Function m
ntFromMorph m
m o
o = Function {codomain :: Set m
codomain = (o
-> Diagram
(Op c) (OpMorphism m) o (FinSet Any) (Function m) (Set m)
forall {a}.
o
-> Diagram (Op c) (OpMorphism m) o (FinSet a) (Function m) (Set m)
presheaf (m -> o
forall m o. Morphism m o => m -> o
target m
m)) Diagram (Op c) (OpMorphism m) o (FinSet Any) (Function m) (Set m)
-> o -> Set m
forall o1 c1 m1 c2 m2 o2.
Eq o1 =>
Diagram c1 m1 o1 c2 m2 o2 -> o1 -> o2
->$ o
o
, function :: Map m m
function = AssociationList m m -> Map m m
forall k v. AssociationList k v -> Map k v
weakMap (AssociationList m m -> Map m m) -> AssociationList m m -> Map m m
forall a b. (a -> b) -> a -> b
$ [m] -> [m] -> AssociationList m m
forall a b. [a] -> [b] -> [(a, b)]
zip [m]
domain [m]
postcom }
where
domain :: [m]
domain = Set m -> [m]
forall a. Eq a => Set a -> [a]
Set.toList (Set m -> [m]) -> Set m -> [m]
forall a b. (a -> b) -> a -> b
$ (o
-> Diagram
(Op c) (OpMorphism m) o (FinSet Any) (Function m) (Set m)
forall {a}.
o
-> Diagram (Op c) (OpMorphism m) o (FinSet a) (Function m) (Set m)
presheaf (m -> o
forall m o. Morphism m o => m -> o
source m
m)) Diagram (Op c) (OpMorphism m) o (FinSet Any) (Function m) (Set m)
-> o -> Set m
forall o1 c1 m1 c2 m2 o2.
Eq o1 =>
Diagram c1 m1 o1 c2 m2 o2 -> o1 -> o2
->$ o
o
postcom :: [m]
postcom = (m
m m -> m -> m
forall m o. Morphism m o => m -> m -> m
@) (m -> m) -> [m] -> [m]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [m]
domain
mmapFunctor :: m
-> NaturalTransformation
(Op c) (OpMorphism m) o (FinSet a) (Function m) (Set m)
mmapFunctor m
m = Diagram (Op c) (OpMorphism m) o (FinSet a) (Function m) (Set m)
-> Diagram (Op c) (OpMorphism m) o (FinSet a) (Function m) (Set m)
-> Map o (Function m)
-> NaturalTransformation
(Op c) (OpMorphism m) o (FinSet a) (Function m) (Set m)
forall c1 m1 o1 c2 m2 o2.
Diagram c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 c2 m2 o2
-> Map o1 m2
-> NaturalTransformation c1 m1 o1 c2 m2 o2
unsafeNaturalTransformation (o
-> Diagram (Op c) (OpMorphism m) o (FinSet a) (Function m) (Set m)
forall {a}.
o
-> Diagram (Op c) (OpMorphism m) o (FinSet a) (Function m) (Set m)
presheaf (m -> o
forall m o. Morphism m o => m -> o
source m
m)) (o
-> Diagram (Op c) (OpMorphism m) o (FinSet a) (Function m) (Set m)
forall {a}.
o
-> Diagram (Op c) (OpMorphism m) o (FinSet a) (Function m) (Set m)
presheaf (m -> o
forall m o. Morphism m o => m -> o
target m
m)) ((o -> Function m) -> Set o -> Map o (Function m)
forall k v. (k -> v) -> Set k -> Map k v
memorizeFunction (m -> o -> Function m
ntFromMorph m
m) (c -> Set o
forall c m o. FiniteCategory c m o => c -> Set o
ob c
cat))
presheavesCat :: FunctorCategory (Op c) m1 o1 (FinSet a) m2 o2
presheavesCat = Op c -> FinSet a -> FunctorCategory (Op c) m1 o1 (FinSet a) m2 o2
forall c1 m1 o1 c2 m2 o2.
c1 -> c2 -> FunctorCategory c1 m1 o1 c2 m2 o2
FunctorCategory (c -> Op c
forall c. c -> Op c
Op c
cat) FinSet a
forall a. FinSet a
FinSet
functor :: Diagram
c
m
o
(FunctorCategory (Op c) m1 o1 (FinSet a) m2 o2)
(NaturalTransformation
(Op c) (OpMorphism m) o (FinSet a) (Function m) (Set m))
(Diagram (Op c) (OpMorphism m) o (FinSet a) (Function m) (Set m))
functor = Diagram { src :: c
src = c
cat
, tgt :: FunctorCategory (Op c) m1 o1 (FinSet a) m2 o2
tgt = FunctorCategory (Op c) m1 o1 (FinSet a) m2 o2
forall {m1} {o1} {a} {m2} {o2}.
FunctorCategory (Op c) m1 o1 (FinSet a) m2 o2
presheavesCat
, omap :: Map
o (Diagram (Op c) (OpMorphism m) o (FinSet a) (Function m) (Set m))
omap = (o
-> Diagram (Op c) (OpMorphism m) o (FinSet a) (Function m) (Set m))
-> Set o
-> Map
o (Diagram (Op c) (OpMorphism m) o (FinSet a) (Function m) (Set m))
forall k v. (k -> v) -> Set k -> Map k v
memorizeFunction o
-> Diagram (Op c) (OpMorphism m) o (FinSet a) (Function m) (Set m)
forall {a}.
o
-> Diagram (Op c) (OpMorphism m) o (FinSet a) (Function m) (Set m)
presheaf (c -> Set o
forall c m o. FiniteCategory c m o => c -> Set o
ob c
cat)
, mmap :: Map
m
(NaturalTransformation
(Op c) (OpMorphism m) o (FinSet a) (Function m) (Set m))
mmap = (m
-> NaturalTransformation
(Op c) (OpMorphism m) o (FinSet a) (Function m) (Set m))
-> Set m
-> Map
m
(NaturalTransformation
(Op c) (OpMorphism m) o (FinSet a) (Function m) (Set m))
forall k v. (k -> v) -> Set k -> Map k v
memorizeFunction m
-> NaturalTransformation
(Op c) (OpMorphism m) o (FinSet a) (Function m) (Set m)
forall {a}.
m
-> NaturalTransformation
(Op c) (OpMorphism m) o (FinSet a) (Function m) (Set m)
mmapFunctor (c -> Set m
forall c m o. (FiniteCategory c m o, Morphism m o) => c -> Set m
arrows c
cat)
}