{-| Module  : FiniteCategories
Description : An example of 'FullSubcategory' of __'FinGrph'__ and an example of 'Graph'.
Copyright   : Guillaume Sabbagh 2022
License     : GPL-3
Maintainer  : guillaumesabbagh@protonmail.com
Stability   : experimental
Portability : portable

An example of 'FullSubcategory' of __'FinGrph'__ and an example of 'Graph'.


-}
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
    
    -- | Return the divisibility graph of number lesser or equal than a given n.

    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])
    
    
    -- | Example of graph : divisibility graph of numbers lesser or equal than 10.

    exampleGraph :: Graph Int Int
    exampleGraph :: Graph Int Int
exampleGraph = Int -> Graph Int Int
divisibilityGraph Int
10
            
    -- | Example of a 'FullSubcategory' of 'FinGrph'.

    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]))
    
    -- | Example of a discrete diagram selecting two graphs.

    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
            
    -- | Product of 'exampleDiscreteDiagramToFinGrph'.

    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 
    
    -- | Example of a parallel diagram selecting two graphs.

    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
            
    -- | Limit of 'exampleParallelDiagramToFinGrph'.

    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
    
    -- | Example of a 'Diagram' from 'Hat' to 'FinGrph'.

    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)]}
            
    -- | Example of a colimit of graphs.

    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