{-# LANGUAGE NoImplicitPrelude #-}

{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE FlexibleInstances, FlexibleContexts #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE DataKinds #-}

-- |

-- Module      : OAlg.Limes.Cone.FactorChain

-- Description : consturction of a cones for chains.

-- Copyright   : (c) Erich Gut

-- License     : BSD3

-- Maintainer  : zerich.gut@gmail.com

-- 

-- predicate for a factor with 'end' point at the starting point of a given chain.

module OAlg.Limes.Cone.FactorChain
  ( -- * Chain

    FactorChain(..)
  , cnPrjChainTo, cnPrjChainToInv
  , cnPrjChainFrom, cnPrjChainFromInv
  ) where

import OAlg.Prelude

import OAlg.Entity.Natural
import OAlg.Entity.FinList
import OAlg.Entity.Diagram

import OAlg.Structure.Oriented
import OAlg.Structure.Multiplicative

import OAlg.Limes.Perspective

import OAlg.Limes.Cone.Definition

--------------------------------------------------------------------------------

-- FactorChain -


-- | predicate for a factor with 'end' point at the starting point of the given chain.

--

-- __Property__

--

-- (1) Let @'FactorChain' f d@ be in @'FactorChain' 'To'  __n__ __a__@

-- for a 'Multiplicative' structure @__a__@ then holds:

-- @'end' f '==' 'chnToStart' ('diagram' d)@.

--

-- (2) Let @'FactorChain' f d@ be in @'FactorChain' 'From'  __n__ __a__@

-- for a 'Multiplicative' structure @__a__@ then holds:

-- @'end' f '==' 'chnFromStart' ('diagram' d)@.

data FactorChain d s n x = FactorChain x (d (Chain s) (n+1) n x)

deriving instance (Show x, ShowPoint x) => Show (FactorChain Diagram s n x)
deriving instance (Eq x, EqPoint x) => Eq (FactorChain Diagram s n x)

instance (Diagrammatic d, Oriented x) => Validable (FactorChain d To n x) where
  valid :: FactorChain d 'To n x -> Statement
valid (FactorChain x
f d ('Chain 'To) (n + 1) n x
d)
    = [Statement] -> Statement
And [ x -> Statement
forall a. Validable a => a -> Statement
valid x
f
          , Diagram ('Chain 'To) ('S n) n x -> Statement
forall a. Validable a => a -> Statement
valid Diagram ('Chain 'To) ('S n) n x
d'
          , x -> Point x
forall q. Oriented q => q -> Point q
end x
f Point x -> Point x -> Statement
forall a. Eq a => a -> a -> Statement
.==. Diagram ('Chain 'To) ('S n) n x -> Point x
forall a (n :: N') (m :: N').
Oriented a =>
Diagram ('Chain 'To) n m a -> Point a
chnToStart Diagram ('Chain 'To) ('S n) n x
d'
          ]
    where d' :: Diagram ('Chain 'To) ('S n) n x
d' = d ('Chain 'To) ('S n) n x -> Diagram ('Chain 'To) ('S n) n x
forall (t :: DiagramType) (n :: N') (m :: N') x.
d t n m x -> Diagram t n m x
forall (d :: DiagramType -> N' -> N' -> * -> *) (t :: DiagramType)
       (n :: N') (m :: N') x.
Diagrammatic d =>
d t n m x -> Diagram t n m x
diagram d ('Chain 'To) (n + 1) n x
d ('Chain 'To) ('S n) n x
d

instance (Diagrammatic d, Oriented x) => Validable (FactorChain d From n x) where
  valid :: FactorChain d 'From n x -> Statement
valid (FactorChain x
f d ('Chain 'From) (n + 1) n x
d)
    = [Statement] -> Statement
And [ x -> Statement
forall a. Validable a => a -> Statement
valid x
f
          , Diagram ('Chain 'From) ('S n) n x -> Statement
forall a. Validable a => a -> Statement
valid Diagram ('Chain 'From) ('S n) n x
d'
          , x -> Point x
forall q. Oriented q => q -> Point q
end x
f Point x -> Point x -> Statement
forall a. Eq a => a -> a -> Statement
.==. Diagram ('Chain 'From) ('S n) n x -> Point x
forall (n :: N') (m :: N') a.
Diagram ('Chain 'From) n m a -> Point a
chnFromStart Diagram ('Chain 'From) ('S n) n x
d'
          ]
    where d' :: Diagram ('Chain 'From) ('S n) n x
d' = d ('Chain 'From) ('S n) n x -> Diagram ('Chain 'From) ('S n) n x
forall (t :: DiagramType) (n :: N') (m :: N') x.
d t n m x -> Diagram t n m x
forall (d :: DiagramType -> N' -> N' -> * -> *) (t :: DiagramType)
       (n :: N') (m :: N') x.
Diagrammatic d =>
d t n m x -> Diagram t n m x
diagram d ('Chain 'From) (n + 1) n x
d ('Chain 'From) ('S n) n x
d

--------------------------------------------------------------------------------

-- cnPrjChainTo


-- | the induced 'Projective' cone with ending factor given by the given 'FactorChain'.

--

-- __Property__ Let @h = 'FactorChain' f d@ be in

-- @'FactorChain' 'To' __n__ __a__@ for a 'Multiplicative' structure @__a__@ and

-- @'ConeProjective' d' _ (_':|'..':|'c':|''Nil') = 'cnPrjChainTo' h@ then holds:

-- @d' '==' d@ and @c '==' f@.

cnPrjChainTo :: (Diagrammatic d, Multiplicative x)
  => FactorChain d To n x -> Cone Mlt Projective d (Chain To) (n+1) n x
cnPrjChainTo :: forall (d :: DiagramType -> N' -> N' -> * -> *) x (n :: N').
(Diagrammatic d, Multiplicative x) =>
FactorChain d 'To n x
-> Cone Mlt 'Projective d ('Chain 'To) (n + 1) n x
cnPrjChainTo (FactorChain x
f d ('Chain 'To) (n + 1) n x
d) = d ('Chain 'To) ('S n) n x
-> Point x
-> FinList ('S n) x
-> Cone Mlt 'Projective d ('Chain 'To) ('S n) n x
forall a (d :: DiagramType -> N' -> N' -> * -> *)
       (t :: DiagramType) (n :: N') (m :: N').
Multiplicative a =>
d t n m a
-> Point a -> FinList n a -> Cone Mlt 'Projective d t n m a
ConeProjective d ('Chain 'To) (n + 1) n x
d ('Chain 'To) ('S n) n x
d (x -> Point x
forall q. Oriented q => q -> Point q
start x
f) (x -> FinList n x -> FinList (n + 1) x
forall a (n :: N').
Multiplicative a =>
a -> FinList n a -> FinList (n + 1) a
cmp x
f FinList n x
as) where
  as :: FinList n x
as = Diagram ('Chain 'To) ('S n) n x -> FinList n x
forall (t :: DiagramType) (n :: N') (m :: N') a.
Diagram t n m a -> FinList m a
dgArrows (Diagram ('Chain 'To) ('S n) n x -> FinList n x)
-> Diagram ('Chain 'To) ('S n) n x -> FinList n x
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ d ('Chain 'To) ('S n) n x -> Diagram ('Chain 'To) ('S n) n x
forall (t :: DiagramType) (n :: N') (m :: N') x.
d t n m x -> Diagram t n m x
forall (d :: DiagramType -> N' -> N' -> * -> *) (t :: DiagramType)
       (n :: N') (m :: N') x.
Diagrammatic d =>
d t n m x -> Diagram t n m x
diagram d ('Chain 'To) (n + 1) n x
d ('Chain 'To) ('S n) n x
d

  cmp :: Multiplicative a => a -> FinList n a -> FinList (n+1) a
  cmp :: forall a (n :: N').
Multiplicative a =>
a -> FinList n a -> FinList (n + 1) a
cmp a
f FinList n a
Nil     = a
fa -> FinList 'N0 a -> FinList ('N0 + 1) a
forall a (n1 :: N'). a -> FinList n1 a -> FinList (n1 + 1) a
:|FinList 'N0 a
forall a. FinList 'N0 a
Nil
  cmp a
f (a
a:|FinList n1 a
as) = (a
aa -> a -> a
forall c. Multiplicative c => c -> c -> c
*a
c)a -> FinList ('S n1) a -> FinList ('S n1 + 1) a
forall a (n1 :: N'). a -> FinList n1 a -> FinList (n1 + 1) a
:|FinList (n1 + 1) a
FinList ('S n1) a
cs where cs :: FinList (n1 + 1) a
cs@(a
c:|FinList n1 a
_) = a -> FinList n1 a -> FinList (n1 + 1) a
forall a (n :: N').
Multiplicative a =>
a -> FinList n a -> FinList (n + 1) a
cmp a
f FinList n1 a
as

--------------------------------------------------------------------------------

-- cnPrjChainToInv -


-- | the underlying factor chain of a projective chain to cone, i.e the inverse of

-- 'cnPrjChainToInv'.

cnPrjChainToInv :: Cone Mlt Projective d (Chain To) (n+1) n x -> FactorChain d To n x
cnPrjChainToInv :: forall (d :: DiagramType -> N' -> N' -> * -> *) (n :: N') x.
Cone Mlt 'Projective d ('Chain 'To) (n + 1) n x
-> FactorChain d 'To n x
cnPrjChainToInv (ConeProjective d ('Chain 'To) (n + 1) n x
d Point x
_ FinList (n + 1) x
cs) = x -> d ('Chain 'To) (n + 1) n x -> FactorChain d 'To n x
forall (d :: DiagramType -> N' -> N' -> * -> *) (s :: Site)
       (n :: N') x.
x -> d ('Chain s) (n + 1) n x -> FactorChain d s n x
FactorChain (FinList (n + 1) x -> x
forall (n :: N') x. FinList (n + 1) x -> x
f FinList (n + 1) x
cs) d ('Chain 'To) (n + 1) n x
d where
  f :: FinList (n+1) x -> x
  f :: forall (n :: N') x. FinList (n + 1) x -> x
f (x
c:|FinList n1 x
Nil)       = x
c
  f (x
_:|cs :: FinList n1 x
cs@(x
_:|FinList n1 x
_)) = FinList (n1 + 1) x -> x
forall (n :: N') x. FinList (n + 1) x -> x
f FinList n1 x
FinList (n1 + 1) x
cs

--------------------------------------------------------------------------------

-- chPrjChainFrom -


-- | the induced 'Projective' cone with starting factor given by the given 'FactorChain'.

--

-- __Property__ Let @h = 'FactorChain' f d@ be in

-- @'FactorChain' 'From' __n__ __a__@ for a 'Multiplicative' structure @__a__@ and

-- @'ConeProjective' d' _ (c':|'_) = 'cnPrjChainFrom' h@ then holds:

-- @d' '==' d@ and @c '==' f@.

cnPrjChainFrom :: (Diagrammatic d, Multiplicative x)
  => FactorChain d From n x -> Cone Mlt Projective d (Chain From) (n+1) n x
cnPrjChainFrom :: forall (d :: DiagramType -> N' -> N' -> * -> *) x (n :: N').
(Diagrammatic d, Multiplicative x) =>
FactorChain d 'From n x
-> Cone Mlt 'Projective d ('Chain 'From) (n + 1) n x
cnPrjChainFrom (FactorChain x
f d ('Chain 'From) (n + 1) n x
d) = d ('Chain 'From) ('S n) n x
-> Point x
-> FinList ('S n) x
-> Cone Mlt 'Projective d ('Chain 'From) ('S n) n x
forall a (d :: DiagramType -> N' -> N' -> * -> *)
       (t :: DiagramType) (n :: N') (m :: N').
Multiplicative a =>
d t n m a
-> Point a -> FinList n a -> Cone Mlt 'Projective d t n m a
ConeProjective d ('Chain 'From) (n + 1) n x
d ('Chain 'From) ('S n) n x
d (x -> Point x
forall q. Oriented q => q -> Point q
start x
f) (x -> FinList n x -> FinList (n + 1) x
forall a (n :: N').
Multiplicative a =>
a -> FinList n a -> FinList (n + 1) a
cmp x
f FinList n x
as) where
  as :: FinList n x
as = Diagram ('Chain 'From) ('S n) n x -> FinList n x
forall (t :: DiagramType) (n :: N') (m :: N') a.
Diagram t n m a -> FinList m a
dgArrows (Diagram ('Chain 'From) ('S n) n x -> FinList n x)
-> Diagram ('Chain 'From) ('S n) n x -> FinList n x
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ d ('Chain 'From) ('S n) n x -> Diagram ('Chain 'From) ('S n) n x
forall (t :: DiagramType) (n :: N') (m :: N') x.
d t n m x -> Diagram t n m x
forall (d :: DiagramType -> N' -> N' -> * -> *) (t :: DiagramType)
       (n :: N') (m :: N') x.
Diagrammatic d =>
d t n m x -> Diagram t n m x
diagram d ('Chain 'From) (n + 1) n x
d ('Chain 'From) ('S n) n x
d
  
  cmp :: Multiplicative x => x -> FinList n x -> FinList (n+1) x
  cmp :: forall a (n :: N').
Multiplicative a =>
a -> FinList n a -> FinList (n + 1) a
cmp x
f FinList n x
Nil     = x
fx -> FinList 'N0 x -> FinList ('N0 + 1) x
forall a (n1 :: N'). a -> FinList n1 a -> FinList (n1 + 1) a
:|FinList 'N0 x
forall a. FinList 'N0 a
Nil
  cmp x
f (x
a:|FinList n1 x
as) = x
f x -> FinList ('S n1) x -> FinList ('S n1 + 1) x
forall a (n1 :: N'). a -> FinList n1 a -> FinList (n1 + 1) a
:| x -> FinList n1 x -> FinList (n1 + 1) x
forall a (n :: N').
Multiplicative a =>
a -> FinList n a -> FinList (n + 1) a
cmp x
f' FinList n1 x
as where f' :: x
f' = x
ax -> x -> x
forall c. Multiplicative c => c -> c -> c
*x
f

--------------------------------------------------------------------------------

-- cnPrjChainFromInv -


-- | the underlying factor chain of a projective chain from cone, i.e. the inverse of

-- 'cnPrjChainFrom'.

cnPrjChainFromInv :: Cone Mlt Projective d (Chain From) (n+1) n x -> FactorChain d From n x
cnPrjChainFromInv :: forall (d :: DiagramType -> N' -> N' -> * -> *) (n :: N') x.
Cone Mlt 'Projective d ('Chain 'From) (n + 1) n x
-> FactorChain d 'From n x
cnPrjChainFromInv (ConeProjective d ('Chain 'From) (n + 1) n x
d Point x
_ (x
c:|FinList n1 x
_)) = x -> d ('Chain 'From) (n + 1) n x -> FactorChain d 'From n x
forall (d :: DiagramType -> N' -> N' -> * -> *) (s :: Site)
       (n :: N') x.
x -> d ('Chain s) (n + 1) n x -> FactorChain d s n x
FactorChain x
c d ('Chain 'From) (n + 1) n x
d