{-# LANGUAGE NoImplicitPrelude #-}

{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}

-- |
-- Module      : OAlg.AbelianGroup.Free.Limes
-- Description : limits for matrices over integers.
-- Copyright   : (c) Erich Gut
-- License     : BSD3
-- Maintainer  : zerich.gut@gmail.com
--
-- limits for 'Z'-matrices.
module OAlg.AbelianGroup.Free.Limes
  ( -- * Projective
    zmxKernels
  , zmxPullbacks
  ) where

import Data.List (filter)

import OAlg.Prelude

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

import OAlg.Entity.Natural
import OAlg.Entity.Diagram
import OAlg.Entity.FinList
import OAlg.Entity.Matrix
import OAlg.Entity.Sequence

import OAlg.Limes.Definition
import OAlg.Limes.Cone
import OAlg.Limes.Limits
import OAlg.Limes.KernelsAndCokernels
import OAlg.Limes.PullbacksAndPushouts

import OAlg.AbelianGroup.Free.SmithNormalForm

--------------------------------------------------------------------------------
-- zmxKernel -

zmxKernel :: KernelDiagram N1 (Matrix Z) -> Kernel N1 (Matrix Z)
zmxKernel :: KernelDiagram N1 (Matrix Z) -> Kernel N1 (Matrix Z)
zmxKernel kDgm :: KernelDiagram N1 (Matrix Z)
kDgm@(DiagramParallelLR Point (Matrix Z)
_ Point (Matrix Z)
_ (Matrix Z
h:|FinList n1 (Matrix Z)
Nil)) = Cone Dst 'Projective ('Parallel 'LeftToRight) N2 N1 (Matrix Z)
-> (Cone Dst 'Projective ('Parallel 'LeftToRight) N2 N1 (Matrix Z)
    -> Matrix Z)
-> Kernel N1 (Matrix Z)
forall s (t :: DiagramType) (n :: N') (m :: N') a.
Cone s 'Projective t n m a
-> (Cone s 'Projective t n m a -> a) -> Limes s 'Projective t n m a
LimesProjective Cone Dst 'Projective ('Parallel 'LeftToRight) N2 N1 (Matrix Z)
lim Cone Dst 'Projective ('Parallel 'LeftToRight) N2 N1 (Matrix Z)
-> Matrix Z
univ where
  
  DiagonalForm [Z]
d RowTrafo Z
_ (ColTrafo GLT Z
t) = Matrix Z -> DiagonalForm Z
zmxDiagonalForm Matrix Z
h
  -- d = (rt*>h)<*ct

  Inv Matrix Z
b Matrix Z
bInv = GLApp (GLT Z) (Inv (Matrix Z)) -> GLT Z -> Inv (Matrix Z)
forall a b. GLApp a b -> a -> b
forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
amap GLApp (GLT Z) (Inv (Matrix Z))
forall x1. Distributive x1 => GLApp (GLT x1) (Inv (Matrix x1))
GLTGL GLT Z
t
  
  m :: N
m = Dim Z () -> N
forall x. LengthN x => x -> N
lengthN (Matrix Z -> Point (Matrix Z)
forall q. Oriented q => q -> Point q
start Matrix Z
h)
  s :: N
s = [Z] -> N
forall x. LengthN x => x -> N
lengthN [Z]
d
  r :: N
r = N
m N -> N -> N
>- N
s

  k :: Matrix Z
k = Matrix (Matrix Z) -> Matrix Z
forall x. Oriented x => Matrix (Matrix x) -> Matrix x
mtxJoin (Matrix (Matrix Z) -> Matrix Z) -> Matrix (Matrix Z) -> Matrix Z
forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ [Dim' Z] -> [Dim' Z] -> [(Matrix Z, N, N)] -> Matrix (Matrix Z)
forall x.
(Additive x, FibredOriented x) =>
[Dim' x] -> [Dim' x] -> [(Matrix x, N, N)] -> Matrix (Matrix x)
matrixBlc [Dim Z ()
Dim' Z
ds,Dim Z ()
Dim' Z
dr] [Dim Z ()
Dim' Z
dr] [(Point (Matrix Z) -> Matrix Z
forall c. Multiplicative c => Point c -> c
one Point (Matrix Z)
Dim Z ()
dr,N
1,N
0)] where
    ds :: Dim Z ()
ds = () -> Dim Z ()
forall p x. (Entity p, p ~ Point x) => p -> Dim x p
dim () Dim Z () -> Exponent (Dim Z ()) -> Dim Z ()
forall f. Exponential f => f -> Exponent f -> f
^ N
Exponent (Dim Z ())
s
    dr :: Dim Z ()
dr = () -> Dim Z ()
forall p x. (Entity p, p ~ Point x) => p -> Dim x p
dim () Dim Z () -> Exponent (Dim Z ()) -> Dim Z ()
forall f. Exponential f => f -> Exponent f -> f
^ N
Exponent (Dim Z ())
r

  kPrj :: Matrix Z -> Matrix Z
kPrj (Matrix Dim' Z
_ Dim' Z
c Entries N N Z
xs) = Dim' Z -> Dim' Z -> Entries N N Z -> Matrix Z
forall x. Dim' x -> Dim' x -> Entries N N x -> Matrix x
Matrix (Matrix Z -> Point (Matrix Z)
forall q. Oriented q => q -> Point q
start Matrix Z
k) Dim' Z
c Entries N N Z
xs' where
    xs' :: Entries N N Z
xs' = PSequence (N, N) Z -> Entries N N Z
forall i j x. PSequence (i, j) x -> Entries i j x
Entries (PSequence (N, N) Z -> Entries N N Z)
-> PSequence (N, N) Z -> Entries N N Z
forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ [(Z, (N, N))] -> PSequence (N, N) Z
forall i x. [(x, i)] -> PSequence i x
PSequence
        ([(Z, (N, N))] -> PSequence (N, N) Z)
-> [(Z, (N, N))] -> PSequence (N, N) Z
forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ ((Z, N, N) -> (Z, (N, N))) -> [(Z, N, N)] -> [(Z, (N, N))]
forall a b. (a -> b) -> [a] -> [b]
forall (h :: * -> * -> *) (f :: * -> *) a b.
Applicative1 h f =>
h a b -> f a -> f b
amap1 (\(Z
x,N
i,N
j) -> (Z
x,(N
iN -> N -> N
>-N
s,N
j)))
        ([(Z, N, N)] -> [(Z, (N, N))]) -> [(Z, N, N)] -> [(Z, (N, N))]
forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ ((Z, N, N) -> Bool) -> [(Z, N, N)] -> [(Z, N, N)]
forall a. (a -> Bool) -> [a] -> [a]
filter (\(Z
_,N
i,N
_) -> N
s N -> N -> Bool
forall a. Ord a => a -> a -> Bool
<= N
i)
        ([(Z, N, N)] -> [(Z, N, N)]) -> [(Z, N, N)] -> [(Z, N, N)]
forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ Entries N N Z -> [(Z, N, N)]
forall i j x. Entries i j x -> [(x, i, j)]
etsxs Entries N N Z
xs

  lim :: Cone Dst 'Projective ('Parallel 'LeftToRight) N2 N1 (Matrix Z)
lim = KernelDiagram N1 (Matrix Z)
-> Matrix Z
-> Cone Dst 'Projective ('Parallel 'LeftToRight) N2 N1 (Matrix Z)
forall a (m :: N').
Distributive a =>
Diagram ('Parallel 'LeftToRight) N2 m a
-> a -> Cone Dst 'Projective ('Parallel 'LeftToRight) N2 m a
ConeKernel KernelDiagram N1 (Matrix Z)
kDgm (Matrix Z
bMatrix Z -> Matrix Z -> Matrix Z
forall c. Multiplicative c => c -> c -> c
*Matrix Z
k)
  
  univ :: Cone Dst 'Projective ('Parallel 'LeftToRight) N2 N1 (Matrix Z)
-> Matrix Z
univ (ConeKernel KernelDiagram N1 (Matrix Z)
_ Matrix Z
x) = Matrix Z -> Matrix Z
kPrj (Matrix Z
bInv Matrix Z -> Matrix Z -> Matrix Z
forall c. Multiplicative c => c -> c -> c
* Matrix Z
x)

--------------------------------------------------------------------------------
-- zmxKernels1 -

-- | 'N1'-kernels for 'Z'-matrices.
zmxKernels1 :: Kernels N1 (Matrix Z)
zmxKernels1 :: Kernels N1 (Matrix Z)
zmxKernels1 = (KernelDiagram N1 (Matrix Z) -> Kernel N1 (Matrix Z))
-> Kernels N1 (Matrix Z)
forall s (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N')
       a.
(Diagram t n m a -> Limes s p t n m a) -> Limits s p t n m a
Limits KernelDiagram N1 (Matrix Z) -> Kernel N1 (Matrix Z)
zmxKernel

--------------------------------------------------------------------------------
-- zmxKernels -

-- | kernels for 'Z'-matrices.
zmxKernels :: Kernels n (Matrix Z)
zmxKernels :: forall (n :: N'). Kernels n (Matrix Z)
zmxKernels = Kernels N1 (Matrix Z) -> Kernels n (Matrix Z)
forall a (n :: N'). Distributive a => Kernels N1 a -> Kernels n a
kernels Kernels N1 (Matrix Z)
zmxKernels1

--------------------------------------------------------------------------------
-- zmxPullbacks2 -

-- | 'N2'-pullbacks for 'Z'-matrices.
zmxPullbacks2 :: Pullbacks N2 (Matrix Z)
zmxPullbacks2 :: Pullbacks N2 (Matrix Z)
zmxPullbacks2 = Products N2 (Matrix Z)
-> Equalizers N2 (Matrix Z) -> Pullbacks N2 (Matrix Z)
forall a.
Multiplicative a =>
Products N2 a -> Equalizers N2 a -> Pullbacks N2 a
plbPrdEql2 Products N2 (Matrix Z)
forall x (n :: N'). Distributive x => Products n (Matrix x)
mtxProducts (Kernels N1 (Matrix Z) -> Equalizers (N1 + 1) (Matrix Z)
forall a (n :: N').
(Distributive a, Abelian a) =>
Kernels n a -> Equalizers (n + 1) a
krnEqls Kernels N1 (Matrix Z)
zmxKernels1)

--------------------------------------------------------------------------------
-- zmxPullbacks -

-- | pullbacks for 'Z'-matrices.
zmxPullbacks :: Pullbacks n (Matrix Z)
zmxPullbacks :: forall (n :: N'). Pullbacks n (Matrix Z)
zmxPullbacks = Pullbacks N2 (Matrix Z)
-> Limits Mlt 'Projective ('Star 'To) (n + 1) n (Matrix Z)
forall a (n :: N').
Multiplicative a =>
Pullbacks N2 a -> Pullbacks n a
pullbacks Pullbacks N2 (Matrix Z)
zmxPullbacks2