module Math.FiniteCategories.FinGrph.Examples
(
divisibilityGraph,
exampleGraph,
exampleFinGrph,
exampleDiscreteDiagramToFinGrph,
exampleProductGaphs,
exampleParallelDiagramToFinGrph,
exampleEqualizerInFinGrph,
exampleDiagramHatToFinGrph,
exampleColimitOfGraphs,
)
where
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.Text (Text, pack)
import Math.Categories
import Math.FiniteCategories
import Math.IO.PrettyPrint
import Math.FiniteCategory
import Math.CompleteCategory
import Math.CocompleteCategory
divisibilityGraph :: Int -> Graph Int Int
divisibilityGraph :: Int -> Graph Int Int
divisibilityGraph Int
n = Graph Int Int
result
where
Just Graph Int Int
result = Set Int -> Set (Arrow Int Int) -> Maybe (Graph Int Int)
forall n e. Eq n => Set n -> Set (Arrow n e) -> Maybe (Graph n e)
graph ([Int] -> Set Int
forall a. [a] -> Set a
set [Int
1..Int
n]) ([Arrow Int Int] -> Set (Arrow Int Int)
forall a. [a] -> Set a
set [Arrow{sourceArrow :: Int
sourceArrow = Int
a, targetArrow :: Int
targetArrow = Int
b, labelArrow :: Int
labelArrow = Int
b Int -> Int -> Int
forall a. Integral a => a -> a -> a
`div` Int
a} | Int
a <- [Int
1..Int
n], Int
b <- [Int
1..Int
n], Int
b Int -> Int -> Int
forall a. Integral a => a -> a -> a
`mod` Int
a Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
0])
exampleGraph :: Graph Int Int
exampleGraph :: Graph Int Int
exampleGraph = Int -> Graph Int Int
divisibilityGraph Int
10
exampleFinGrph :: FullSubcategory (FinGrph Int Int) (GraphHomomorphism Int Int) (Graph Int Int)
exampleFinGrph :: FullSubcategory
(FinGrph Int Int) (GraphHomomorphism Int Int) (Graph Int Int)
exampleFinGrph = FinGrph Int Int
-> Set (Graph Int Int)
-> FullSubcategory
(FinGrph Int Int) (GraphHomomorphism Int Int) (Graph Int Int)
forall c m o. c -> Set o -> FullSubcategory c m o
FullSubcategory FinGrph Int Int
forall n e. FinGrph n e
FinGrph ([Graph Int Int] -> Set (Graph Int Int)
forall a. [a] -> Set a
set (Int -> Graph Int Int
divisibilityGraph (Int -> Graph Int Int) -> [Int] -> [Graph Int Int]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Int
1..Int
3]))
exampleDiscreteDiagramToFinGrph :: Diagram (DiscreteCategory Int) (DiscreteMorphism Int) Int (FinGrph Text Text) (GraphHomomorphism Text Text) (Graph Text Text)
exampleDiscreteDiagramToFinGrph :: Diagram
(DiscreteCategory Int)
(DiscreteMorphism Int)
Int
(FinGrph Text Text)
(GraphHomomorphism Text Text)
(Graph Text Text)
exampleDiscreteDiagramToFinGrph = FinGrph Text Text
-> [Graph Text Text]
-> Diagram
(DiscreteCategory Int)
(DiscreteMorphism Int)
Int
(FinGrph Text Text)
(GraphHomomorphism Text Text)
(Graph Text Text)
forall c m o.
(Category c m o, Morphism m o, Eq o) =>
c
-> [o]
-> Diagram (DiscreteCategory Int) (DiscreteMorphism Int) Int c m o
discreteDiagram FinGrph Text Text
forall n e. FinGrph n e
FinGrph [Graph Text Text
g1,Graph Text Text
g2]
where
Right CG
cg1 = String
-> Either (FiniteCategoryError (CGMorphism Text Text) Text) CG
readCGString String
"A -f-> B"
g1 :: Graph Text Text
g1 = CG -> Graph Text Text
forall a b. CompositionGraph a b -> Graph a b
support CG
cg1
Right CG
cg2 = String
-> Either (FiniteCategoryError (CGMorphism Text Text) Text) CG
readCGString String
"C -g-> D"
g2 :: Graph Text Text
g2 = CG -> Graph Text Text
forall a b. CompositionGraph a b -> Graph a b
support CG
cg2
exampleProductGaphs :: Cone (DiscreteCategory Int) (DiscreteMorphism Int) Int (FinGrph (Limit Int Text) (Limit Int Text)) (GraphHomomorphism (Limit Int Text) (Limit Int Text)) (Graph (Limit Int Text) (Limit Int Text))
exampleProductGaphs :: Cone
(DiscreteCategory Int)
(DiscreteMorphism Int)
Int
(FinGrph (Limit Int Text) (Limit Int Text))
(GraphHomomorphism (Limit Int Text) (Limit Int Text))
(Graph (Limit Int Text) (Limit Int Text))
exampleProductGaphs = Diagram
(DiscreteCategory Int)
(DiscreteMorphism Int)
Int
(FinGrph Text Text)
(GraphHomomorphism Text Text)
(Graph Text Text)
-> Cone
(DiscreteCategory Int)
(DiscreteMorphism Int)
Int
(FinGrph (Limit Int Text) (Limit Int Text))
(GraphHomomorphism (Limit Int Text) (Limit Int Text))
(Graph (Limit Int Text) (Limit Int Text))
forall c m o cLim mLim oLim oIndex.
HasProducts c m o cLim mLim oLim oIndex =>
Diagram
(DiscreteCategory oIndex) (DiscreteMorphism oIndex) oIndex c m o
-> Cone
(DiscreteCategory oIndex)
(DiscreteMorphism oIndex)
oIndex
cLim
mLim
oLim
Math.CompleteCategory.product Diagram
(DiscreteCategory Int)
(DiscreteMorphism Int)
Int
(FinGrph Text Text)
(GraphHomomorphism Text Text)
(Graph Text Text)
exampleDiscreteDiagramToFinGrph
exampleParallelDiagramToFinGrph :: Diagram Parallel ParallelAr ParallelOb (FinGrph Char Char) (GraphHomomorphism Char Char) (Graph Char Char)
exampleParallelDiagramToFinGrph :: Diagram
Parallel
ParallelAr
ParallelOb
(FinGrph Char Char)
(GraphHomomorphism Char Char)
(Graph Char Char)
exampleParallelDiagramToFinGrph = FinGrph Char Char
-> GraphHomomorphism Char Char
-> GraphHomomorphism Char Char
-> Diagram
Parallel
ParallelAr
ParallelOb
(FinGrph Char Char)
(GraphHomomorphism Char Char)
(Graph Char Char)
forall c m o.
(Category c m o, Morphism m o, Eq o) =>
c -> m -> m -> Diagram Parallel ParallelAr ParallelOb c m o
parallelDiagram FinGrph Char Char
forall n e. FinGrph n e
FinGrph GraphHomomorphism Char Char
gh1 GraphHomomorphism Char Char
gh2
where
x :: Arrow Char Char
x = Arrow{sourceArrow :: Char
sourceArrow = Char
'A', targetArrow :: Char
targetArrow = Char
'B', labelArrow :: Char
labelArrow = Char
'x'}
y :: Arrow Char Char
y = Arrow{sourceArrow :: Char
sourceArrow = Char
'C', targetArrow :: Char
targetArrow = Char
'D', labelArrow :: Char
labelArrow = Char
'y'}
Just Graph Char Char
g = Set Char -> Set (Arrow Char Char) -> Maybe (Graph Char Char)
forall n e. Eq n => Set n -> Set (Arrow n e) -> Maybe (Graph n e)
graph (String -> Set Char
forall a. [a] -> Set a
set String
"ABCD") ([Arrow Char Char] -> Set (Arrow Char Char)
forall a. [a] -> Set a
set [Arrow Char Char
x,Arrow Char Char
y])
Just GraphHomomorphism Char Char
gh1 = Map Char Char
-> Map (Arrow Char Char) (Arrow Char Char)
-> Graph Char Char
-> Maybe (GraphHomomorphism Char Char)
forall n e.
(Eq n, Eq e) =>
Map n n
-> Map (Arrow n e) (Arrow n e)
-> Graph n e
-> Maybe (GraphHomomorphism n e)
graphHomomorphism (AssociationList Char Char -> Map Char Char
forall k v. AssociationList k v -> Map k v
weakMap [(Char
'A',Char
'A'),(Char
'B',Char
'B'),(Char
'C',Char
'A'),(Char
'D',Char
'B')]) (AssociationList (Arrow Char Char) (Arrow Char Char)
-> Map (Arrow Char Char) (Arrow Char Char)
forall k v. AssociationList k v -> Map k v
weakMap [(Arrow Char Char
x,Arrow Char Char
x),(Arrow Char Char
y,Arrow Char Char
x)]) Graph Char Char
g
Just GraphHomomorphism Char Char
gh2 = Map Char Char
-> Map (Arrow Char Char) (Arrow Char Char)
-> Graph Char Char
-> Maybe (GraphHomomorphism Char Char)
forall n e.
(Eq n, Eq e) =>
Map n n
-> Map (Arrow n e) (Arrow n e)
-> Graph n e
-> Maybe (GraphHomomorphism n e)
graphHomomorphism (AssociationList Char Char -> Map Char Char
forall k v. AssociationList k v -> Map k v
weakMap [(Char
'A',Char
'A'),(Char
'B',Char
'B'),(Char
'C',Char
'C'),(Char
'D',Char
'D')]) (AssociationList (Arrow Char Char) (Arrow Char Char)
-> Map (Arrow Char Char) (Arrow Char Char)
forall k v. AssociationList k v -> Map k v
weakMap [(Arrow Char Char
x,Arrow Char Char
x),(Arrow Char Char
y,Arrow Char Char
y)]) Graph Char Char
g
exampleEqualizerInFinGrph :: Cone Parallel ParallelAr ParallelOb (FinGrph (Limit ParallelOb Char) (Limit ParallelOb Char)) (GraphHomomorphism (Limit ParallelOb Char) (Limit ParallelOb Char)) (Graph (Limit ParallelOb Char) (Limit ParallelOb Char))
exampleEqualizerInFinGrph :: Cone
Parallel
ParallelAr
ParallelOb
(FinGrph (Limit ParallelOb Char) (Limit ParallelOb Char))
(GraphHomomorphism (Limit ParallelOb Char) (Limit ParallelOb Char))
(Graph (Limit ParallelOb Char) (Limit ParallelOb Char))
exampleEqualizerInFinGrph = Diagram
Parallel
ParallelAr
ParallelOb
(FinGrph Char Char)
(GraphHomomorphism Char Char)
(Graph Char Char)
-> Cone
Parallel
ParallelAr
ParallelOb
(FinGrph (Limit ParallelOb Char) (Limit ParallelOb Char))
(GraphHomomorphism (Limit ParallelOb Char) (Limit ParallelOb Char))
(Graph (Limit ParallelOb Char) (Limit ParallelOb Char))
forall c m o cLim mLim oLim cIndex mIndex oIndex.
(CompleteCategory c m o cLim mLim oLim cIndex mIndex oIndex,
FiniteCategory cIndex mIndex oIndex, Morphism mIndex oIndex,
Eq cIndex, Eq mIndex, Eq oIndex) =>
Diagram cIndex mIndex oIndex c m o
-> Cone cIndex mIndex oIndex cLim mLim oLim
limit Diagram
Parallel
ParallelAr
ParallelOb
(FinGrph Char Char)
(GraphHomomorphism Char Char)
(Graph Char Char)
exampleParallelDiagramToFinGrph
exampleDiagramHatToFinGrph :: Diagram Hat HatAr HatOb (FinGrph Char Char) (GraphHomomorphism Char Char) (Graph Char Char)
exampleDiagramHatToFinGrph :: Diagram
Hat
HatAr
HatOb
(FinGrph Char Char)
(GraphHomomorphism Char Char)
(Graph Char Char)
exampleDiagramHatToFinGrph = Diagram
Hat
HatAr
HatOb
(FinGrph Char Char)
(GraphHomomorphism Char Char)
(Graph Char Char)
diag
where
f :: Arrow Char Char
f = Arrow{sourceArrow :: Char
sourceArrow = Char
'A', targetArrow :: Char
targetArrow = Char
'B', labelArrow :: Char
labelArrow = Char
'f'}
g :: Arrow Char Char
g = Arrow{sourceArrow :: Char
sourceArrow = Char
'B', targetArrow :: Char
targetArrow = Char
'C', labelArrow :: Char
labelArrow = Char
'g'}
Just Graph Char Char
g1 = Set Char -> Set (Arrow Char Char) -> Maybe (Graph Char Char)
forall n e. Eq n => Set n -> Set (Arrow n e) -> Maybe (Graph n e)
graph (String -> Set Char
forall a. [a] -> Set a
set String
"AB") ([Arrow Char Char] -> Set (Arrow Char Char)
forall a. [a] -> Set a
set [Arrow Char Char
f])
Just Graph Char Char
g2 = Set Char -> Set (Arrow Char Char) -> Maybe (Graph Char Char)
forall n e. Eq n => Set n -> Set (Arrow n e) -> Maybe (Graph n e)
graph (String -> Set Char
forall a. [a] -> Set a
set String
"BC") ([Arrow Char Char] -> Set (Arrow Char Char)
forall a. [a] -> Set a
set [Arrow Char Char
g])
Just Graph Char e
g3 = Set Char -> Set (Arrow Char e) -> Maybe (Graph Char e)
forall n e. Eq n => Set n -> Set (Arrow n e) -> Maybe (Graph n e)
graph (String -> Set Char
forall a. [a] -> Set a
set String
"B") ([Arrow Char e] -> Set (Arrow Char e)
forall a. [a] -> Set a
set [])
Just GraphHomomorphism Char Char
gh1 = Map Char Char
-> Map (Arrow Char Char) (Arrow Char Char)
-> Graph Char Char
-> Maybe (GraphHomomorphism Char Char)
forall n e.
(Eq n, Eq e) =>
Map n n
-> Map (Arrow n e) (Arrow n e)
-> Graph n e
-> Maybe (GraphHomomorphism n e)
graphHomomorphism (AssociationList Char Char -> Map Char Char
forall k v. AssociationList k v -> Map k v
weakMap [(Char
'B',Char
'B')]) (AssociationList (Arrow Char Char) (Arrow Char Char)
-> Map (Arrow Char Char) (Arrow Char Char)
forall k v. AssociationList k v -> Map k v
weakMap []) Graph Char Char
g1
Just GraphHomomorphism Char Char
gh2 = Map Char Char
-> Map (Arrow Char Char) (Arrow Char Char)
-> Graph Char Char
-> Maybe (GraphHomomorphism Char Char)
forall n e.
(Eq n, Eq e) =>
Map n n
-> Map (Arrow n e) (Arrow n e)
-> Graph n e
-> Maybe (GraphHomomorphism n e)
graphHomomorphism (AssociationList Char Char -> Map Char Char
forall k v. AssociationList k v -> Map k v
weakMap [(Char
'B',Char
'B')]) (AssociationList (Arrow Char Char) (Arrow Char Char)
-> Map (Arrow Char Char) (Arrow Char Char)
forall k v. AssociationList k v -> Map k v
weakMap []) Graph Char Char
g2
diag :: Diagram
Hat
HatAr
HatOb
(FinGrph Char Char)
(GraphHomomorphism Char Char)
(Graph Char Char)
diag = Diagram
Hat
HatAr
HatOb
(FinGrph Char Char)
(GraphHomomorphism Char Char)
(Graph Char Char)
-> Diagram
Hat
HatAr
HatOb
(FinGrph Char Char)
(GraphHomomorphism Char Char)
(Graph Char Char)
forall c1 m1 o1 c2 m2 o2.
(FiniteCategory c1 m1 o1, Morphism m1 o1, Eq m1, Eq o1,
Category c2 m2 o2, Morphism m2 o2) =>
Diagram c1 m1 o1 c2 m2 o2 -> Diagram c1 m1 o1 c2 m2 o2
completeDiagram Diagram{src :: Hat
src = Hat
Hat, tgt :: FinGrph Char Char
tgt = FinGrph Char Char
forall n e. FinGrph n e
FinGrph, omap :: Map HatOb (Graph Char Char)
omap = AssociationList HatOb (Graph Char Char)
-> Map HatOb (Graph Char Char)
forall k v. AssociationList k v -> Map k v
weakMap [(HatOb
HatA,Graph Char Char
forall {e}. Graph Char e
g3),(HatOb
HatB,Graph Char Char
g1),(HatOb
HatC,Graph Char Char
g2)], mmap :: Map HatAr (GraphHomomorphism Char Char)
mmap = AssociationList HatAr (GraphHomomorphism Char Char)
-> Map HatAr (GraphHomomorphism Char Char)
forall k v. AssociationList k v -> Map k v
weakMap [(HatAr
HatF,GraphHomomorphism Char Char
gh1),(HatAr
HatG,GraphHomomorphism Char Char
gh2)]}
exampleColimitOfGraphs :: Cocone Hat HatAr HatOb (FinGrph (Colimit HatOb Char) (Colimit HatOb Char)) (GraphHomomorphism (Colimit HatOb Char) (Colimit HatOb Char)) (Graph (Colimit HatOb Char) (Colimit HatOb Char))
exampleColimitOfGraphs :: Cocone
Hat
HatAr
HatOb
(FinGrph (Colimit HatOb Char) (Colimit HatOb Char))
(GraphHomomorphism (Colimit HatOb Char) (Colimit HatOb Char))
(Graph (Colimit HatOb Char) (Colimit HatOb Char))
exampleColimitOfGraphs = Diagram
Hat
HatAr
HatOb
(FinGrph Char Char)
(GraphHomomorphism Char Char)
(Graph Char Char)
-> Cocone
Hat
HatAr
HatOb
(FinGrph (Colimit HatOb Char) (Colimit HatOb Char))
(GraphHomomorphism (Colimit HatOb Char) (Colimit HatOb Char))
(Graph (Colimit HatOb Char) (Colimit HatOb Char))
forall c m o cLim mLim oLim cIndex mIndex oIndex.
(CocompleteCategory c m o cLim mLim oLim cIndex mIndex oIndex,
FiniteCategory cIndex mIndex oIndex, Morphism mIndex oIndex,
Eq cIndex, Eq mIndex, Eq oIndex) =>
Diagram cIndex mIndex oIndex c m o
-> Cocone cIndex mIndex oIndex cLim mLim oLim
colimit Diagram
Hat
HatAr
HatOb
(FinGrph Char Char)
(GraphHomomorphism Char Char)
(Graph Char Char)
exampleDiagramHatToFinGrph