{-# LANGUAGE NoImplicitPrelude #-}

{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE FlexibleContexts, FlexibleInstances #-}
{-# LANGUAGE StandaloneDeriving, GeneralizedNewtypeDeriving #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE DataKinds #-}
-- |

-- Module      : OAlg.Entity.Matrix.ProductsAndSums

-- Description : products and sums for matrices

-- Copyright   : (c) Erich Gut

-- License     : BSD3

-- Maintainer  : zerich.gut@gmail.com

-- 

-- 'Products' and 'Sums' for matrices.

module OAlg.Entity.Matrix.ProductsAndSums
  ( mtxProducts, mtxSums
  ) where

import Data.Foldable
import Data.List (map)

import OAlg.Prelude

import OAlg.Category.SDuality

import OAlg.Data.Variant
import OAlg.Data.Either

import OAlg.Structure.Oriented
import OAlg.Structure.Multiplicative
import OAlg.Structure.Additive
import OAlg.Structure.Distributive

import OAlg.Entity.FinList
import OAlg.Entity.Diagram
import OAlg.Entity.Sequence.PSequence

import OAlg.Limes.Cone
import OAlg.Limes.Definition
import OAlg.Limes.Limits
import OAlg.Limes.ProductsAndSums

import OAlg.Entity.Matrix.Dim
import OAlg.Entity.Matrix.Definition
import OAlg.Entity.Matrix.Entries

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

-- mtxProducts -


-- | products for matrices.

mtxProducts :: Distributive x => Products n (Matrix x)
mtxProducts :: forall x (n :: N'). Distributive x => Products n (Matrix x)
mtxProducts = (Diagram 'Discrete n N0 (Matrix x)
 -> LimesG Cone Mlt 'Projective Diagram 'Discrete n N0 (Matrix x))
-> LimitsG Cone Mlt 'Projective Diagram 'Discrete n N0 (Matrix x)
forall (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       s (p :: Perspective) (d :: DiagramType -> N' -> N' -> * -> *)
       (t :: DiagramType) (n :: N') (m :: N') x.
(d t n m x -> LimesG c s p d t n m x) -> LimitsG c s p d t n m x
LimitsG Diagram 'Discrete n N0 (Matrix x)
-> LimesG Cone Mlt 'Projective Diagram 'Discrete n N0 (Matrix x)
forall x (n :: N').
Distributive x =>
ProductDiagram n (Matrix x) -> Product n (Matrix x)
prd where
  
  prd :: Distributive x => ProductDiagram n (Matrix x) -> Product n (Matrix x)
  prd :: forall x (n :: N').
Distributive x =>
ProductDiagram n (Matrix x) -> Product n (Matrix x)
prd ProductDiagram n (Matrix x)
d = Cone Mlt 'Projective Diagram 'Discrete n N0 (Matrix x)
-> (Cone Mlt 'Projective Diagram 'Discrete n N0 (Matrix x)
    -> Matrix x)
-> LimesG Cone Mlt 'Projective Diagram 'Discrete n N0 (Matrix x)
forall (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       s (d :: DiagramType -> N' -> N' -> * -> *) (t :: DiagramType)
       (n :: N') (m :: N') x.
c s 'Projective d t n m x
-> (Cone s 'Projective d t n m x -> x)
-> LimesG c s 'Projective d t n m x
LimesProjective Cone Mlt 'Projective Diagram 'Discrete n N0 (Matrix x)
l Cone Mlt 'Projective Diagram 'Discrete n N0 (Matrix x) -> Matrix x
forall {n :: N'}. ProductCone n (Matrix x) -> Matrix x
u where
    l :: Cone Mlt 'Projective Diagram 'Discrete n N0 (Matrix x)
l = ProductDiagram n (Matrix x)
-> Cone Mlt 'Projective Diagram 'Discrete n N0 (Matrix x)
forall x (n :: N').
Distributive x =>
ProductDiagram n (Matrix x) -> ProductCone n (Matrix x)
lim ProductDiagram n (Matrix x)
d
    u :: ProductCone n (Matrix x) -> Matrix x
u = ProductCone n (Matrix x) -> Matrix x
forall x (n :: N').
Distributive x =>
ProductCone n (Matrix x) -> Matrix x
univ

  lim :: Distributive x => ProductDiagram n (Matrix x) -> ProductCone n (Matrix x)
  lim :: forall x (n :: N').
Distributive x =>
ProductDiagram n (Matrix x) -> ProductCone n (Matrix x)
lim d :: ProductDiagram n (Matrix x)
d@(DiagramDiscrete FinList n (Point (Matrix x))
ps)  = ProductDiagram n (Matrix x)
-> Point (Matrix x)
-> FinList n (Matrix x)
-> Cone Mlt 'Projective Diagram 'Discrete n N0 (Matrix 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 ProductDiagram n (Matrix x)
d Point (Matrix x)
Dim x (Point x)
l (N
-> Dim x (Point x)
-> FinList n (Dim x (Point x))
-> FinList n (Matrix x)
forall x (n :: N').
Distributive x =>
N
-> Dim x (Point x)
-> FinList n (Dim x (Point x))
-> FinList n (Matrix x)
prjs N
0 Dim x (Point x)
l FinList n (Point (Matrix x))
FinList n (Dim x (Point x))
ps) where
    l :: Dim x (Point x)
l = Dim' (Matrix x) -> Dim x (Point x)
Dim (Matrix x) (Dim x (Point x)) -> Dim x (Point x)
forall x. Oriented x => Dim' (Matrix x) -> Dim' x
mtxJoinDim (Dim (Matrix x) (Dim x (Point x)) -> Dim x (Point x))
-> Dim (Matrix x) (Dim x (Point x)) -> Dim x (Point x)
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ [Point (Matrix x)] -> Dim' (Matrix x)
[Dim x (Point x)] -> Dim (Matrix x) (Dim x (Point x))
forall p x. (Entity p, p ~ Point x) => [p] -> Dim x p
productDim ([Dim x (Point x)] -> Dim (Matrix x) (Dim x (Point x)))
-> [Dim x (Point x)] -> Dim (Matrix x) (Dim x (Point x))
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ FinList n (Dim x (Point x)) -> [Dim x (Point x)]
forall a. FinList n a -> [a]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList FinList n (Point (Matrix x))
FinList n (Dim x (Point x))
ps

    prjs :: Distributive x
      => N -> Dim x (Point x) -> FinList n (Dim x (Point x)) -> FinList n (Matrix x)
    prjs :: forall x (n :: N').
Distributive x =>
N
-> Dim x (Point x)
-> FinList n (Dim x (Point x))
-> FinList n (Matrix x)
prjs N
_ Dim x (Point x)
_ FinList n (Dim x (Point x))
Nil     = FinList n (Matrix x)
FinList N0 (Matrix x)
forall a. FinList N0 a
Nil
    prjs N
j Dim x (Point x)
l (Dim x (Point x)
r:|FinList n1 (Dim x (Point x))
rs) = N -> Dim x (Point x) -> Dim x (Point x) -> Matrix x
forall {x}.
(Additive x, Multiplicative x) =>
N -> Dim x (Point x) -> Dim x (Point x) -> Matrix x
prj N
j Dim x (Point x)
l Dim x (Point x)
r Matrix x -> FinList n1 (Matrix x) -> FinList (n1 + 1) (Matrix x)
forall a (n1 :: N'). a -> FinList n1 a -> FinList (n1 + 1) a
:| N
-> Dim x (Point x)
-> FinList n1 (Dim x (Point x))
-> FinList n1 (Matrix x)
forall x (n :: N').
Distributive x =>
N
-> Dim x (Point x)
-> FinList n (Dim x (Point x))
-> FinList n (Matrix x)
prjs (N
jN -> N -> N
forall a. Additive a => a -> a -> a
+N
rl) Dim x (Point x)
l FinList n1 (Dim x (Point x))
rs where
      rl :: N
rl = Dim x (Point x) -> N
forall x. LengthN x => x -> N
lengthN Dim x (Point x)
r

    prj :: N -> Dim x (Point x) -> Dim x (Point x) -> Matrix x
prj N
j Dim x (Point x)
l Dim x (Point x)
r = Dim x (Point x) -> Dim x (Point x) -> Entries N N x -> Matrix x
forall x. Dim' x -> Dim' x -> Entries N N x -> Matrix x
Matrix Dim x (Point x)
r Dim x (Point x)
l Entries N N x
os where
      os :: Entries N N x
os = Entries N N x -> Entries N N x
forall x i j. Additive x => Entries i j x -> Entries i j x
etsElimZeros (Entries N N x -> Entries N N x) -> Entries N N x -> Entries N N x
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ PSequence (N, N) x -> Entries N N x
forall i j x. PSequence (i, j) x -> Entries i j x
Entries (PSequence (N, N) x -> Entries N N x)
-> PSequence (N, N) x -> Entries N N x
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ [(x, (N, N))] -> PSequence (N, N) x
forall i x. [(x, i)] -> PSequence i x
PSequence ([(x, (N, N))] -> PSequence (N, N) x)
-> [(x, (N, N))] -> PSequence (N, N) x
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ ((Point x, N) -> (x, (N, N))) -> [(Point x, N)] -> [(x, (N, N))]
forall a b. (a -> b) -> [a] -> [b]
map (\(Point x
p,N
i) -> (Point x -> x
forall c. Multiplicative c => Point c -> c
one Point x
p,(N
i,N
iN -> N -> N
forall a. Additive a => a -> a -> a
+N
j))) ([(Point x, N)] -> [(x, (N, N))])
-> [(Point x, N)] -> [(x, (N, N))]
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ Dim x (Point x) -> [(Point x, N)]
forall p x. (p ~ Point x) => Dim x p -> [(p, N)]
dimxs Dim x (Point x)
r

  univ :: Distributive x
    => ProductCone n (Matrix x) -> Matrix x
  univ :: forall x (n :: N').
Distributive x =>
ProductCone n (Matrix x) -> Matrix x
univ (ConeProjective Diagram 'Discrete n N0 (Matrix x)
_ Point (Matrix x)
t FinList n (Matrix x)
cs)
    = Matrix (Matrix x) -> Matrix x
forall x. Oriented x => Matrix (Matrix x) -> Matrix x
mtxJoin (Matrix (Matrix x) -> Matrix x) -> Matrix (Matrix x) -> Matrix x
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ Dim' (Matrix x)
-> Dim' (Matrix x) -> Entries N N (Matrix x) -> Matrix (Matrix x)
forall x. Dim' x -> Dim' x -> Entries N N x -> Matrix x
Matrix Dim' (Matrix x)
rw Dim' (Matrix x)
cl (Entries N N (Matrix x) -> Matrix (Matrix x))
-> Entries N N (Matrix x) -> Matrix (Matrix x)
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ Entries N N (Matrix x) -> Entries N N (Matrix x)
forall x i j. Additive x => Entries i j x -> Entries i j x
etsElimZeros (Entries N N (Matrix x) -> Entries N N (Matrix x))
-> Entries N N (Matrix x) -> Entries N N (Matrix x)
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ PSequence (N, N) (Matrix x) -> Entries N N (Matrix x)
forall i j x. PSequence (i, j) x -> Entries i j x
Entries (PSequence (N, N) (Matrix x) -> Entries N N (Matrix x))
-> PSequence (N, N) (Matrix x) -> Entries N N (Matrix x)
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ [(Matrix x, (N, N))] -> PSequence (N, N) (Matrix x)
forall i x. [(x, i)] -> PSequence i x
PSequence ([(Matrix x, (N, N))] -> PSequence (N, N) (Matrix x))
-> [(Matrix x, (N, N))] -> PSequence (N, N) (Matrix x)
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ N -> FinList n (Matrix x) -> [(Matrix x, (N, N))]
forall x (n :: N').
Distributive x =>
N -> FinList n (Matrix x) -> [(Matrix x, (N, N))]
u N
0 FinList n (Matrix x)
cs where
      rw :: Dim' (Matrix x)
rw = [Point (Matrix x)] -> Dim' (Matrix x)
forall p x. (Entity p, p ~ Point x) => [p] -> Dim x p
productDim ([Point (Matrix x)] -> Dim' (Matrix x))
-> [Point (Matrix x)] -> Dim' (Matrix x)
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ FinList n (Point (Matrix x)) -> [Point (Matrix x)]
forall a. FinList n a -> [a]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList (FinList n (Point (Matrix x)) -> [Point (Matrix x)])
-> FinList n (Point (Matrix x)) -> [Point (Matrix x)]
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ (Matrix x -> Point (Matrix x))
-> FinList n (Matrix x) -> FinList n (Point (Matrix x))
forall (h :: * -> * -> *) (f :: * -> *) x y.
Applicative1 h f =>
h x y -> f x -> f y
amap1 Matrix x -> Point (Matrix x)
forall q. Oriented q => q -> Point q
end FinList n (Matrix x)
cs
      cl :: Dim' (Matrix x)
cl = Point (Matrix x) -> Dim' (Matrix x)
forall p x. (Entity p, p ~ Point x) => p -> Dim x p
dim Point (Matrix x)
t
      
      u :: Distributive x => N -> FinList n (Matrix x) -> [(Matrix x,(N,N))]
      u :: forall x (n :: N').
Distributive x =>
N -> FinList n (Matrix x) -> [(Matrix x, (N, N))]
u N
_ FinList n (Matrix x)
Nil     = []
      u N
i (Matrix x
c:|FinList n1 (Matrix x)
cs) = (Matrix x
c,(N
i,N
0)) (Matrix x, (N, N)) -> [(Matrix x, (N, N))] -> [(Matrix x, (N, N))]
forall a. a -> [a] -> [a]
: N -> FinList n1 (Matrix x) -> [(Matrix x, (N, N))]
forall x (n :: N').
Distributive x =>
N -> FinList n (Matrix x) -> [(Matrix x, (N, N))]
u (N -> N
forall a. Enum a => a -> a
succ N
i) FinList n1 (Matrix x)
cs 


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

-- mtxSums -


-- | sums for matrices.

mtxSums :: Distributive x => Sums n (Matrix x)
mtxSums :: forall x (n :: N'). Distributive x => Sums n (Matrix x)
mtxSums = Dual1
  (LimitsG Cone Mlt 'Projective Diagram 'Discrete n N0) (Matrix x)
LimitsG Cone Mlt 'Injective Diagram 'Discrete n N0 (Matrix x)
sms where
  Contravariant2 IsoCo Matrix Dst Op (Matrix x) (Matrix (Op x))
i    = Variant2
  'Contravariant
  (Inv2 (HomCo Matrix Dst Op))
  (Matrix x)
  (Matrix (Op x))
forall x.
Distributive x =>
Variant2
  'Contravariant
  (Inv2 (HomCo Matrix Dst Op))
  (Matrix x)
  (Matrix (Op x))
isoCoMatrixOp
  SDualBi (Left1 Dual1
  (LimitsG Cone Mlt 'Projective Diagram 'Discrete n N0) (Matrix x)
sms) = Inv2 (HomCo Matrix Dst Op) (Matrix (Op x)) (Matrix x)
-> SDualBi
     (LimitsG Cone Mlt 'Projective Diagram 'Discrete n N0)
     (Matrix (Op x))
-> SDualBi
     (LimitsG Cone Mlt 'Projective Diagram 'Discrete n N0) (Matrix x)
forall (t :: * -> *) (a :: * -> * -> *) (b :: * -> * -> *) x y.
FunctorialG t a b =>
a x y -> b (t x) (t y)
amapF (IsoCo Matrix Dst Op (Matrix x) (Matrix (Op x))
-> Inv2 (HomCo Matrix Dst Op) (Matrix (Op x)) (Matrix x)
forall (c :: * -> * -> *) x y. Inv2 c x y -> Inv2 c y x
inv2 IsoCo Matrix Dst Op (Matrix x) (Matrix (Op x))
i) (Either1
  (Dual1 (LimitsG Cone Mlt 'Projective Diagram 'Discrete n N0))
  (LimitsG Cone Mlt 'Projective Diagram 'Discrete n N0)
  (Matrix (Op x))
-> SDualBi
     (LimitsG Cone Mlt 'Projective Diagram 'Discrete n N0)
     (Matrix (Op x))
forall (d :: * -> *) x. Either1 (Dual1 d) d x -> SDualBi d x
SDualBi (LimitsG Cone Mlt 'Projective Diagram 'Discrete n N0 (Matrix (Op x))
-> Either1
     (LimitsG Cone Mlt 'Injective Diagram 'Discrete n N0)
     (LimitsG Cone Mlt 'Projective Diagram 'Discrete n N0)
     (Matrix (Op x))
forall (g :: * -> *) x (f :: * -> *). g x -> Either1 f g x
Right1 LimitsG Cone Mlt 'Projective Diagram 'Discrete n N0 (Matrix (Op x))
forall x (n :: N'). Distributive x => Products n (Matrix x)
mtxProducts))