{-# 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 Diagram ('Parallel 'LeftToRight) N2 N1 (Matrix Z)
-> (Cone
      Dst 'Projective Diagram ('Parallel 'LeftToRight) N2 N1 (Matrix Z)
    -> Matrix Z)
-> Kernel N1 (Matrix Z)
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
  Dst 'Projective Diagram ('Parallel 'LeftToRight) N2 N1 (Matrix Z)
lim Cone
  Dst 'Projective Diagram ('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 (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
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 :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ [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 :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ [(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 :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ ((Z, N, N) -> (Z, (N, N))) -> [(Z, N, N)] -> [(Z, (N, N))]
forall (h :: * -> * -> *) (f :: * -> *) x y.
Applicative1 h f =>
h x y -> f x -> f y
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 :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ ((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 :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ 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 Diagram ('Parallel 'LeftToRight) N2 N1 (Matrix Z)
lim = KernelDiagram N1 (Matrix Z)
-> Matrix Z
-> Cone
     Dst 'Projective Diagram ('Parallel 'LeftToRight) N2 N1 (Matrix Z)
forall a (d :: DiagramType -> N' -> N' -> * -> *) (m :: N').
Distributive a =>
d ('Parallel 'LeftToRight) N2 m a
-> a -> Cone Dst 'Projective d ('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 Diagram ('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 (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 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 x (n :: N'). Distributive x => Kernels N1 x -> Kernels n x
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 x.
Multiplicative x =>
Products N2 x -> Equalizers N2 x -> Pullbacks N2 x
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 x (n :: N').
(Distributive x, Abelian x) =>
Kernels n x -> Equalizers (n + 1) x
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)
-> LimitsG
     Cone Mlt 'Projective Diagram ('Star 'To) (n + 1) n (Matrix Z)
forall x (n :: N').
Multiplicative x =>
Pullbacks N2 x -> Pullbacks n x
pullbacks Pullbacks N2 (Matrix Z)
zmxPullbacks2