{-# LANGUAGE NoImplicitPrelude #-}

{-# LANGUAGE TypeFamilies, TypeOperators #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FlexibleInstances, FlexibleContexts #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE StandaloneDeriving, GeneralizedNewtypeDeriving #-}
{-# LANGUAGE DataKinds, RankNTypes #-}

-- |
-- Module      : OAlg.AbelianGroup.KernelsAndCokernels
-- Description : kernels and cokernels for homomorphisms between finitely generated abelian groups
-- Copyright   : (c) Erich Gut
-- License     : BSD3
-- Maintainer  : zerich.gut@gmail.com
--
-- 'Kernels' and 'Cokernels' for homomorphisms between finitely generated abelian groups.
module OAlg.AbelianGroup.KernelsAndCokernels
  (
    -- * Kernels
    abhKernels

    -- * Cokernels
  , abhCokernels
    
    -- * Smith Normal
  , isoSmithNormal

    -- * Adjunction
  , abhSliceFreeAdjunction

  )
  where

import Control.Monad

import Data.List (map,(++),repeat,zip)

import OAlg.Prelude

import OAlg.Data.Canonical
import OAlg.Data.Generator

import OAlg.Structure.Oriented
import OAlg.Structure.Multiplicative as M
import OAlg.Structure.Additive
import OAlg.Structure.Exponential
import OAlg.Structure.Operational
import OAlg.Structure.Number

import OAlg.Hom.Oriented

import OAlg.Adjunction

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

import OAlg.Entity.Natural hiding ((++))
import OAlg.Entity.FinList as F hiding ((++),repeat,zip)
import OAlg.Entity.Diagram
import OAlg.Entity.Sequence
import OAlg.Entity.Matrix as M
import OAlg.Entity.Slice
import OAlg.Entity.Product (fromWord)

import OAlg.AbelianGroup.Definition
import OAlg.AbelianGroup.ZMod
import OAlg.AbelianGroup.Euclid
import OAlg.AbelianGroup.Free

--------------------------------------------------------------------------------
-- abhCokernelFree -

-- | the cokernel of a free cokernel diagram.
--
--  __Properties__ Let @d@ be in @'CokernelDiagramFree' 'N1' 'AbHom'@ and
-- @coker = 'abhCokernelFree' d@, then holds: 
--
-- (1) @'diagram' coker '==' d@.
--
-- (2) @'tip' ('universalCone' coker)@ is smith normal (see t'AbGroup').
abhCokernelFree :: CokernelDiagramFree N1 AbHom -> Cokernel N1 AbHom
abhCokernelFree :: CokernelDiagramFree N1 AbHom -> Cokernel N1 AbHom
abhCokernelFree (DiagramFree FinList N2 (SomeFree AbHom)
_ d :: Diagram ('Parallel 'RightToLeft) N2 N1 AbHom
d@(DiagramParallelRL Point AbHom
_ Point AbHom
_ (AbHom
h:|FinList n1 AbHom
Nil)))
  = Cone Dst 'Injective ('Parallel 'RightToLeft) N2 N1 AbHom
-> (Cone Dst 'Injective ('Parallel 'RightToLeft) N2 N1 AbHom
    -> AbHom)
-> Cokernel N1 AbHom
forall s (t :: DiagramType) (n :: N') (m :: N') a.
Cone s 'Injective t n m a
-> (Cone s 'Injective t n m a -> a) -> Limes s 'Injective t n m a
LimesInjective (Diagram ('Parallel 'RightToLeft) N2 N1 AbHom
-> AbHom
-> Cone Dst 'Injective ('Parallel 'RightToLeft) N2 N1 AbHom
forall a (m :: N').
Distributive a =>
Diagram ('Parallel 'RightToLeft) N2 m a
-> a -> Cone Dst 'Injective ('Parallel 'RightToLeft) N2 m a
ConeCokernel Diagram ('Parallel 'RightToLeft) N2 N1 AbHom
d AbHom
coker) Cone Dst 'Injective ('Parallel 'RightToLeft) N2 N1 AbHom -> AbHom
univ where

  m :: Matrix Z
m = AbHom -> Matrix Z
abhz AbHom
h
  SmithNormalForm N
o [Z]
ds (RowTrafo GLT Z
ra) ColTrafo Z
_ = Matrix Z -> SmithNormalForm Z
smithNormalForm Matrix Z
m
  Inv Matrix Z
a Matrix Z
aInv = 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
ra
  AbHom Matrix ZModHom
aInv' = Matrix Z -> AbHom
zabh Matrix Z
aInv
  p :: N
p = [Z] -> N
forall x. LengthN x => x -> N
lengthN [Z]
ds
  q :: N
q = Dim Z () -> N
forall x. LengthN x => x -> N
lengthN (Matrix Z -> Dim' Z
forall x. Matrix x -> Dim' x
rows Matrix Z
m) N -> N -> N
>- (N
o N -> N -> N
forall a. Additive a => a -> a -> a
+ N
p)

  d0 :: Dim ZModHom ZMod
d0 = ZMod -> Dim ZModHom ZMod
forall p x. (Entity p, p ~ Point x) => p -> Dim x p
dim (N -> ZMod
ZMod N
0)
  gp :: Dim ZModHom ZMod
gp = CSequence (Point ZModHom) -> Dim ZModHom (Point ZModHom)
ProductSymbol ZMod -> Dim ZModHom ZMod
forall x. CSequence (Point x) -> Dim x (Point x)
Dim (ProductSymbol ZMod -> Dim ZModHom ZMod)
-> ProductSymbol ZMod -> Dim ZModHom ZMod
forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ [ZMod] -> ProductSymbol ZMod
forall x. Entity x => [x] -> ProductSymbol x
productSymbol ([ZMod] -> ProductSymbol ZMod) -> [ZMod] -> ProductSymbol ZMod
forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ (Z -> ZMod) -> [Z] -> [ZMod]
forall a b. (a -> b) -> [a] -> [b]
forall (h :: * -> * -> *) (f :: * -> *) a b.
Applicative1 h f =>
h a b -> f a -> f b
amap1 (N -> ZMod
ZMod (N -> ZMod) -> (Z -> N) -> Z -> ZMod
forall y z x. (y -> z) -> (x -> y) -> x -> z
forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. Z -> N
forall a b. Projectible a b => b -> a
prj) [Z]
ds
  gq :: Dim ZModHom ZMod
gq = Dim ZModHom ZMod
d0 Dim ZModHom ZMod -> Exponent (Dim ZModHom ZMod) -> Dim ZModHom ZMod
forall f. Exponential f => f -> Exponent f -> f
^ N
Exponent (Dim ZModHom ZMod)
q
  gpq :: Dim ZModHom ZMod
gpq = Dim ZModHom ZMod
gp Dim ZModHom ZMod -> Dim ZModHom ZMod -> Dim ZModHom ZMod
forall c. Multiplicative c => c -> c -> c
* Dim ZModHom ZMod
gq
  
  coker :: AbHom
coker = ( Matrix ZModHom -> AbHom
AbHom (Matrix ZModHom -> AbHom) -> Matrix ZModHom -> AbHom
forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ Matrix (Matrix ZModHom) -> Matrix ZModHom
forall x. Oriented x => Matrix (Matrix x) -> Matrix x
mtxJoin
          (Matrix (Matrix ZModHom) -> Matrix ZModHom)
-> Matrix (Matrix ZModHom) -> Matrix ZModHom
forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ [Dim ZModHom (Point ZModHom)]
-> [Dim ZModHom (Point ZModHom)]
-> [(Matrix ZModHom, N, N)]
-> Matrix (Matrix ZModHom)
forall x.
(Additive x, FibredOriented x) =>
[Dim' x] -> [Dim' x] -> [(Matrix x, N, N)] -> Matrix (Matrix x)
matrixBlc [Dim ZModHom (Point ZModHom)
Dim ZModHom ZMod
gp,Dim ZModHom (Point ZModHom)
Dim ZModHom ZMod
gq] [Dim ZModHom ZMod
d0Dim ZModHom ZMod -> Exponent (Dim ZModHom ZMod) -> Dim ZModHom ZMod
forall f. Exponential f => f -> Exponent f -> f
^N
Exponent (Dim ZModHom ZMod)
o,Dim ZModHom ZMod
d0Dim ZModHom ZMod -> Exponent (Dim ZModHom ZMod) -> Dim ZModHom ZMod
forall f. Exponential f => f -> Exponent f -> f
^N
Exponent (Dim ZModHom ZMod)
p,Dim ZModHom (Point ZModHom)
Dim ZModHom ZMod
gq] [(Dim ZModHom ZMod
-> Dim ZModHom ZMod -> [(ZModHom, N, N)] -> Matrix ZModHom
forall x p.
(Additive x, p ~ Point x) =>
Dim x p -> Dim x p -> [(x, N, N)] -> Matrix x
matrix Dim ZModHom ZMod
gp (Dim ZModHom ZMod
d0Dim ZModHom ZMod -> Exponent (Dim ZModHom ZMod) -> Dim ZModHom ZMod
forall f. Exponential f => f -> Exponent f -> f
^N
Exponent (Dim ZModHom ZMod)
p) [(ZModHom, N, N)]
ps,N
0,N
1),(Point (Matrix ZModHom) -> Matrix ZModHom
forall c. Multiplicative c => Point c -> c
one Point (Matrix ZModHom)
Dim ZModHom ZMod
gq,N
1,N
2)]
          )
        AbHom -> AbHom -> AbHom
forall c. Multiplicative c => c -> c -> c
* Matrix Z -> AbHom
zabh Matrix Z
a where
    ps :: [(ZModHom, N, N)]
ps = [(Orientation ZMod -> Z -> ZModHom
zmh (N -> ZMod
ZMod N
0 ZMod -> ZMod -> Orientation ZMod
forall p. p -> p -> Orientation p
:> N -> ZMod
ZMod (Z -> N
forall a b. Projectible a b => b -> a
prj Z
d)) Z
1,N
i,N
i)| (Z
d,N
i) <- [Z]
ds [Z] -> [N] -> [(Z, N)]
forall a b. [a] -> [b] -> [(a, b)]
`zip` [N
0..]]
    -- @0 < d@ for all d in ds as ds is the diagonal of the smith normal form

  univ :: CokernelCone N1 AbHom -> AbHom
  univ :: Cone Dst 'Injective ('Parallel 'RightToLeft) N2 N1 AbHom -> AbHom
univ (ConeCokernel Diagram ('Parallel 'RightToLeft) N2 N1 AbHom
_ (AbHom Matrix ZModHom
x))
    = Matrix ZModHom -> AbHom
AbHom
    (Matrix ZModHom -> AbHom) -> Matrix ZModHom -> AbHom
forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ Dim ZModHom (Point ZModHom)
-> Dim ZModHom (Point ZModHom)
-> Entries N N ZModHom
-> Matrix ZModHom
forall x. Dim' x -> Dim' x -> Entries N N x -> Matrix x
Matrix (Matrix ZModHom -> Dim ZModHom (Point ZModHom)
forall x. Matrix x -> Dim' x
rows Matrix ZModHom
x) Dim ZModHom (Point ZModHom)
Dim ZModHom ZMod
gpq
    (Entries N N ZModHom -> Matrix ZModHom)
-> Entries N N ZModHom -> Matrix ZModHom
forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ Row N (Col N ZModHom) -> Entries N N ZModHom
forall i j x. (Ord i, Ord j) => Row j (Col i x) -> Entries i j x
rcets (Row N (Col N ZModHom) -> Entries N N ZModHom)
-> Row N (Col N ZModHom) -> Entries N N ZModHom
forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ PSequence N (Col N ZModHom) -> Row N (Col N ZModHom)
forall j x. PSequence j x -> Row j x
Row (PSequence N (Col N ZModHom) -> Row N (Col N ZModHom))
-> PSequence N (Col N ZModHom) -> Row N (Col N ZModHom)
forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ [(Col N ZModHom, N)] -> PSequence N (Col N ZModHom)
forall i x. [(x, i)] -> PSequence i x
PSequence
    ([(Col N ZModHom, N)] -> PSequence N (Col N ZModHom))
-> [(Col N ZModHom, N)] -> PSequence N (Col N ZModHom)
forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ ((Col N ZModHom, N) -> (Col N ZModHom, N))
-> [(Col N ZModHom, N)] -> [(Col N ZModHom, N)]
forall a b. (a -> b) -> [a] -> [b]
map (\(Col N ZModHom
cl,N
j) -> (Col N ZModHom
cl,N
jN -> N -> N
>-N
o))
    ([(Col N ZModHom, N)] -> [(Col N ZModHom, N)])
-> [(Col N ZModHom, N)] -> [(Col N ZModHom, N)]
forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ N -> [ZMod] -> [(Col N ZModHom, N)] -> [(Col N ZModHom, N)]
forall j i.
(Enum j, Ord j) =>
j -> [ZMod] -> [(Col i ZModHom, j)] -> [(Col i ZModHom, j)]
fcts N
o (((ZMod, N) -> ZMod) -> [(ZMod, N)] -> [ZMod]
forall a b. (a -> b) -> [a] -> [b]
map (ZMod, N) -> ZMod
forall a b. (a, b) -> a
fst ([(ZMod, N)] -> [ZMod]) -> [(ZMod, N)] -> [ZMod]
forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ Dim ZModHom ZMod -> [(ZMod, N)]
forall (s :: * -> *) x. Sequence s N x => s x -> [(x, N)]
listN Dim ZModHom ZMod
gp)
    ([(Col N ZModHom, N)] -> [(Col N ZModHom, N)])
-> [(Col N ZModHom, N)] -> [(Col N ZModHom, N)]
forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ Row N (Col N ZModHom) -> [(Col N ZModHom, N)]
forall (s :: * -> *) x. Sequence s N x => s x -> [(x, N)]
listN (Row N (Col N ZModHom) -> [(Col N ZModHom, N)])
-> Row N (Col N ZModHom) -> [(Col N ZModHom, N)]
forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ Entries N N ZModHom -> Row N (Col N ZModHom)
forall i j x. (Ord i, Ord j) => Entries i j x -> Row j (Col i x)
etsrc (Entries N N ZModHom -> Row N (Col N ZModHom))
-> Entries N N ZModHom -> Row N (Col N ZModHom)
forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ Matrix ZModHom -> Entries N N ZModHom
forall x. Matrix x -> Entries N N x
mtxxs (Matrix ZModHom
xMatrix ZModHom -> Matrix ZModHom -> Matrix ZModHom
forall c. Multiplicative c => c -> c -> c
*Matrix ZModHom
aInv')
    where
      
      fcts :: (Enum j, Ord j) => j -> [ZMod] -> [(Col i ZModHom,j)] -> [(Col i ZModHom,j)] 
      fcts :: forall j i.
(Enum j, Ord j) =>
j -> [ZMod] -> [(Col i ZModHom, j)] -> [(Col i ZModHom, j)]
fcts j
_ [] [(Col i ZModHom, j)]
cls = [(Col i ZModHom, j)]
cls
      fcts j
_ [ZMod]
_ []   = []
      fcts j
j (ZMod
z:[ZMod]
zs) cls :: [(Col i ZModHom, j)]
cls@((Col i ZModHom
cl,j
j'):[(Col i ZModHom, j)]
cls') = if j
j j -> j -> Bool
forall a. Ord a => a -> a -> Bool
< j
j'
        then j -> [ZMod] -> [(Col i ZModHom, j)] -> [(Col i ZModHom, j)]
forall j i.
(Enum j, Ord j) =>
j -> [ZMod] -> [(Col i ZModHom, j)] -> [(Col i ZModHom, j)]
fcts (j -> j
forall a. Enum a => a -> a
succ j
j) [ZMod]
zs [(Col i ZModHom, j)]
cls
        else (((ZModHom -> ZModHom) -> Col i ZModHom -> Col i ZModHom
forall a b. (a -> b) -> Col i a -> Col i b
forall (h :: * -> * -> *) (f :: * -> *) a b.
Applicative1 h f =>
h a b -> f a -> f b
amap1 (ZMod -> ZModHom -> ZModHom
fct ZMod
z) Col i ZModHom
cl,j
j')(Col i ZModHom, j) -> [(Col i ZModHom, j)] -> [(Col i ZModHom, j)]
forall a. a -> [a] -> [a]
:j -> [ZMod] -> [(Col i ZModHom, j)] -> [(Col i ZModHom, j)]
forall j i.
(Enum j, Ord j) =>
j -> [ZMod] -> [(Col i ZModHom, j)] -> [(Col i ZModHom, j)]
fcts (j -> j
forall a. Enum a => a -> a
succ j
j) [ZMod]
zs [(Col i ZModHom, j)]
cls')

      fct :: ZMod -> ZModHom -> ZModHom
      fct :: ZMod -> ZModHom -> ZModHom
fct ZMod
z ZModHom
h = Orientation ZMod -> Z -> ZModHom
zmh (ZMod
zZMod -> ZMod -> Orientation ZMod
forall p. p -> p -> Orientation p
:>ZModHom -> Point ZModHom
forall q. Oriented q => q -> Point q
end ZModHom
h) (ZModHom -> Z
toZ ZModHom
h)
      
--------------------------------------------------------------------------------
-- abhCokernelFreeTo -

-- | the cokernel of a free site to.
--
--  __Properties__ Let @s = 'SliceTo' _ h@ be in @'Slice' 'To' ('Free' __k__) 'AbHom'@ and
-- @coker = 'abhCokernelFreeTo' s@, then holds: 
--
-- (1) @'diagram' coker '==' 'cokernelDiagram' h@.
--
-- (2) @'tip' ('universalCone' coker)@ is smith normal (see t'AbGroup').
abhCokernelFreeTo :: Attestable k
  => Slice To (Free k) AbHom -> Cokernel N1 AbHom
abhCokernelFreeTo :: forall (k :: N').
Attestable k =>
Slice 'To (Free k) AbHom -> Cokernel N1 AbHom
abhCokernelFreeTo (SliceTo Free k AbHom
k AbHom
h) = Cone Dst 'Injective ('Parallel 'RightToLeft) N2 N1 AbHom
-> (Cone Dst 'Injective ('Parallel 'RightToLeft) N2 N1 AbHom
    -> AbHom)
-> Cokernel N1 AbHom
forall s (t :: DiagramType) (n :: N') (m :: N') a.
Cone s 'Injective t n m a
-> (Cone s 'Injective t n m a -> a) -> Limes s 'Injective t n m a
LimesInjective Cone Dst 'Injective ('Parallel 'RightToLeft) N2 N1 AbHom
hCoker Cone Dst 'Injective ('Parallel 'RightToLeft) N2 N1 AbHom -> AbHom
hUniv where

  h' :: AbHom
h' = AbHomFree (Matrix Z) AbHom -> Matrix Z -> AbHom
forall a b. AbHomFree a b -> a -> b
forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
amap AbHomFree (Matrix Z) AbHom
FreeAbHom (AbHomFree AbHom (Matrix Z) -> AbHom -> Matrix Z
forall a b. AbHomFree a b -> a -> b
forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
amap AbHomFree AbHom (Matrix Z)
AbHomFree AbHom
h)
  -- h' has free start and end
  -- as end h is free it follows that, end h == end h' and
  -- unitRight abhFreeAdjunction (end h) == one (end h) and hence
  -- h == h' * unitRight abhFreeAdjunction (start h)

  h'Dgm :: CokernelDiagramFree N1 AbHom
h'Dgm = case N -> SomeNatural
someNatural (AbGroup -> N
forall x. LengthN x => x -> N
lengthN (AbGroup -> N) -> AbGroup -> N
forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ AbHom -> Point AbHom
forall q. Oriented q => q -> Point q
start AbHom
h') of
    SomeNatural W n
k' -> FinList N2 (SomeFree AbHom)
-> Diagram ('Parallel 'RightToLeft) N2 N1 AbHom
-> CokernelDiagramFree N1 AbHom
forall (t :: DiagramType) (n :: N') (m :: N') a.
FinList n (SomeFree a) -> Diagram t n m a -> DiagramFree t n m a
DiagramFree FinList (N1 + 1) (SomeFree AbHom)
FinList N2 (SomeFree AbHom)
ks (AbHom -> Diagram ('Parallel 'RightToLeft) N2 N1 AbHom
forall c. Oriented c => c -> CokernelDiagram N1 c
cokernelDiagram AbHom
h') where
      ks :: FinList (N1 + 1) (SomeFree AbHom)
ks = Free k AbHom -> SomeFree AbHom
forall (k :: N') c.
(Attestable k, Sliced (Free k) c) =>
Free k c -> SomeFree c
SomeFree Free k AbHom
kSomeFree AbHom
-> FinList N1 (SomeFree AbHom) -> FinList (N1 + 1) (SomeFree AbHom)
forall a (n1 :: N'). a -> FinList n1 a -> FinList (n1 + 1) a
:|Free n AbHom -> SomeFree AbHom
forall (k :: N') c.
(Attestable k, Sliced (Free k) c) =>
Free k c -> SomeFree c
SomeFree (W n -> Free n AbHom
forall (k :: N') c. Any k -> Free k c
Free W n
k')SomeFree AbHom
-> FinList 'N0 (SomeFree AbHom)
-> FinList ('N0 + 1) (SomeFree AbHom)
forall a (n1 :: N'). a -> FinList n1 a -> FinList (n1 + 1) a
:|FinList 'N0 (SomeFree AbHom)
forall a. FinList 'N0 a
Nil

  h'Coker :: Cokernel N1 AbHom
h'Coker = CokernelDiagramFree N1 AbHom -> Cokernel N1 AbHom
abhCokernelFree CokernelDiagramFree N1 AbHom
h'Dgm
  
  -- as unitRight abhFreeAdjunction (start h) is an epimorphism it follows
  -- that h and h' have the same cokernelFactor!
  hCoker :: Cone Dst 'Injective ('Parallel 'RightToLeft) N2 N1 AbHom
hCoker = Diagram ('Parallel 'RightToLeft) N2 N1 AbHom
-> AbHom
-> Cone Dst 'Injective ('Parallel 'RightToLeft) N2 N1 AbHom
forall a (m :: N').
Distributive a =>
Diagram ('Parallel 'RightToLeft) N2 m a
-> a -> Cone Dst 'Injective ('Parallel 'RightToLeft) N2 m a
ConeCokernel (AbHom -> Diagram ('Parallel 'RightToLeft) N2 N1 AbHom
forall c. Oriented c => c -> CokernelDiagram N1 c
cokernelDiagram AbHom
h) (Cone Dst 'Injective ('Parallel 'RightToLeft) N2 N1 AbHom -> AbHom
forall c. CokernelCone N1 c -> c
cokernelFactor (Cone Dst 'Injective ('Parallel 'RightToLeft) N2 N1 AbHom -> AbHom)
-> Cone Dst 'Injective ('Parallel 'RightToLeft) N2 N1 AbHom
-> AbHom
forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ Cokernel N1 AbHom
-> Cone Dst 'Injective ('Parallel 'RightToLeft) N2 N1 AbHom
forall s (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N')
       a.
Limes s p t n m a -> Cone s p t n m a
universalCone Cokernel N1 AbHom
h'Coker)

  hUniv :: Cone Dst 'Injective ('Parallel 'RightToLeft) N2 N1 AbHom -> AbHom
hUniv (ConeCokernel Diagram ('Parallel 'RightToLeft) N2 N1 AbHom
_ AbHom
x) = Cokernel N1 AbHom
-> Cone Dst 'Injective ('Parallel 'RightToLeft) N2 N1 AbHom
-> AbHom
forall s (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N')
       a.
Limes s p t n m a -> Cone s p t n m a -> a
universalFactor Cokernel N1 AbHom
h'Coker (Diagram ('Parallel 'RightToLeft) N2 N1 AbHom
-> AbHom
-> Cone Dst 'Injective ('Parallel 'RightToLeft) N2 N1 AbHom
forall a (m :: N').
Distributive a =>
Diagram ('Parallel 'RightToLeft) N2 m a
-> a -> Cone Dst 'Injective ('Parallel 'RightToLeft) N2 m a
ConeCokernel (Cokernel N1 AbHom -> Diagram ('Parallel 'RightToLeft) N2 N1 AbHom
forall s (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N')
       a.
Limes s p t n m a -> Diagram t n m a
diagram Cokernel N1 AbHom
h'Coker) AbHom
x)

--------------------------------------------------------------------------------
-- abhPullbackFree -

-- | the pullback with a free tip of its universal cone for the given free pullback diagram.
--
--  __Property__ Let @d = 'DiagramFree' _ d'@ be in @'PullbackDiagramFree' __n__ 'AbHom'@,
--  then holds: @'diagram' ('limesFree' p) = d'@ where @p = 'abhPullbackFree' d@.
abhPullbackFree :: PullbackDiagramFree n AbHom -> PullbackFree n AbHom
abhPullbackFree :: forall (n :: N').
PullbackDiagramFree n AbHom -> PullbackFree n AbHom
abhPullbackFree (DiagramFree FinList (n + 1) (SomeFree AbHom)
_ Diagram ('Star 'To) (n + 1) n AbHom
d') = case Pullback n AbHom -> SomeFree AbHom
forall (n :: N'). Pullback n AbHom -> SomeFree AbHom
freeTip Pullback n AbHom
Limes Mlt 'Projective ('Star 'To) ('S n) n AbHom
p of
  SomeFree Free k AbHom
k -> Free k AbHom
-> Limes Mlt 'Projective ('Star 'To) ('S n) n AbHom
-> LimesFree Mlt 'Projective ('Star 'To) ('S n) n AbHom
forall (k :: N') a s (p :: Perspective) (t :: DiagramType)
       (n :: N') (m :: N').
(Attestable k, Sliced (Free k) a) =>
Free k a -> Limes s p t n m a -> LimesFree s p t n m a
LimesFree Free k AbHom
k Limes Mlt 'Projective ('Star 'To) ('S n) n AbHom
p
  where
    -- if d = DiagramFree _ d' is valid, then the r (l d') == d' for the right
    -- and left adjoint of abhFreeAdjunction. Furthermore the tip of p is free!
    freeTip :: Pullback n AbHom -> SomeFree AbHom
    freeTip :: forall (n :: N'). Pullback n AbHom -> SomeFree AbHom
freeTip Pullback n AbHom
p = case N -> SomeNatural
someNatural N
n of
      SomeNatural W n
n' -> Free n AbHom -> SomeFree AbHom
forall (k :: N') c.
(Attestable k, Sliced (Free k) c) =>
Free k c -> SomeFree c
SomeFree (W n -> Free n AbHom
forall (k :: N') c. Any k -> Free k c
Free W n
n')
      where n :: N
n = Point AbHom -> N
forall x. LengthN x => x -> N
lengthN (Point AbHom -> N) -> Point AbHom -> N
forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ Cone Mlt 'Projective ('Star 'To) ('S n) n AbHom -> Point AbHom
forall s (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N')
       a.
Cone s p t n m a -> Point a
tip (Cone Mlt 'Projective ('Star 'To) ('S n) n AbHom -> Point AbHom)
-> Cone Mlt 'Projective ('Star 'To) ('S n) n AbHom -> Point AbHom
forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ Limes Mlt 'Projective ('Star 'To) ('S n) n AbHom
-> Cone Mlt 'Projective ('Star 'To) ('S n) n AbHom
forall s (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N')
       a.
Limes s p t n m a -> Cone s p t n m a
universalCone Pullback n AbHom
Limes Mlt 'Projective ('Star 'To) ('S n) n AbHom
p

    p :: Limes Mlt 'Projective ('Star 'To) ('S n) n AbHom
p = Adjunction AbHomFree (Matrix Z) AbHom
-> Limes Mlt 'Projective ('Star 'To) ('S n) n (Matrix Z)
-> Limes Mlt 'Projective ('Star 'To) ('S n) n AbHom
forall (h :: * -> * -> *) d c (t :: DiagramType) (n :: N')
       (m :: N').
Hom Mlt h =>
Adjunction h d c
-> Limes Mlt 'Projective t n m d -> Limes Mlt 'Projective t n m c
lmPrjMap Adjunction AbHomFree (Matrix Z) AbHom
adj (Limes Mlt 'Projective ('Star 'To) ('S n) n (Matrix Z)
 -> Limes Mlt 'Projective ('Star 'To) ('S n) n AbHom)
-> Limes Mlt 'Projective ('Star 'To) ('S n) n (Matrix Z)
-> Limes Mlt 'Projective ('Star 'To) ('S n) n AbHom
forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ Limits Mlt 'Projective ('Star 'To) ('S n) n (Matrix Z)
-> Diagram ('Star 'To) ('S n) n (Matrix Z)
-> Limes Mlt 'Projective ('Star 'To) ('S n) n (Matrix Z)
forall s (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N')
       a.
Limits s p t n m a -> Diagram t n m a -> Limes s p t n m a
limes Pullbacks n (Matrix Z)
Limits Mlt 'Projective ('Star 'To) ('S n) n (Matrix Z)
forall (n :: N'). Pullbacks n (Matrix Z)
zmxPullbacks (Diagram ('Star 'To) ('S n) n (Matrix Z)
 -> Limes Mlt 'Projective ('Star 'To) ('S n) n (Matrix Z))
-> Diagram ('Star 'To) ('S n) n (Matrix Z)
-> Limes Mlt 'Projective ('Star 'To) ('S n) n (Matrix Z)
forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ AbHomFree AbHom (Matrix Z)
-> Diagram ('Star 'To) ('S n) n AbHom
-> Diagram ('Star 'To) ('S n) n (Matrix Z)
forall (h :: * -> * -> *) a b (t :: DiagramType) (n :: N')
       (m :: N').
Hom Ort h =>
h a b -> Diagram t n m a -> Diagram t n m b
dgMap AbHomFree AbHom (Matrix Z)
l Diagram ('Star 'To) (n + 1) n AbHom
Diagram ('Star 'To) ('S n) n AbHom
d' where
      adj :: Adjunction AbHomFree (Matrix Z) AbHom
adj = Adjunction AbHomFree (Matrix Z) AbHom
abhFreeAdjunction
      Adjunction AbHomFree AbHom (Matrix Z)
l AbHomFree (Matrix Z) AbHom
_ Point AbHom -> AbHom
_ Point (Matrix Z) -> Matrix Z
_ = Adjunction AbHomFree (Matrix Z) AbHom
adj

someFree :: N -> SomeFree AbHom
someFree :: N -> SomeFree AbHom
someFree N
n = case N -> SomeNatural
someNatural N
n of
  SomeNatural W n
n' -> Free n AbHom -> SomeFree AbHom
forall (k :: N') c.
(Attestable k, Sliced (Free k) c) =>
Free k c -> SomeFree c
SomeFree (W n -> Free n AbHom
forall (k :: N') c. Any k -> Free k c
Free W n
n')

plbDgmFree :: PullbackDiagram n (Matrix Z) -> PullbackDiagramFree n AbHom
plbDgmFree :: forall (n :: N').
PullbackDiagram n (Matrix Z) -> PullbackDiagramFree n AbHom
plbDgmFree PullbackDiagram n (Matrix Z)
d = FinList ('S n) (SomeFree AbHom)
-> Diagram ('Star 'To) ('S n) n AbHom
-> DiagramFree ('Star 'To) ('S n) n AbHom
forall (t :: DiagramType) (n :: N') (m :: N') a.
FinList n (SomeFree a) -> Diagram t n m a -> DiagramFree t n m a
DiagramFree ((Dim Z () -> SomeFree AbHom)
-> FinList ('S n) (Dim Z ()) -> FinList ('S n) (SomeFree AbHom)
forall a b. (a -> b) -> FinList ('S n) a -> FinList ('S n) b
forall (h :: * -> * -> *) (f :: * -> *) a b.
Applicative1 h f =>
h a b -> f a -> f b
amap1 (N -> SomeFree AbHom
someFree (N -> SomeFree AbHom)
-> (Dim Z () -> N) -> Dim Z () -> SomeFree AbHom
forall y z x. (y -> z) -> (x -> y) -> x -> z
forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. Dim Z () -> N
forall x. LengthN x => x -> N
lengthN) (FinList ('S n) (Dim Z ()) -> FinList ('S n) (SomeFree AbHom))
-> FinList ('S n) (Dim Z ()) -> FinList ('S n) (SomeFree AbHom)
forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ Diagram ('Star 'To) ('S n) n (Matrix Z)
-> FinList ('S n) (Point (Matrix Z))
forall a (t :: DiagramType) (n :: N') (m :: N').
Oriented a =>
Diagram t n m a -> FinList n (Point a)
dgPoints PullbackDiagram n (Matrix Z)
Diagram ('Star 'To) ('S n) n (Matrix Z)
d) (AbHomFree (Matrix Z) AbHom
-> Diagram ('Star 'To) ('S n) n (Matrix Z)
-> Diagram ('Star 'To) ('S n) n AbHom
forall (h :: * -> * -> *) a b (t :: DiagramType) (n :: N')
       (m :: N').
Hom Ort h =>
h a b -> Diagram t n m a -> Diagram t n m b
dgMap AbHomFree (Matrix Z) AbHom
FreeAbHom PullbackDiagram n (Matrix Z)
Diagram ('Star 'To) ('S n) n (Matrix Z)
d)

pp1 :: Statement
pp1 :: Statement
pp1 = X (DiagramFree ('Star 'To) ('S ('S N2)) ('S N2) AbHom)
-> (DiagramFree ('Star 'To) ('S ('S N2)) ('S N2) AbHom
    -> Statement)
-> Statement
forall x. X x -> (x -> Statement) -> Statement
Forall X (DiagramFree ('Star 'To) ('S ('S N2)) ('S N2) AbHom)
xd (Limes Mlt 'Projective ('Star 'To) ('S ('S N2)) ('S N2) AbHom
-> Statement
forall a. Validable a => a -> Statement
valid (Limes Mlt 'Projective ('Star 'To) ('S ('S N2)) ('S N2) AbHom
 -> Statement)
-> (DiagramFree ('Star 'To) ('S ('S N2)) ('S N2) AbHom
    -> Limes Mlt 'Projective ('Star 'To) ('S ('S N2)) ('S N2) AbHom)
-> DiagramFree ('Star 'To) ('S ('S N2)) ('S N2) AbHom
-> Statement
forall y z x. (y -> z) -> (x -> y) -> x -> z
forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. LimesFree Mlt 'Projective ('Star 'To) ('S ('S N2)) ('S N2) AbHom
-> Limes Mlt 'Projective ('Star 'To) ('S ('S N2)) ('S N2) AbHom
forall s (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N')
       a.
LimesFree s p t n m a -> Limes s p t n m a
limesFree (LimesFree Mlt 'Projective ('Star 'To) ('S ('S N2)) ('S N2) AbHom
 -> Limes Mlt 'Projective ('Star 'To) ('S ('S N2)) ('S N2) AbHom)
-> (DiagramFree ('Star 'To) ('S ('S N2)) ('S N2) AbHom
    -> LimesFree
         Mlt 'Projective ('Star 'To) ('S ('S N2)) ('S N2) AbHom)
-> DiagramFree ('Star 'To) ('S ('S N2)) ('S N2) AbHom
-> Limes Mlt 'Projective ('Star 'To) ('S ('S N2)) ('S N2) AbHom
forall y z x. (y -> z) -> (x -> y) -> x -> z
forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. PullbackDiagramFree ('S N2) AbHom -> PullbackFree ('S N2) AbHom
DiagramFree ('Star 'To) ('S ('S N2)) ('S N2) AbHom
-> LimesFree Mlt 'Projective ('Star 'To) ('S ('S N2)) ('S N2) AbHom
forall (n :: N').
PullbackDiagramFree n AbHom -> PullbackFree n AbHom
abhPullbackFree) where
  xd :: X (DiagramFree ('Star 'To) ('S ('S N2)) ('S N2) AbHom)
xd = (Diagram ('Star 'To) ('S ('S N2)) ('S N2) (Matrix Z)
 -> DiagramFree ('Star 'To) ('S ('S N2)) ('S N2) AbHom)
-> X (Diagram ('Star 'To) ('S ('S N2)) ('S N2) (Matrix Z))
-> X (DiagramFree ('Star 'To) ('S ('S N2)) ('S N2) AbHom)
forall a b. (a -> b) -> X a -> X b
forall (h :: * -> * -> *) (f :: * -> *) a b.
Applicative1 h f =>
h a b -> f a -> f b
amap1 PullbackDiagram ('S N2) (Matrix Z)
-> PullbackDiagramFree ('S N2) AbHom
Diagram ('Star 'To) ('S ('S N2)) ('S N2) (Matrix Z)
-> DiagramFree ('Star 'To) ('S ('S N2)) ('S N2) AbHom
forall (n :: N').
PullbackDiagram n (Matrix Z) -> PullbackDiagramFree n AbHom
plbDgmFree (X (PullbackDiagram ('S N2) (Matrix Z))
X (Diagram ('Star 'To) ('S ('S N2)) ('S N2) (Matrix Z))
forall x. XStandard x => X x
xStandard :: X (PullbackDiagram N3 (Matrix Z)))
  
--------------------------------------------------------------------------------
-- abhSplitCy -

-- | splits an abelian homomorphism @h@ into a list @hs@ where each
-- @h'@ in @hs@ has as start point equal to the start point of @h@ and end point a
-- cyclic group to the power of some order such that all  @h'@ /cover/ @h@.
--
-- __Properties__ Let @h@ be in 'AbHom' and @hs = 'abhSplitCy', then holds:
--
-- (1) For all @h'@ in @hs@ holds: @'orientation' h' '==' 'start' h ':>' 'abg' n '^' r@
-- for some @n@, @r@ in 'N'.
--
-- (2) For all @x@ in 'AbHom' with @'end' x '==' 'start' h@ holds: @h v'*' x '==' 0@
-- if and only if @h' v'*' x '==' 0@ for all @h'@ in @hs@.
abhSplitCy :: AbHom -> [AbHom]
abhSplitCy :: AbHom -> [AbHom]
abhSplitCy (AbHom m :: Matrix ZModHom
m@(Matrix Dim ZModHom (Point ZModHom)
r Dim ZModHom (Point ZModHom)
_ Entries N N ZModHom
_))
  = ((Matrix ZModHom, N, N) -> AbHom)
-> [(Matrix ZModHom, N, N)] -> [AbHom]
forall a b. (a -> b) -> [a] -> [b]
forall (h :: * -> * -> *) (f :: * -> *) a b.
Applicative1 h f =>
h a b -> f a -> f b
amap1 (\(Matrix ZModHom
m',N
_,N
_) -> Matrix ZModHom -> AbHom
AbHom Matrix ZModHom
m')
  ([(Matrix ZModHom, N, N)] -> [AbHom])
-> [(Matrix ZModHom, N, N)] -> [AbHom]
forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ Entries N N (Matrix ZModHom) -> [(Matrix ZModHom, N, N)]
forall i j x. Entries i j x -> [(x, i, j)]
etsxs
  (Entries N N (Matrix ZModHom) -> [(Matrix ZModHom, N, N)])
-> Entries N N (Matrix ZModHom) -> [(Matrix ZModHom, N, N)]
forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ Matrix (Matrix ZModHom) -> Entries N N (Matrix ZModHom)
forall x. Matrix x -> Entries N N x
mtxxs
  (Matrix (Matrix ZModHom) -> Entries N N (Matrix ZModHom))
-> Matrix (Matrix ZModHom) -> Entries N N (Matrix ZModHom)
forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ Matrix ZModHom -> Matrix (Matrix ZModHom)
forall x. Distributive x => Matrix x -> Matrix (Matrix x)
mtxGroupRow
  (Matrix ZModHom -> Matrix (Matrix ZModHom))
-> Matrix ZModHom -> Matrix (Matrix ZModHom)
forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ (GLT ZModHom -> RowTrafo ZModHom
forall a. GLT a -> RowTrafo a
RowTrafo (Dim ZModHom (Point ZModHom)
-> Dim ZModHom (Point ZModHom) -> Permutation N -> GLT ZModHom
forall x.
Distributive x =>
Dim' x -> Dim' x -> Permutation N -> GLT x
permute Dim ZModHom (Point ZModHom)
Dim ZModHom ZMod
r' Dim ZModHom (Point ZModHom)
r Permutation N
p) RowTrafo ZModHom -> Matrix ZModHom -> Matrix ZModHom
forall f x. Opl f x => f -> x -> x
*> Matrix ZModHom
m)
  where (Dim ZModHom ZMod
r',Permutation N
p) = Proxy N
-> (ZMod -> ZMod -> Ordering)
-> (ZMod -> ZMod)
-> Dim ZModHom ZMod
-> (Dim ZModHom ZMod, Permutation N)
forall (p :: * -> *) w.
p N
-> (w -> w -> Ordering)
-> (ZMod -> w)
-> Dim ZModHom ZMod
-> (Dim ZModHom ZMod, Permutation N)
forall (s :: * -> *) i x (p :: * -> *) w.
PermutableSequence s i x =>
p i
-> (w -> w -> Ordering) -> (x -> w) -> s x -> (s x, Permutation i)
permuteBy Proxy N
nProxy ZMod -> ZMod -> Ordering
forall a. Ord a => a -> a -> Ordering
compare ZMod -> ZMod
forall x. x -> x
id Dim ZModHom (Point ZModHom)
Dim ZModHom ZMod
r
  
--------------------------------------------------------------------------------
-- abhFreeFromSplitCy -

-- | splits an abelian homomorphism @h@ into some finite list @hs@ where each
--  @h'@ in @hs@ has as end point a cyclic group to the power of some order such that all
--  @h'@ /cover/ @h@.
--
-- __Properties__ Let @s = 'SliceFrom' _ h@ be in @'Slice' 'From' ('Free' __k__) 'AbHom'@
-- and @hs = 'abhFreeFromSplitCy' s@, then holds:
--
-- (1) For all @'SliceFrom' _ h'@ in @hs@ exists a @n@, @r@ in 'N' such that
-- @'end' h' '==' 'abg' n '^' r@.
--
-- (2) For all @x@ in 'AbHom' with @'end' x '==' 'start' h@ holds: @h v'*' x '==' 0@ if
-- and only if @h' v'*' x '==' 0@ for all @'SliceFrom' _ h'@ in @hs@.
abhFreeFromSplitCy :: Slice From (Free k) AbHom -> SomeFinList (Slice From (Free k) AbHom)
abhFreeFromSplitCy :: forall (k :: N').
Slice 'From (Free k) AbHom
-> SomeFinList (Slice 'From (Free k) AbHom)
abhFreeFromSplitCy (SliceFrom Free k AbHom
k AbHom
h)
  = [Slice 'From (Free k) AbHom]
-> SomeFinList (Slice 'From (Free k) AbHom)
forall a. [a] -> SomeFinList a
someFinList ([Slice 'From (Free k) AbHom]
 -> SomeFinList (Slice 'From (Free k) AbHom))
-> [Slice 'From (Free k) AbHom]
-> SomeFinList (Slice 'From (Free k) AbHom)
forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ (AbHom -> Slice 'From (Free k) AbHom)
-> [AbHom] -> [Slice 'From (Free k) AbHom]
forall a b. (a -> b) -> [a] -> [b]
forall (h :: * -> * -> *) (f :: * -> *) a b.
Applicative1 h f =>
h a b -> f a -> f b
amap1 (Free k AbHom -> AbHom -> Slice 'From (Free k) AbHom
forall (i :: * -> *) c. i c -> c -> Slice 'From i c
SliceFrom Free k AbHom
k) ([AbHom] -> [Slice 'From (Free k) AbHom])
-> [AbHom] -> [Slice 'From (Free k) AbHom]
forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ AbHom -> [AbHom]
abhSplitCy AbHom
h 

--------------------------------------------------------------------------------
-- abhKernelFreeFromCy -

xFreeFromCy :: Free k AbHom -> X (Slice From (Free k) AbHom)
xFreeFromCy :: forall (k :: N'). Free k AbHom -> X (Slice 'From (Free k) AbHom)
xFreeFromCy k :: Free k AbHom
k@(Free Any k
k') = do
  N
n <- N -> N -> X N
xNB N
0 N
1000
  N
r <- N -> N -> X N
xNB N
0 N
10
  AbHom
h <- Q -> Orientation AbGroup -> X AbHom
xAbHom Q
0.3 (N -> AbGroup
abg N
0 AbGroup -> Exponent AbGroup -> AbGroup
forall f. Exponential f => f -> Exponent f -> f
^ (Any k -> N
forall x. LengthN x => x -> N
lengthN Any k
k') AbGroup -> AbGroup -> Orientation AbGroup
forall p. p -> p -> Orientation p
:> N -> AbGroup
abg N
n AbGroup -> Exponent AbGroup -> AbGroup
forall f. Exponential f => f -> Exponent f -> f
^ N
Exponent AbGroup
r)
  Slice 'From (Free k) AbHom -> X (Slice 'From (Free k) AbHom)
forall a. a -> X a
forall (m :: * -> *) a. Monad m => a -> m a
return (Free k AbHom -> AbHom -> Slice 'From (Free k) AbHom
forall (i :: * -> *) c. i c -> c -> Slice 'From i c
SliceFrom Free k AbHom
k AbHom
h)

pp2 :: Attestable k => Free k AbHom -> Statement
pp2 :: forall (k :: N'). Attestable k => Free k AbHom -> Statement
pp2 Free k AbHom
k = X (Slice 'From (Free k) AbHom)
-> (Slice 'From (Free k) AbHom -> Statement) -> Statement
forall x. X x -> (x -> Statement) -> Statement
Forall X (Slice 'From (Free k) AbHom)
xs (KernelFree N1 AbHom -> Statement
forall a. Validable a => a -> Statement
valid (KernelFree N1 AbHom -> Statement)
-> (Slice 'From (Free k) AbHom -> KernelFree N1 AbHom)
-> Slice 'From (Free k) AbHom
-> Statement
forall y z x. (y -> z) -> (x -> y) -> x -> z
forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. Slice 'From (Free k) AbHom -> KernelFree N1 AbHom
forall (k :: N').
Attestable k =>
Slice 'From (Free k) AbHom -> KernelFree N1 AbHom
abhKernelFreeFromCy) where
  xs :: X (Slice 'From (Free k) AbHom)
xs = Free k AbHom -> X (Slice 'From (Free k) AbHom)
forall (k :: N'). Free k AbHom -> X (Slice 'From (Free k) AbHom)
xFreeFromCy Free k AbHom
k
  
-- | free kernel where the end point is equal to some cyclic group to some order.
--
-- __Property__ Let @s = 'SliceFrom' _ h@ where @'end' h '==' abg n '^' r@ for some
-- @n@, @r@ in 'N', then holds:
-- @'diagram' ('limesFree' ker) '==' 'kernelDiagram' h@ where @ker = 'abhKernelFreeFromCy' s@.
abhKernelFreeFromCy :: Attestable k => Slice From (Free k) AbHom -> KernelFree N1 AbHom
abhKernelFreeFromCy :: forall (k :: N').
Attestable k =>
Slice 'From (Free k) AbHom -> KernelFree N1 AbHom
abhKernelFreeFromCy s :: Slice 'From (Free k) AbHom
s@(SliceFrom Free k AbHom
k AbHom
h) = [(ZMod, N)] -> KernelFree N1 AbHom
hKer ([(ZMod, N)] -> KernelFree N1 AbHom)
-> [(ZMod, N)] -> KernelFree N1 AbHom
forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ Word N ZMod -> [(ZMod, N)]
forall r a. Word r a -> [(a, r)]
fromWord (Word N ZMod -> [(ZMod, N)]) -> Word N ZMod -> [(ZMod, N)]
forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ Dim ZModHom (Point ZModHom) -> Word N (Point ZModHom)
Dim ZModHom ZMod -> Word N ZMod
forall p x. (Entity p, p ~ Point x) => Dim x p -> Word N p
dimwrd (Dim ZModHom ZMod -> Word N ZMod)
-> Dim ZModHom ZMod -> Word N ZMod
forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ AbGroup -> Dim ZModHom (Point ZModHom)
AbGroup -> Dim ZModHom ZMod
abgDim (AbGroup -> Dim ZModHom ZMod) -> AbGroup -> Dim ZModHom ZMod
forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ AbHom -> Point AbHom
forall q. Oriented q => q -> Point q
end AbHom
h where

  freeTip :: Kernel N1 AbHom -> SomeFree AbHom
  freeTip :: Kernel N1 AbHom -> SomeFree AbHom
freeTip Kernel N1 AbHom
k = case N -> SomeNatural
someNatural N
n of
    SomeNatural W n
n' -> Free n AbHom -> SomeFree AbHom
forall (k :: N') c.
(Attestable k, Sliced (Free k) c) =>
Free k c -> SomeFree c
SomeFree (W n -> Free n AbHom
forall (k :: N') c. Any k -> Free k c
Free W n
n')
    where n :: N
n = Point AbHom -> N
forall x. LengthN x => x -> N
lengthN (Point AbHom -> N) -> Point AbHom -> N
forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ Cone Dst 'Projective ('Parallel 'LeftToRight) N2 N1 AbHom
-> Point AbHom
forall s (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N')
       a.
Cone s p t n m a -> Point a
tip (Cone Dst 'Projective ('Parallel 'LeftToRight) N2 N1 AbHom
 -> Point AbHom)
-> Cone Dst 'Projective ('Parallel 'LeftToRight) N2 N1 AbHom
-> Point AbHom
forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ Kernel N1 AbHom
-> Cone Dst 'Projective ('Parallel 'LeftToRight) N2 N1 AbHom
forall s (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N')
       a.
Limes s p t n m a -> Cone s p t n m a
universalCone Kernel N1 AbHom
k

  hKer :: [(ZMod, N)] -> KernelFree N1 AbHom
hKer [] = Free k AbHom -> Kernel N1 AbHom -> KernelFree N1 AbHom
forall (k :: N') a s (p :: Perspective) (t :: DiagramType)
       (n :: N') (m :: N').
(Attestable k, Sliced (Free k) a) =>
Free k a -> Limes s p t n m a -> LimesFree s p t n m a
LimesFree Free k AbHom
k (Slice 'From (Free k) AbHom
-> Orientation (Point AbHom) -> Kernel N1 AbHom
forall c (p :: * -> *).
Distributive c =>
p c -> Orientation (Point c) -> Kernel N1 c
kernelZero Slice 'From (Free k) AbHom
s (AbHom -> Orientation (Point AbHom)
forall q. Oriented q => q -> Orientation (Point q)
orientation AbHom
h))
  -- h == 0

  hKer [(ZMod N
0,N
_)] = case Kernel N1 AbHom -> SomeFree AbHom
freeTip Kernel N1 AbHom
ker of
    SomeFree Free k AbHom
k' -> Free k AbHom -> Kernel N1 AbHom -> KernelFree N1 AbHom
forall (k :: N') a s (p :: Perspective) (t :: DiagramType)
       (n :: N') (m :: N').
(Attestable k, Sliced (Free k) a) =>
Free k a -> Limes s p t n m a -> LimesFree s p t n m a
LimesFree Free k AbHom
k' Kernel N1 AbHom
ker
    where ker :: Kernel N1 AbHom
ker = Adjunction AbHomFree (Matrix Z) AbHom
-> Limes Dst 'Projective ('Parallel 'LeftToRight) N2 N1 (Matrix Z)
-> Kernel N1 AbHom
forall (h :: * -> * -> *) d c (t :: DiagramType) (n :: N')
       (m :: N').
Hom Dst h =>
Adjunction h d c
-> Limes Dst 'Projective t n m d -> Limes Dst 'Projective t n m c
lmPrjMapDst Adjunction AbHomFree (Matrix Z) AbHom
adj (Limes Dst 'Projective ('Parallel 'LeftToRight) N2 N1 (Matrix Z)
 -> Kernel N1 AbHom)
-> Limes Dst 'Projective ('Parallel 'LeftToRight) N2 N1 (Matrix Z)
-> Kernel N1 AbHom
forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ Limits Dst 'Projective ('Parallel 'LeftToRight) N2 N1 (Matrix Z)
-> Diagram ('Parallel 'LeftToRight) N2 N1 (Matrix Z)
-> Limes Dst 'Projective ('Parallel 'LeftToRight) N2 N1 (Matrix Z)
forall s (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N')
       a.
Limits s p t n m a -> Diagram t n m a -> Limes s p t n m a
limes Limits Dst 'Projective ('Parallel 'LeftToRight) N2 N1 (Matrix Z)
forall (n :: N'). Kernels n (Matrix Z)
zmxKernels (Diagram ('Parallel 'LeftToRight) N2 N1 (Matrix Z)
 -> Limes Dst 'Projective ('Parallel 'LeftToRight) N2 N1 (Matrix Z))
-> Diagram ('Parallel 'LeftToRight) N2 N1 (Matrix Z)
-> Limes Dst 'Projective ('Parallel 'LeftToRight) N2 N1 (Matrix Z)
forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ AbHomFree AbHom (Matrix Z)
-> Diagram ('Parallel 'LeftToRight) N2 N1 AbHom
-> Diagram ('Parallel 'LeftToRight) N2 N1 (Matrix Z)
forall (h :: * -> * -> *) a b (t :: DiagramType) (n :: N')
       (m :: N').
Hom Ort h =>
h a b -> Diagram t n m a -> Diagram t n m b
dgMap AbHomFree AbHom (Matrix Z)
l (AbHom -> Diagram ('Parallel 'LeftToRight) N2 N1 AbHom
forall c. Oriented c => c -> KernelDiagram N1 c
kernelDiagram AbHom
h)
          adj :: Adjunction AbHomFree (Matrix Z) AbHom
adj = Adjunction AbHomFree (Matrix Z) AbHom
abhFreeAdjunction
          Adjunction AbHomFree AbHom (Matrix Z)
l AbHomFree (Matrix Z) AbHom
_ Point AbHom -> AbHom
_ Point (Matrix Z) -> Matrix Z
_ = Adjunction AbHomFree (Matrix Z) AbHom
adj

  hKer [(ZMod N
1,N
_)] = [(ZMod, N)] -> KernelFree N1 AbHom
hKer []

  hKer [(ZMod N
c,N
_)] = case Kernel N1 AbHom -> SomeFree AbHom
freeTip Kernel N1 AbHom
ker of
    SomeFree Free k AbHom
k' -> Free k AbHom -> Kernel N1 AbHom -> KernelFree N1 AbHom
forall (k :: N') a s (p :: Perspective) (t :: DiagramType)
       (n :: N') (m :: N').
(Attestable k, Sliced (Free k) a) =>
Free k a -> Limes s p t n m a -> LimesFree s p t n m a
LimesFree Free k AbHom
k' Kernel N1 AbHom
ker
    where
      ker :: Kernel N1 AbHom
ker = Cone Dst 'Projective ('Parallel 'LeftToRight) N2 N1 AbHom
-> (Cone Dst 'Projective ('Parallel 'LeftToRight) N2 N1 AbHom
    -> AbHom)
-> Kernel N1 AbHom
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 AbHom
kCone Cone Dst 'Projective ('Parallel 'LeftToRight) N2 N1 AbHom -> AbHom
kUniv

      DiagonalForm [Z]
d RowTrafo Z
_ (ColTrafo GLT Z
t) = Matrix Z -> DiagonalForm Z
zmxDiagonalForm (AbHom -> Matrix Z
abhz AbHom
h)
      -- d = (rt*>h)<*ct
    
      m :: N
m = AbGroup -> N
forall x. LengthN x => x -> N
lengthN (AbHom -> Point AbHom
forall q. Oriented q => q -> Point q
start AbHom
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

      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

      dm :: Dim Z ()
dm = () -> 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 ())
m
      kDgm :: Diagram ('Parallel 'LeftToRight) N2 N1 AbHom
kDgm = Point AbHom
-> Point AbHom
-> FinList N1 AbHom
-> Diagram ('Parallel 'LeftToRight) N2 N1 AbHom
forall a (m :: N').
Point a
-> Point a
-> FinList m a
-> Diagram ('Parallel 'LeftToRight) N2 m a
DiagramParallelLR (AbHom -> Point AbHom
forall q. Oriented q => q -> Point q
start AbHom
h) (AbHom -> Point AbHom
forall q. Oriented q => q -> Point q
end AbHom
h) (AbHom
hAbHom -> FinList 'N0 AbHom -> FinList ('N0 + 1) AbHom
forall a (n1 :: N'). a -> FinList n1 a -> FinList (n1 + 1) a
:|FinList 'N0 AbHom
forall a. FinList 'N0 a
Nil)
  
      k :: [Z]
k = (Z -> Z) -> [Z] -> [Z]
forall a b. (a -> b) -> [a] -> [b]
map Z -> Z
f [Z]
d [Z] -> [Z] -> [Z]
forall a. [a] -> [a] -> [a]
++ N -> [Z] -> [Z]
forall a. N -> [a] -> [a]
takeN N
r (Z -> [Z]
forall a. a -> [a]
repeat Z
1)
      -- 0 < d
      f :: Z -> Z
f Z
d = if N
d' N -> N -> Bool
forall a. Eq a => a -> a -> Bool
== N
0 then Z
1 else N -> Z
forall a b. Embeddable a b => a -> b
inj (N -> N -> N
lcm N
d' N
c) Z -> N -> Z
// N
d' where d' :: N
d' = Z -> N
forall a b. Projectible a b => b -> a
prj (Z -> N -> Z
mod0 Z
d N
c)

      kLim :: AbHom
kLim = Matrix Z -> AbHom
zabh (Matrix Z
bMatrix Z -> Matrix Z -> Matrix Z
forall c. Multiplicative c => c -> c -> c
*Dim' Z -> Dim' Z -> [Z] -> Matrix Z
forall x. Additive x => Dim' x -> Dim' x -> [x] -> Matrix x
diagonal Dim Z ()
Dim' Z
dm Dim Z ()
Dim' Z
dm [Z]
k)
      kCone :: Cone Dst 'Projective ('Parallel 'LeftToRight) N2 N1 AbHom
kCone = Diagram ('Parallel 'LeftToRight) N2 N1 AbHom
-> AbHom
-> Cone Dst 'Projective ('Parallel 'LeftToRight) N2 N1 AbHom
forall a (m :: N').
Distributive a =>
Diagram ('Parallel 'LeftToRight) N2 m a
-> a -> Cone Dst 'Projective ('Parallel 'LeftToRight) N2 m a
ConeKernel Diagram ('Parallel 'LeftToRight) N2 N1 AbHom
kDgm AbHom
kLim

      kUniv :: Cone Dst 'Projective ('Parallel 'LeftToRight) N2 N1 AbHom -> AbHom
kUniv cn :: Cone Dst 'Projective ('Parallel 'LeftToRight) N2 N1 AbHom
cn@(ConeKernel Diagram ('Parallel 'LeftToRight) N2 N1 AbHom
_ AbHom
x) = Matrix ZModHom -> AbHom
AbHom (Matrix ZModHom -> AbHom) -> Matrix ZModHom -> AbHom
forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ Dim ZModHom (Point ZModHom)
-> Dim ZModHom (Point ZModHom)
-> Entries N N ZModHom
-> Matrix ZModHom
forall x. Dim' x -> Dim' x -> Entries N N x -> Matrix x
Matrix (CSequence (Point ZModHom) -> Dim ZModHom (Point ZModHom)
forall x. CSequence (Point x) -> Dim x (Point x)
Dim CSequence (Point ZModHom)
ProductSymbol ZMod
e) (CSequence (Point ZModHom) -> Dim ZModHom (Point ZModHom)
forall x. CSequence (Point x) -> Dim x (Point x)
Dim CSequence (Point ZModHom)
ProductSymbol ZMod
sx) Entries N N ZModHom
xs'' where
        -- note: from x valid and eligible follows that
        -- for all non zero (z,i,j) in x holds: orientation z = cy 0 :> cy 0
        AbGroup ProductSymbol ZMod
e = AbHom -> Point AbHom
forall q. Oriented q => q -> Point q
end AbHom
kLim
        
        AbGroup ProductSymbol ZMod
sx = Cone Dst 'Projective ('Parallel 'LeftToRight) N2 N1 AbHom
-> Point AbHom
forall s (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N')
       a.
Cone s p t n m a -> Point a
tip Cone Dst 'Projective ('Parallel 'LeftToRight) N2 N1 AbHom
cn
        
        Matrix Dim' Z
_ Dim' Z
_ Entries N N Z
xs'  = Matrix Z
bInv Matrix Z -> Matrix Z -> Matrix Z
forall c. Multiplicative c => c -> c -> c
* AbHom -> Matrix Z
abhz AbHom
x
        xs'' :: Entries N N ZModHom
xs'' = Col N (Row N ZModHom) -> Entries N N ZModHom
forall i j x. Col i (Row j x) -> Entries i j x
crets (Col N (Row N ZModHom) -> Entries N N ZModHom)
-> Col N (Row N ZModHom) -> Entries N N ZModHom
forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ PSequence N (Row N ZModHom) -> Col N (Row N ZModHom)
forall i x. PSequence i x -> Col i x
Col (PSequence N (Row N ZModHom) -> Col N (Row N ZModHom))
-> PSequence N (Row N ZModHom) -> Col N (Row N ZModHom)
forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ [(Row N ZModHom, N)] -> PSequence N (Row N ZModHom)
forall i x. [(x, i)] -> PSequence i x
PSequence ([(Row N ZModHom, N)] -> PSequence N (Row N ZModHom))
-> [(Row N ZModHom, N)] -> PSequence N (Row N ZModHom)
forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ [(Row N Z, N)] -> [(Z, N)] -> [(Row N ZModHom, N)]
forall i j.
Ord i =>
[(Row j Z, i)] -> [(Z, i)] -> [(Row j ZModHom, i)]
div' (Proxy N -> Col N (Row N Z) -> [(Row N Z, N)]
forall (p :: * -> *). p N -> Col N (Row N Z) -> [(Row N Z, N)]
forall (s :: * -> *) i x (p :: * -> *).
Sequence s i x =>
p i -> s x -> [(x, i)]
list Proxy N
nProxy (Col N (Row N Z) -> [(Row N Z, N)])
-> Col N (Row N Z) -> [(Row N Z, N)]
forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ Entries N N Z -> Col N (Row N Z)
forall i j x. Eq i => Entries i j x -> Col i (Row j x)
etscr Entries N N Z
xs') ([Z]
k [Z] -> [N] -> [(Z, N)]
forall a b. [a] -> [b] -> [(a, b)]
`zip` [N
0..])
  
        div' :: Ord i => [(Row j Z,i)] -> [(Z,i)] -> [(Row j ZModHom,i)]
        div' :: forall i j.
Ord i =>
[(Row j Z, i)] -> [(Z, i)] -> [(Row j ZModHom, i)]
div' [] [(Z, i)]
_             = []
        div' ((Row j Z
rw,i
i):[(Row j Z, i)]
rws') [] = ((Z -> ZModHom) -> Row j Z -> Row j ZModHom
forall a b. (a -> b) -> Row j a -> Row j b
forall (h :: * -> * -> *) (f :: * -> *) a b.
Applicative1 h f =>
h a b -> f a -> f b
amap1 Z -> ZModHom
fromZ Row j Z
rw,i
i)(Row j ZModHom, i) -> [(Row j ZModHom, i)] -> [(Row j ZModHom, i)]
forall a. a -> [a] -> [a]
:[(Row j Z, i)] -> [(Z, i)] -> [(Row j ZModHom, i)]
forall i j.
Ord i =>
[(Row j Z, i)] -> [(Z, i)] -> [(Row j ZModHom, i)]
div' [(Row j Z, i)]
rws' []
        div' rws :: [(Row j Z, i)]
rws@((Row j Z
rw,i
i):[(Row j Z, i)]
rws') ((Z
k,i
i'):[(Z, i)]
kis')
          | i
i' i -> i -> Bool
forall a. Ord a => a -> a -> Bool
< i
i    = [(Row j Z, i)] -> [(Z, i)] -> [(Row j ZModHom, i)]
forall i j.
Ord i =>
[(Row j Z, i)] -> [(Z, i)] -> [(Row j ZModHom, i)]
div' [(Row j Z, i)]
rws [(Z, i)]
kis'
          | Bool
otherwise = ((Z -> ZModHom) -> Row j Z -> Row j ZModHom
forall a b. (a -> b) -> Row j a -> Row j b
forall (h :: * -> * -> *) (f :: * -> *) a b.
Applicative1 h f =>
h a b -> f a -> f b
amap1 (Z -> ZModHom
fromZ (Z -> ZModHom) -> (Z -> Z) -> Z -> ZModHom
forall y z x. (y -> z) -> (x -> y) -> x -> z
forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. \Z
z -> Z -> Z -> Z
forall a. Integral a => a -> a -> a
div Z
z Z
k) Row j Z
rw,i
i)(Row j ZModHom, i) -> [(Row j ZModHom, i)] -> [(Row j ZModHom, i)]
forall a. a -> [a] -> [a]
:[(Row j Z, i)] -> [(Z, i)] -> [(Row j ZModHom, i)]
forall i j.
Ord i =>
[(Row j Z, i)] -> [(Z, i)] -> [(Row j ZModHom, i)]
div' [(Row j Z, i)]
rws' [(Z, i)]
kis' 

  hKer [(ZMod, N)]
_ = [Char] -> KernelFree N1 AbHom
forall a. HasCallStack => [Char] -> a
error [Char]
"faild precondition"

--------------------------------------------------------------------------------
-- abhKernelFreeFrom -

xFreeFrom :: Free k AbHom -> X (Slice From (Free k) AbHom)
xFreeFrom :: forall (k :: N'). Free k AbHom -> X (Slice 'From (Free k) AbHom)
xFreeFrom k :: Free k AbHom
k@(Free Any k
k') = do
  AbHom
h <- AbGroup -> X AbHom
xh (N -> AbGroup
abg N
0 AbGroup -> Exponent AbGroup -> AbGroup
forall f. Exponential f => f -> Exponent f -> f
^ (Any k -> N
forall x. LengthN x => x -> N
lengthN Any k
k'))
  Slice 'From (Free k) AbHom -> X (Slice 'From (Free k) AbHom)
forall a. a -> X a
forall (m :: * -> *) a. Monad m => a -> m a
return (Free k AbHom -> AbHom -> Slice 'From (Free k) AbHom
forall (i :: * -> *) c. i c -> c -> Slice 'From i c
SliceFrom Free k AbHom
k AbHom
h)
  where XStart X (Point AbHom)
_ Point AbHom -> X AbHom
AbGroup -> X AbHom
xh = XOrtSite 'From AbHom
forall (s :: Site) a. XStandardOrtSite s a => XOrtSite s a
xStandardOrtSite :: XOrtSite From AbHom 

pp3 :: Attestable k => Free k AbHom -> Statement
pp3 :: forall (k :: N'). Attestable k => Free k AbHom -> Statement
pp3 Free k AbHom
k = X (Slice 'From (Free k) AbHom)
-> (Slice 'From (Free k) AbHom -> Statement) -> Statement
forall x. X x -> (x -> Statement) -> Statement
Forall X (Slice 'From (Free k) AbHom)
xs Slice 'From (Free k) AbHom -> Statement
forall a. Validable a => a -> Statement
valid where xs :: X (Slice 'From (Free k) AbHom)
xs = Free k AbHom -> X (Slice 'From (Free k) AbHom)
forall (k :: N'). Free k AbHom -> X (Slice 'From (Free k) AbHom)
xFreeFrom Free k AbHom
k

-- | the kernel of a free site from.
--
-- @
--          h
--      a ------> b
--      
-- @ where @a@ is free of some order @k@.
--
-- __Property__ Let @s = 'SliceFrom' _ h@ be in @'Slice' 'From' ('Free' __k__)@ and
-- @ker = 'abhKernelFreeFrom' s@, then holds:
-- @'diagram' ('limesFree' ker) '==' 'kernelDiagram' h@.
abhKernelFreeFrom :: Attestable k => Slice From (Free k) AbHom -> KernelFree N1 AbHom
abhKernelFreeFrom :: forall (k :: N').
Attestable k =>
Slice 'From (Free k) AbHom -> KernelFree N1 AbHom
abhKernelFreeFrom Slice 'From (Free k) AbHom
s = Slice 'From (Free k) AbHom
-> SomeFinList (KernelFree N1 AbHom) -> KernelFree N1 AbHom
forall (k :: N').
Attestable k =>
Slice 'From (Free k) AbHom
-> SomeFinList (KernelFree N1 AbHom) -> KernelFree N1 AbHom
ker Slice 'From (Free k) AbHom
s ((Slice 'From (Free k) AbHom -> KernelFree N1 AbHom)
-> SomeFinList (Slice 'From (Free k) AbHom)
-> SomeFinList (KernelFree N1 AbHom)
forall a b. (a -> b) -> SomeFinList a -> SomeFinList b
forall (h :: * -> * -> *) (f :: * -> *) a b.
Applicative1 h f =>
h a b -> f a -> f b
amap1 Slice 'From (Free k) AbHom -> KernelFree N1 AbHom
forall (k :: N').
Attestable k =>
Slice 'From (Free k) AbHom -> KernelFree N1 AbHom
abhKernelFreeFromCy (SomeFinList (Slice 'From (Free k) AbHom)
 -> SomeFinList (KernelFree N1 AbHom))
-> SomeFinList (Slice 'From (Free k) AbHom)
-> SomeFinList (KernelFree N1 AbHom)
forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ Slice 'From (Free k) AbHom
-> SomeFinList (Slice 'From (Free k) AbHom)
forall (k :: N').
Slice 'From (Free k) AbHom
-> SomeFinList (Slice 'From (Free k) AbHom)
abhFreeFromSplitCy Slice 'From (Free k) AbHom
s) where

  plbDgm :: Attestable k
    => Free k AbHom -> FinList n (KernelFree N1 AbHom) -> PullbackDiagramFree n AbHom
  plbDgm :: forall (k :: N') (n :: N').
Attestable k =>
Free k AbHom
-> FinList n (KernelFree N1 AbHom) -> PullbackDiagramFree n AbHom
plbDgm Free k AbHom
k FinList n (KernelFree N1 AbHom)
kers = FinList ('S n) (SomeFree AbHom)
-> Diagram ('Star 'To) ('S n) n AbHom
-> DiagramFree ('Star 'To) ('S n) n AbHom
forall (t :: DiagramType) (n :: N') (m :: N') a.
FinList n (SomeFree a) -> Diagram t n m a -> DiagramFree t n m a
DiagramFree FinList (n + 1) (SomeFree AbHom)
FinList ('S n) (SomeFree AbHom)
ks Diagram ('Star 'To) ('S n) n AbHom
dgm where
    ks :: FinList (n + 1) (SomeFree AbHom)
ks = Free k AbHom -> SomeFree AbHom
forall (k :: N') c.
(Attestable k, Sliced (Free k) c) =>
Free k c -> SomeFree c
SomeFree Free k AbHom
k SomeFree AbHom
-> FinList n (SomeFree AbHom) -> FinList (n + 1) (SomeFree AbHom)
forall a (n1 :: N'). a -> FinList n1 a -> FinList (n1 + 1) a
:| (KernelFree N1 AbHom -> SomeFree AbHom)
-> FinList n (KernelFree N1 AbHom) -> FinList n (SomeFree AbHom)
forall a b. (a -> b) -> FinList n a -> FinList n b
forall (h :: * -> * -> *) (f :: * -> *) a b.
Applicative1 h f =>
h a b -> f a -> f b
amap1 (\(LimesFree Free k AbHom
k' Kernel N1 AbHom
_) -> Free k AbHom -> SomeFree AbHom
forall (k :: N') c.
(Attestable k, Sliced (Free k) c) =>
Free k c -> SomeFree c
SomeFree Free k AbHom
k') FinList n (KernelFree N1 AbHom)
kers
    dgm :: Diagram ('Star 'To) ('S n) n AbHom
dgm = Point AbHom
-> FinList n AbHom -> Diagram ('Star 'To) (n + 1) n AbHom
forall a (m :: N').
Point a -> FinList m a -> Diagram ('Star 'To) (m + 1) m a
DiagramSink (Free k AbHom -> Point AbHom
forall (i :: * -> *) c. Sliced i c => i c -> Point c
slicePoint Free k AbHom
k)
      (FinList n AbHom -> Diagram ('Star 'To) ('S n) n AbHom)
-> FinList n AbHom -> Diagram ('Star 'To) ('S n) n AbHom
forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ (KernelFree N1 AbHom -> AbHom)
-> FinList n (KernelFree N1 AbHom) -> FinList n AbHom
forall a b. (a -> b) -> FinList n a -> FinList n b
forall (h :: * -> * -> *) (f :: * -> *) a b.
Applicative1 h f =>
h a b -> f a -> f b
amap1 (Cone Dst 'Projective ('Parallel 'LeftToRight) N2 N1 AbHom -> AbHom
forall c. KernelCone N1 c -> c
kernelFactor (Cone Dst 'Projective ('Parallel 'LeftToRight) N2 N1 AbHom
 -> AbHom)
-> (KernelFree N1 AbHom
    -> Cone Dst 'Projective ('Parallel 'LeftToRight) N2 N1 AbHom)
-> KernelFree N1 AbHom
-> AbHom
forall y z x. (y -> z) -> (x -> y) -> x -> z
forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. Kernel N1 AbHom
-> Cone Dst 'Projective ('Parallel 'LeftToRight) N2 N1 AbHom
forall s (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N')
       a.
Limes s p t n m a -> Cone s p t n m a
universalCone (Kernel N1 AbHom
 -> Cone Dst 'Projective ('Parallel 'LeftToRight) N2 N1 AbHom)
-> (KernelFree N1 AbHom -> Kernel N1 AbHom)
-> KernelFree N1 AbHom
-> Cone Dst 'Projective ('Parallel 'LeftToRight) N2 N1 AbHom
forall y z x. (y -> z) -> (x -> y) -> x -> z
forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. KernelFree N1 AbHom -> Kernel N1 AbHom
forall s (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N')
       a.
LimesFree s p t n m a -> Limes s p t n m a
limesFree)
      (FinList n (KernelFree N1 AbHom) -> FinList n AbHom)
-> FinList n (KernelFree N1 AbHom) -> FinList n AbHom
forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ FinList n (KernelFree N1 AbHom)
kers
  
  ker :: Attestable k
    => Slice From (Free k) AbHom -> SomeFinList (KernelFree N1 AbHom)
    -> KernelFree N1 AbHom
  ker :: forall (k :: N').
Attestable k =>
Slice 'From (Free k) AbHom
-> SomeFinList (KernelFree N1 AbHom) -> KernelFree N1 AbHom
ker s :: Slice 'From (Free k) AbHom
s@(SliceFrom Free k AbHom
k AbHom
_) (SomeFinList FinList n (KernelFree N1 AbHom)
kers) = Slice 'From (Free k) AbHom
-> FinList n (KernelFree N1 AbHom)
-> PullbackFree n AbHom
-> KernelFree N1 AbHom
forall (k :: N') (n :: N').
Slice 'From (Free k) AbHom
-> FinList n (KernelFree N1 AbHom)
-> PullbackFree n AbHom
-> KernelFree N1 AbHom
ker' Slice 'From (Free k) AbHom
s FinList n (KernelFree N1 AbHom)
kers (PullbackDiagramFree n AbHom -> PullbackFree n AbHom
DiagramFree ('Star 'To) ('S n) n AbHom
-> LimesFree Mlt 'Projective ('Star 'To) ('S n) n AbHom
forall (n :: N').
PullbackDiagramFree n AbHom -> PullbackFree n AbHom
abhPullbackFree (DiagramFree ('Star 'To) ('S n) n AbHom
 -> LimesFree Mlt 'Projective ('Star 'To) ('S n) n AbHom)
-> DiagramFree ('Star 'To) ('S n) n AbHom
-> LimesFree Mlt 'Projective ('Star 'To) ('S n) n AbHom
forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ Free k AbHom
-> FinList n (KernelFree N1 AbHom) -> PullbackDiagramFree n AbHom
forall (k :: N') (n :: N').
Attestable k =>
Free k AbHom
-> FinList n (KernelFree N1 AbHom) -> PullbackDiagramFree n AbHom
plbDgm Free k AbHom
k FinList n (KernelFree N1 AbHom)
kers)

  ker'
    :: Slice From (Free k) AbHom
    -> FinList n (KernelFree N1 AbHom)
    -> PullbackFree n AbHom
    -> KernelFree N1 AbHom
  ker' :: forall (k :: N') (n :: N').
Slice 'From (Free k) AbHom
-> FinList n (KernelFree N1 AbHom)
-> PullbackFree n AbHom
-> KernelFree N1 AbHom
ker' (SliceFrom Free k AbHom
_ AbHom
h) FinList n (KernelFree N1 AbHom)
kers (LimesFree Free k AbHom
kt Limes Mlt 'Projective ('Star 'To) (n + 1) n AbHom
plb)
    = Free k AbHom -> Kernel N1 AbHom -> KernelFree N1 AbHom
forall (k :: N') a s (p :: Perspective) (t :: DiagramType)
       (n :: N') (m :: N').
(Attestable k, Sliced (Free k) a) =>
Free k a -> Limes s p t n m a -> LimesFree s p t n m a
LimesFree Free k AbHom
kt (Cone Dst 'Projective ('Parallel 'LeftToRight) N2 N1 AbHom
-> (Cone Dst 'Projective ('Parallel 'LeftToRight) N2 N1 AbHom
    -> AbHom)
-> Kernel N1 AbHom
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 AbHom
hKer Cone Dst 'Projective ('Parallel 'LeftToRight) N2 N1 AbHom -> AbHom
hUniv) where
    
    hDgm :: Diagram ('Parallel 'LeftToRight) N2 N1 AbHom
hDgm = AbHom -> Diagram ('Parallel 'LeftToRight) N2 N1 AbHom
forall c. Oriented c => c -> KernelDiagram N1 c
kernelDiagram AbHom
h
    hKer :: Cone Dst 'Projective ('Parallel 'LeftToRight) N2 N1 AbHom
hKer = Diagram ('Parallel 'LeftToRight) N2 N1 AbHom
-> AbHom
-> Cone Dst 'Projective ('Parallel 'LeftToRight) N2 N1 AbHom
forall a (m :: N').
Distributive a =>
Diagram ('Parallel 'LeftToRight) N2 m a
-> a -> Cone Dst 'Projective ('Parallel 'LeftToRight) N2 m a
ConeKernel Diagram ('Parallel 'LeftToRight) N2 N1 AbHom
hDgm (FinList (n + 1) AbHom -> AbHom
FinList ('S n) AbHom -> AbHom
forall (n :: N') a. FinList (n + 1) a -> a
F.head (FinList ('S n) AbHom -> AbHom) -> FinList ('S n) AbHom -> AbHom
forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ Cone Mlt 'Projective ('Star 'To) ('S n) n AbHom
-> FinList ('S n) AbHom
forall s (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N')
       a.
Cone s p t n m a -> FinList n a
shell (Cone Mlt 'Projective ('Star 'To) ('S n) n AbHom
 -> FinList ('S n) AbHom)
-> Cone Mlt 'Projective ('Star 'To) ('S n) n AbHom
-> FinList ('S n) AbHom
forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ Limes Mlt 'Projective ('Star 'To) ('S n) n AbHom
-> Cone Mlt 'Projective ('Star 'To) ('S n) n AbHom
forall s (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N')
       a.
Limes s p t n m a -> Cone s p t n m a
universalCone Limes Mlt 'Projective ('Star 'To) (n + 1) n AbHom
Limes Mlt 'Projective ('Star 'To) ('S n) n AbHom
plb)
    
    hUniv :: Cone Dst 'Projective ('Parallel 'LeftToRight) N2 N1 AbHom -> AbHom
hUniv (ConeKernel Diagram ('Parallel 'LeftToRight) N2 N1 AbHom
_ AbHom
x) = Limes Mlt 'Projective ('Star 'To) ('S n) n AbHom
-> Cone Mlt 'Projective ('Star 'To) ('S n) n AbHom -> AbHom
forall s (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N')
       a.
Limes s p t n m a -> Cone s p t n m a -> a
universalFactor Limes Mlt 'Projective ('Star 'To) (n + 1) n AbHom
Limes Mlt 'Projective ('Star 'To) ('S n) n AbHom
plb Cone Mlt 'Projective ('Star 'To) ('S n) n AbHom
plbCone where
      plbCone :: Cone Mlt 'Projective ('Star 'To) ('S n) n AbHom
plbCone = Diagram ('Star 'To) ('S n) n AbHom
-> Point AbHom
-> FinList ('S n) AbHom
-> Cone Mlt 'Projective ('Star 'To) ('S n) n AbHom
forall a (t :: DiagramType) (n :: N') (m :: N').
Multiplicative a =>
Diagram t n m a
-> Point a -> FinList n a -> Cone Mlt 'Projective t n m a
ConeProjective (Limes Mlt 'Projective ('Star 'To) ('S n) n AbHom
-> Diagram ('Star 'To) ('S n) n AbHom
forall s (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N')
       a.
Limes s p t n m a -> Diagram t n m a
diagram Limes Mlt 'Projective ('Star 'To) (n + 1) n AbHom
Limes Mlt 'Projective ('Star 'To) ('S n) n AbHom
plb) (AbHom -> Point AbHom
forall q. Oriented q => q -> Point q
start AbHom
x) FinList (n + 1) AbHom
FinList ('S n) AbHom
cs
      cs :: FinList (n + 1) AbHom
cs = AbHom
xAbHom -> FinList n AbHom -> FinList (n + 1) AbHom
forall a (n1 :: N'). a -> FinList n1 a -> FinList (n1 + 1) a
:|(KernelFree N1 AbHom -> AbHom)
-> FinList n (KernelFree N1 AbHom) -> FinList n AbHom
forall a b. (a -> b) -> FinList n a -> FinList n b
forall (h :: * -> * -> *) (f :: * -> *) a b.
Applicative1 h f =>
h a b -> f a -> f b
amap1
        (\(LimesFree Free k AbHom
_ Kernel N1 AbHom
ker)
         -> Kernel N1 AbHom
-> Cone Dst 'Projective ('Parallel 'LeftToRight) N2 N1 AbHom
-> AbHom
forall s (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N')
       a.
Limes s p t n m a -> Cone s p t n m a -> a
universalFactor Kernel N1 AbHom
ker (Diagram ('Parallel 'LeftToRight) N2 N1 AbHom
-> AbHom
-> Cone Dst 'Projective ('Parallel 'LeftToRight) N2 N1 AbHom
forall a (m :: N').
Distributive a =>
Diagram ('Parallel 'LeftToRight) N2 m a
-> a -> Cone Dst 'Projective ('Parallel 'LeftToRight) N2 m a
ConeKernel (Kernel N1 AbHom -> Diagram ('Parallel 'LeftToRight) N2 N1 AbHom
forall s (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N')
       a.
Limes s p t n m a -> Diagram t n m a
diagram Kernel N1 AbHom
ker) AbHom
x)
          -- the cone is eligible because of the property (2) of abhFreeFromSplitCy
        ) FinList n (KernelFree N1 AbHom)
kers

--------------------------------------------------------------------------------
-- abhKernel -

-- | kernel for a given additive homomorphism.
--
-- __Properties__ Let @d@ be in @'KernelDiagram' 'N1' 'AbHom'@ and
-- @ker = 'abhKernel' d@, then holds:
--
-- (1) @'diagram' ker '==' d@.
--
-- (2) @'tip' ('universalCone' ker)@ is smith normal.
--
-- The construction follows the diagram below by using 'abgGeneratorTo':
--
-- @
--         k''         
--    r'' ------> s'' 
--     |           | 
--  q' |        p' | 
--     |           | 
--     v    k'     v
--    r' --------> s'
--     |           |
--  q  |         p | 
--     |           | 
--     v   hKer    v     h 
--     r --------> s -------> e
-- @
abhKernel :: KernelDiagram N1 AbHom -> Kernel N1 AbHom
abhKernel :: Diagram ('Parallel 'LeftToRight) N2 N1 AbHom -> Kernel N1 AbHom
abhKernel Diagram ('Parallel 'LeftToRight) N2 N1 AbHom
d = Diagram ('Parallel 'LeftToRight) N2 N1 AbHom
-> Generator 'To AbHom -> Kernel N1 AbHom
hKer Diagram ('Parallel 'LeftToRight) N2 N1 AbHom
d (AbGroup -> Generator 'To AbHom
abgGeneratorTo (AbHom -> Point AbHom
forall q. Oriented q => q -> Point q
start AbHom
h)) where

  DiagramParallelLR Point AbHom
_ Point AbHom
_ (AbHom
h:|FinList n1 AbHom
Nil) = Diagram ('Parallel 'LeftToRight) N2 N1 AbHom
d
  
  hKer :: KernelDiagram N1 AbHom -> Generator To AbHom -> Kernel N1 AbHom
  hKer :: Diagram ('Parallel 'LeftToRight) N2 N1 AbHom
-> Generator 'To AbHom -> Kernel N1 AbHom
hKer
    d :: Diagram ('Parallel 'LeftToRight) N2 N1 AbHom
d@(DiagramParallelLR Point AbHom
_ Point AbHom
_ (AbHom
h:|FinList n1 AbHom
Nil))
    g :: Generator 'To AbHom
g@(GeneratorTo (DiagramChainTo Point AbHom
_ (AbHom
p:|AbHom
_:|FinList n1 AbHom
Nil)) Free k' AbHom
ns' Free k'' AbHom
_ Cokernel N1 AbHom
_ Kernel N1 AbHom
_ forall (k :: N'). Slice 'From (Free k) AbHom -> AbHom
_)
    = Diagram ('Parallel 'LeftToRight) N2 N1 AbHom
-> Generator 'To AbHom -> KernelFree N1 AbHom -> Kernel N1 AbHom
hKer' Diagram ('Parallel 'LeftToRight) N2 N1 AbHom
d Generator 'To AbHom
g (Slice 'From (Free k') AbHom -> KernelFree N1 AbHom
forall (k :: N').
Attestable k =>
Slice 'From (Free k) AbHom -> KernelFree N1 AbHom
abhKernelFreeFrom (Free k' AbHom -> AbHom -> Slice 'From (Free k') AbHom
forall (i :: * -> *) c. i c -> c -> Slice 'From i c
SliceFrom Free k' AbHom
ns' (AbHom
hAbHom -> AbHom -> AbHom
forall c. Multiplicative c => c -> c -> c
*AbHom
p)))

  hKer'
    :: KernelDiagram N1 AbHom
    -> Generator To AbHom
    -> KernelFree N1 AbHom
    -> Kernel N1 AbHom
  hKer' :: Diagram ('Parallel 'LeftToRight) N2 N1 AbHom
-> Generator 'To AbHom -> KernelFree N1 AbHom -> Kernel N1 AbHom
hKer'
    Diagram ('Parallel 'LeftToRight) N2 N1 AbHom
d
    g :: Generator 'To AbHom
g@(GeneratorTo (DiagramChainTo Point AbHom
_ (AbHom
_:|AbHom
p':|FinList n1 AbHom
Nil)) Free k' AbHom
ns' Free k'' AbHom
ns'' Cokernel N1 AbHom
_ Kernel N1 AbHom
_ forall (k :: N'). Slice 'From (Free k) AbHom -> AbHom
_)
    hpKerFree :: KernelFree N1 AbHom
hpKerFree@(LimesFree Free k AbHom
nr' Kernel N1 AbHom
hpKer)
    = Diagram ('Parallel 'LeftToRight) N2 N1 AbHom
-> Generator 'To AbHom
-> KernelFree N1 AbHom
-> PullbackFree N2 AbHom
-> Kernel N1 AbHom
hKer'' Diagram ('Parallel 'LeftToRight) N2 N1 AbHom
d Generator 'To AbHom
g KernelFree N1 AbHom
hpKerFree PullbackFree N2 AbHom
k'p'Plb where

    k'p'Plb :: PullbackFree N2 AbHom
k'p'Plb = PullbackDiagramFree N2 AbHom -> PullbackFree N2 AbHom
forall (n :: N').
PullbackDiagramFree n AbHom -> PullbackFree n AbHom
abhPullbackFree
      (FinList ('S N2) (SomeFree AbHom)
-> Diagram ('Star 'To) ('S N2) N2 AbHom
-> DiagramFree ('Star 'To) ('S N2) N2 AbHom
forall (t :: DiagramType) (n :: N') (m :: N') a.
FinList n (SomeFree a) -> Diagram t n m a -> DiagramFree t n m a
DiagramFree (Free k' AbHom -> SomeFree AbHom
forall (k :: N') c.
(Attestable k, Sliced (Free k) c) =>
Free k c -> SomeFree c
SomeFree Free k' AbHom
ns'SomeFree AbHom
-> FinList N2 (SomeFree AbHom) -> FinList (N2 + 1) (SomeFree AbHom)
forall a (n1 :: N'). a -> FinList n1 a -> FinList (n1 + 1) a
:|Free k AbHom -> SomeFree AbHom
forall (k :: N') c.
(Attestable k, Sliced (Free k) c) =>
Free k c -> SomeFree c
SomeFree Free k AbHom
nr'SomeFree AbHom
-> FinList N1 (SomeFree AbHom) -> FinList (N1 + 1) (SomeFree AbHom)
forall a (n1 :: N'). a -> FinList n1 a -> FinList (n1 + 1) a
:|Free k'' AbHom -> SomeFree AbHom
forall (k :: N') c.
(Attestable k, Sliced (Free k) c) =>
Free k c -> SomeFree c
SomeFree Free k'' AbHom
ns''SomeFree AbHom
-> FinList 'N0 (SomeFree AbHom)
-> FinList ('N0 + 1) (SomeFree AbHom)
forall a (n1 :: N'). a -> FinList n1 a -> FinList (n1 + 1) a
:|FinList 'N0 (SomeFree AbHom)
forall a. FinList 'N0 a
Nil) Diagram ('Star 'To) (N2 + 1) N2 AbHom
Diagram ('Star 'To) ('S N2) N2 AbHom
k'p'PlbDgm)
    k'p'PlbDgm :: Diagram ('Star 'To) (N2 + 1) N2 AbHom
k'p'PlbDgm = Point AbHom
-> FinList N2 AbHom -> Diagram ('Star 'To) (N2 + 1) N2 AbHom
forall a (m :: N').
Point a -> FinList m a -> Diagram ('Star 'To) (m + 1) m a
DiagramSink (AbHom -> Point AbHom
forall q. Oriented q => q -> Point q
end AbHom
k') (AbHom
k'AbHom -> FinList N1 AbHom -> FinList (N1 + 1) AbHom
forall a (n1 :: N'). a -> FinList n1 a -> FinList (n1 + 1) a
:|AbHom
p'AbHom -> FinList 'N0 AbHom -> FinList ('N0 + 1) AbHom
forall a (n1 :: N'). a -> FinList n1 a -> FinList (n1 + 1) a
:|FinList 'N0 AbHom
forall a. FinList 'N0 a
Nil)

    k' :: AbHom
k' = Cone Dst 'Projective ('Parallel 'LeftToRight) N2 N1 AbHom -> AbHom
forall c. KernelCone N1 c -> c
kernelFactor (Cone Dst 'Projective ('Parallel 'LeftToRight) N2 N1 AbHom
 -> AbHom)
-> Cone Dst 'Projective ('Parallel 'LeftToRight) N2 N1 AbHom
-> AbHom
forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ Kernel N1 AbHom
-> Cone Dst 'Projective ('Parallel 'LeftToRight) N2 N1 AbHom
forall s (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N')
       a.
Limes s p t n m a -> Cone s p t n m a
universalCone Kernel N1 AbHom
hpKer
    
  hKer''
    :: KernelDiagram N1 AbHom
    -> Generator To AbHom
    -> KernelFree N1 AbHom
    -> PullbackFree N2 AbHom
    -> Kernel N1 AbHom
  hKer'' :: Diagram ('Parallel 'LeftToRight) N2 N1 AbHom
-> Generator 'To AbHom
-> KernelFree N1 AbHom
-> PullbackFree N2 AbHom
-> Kernel N1 AbHom
hKer''
    Diagram ('Parallel 'LeftToRight) N2 N1 AbHom
d
    (GeneratorTo (DiagramChainTo Point AbHom
_ (AbHom
p:|AbHom
_:|FinList n1 AbHom
Nil)) Free k' AbHom
_ Free k'' AbHom
_ Cokernel N1 AbHom
_ Kernel N1 AbHom
_ forall (k :: N'). Slice 'From (Free k) AbHom -> AbHom
lp)
    (LimesFree Free k AbHom
nr' Kernel N1 AbHom
hpKer)
    (LimesFree Free k AbHom
nr'' Limes Mlt 'Projective ('Star 'To) (N2 + 1) N2 AbHom
k'p'Plb)
    = Cone Dst 'Projective ('Parallel 'LeftToRight) N2 N1 AbHom
-> (Cone Dst 'Projective ('Parallel 'LeftToRight) N2 N1 AbHom
    -> AbHom)
-> Kernel N1 AbHom
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 AbHom
hKer Cone Dst 'Projective ('Parallel 'LeftToRight) N2 N1 AbHom -> AbHom
hUniv where

    AbHom
_:|AbHom
q':|FinList n1 AbHom
_   = Cone Mlt 'Projective ('Star 'To) ('S N2) N2 AbHom
-> FinList ('S N2) AbHom
forall s (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N')
       a.
Cone s p t n m a -> FinList n a
shell (Cone Mlt 'Projective ('Star 'To) ('S N2) N2 AbHom
 -> FinList ('S N2) AbHom)
-> Cone Mlt 'Projective ('Star 'To) ('S N2) N2 AbHom
-> FinList ('S N2) AbHom
forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ Limes Mlt 'Projective ('Star 'To) ('S N2) N2 AbHom
-> Cone Mlt 'Projective ('Star 'To) ('S N2) N2 AbHom
forall s (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N')
       a.
Limes s p t n m a -> Cone s p t n m a
universalCone Limes Mlt 'Projective ('Star 'To) (N2 + 1) N2 AbHom
Limes Mlt 'Projective ('Star 'To) ('S N2) N2 AbHom
k'p'Plb
    q'CokerDgm :: Diagram ('Parallel 'RightToLeft) N2 N1 AbHom
q'CokerDgm = AbHom -> Diagram ('Parallel 'RightToLeft) N2 N1 AbHom
forall c. Oriented c => c -> CokernelDiagram N1 c
cokernelDiagram AbHom
q' 
    q'Coker :: Cokernel N1 AbHom
q'Coker    = CokernelDiagramFree N1 AbHom -> Cokernel N1 AbHom
abhCokernelFree
      ( FinList N2 (SomeFree AbHom)
-> Diagram ('Parallel 'RightToLeft) N2 N1 AbHom
-> CokernelDiagramFree N1 AbHom
forall (t :: DiagramType) (n :: N') (m :: N') a.
FinList n (SomeFree a) -> Diagram t n m a -> DiagramFree t n m a
DiagramFree
         (Free k AbHom -> SomeFree AbHom
forall (k :: N') c.
(Attestable k, Sliced (Free k) c) =>
Free k c -> SomeFree c
SomeFree Free k AbHom
nr'SomeFree AbHom
-> FinList N1 (SomeFree AbHom) -> FinList (N1 + 1) (SomeFree AbHom)
forall a (n1 :: N'). a -> FinList n1 a -> FinList (n1 + 1) a
:|Free k AbHom -> SomeFree AbHom
forall (k :: N') c.
(Attestable k, Sliced (Free k) c) =>
Free k c -> SomeFree c
SomeFree Free k AbHom
nr''SomeFree AbHom
-> FinList 'N0 (SomeFree AbHom)
-> FinList ('N0 + 1) (SomeFree AbHom)
forall a (n1 :: N'). a -> FinList n1 a -> FinList (n1 + 1) a
:|FinList 'N0 (SomeFree AbHom)
forall a. FinList 'N0 a
Nil)
         Diagram ('Parallel 'RightToLeft) N2 N1 AbHom
q'CokerDgm
      )
      
    hKer :: Cone Dst 'Projective ('Parallel 'LeftToRight) N2 N1 AbHom
hKer = Diagram ('Parallel 'LeftToRight) N2 N1 AbHom
-> AbHom
-> Cone Dst 'Projective ('Parallel 'LeftToRight) N2 N1 AbHom
forall a (m :: N').
Distributive a =>
Diagram ('Parallel 'LeftToRight) N2 m a
-> a -> Cone Dst 'Projective ('Parallel 'LeftToRight) N2 m a
ConeKernel Diagram ('Parallel 'LeftToRight) N2 N1 AbHom
d AbHom
hKerFactor where
      hKerFactor :: AbHom
hKerFactor = Cokernel N1 AbHom
-> Cone Dst 'Injective ('Parallel 'RightToLeft) N2 N1 AbHom
-> AbHom
forall s (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N')
       a.
Limes s p t n m a -> Cone s p t n m a -> a
universalFactor Cokernel N1 AbHom
q'Coker (Diagram ('Parallel 'RightToLeft) N2 N1 AbHom
-> AbHom
-> Cone Dst 'Injective ('Parallel 'RightToLeft) N2 N1 AbHom
forall a (m :: N').
Distributive a =>
Diagram ('Parallel 'RightToLeft) N2 m a
-> a -> Cone Dst 'Injective ('Parallel 'RightToLeft) N2 m a
ConeCokernel Diagram ('Parallel 'RightToLeft) N2 N1 AbHom
q'CokerDgm (AbHom
pAbHom -> AbHom -> AbHom
forall c. Multiplicative c => c -> c -> c
*AbHom
k'))
      k' :: AbHom
k' = Cone Dst 'Projective ('Parallel 'LeftToRight) N2 N1 AbHom -> AbHom
forall c. KernelCone N1 c -> c
kernelFactor (Cone Dst 'Projective ('Parallel 'LeftToRight) N2 N1 AbHom
 -> AbHom)
-> Cone Dst 'Projective ('Parallel 'LeftToRight) N2 N1 AbHom
-> AbHom
forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ Kernel N1 AbHom
-> Cone Dst 'Projective ('Parallel 'LeftToRight) N2 N1 AbHom
forall s (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N')
       a.
Limes s p t n m a -> Cone s p t n m a
universalCone Kernel N1 AbHom
hpKer
    
    hUniv :: Cone Dst 'Projective ('Parallel 'LeftToRight) N2 N1 AbHom -> AbHom
hUniv cn :: Cone Dst 'Projective ('Parallel 'LeftToRight) N2 N1 AbHom
cn@(ConeKernel Diagram ('Parallel 'LeftToRight) N2 N1 AbHom
_ AbHom
x) = case AbGroup -> Generator 'To AbHom
abgGeneratorTo (AbHom -> Point AbHom
forall q. Oriented q => q -> Point q
start AbHom
x) of
      GeneratorTo (DiagramChainTo Point AbHom
_ (AbHom
t:|FinList n1 AbHom
_)) Free k' AbHom
nv' Free k'' AbHom
_ Cokernel N1 AbHom
t'Coker Kernel N1 AbHom
_ forall (k :: N'). Slice 'From (Free k) AbHom -> AbHom
_
        | Bool -> Bool
forall b. Boolean b => b -> b
not (Diagram ('Parallel 'LeftToRight) N2 N1 AbHom
d Diagram ('Parallel 'LeftToRight) N2 N1 AbHom
-> Diagram ('Parallel 'LeftToRight) N2 N1 AbHom -> Bool
forall a. Eq a => a -> a -> Bool
== Cone Dst 'Projective ('Parallel 'LeftToRight) N2 N1 AbHom
-> Diagram ('Parallel 'LeftToRight) N2 N1 AbHom
forall s (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N')
       a.
Cone s p t n m a -> Diagram t n m a
cnDiagram Cone Dst 'Projective ('Parallel 'LeftToRight) N2 N1 AbHom
cn) -> LimesException -> AbHom
forall a e. Exception e => e -> a
throw (LimesException -> AbHom) -> LimesException -> AbHom
forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ [Char] -> LimesException
ConeNotEligible ([Char] -> LimesException) -> [Char] -> LimesException
forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ Cone Dst 'Projective ('Parallel 'LeftToRight) N2 N1 AbHom -> [Char]
forall a. Show a => a -> [Char]
show Cone Dst 'Projective ('Parallel 'LeftToRight) N2 N1 AbHom
cn
        | Bool
otherwise               -> Cokernel N1 AbHom
-> Cone Dst 'Injective ('Parallel 'RightToLeft) N2 N1 AbHom
-> AbHom
forall s (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N')
       a.
Limes s p t n m a -> Cone s p t n m a -> a
universalFactor Cokernel N1 AbHom
t'Coker Cone Dst 'Injective ('Parallel 'RightToLeft) N2 N1 AbHom
t'Cone where
                
        t'Cone :: Cone Dst 'Injective ('Parallel 'RightToLeft) N2 N1 AbHom
t'Cone = Diagram ('Parallel 'RightToLeft) N2 N1 AbHom
-> AbHom
-> Cone Dst 'Injective ('Parallel 'RightToLeft) N2 N1 AbHom
forall a (m :: N').
Distributive a =>
Diagram ('Parallel 'RightToLeft) N2 m a
-> a -> Cone Dst 'Injective ('Parallel 'RightToLeft) N2 m a
ConeCokernel (Cokernel N1 AbHom -> Diagram ('Parallel 'RightToLeft) N2 N1 AbHom
forall s (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N')
       a.
Limes s p t n m a -> Diagram t n m a
diagram Cokernel N1 AbHom
t'Coker) (AbHom
qAbHom -> AbHom -> AbHom
forall c. Multiplicative c => c -> c -> c
*AbHom
u')
        q :: AbHom
q  = Cone Dst 'Injective ('Parallel 'RightToLeft) N2 N1 AbHom -> AbHom
forall c. CokernelCone N1 c -> c
cokernelFactor (Cone Dst 'Injective ('Parallel 'RightToLeft) N2 N1 AbHom -> AbHom)
-> Cone Dst 'Injective ('Parallel 'RightToLeft) N2 N1 AbHom
-> AbHom
forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ Cokernel N1 AbHom
-> Cone Dst 'Injective ('Parallel 'RightToLeft) N2 N1 AbHom
forall s (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N')
       a.
Limes s p t n m a -> Cone s p t n m a
universalCone Cokernel N1 AbHom
q'Coker
        u' :: AbHom
u' = Kernel N1 AbHom
-> Cone Dst 'Projective ('Parallel 'LeftToRight) N2 N1 AbHom
-> AbHom
forall s (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N')
       a.
Limes s p t n m a -> Cone s p t n m a -> a
universalFactor Kernel N1 AbHom
hpKer Cone Dst 'Projective ('Parallel 'LeftToRight) N2 N1 AbHom
x'Cone

        x'Cone :: Cone Dst 'Projective ('Parallel 'LeftToRight) N2 N1 AbHom
x'Cone = Diagram ('Parallel 'LeftToRight) N2 N1 AbHom
-> AbHom
-> Cone Dst 'Projective ('Parallel 'LeftToRight) N2 N1 AbHom
forall a (m :: N').
Distributive a =>
Diagram ('Parallel 'LeftToRight) N2 m a
-> a -> Cone Dst 'Projective ('Parallel 'LeftToRight) N2 m a
ConeKernel (Kernel N1 AbHom -> Diagram ('Parallel 'LeftToRight) N2 N1 AbHom
forall s (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N')
       a.
Limes s p t n m a -> Diagram t n m a
diagram Kernel N1 AbHom
hpKer) AbHom
x'
        x' :: AbHom
x' = Slice 'From (Free k') AbHom -> AbHom
forall (k :: N'). Slice 'From (Free k) AbHom -> AbHom
lp (Free k' AbHom -> AbHom -> Slice 'From (Free k') AbHom
forall (i :: * -> *) c. i c -> c -> Slice 'From i c
SliceFrom Free k' AbHom
nv' (AbHom
xAbHom -> AbHom -> AbHom
forall c. Multiplicative c => c -> c -> c
*AbHom
t))


--------------------------------------------------------------------------------
-- abhKernels -

-- | kernels for 'AbHom'. 
abhKernels :: Kernels N1 AbHom
abhKernels :: Kernels N1 AbHom
abhKernels = (Diagram ('Parallel 'LeftToRight) N2 N1 AbHom -> Kernel N1 AbHom)
-> Kernels N1 AbHom
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 Diagram ('Parallel 'LeftToRight) N2 N1 AbHom -> Kernel N1 AbHom
abhKernel

--------------------------------------------------------------------------------
-- AbHom - SliceCokernelTo -

instance Attestable k => SliceCokernelTo (Free k) AbHom where
  sliceCokernelTo :: Slice 'To (Free k) AbHom -> Cokernel N1 AbHom
sliceCokernelTo = Slice 'To (Free k) AbHom -> Cokernel N1 AbHom
forall (k :: N').
Attestable k =>
Slice 'To (Free k) AbHom -> Cokernel N1 AbHom
abhCokernelFreeTo

--------------------------------------------------------------------------------
-- AbHom - SliceKernelFrom -

instance Attestable k => SliceKernelFrom (Free k) AbHom where
  sliceKernelFrom :: Slice 'From (Free k) AbHom -> Kernel N1 AbHom
sliceKernelFrom = KernelFree N1 AbHom -> Kernel N1 AbHom
forall s (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N')
       a.
LimesFree s p t n m a -> Limes s p t n m a
limesFree (KernelFree N1 AbHom -> Kernel N1 AbHom)
-> (Slice 'From (Free k) AbHom -> KernelFree N1 AbHom)
-> Slice 'From (Free k) AbHom
-> Kernel N1 AbHom
forall y z x. (y -> z) -> (x -> y) -> x -> z
forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. Slice 'From (Free k) AbHom -> KernelFree N1 AbHom
forall (k :: N').
Attestable k =>
Slice 'From (Free k) AbHom -> KernelFree N1 AbHom
abhKernelFreeFrom

--------------------------------------------------------------------------------
-- abhSliceFreeAdjunction -

-- | the cokernel-kernel adjunction for a given @'Free' __k__@. 
abhSliceFreeAdjunction :: Attestable k
  => Free k AbHom
  -> Adjunction (SliceCokernelKernel (Free k) AbHom)
       (SliceFactor From (Free k) AbHom)
       (SliceFactor To (Free k) AbHom)
abhSliceFreeAdjunction :: forall (k :: N').
Attestable k =>
Free k AbHom
-> Adjunction
     (SliceCokernelKernel (Free k) AbHom)
     (SliceFactor 'From (Free k) AbHom)
     (SliceFactor 'To (Free k) AbHom)
abhSliceFreeAdjunction = Free k AbHom
-> Adjunction
     (SliceCokernelKernel (Free k) AbHom)
     (SliceFactor 'From (Free k) AbHom)
     (SliceFactor 'To (Free k) AbHom)
forall (i :: * -> *) c.
(SliceCokernelTo i c, SliceKernelFrom i c) =>
i c
-> Adjunction
     (SliceCokernelKernel i c)
     (SliceFactor 'From i c)
     (SliceFactor 'To i c)
slcAdjunction

--------------------------------------------------------------------------------
-- abhCokernel -

-- | cokernel for a given additive homomorphism.
--
-- @
--           w          
--     c <------- e'' 
--     ^           | 
--   u |        q' | 
--     |           | 
--     |    h'     v    
--    s' --------> e' -----> h'L
--     |           |          |
--  p  |         q |          | u'
--     |           |          |
--     v     h     v    w'    v
--     s --------> e ------> c'L
-- @
abhCokernel :: CokernelDiagram N1 AbHom -> Cokernel N1 AbHom
abhCokernel :: Diagram ('Parallel 'RightToLeft) N2 N1 AbHom -> Cokernel N1 AbHom
abhCokernel d :: Diagram ('Parallel 'RightToLeft) N2 N1 AbHom
d@(DiagramParallelRL Point AbHom
_ Point AbHom
_ (AbHom
h:|FinList n1 AbHom
Nil))
  = case (AbGroup -> Generator 'To AbHom
abgGeneratorTo (AbHom -> Point AbHom
forall q. Oriented q => q -> Point q
start AbHom
h),AbGroup -> Generator 'To AbHom
abgGeneratorTo (AbHom -> Point AbHom
forall q. Oriented q => q -> Point q
end AbHom
h)) of
  ( GeneratorTo (DiagramChainTo Point AbHom
_ (AbHom
p:|FinList n1 AbHom
_)) Free k' AbHom
ns' Free k'' AbHom
_ Cokernel N1 AbHom
_ Kernel N1 AbHom
_ forall (k :: N'). Slice 'From (Free k) AbHom -> AbHom
_
    , GeneratorTo (DiagramChainTo Point AbHom
_ (AbHom
q:|AbHom
q':|FinList n1 AbHom
Nil)) Free k' AbHom
ne' Free k'' AbHom
_ Cokernel N1 AbHom
q'Coker Kernel N1 AbHom
_ forall (k :: N'). Slice 'From (Free k) AbHom -> AbHom
lq
    ) -> Cone Dst 'Injective ('Parallel 'RightToLeft) N2 N1 AbHom
-> (Cone Dst 'Injective ('Parallel 'RightToLeft) N2 N1 AbHom
    -> AbHom)
-> Cokernel N1 AbHom
forall s (t :: DiagramType) (n :: N') (m :: N') a.
Cone s 'Injective t n m a
-> (Cone s 'Injective t n m a -> a) -> Limes s 'Injective t n m a
LimesInjective Cone Dst 'Injective ('Parallel 'RightToLeft) N2 N1 AbHom
w'Cn Cone Dst 'Injective ('Parallel 'RightToLeft) N2 N1 AbHom -> AbHom
w'Univ where

    adj :: Adjunction
  (SliceCokernelKernel (Free k') AbHom)
  (SliceFactor 'From (Free k') AbHom)
  (SliceFactor 'To (Free k') AbHom)
adj@(Adjunction SliceCokernelKernel
  (Free k')
  AbHom
  (SliceFactor 'To (Free k') AbHom)
  (SliceFactor 'From (Free k') AbHom)
lAdj SliceCokernelKernel
  (Free k')
  AbHom
  (SliceFactor 'From (Free k') AbHom)
  (SliceFactor 'To (Free k') AbHom)
_ Point (SliceFactor 'To (Free k') AbHom)
-> SliceFactor 'To (Free k') AbHom
_ Point (SliceFactor 'From (Free k') AbHom)
-> SliceFactor 'From (Free k') AbHom
_) = Free k' AbHom
-> Adjunction
     (SliceCokernelKernel (Free k') AbHom)
     (SliceFactor 'From (Free k') AbHom)
     (SliceFactor 'To (Free k') AbHom)
forall (k :: N').
Attestable k =>
Free k AbHom
-> Adjunction
     (SliceCokernelKernel (Free k) AbHom)
     (SliceFactor 'From (Free k) AbHom)
     (SliceFactor 'To (Free k) AbHom)
abhSliceFreeAdjunction Free k' AbHom
ne'
    
    q'SliceTo :: Slice 'To (Free k') AbHom
q'SliceTo = Free k' AbHom -> AbHom -> Slice 'To (Free k') AbHom
forall (i :: * -> *) c. i c -> c -> Slice 'To i c
SliceTo Free k' AbHom
ne' AbHom
q'    
    q'Coker' :: Cokernel N1 AbHom
q'Coker'  = Slice 'To (Free k') AbHom -> Cokernel N1 AbHom
forall (i :: * -> *) c.
SliceCokernelTo i c =>
Slice 'To i c -> Cokernel N1 c
sliceCokernelTo Slice 'To (Free k') AbHom
q'SliceTo
    q'L :: Point (SliceFactor 'From (Free k') AbHom)
q'L       = SliceCokernelKernel
  (Free k')
  AbHom
  (SliceFactor 'To (Free k') AbHom)
  (SliceFactor 'From (Free k') AbHom)
-> Point (SliceFactor 'To (Free k') AbHom)
-> Point (SliceFactor 'From (Free k') AbHom)
forall a b.
SliceCokernelKernel (Free k') AbHom a b -> Point a -> Point b
forall (h :: * -> * -> *) a b.
HomOriented h =>
h a b -> Point a -> Point b
pmap SliceCokernelKernel
  (Free k')
  AbHom
  (SliceFactor 'To (Free k') AbHom)
  (SliceFactor 'From (Free k') AbHom)
lAdj Point (SliceFactor 'To (Free k') AbHom)
Slice 'To (Free k') AbHom
q'SliceTo

    qSliceFrom :: Slice 'From (Free k') AbHom
qSliceFrom = Free k' AbHom -> AbHom -> Slice 'From (Free k') AbHom
forall (i :: * -> *) c. i c -> c -> Slice 'From i c
SliceFrom Free k' AbHom
ne' AbHom
q
    
    -- isomorphism with inverse qIso'
    qIso :: SliceFactor 'From (Free k') AbHom
qIso = Slice 'From (Free k') AbHom
-> Slice 'From (Free k') AbHom
-> AbHom
-> SliceFactor 'From (Free k') AbHom
forall (s :: Site) (i :: * -> *) c.
Slice s i c -> Slice s i c -> c -> SliceFactor s i c
SliceFactor Slice 'From (Free k') AbHom
qSliceFrom Point (SliceFactor 'From (Free k') AbHom)
Slice 'From (Free k') AbHom
q'L AbHom
u  where
      u :: AbHom
u = Cokernel N1 AbHom
-> Cone Dst 'Injective ('Parallel 'RightToLeft) N2 N1 AbHom
-> AbHom
forall s (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N')
       a.
Limes s p t n m a -> Cone s p t n m a -> a
universalFactor Cokernel N1 AbHom
q'Coker (Diagram ('Parallel 'RightToLeft) N2 N1 AbHom
-> AbHom
-> Cone Dst 'Injective ('Parallel 'RightToLeft) N2 N1 AbHom
forall a (m :: N').
Distributive a =>
Diagram ('Parallel 'RightToLeft) N2 m a
-> a -> Cone Dst 'Injective ('Parallel 'RightToLeft) N2 m a
ConeCokernel (Cokernel N1 AbHom -> Diagram ('Parallel 'RightToLeft) N2 N1 AbHom
forall s (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N')
       a.
Limes s p t n m a -> Diagram t n m a
diagram Cokernel N1 AbHom
q'Coker) AbHom
i)
      SliceFrom Free k' AbHom
_ AbHom
i = Point (SliceFactor 'From (Free k') AbHom)
q'L 

    qIso' :: SliceFactor 'From (Free k') AbHom
qIso' = Slice 'From (Free k') AbHom
-> Slice 'From (Free k') AbHom
-> AbHom
-> SliceFactor 'From (Free k') AbHom
forall (s :: Site) (i :: * -> *) c.
Slice s i c -> Slice s i c -> c -> SliceFactor s i c
SliceFactor Point (SliceFactor 'From (Free k') AbHom)
Slice 'From (Free k') AbHom
q'L Slice 'From (Free k') AbHom
qSliceFrom AbHom
u where
      u :: AbHom
u = Cokernel N1 AbHom
-> Cone Dst 'Injective ('Parallel 'RightToLeft) N2 N1 AbHom
-> AbHom
forall s (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N')
       a.
Limes s p t n m a -> Cone s p t n m a -> a
universalFactor Cokernel N1 AbHom
q'Coker' (Diagram ('Parallel 'RightToLeft) N2 N1 AbHom
-> AbHom
-> Cone Dst 'Injective ('Parallel 'RightToLeft) N2 N1 AbHom
forall a (m :: N').
Distributive a =>
Diagram ('Parallel 'RightToLeft) N2 m a
-> a -> Cone Dst 'Injective ('Parallel 'RightToLeft) N2 m a
ConeCokernel (Cokernel N1 AbHom -> Diagram ('Parallel 'RightToLeft) N2 N1 AbHom
forall s (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N')
       a.
Limes s p t n m a -> Diagram t n m a
diagram Cokernel N1 AbHom
q'Coker') AbHom
q)
      
    h' :: AbHom
h'        = Slice 'From (Free k') AbHom -> AbHom
forall (k :: N'). Slice 'From (Free k) AbHom -> AbHom
lq (Free k' AbHom -> AbHom -> Slice 'From (Free k') AbHom
forall (i :: * -> *) c. i c -> c -> Slice 'From i c
SliceFrom Free k' AbHom
ns' (AbHom
hAbHom -> AbHom -> AbHom
forall c. Multiplicative c => c -> c -> c
*AbHom
p))
    h'SliceTo :: Slice 'To (Free k') AbHom
h'SliceTo = Free k' AbHom -> AbHom -> Slice 'To (Free k') AbHom
forall (i :: * -> *) c. i c -> c -> Slice 'To i c
SliceTo Free k' AbHom
ne' AbHom
h'
    h'L :: Point (SliceFactor 'From (Free k') AbHom)
h'L       = SliceCokernelKernel
  (Free k')
  AbHom
  (SliceFactor 'To (Free k') AbHom)
  (SliceFactor 'From (Free k') AbHom)
-> Point (SliceFactor 'To (Free k') AbHom)
-> Point (SliceFactor 'From (Free k') AbHom)
forall a b.
SliceCokernelKernel (Free k') AbHom a b -> Point a -> Point b
forall (h :: * -> * -> *) a b.
HomOriented h =>
h a b -> Point a -> Point b
pmap SliceCokernelKernel
  (Free k')
  AbHom
  (SliceFactor 'To (Free k') AbHom)
  (SliceFactor 'From (Free k') AbHom)
lAdj Point (SliceFactor 'To (Free k') AbHom)
Slice 'To (Free k') AbHom
h'SliceTo
    h'Coker :: Cokernel N1 AbHom
h'Coker   = Slice 'To (Free k') AbHom -> Cokernel N1 AbHom
forall (i :: * -> *) c.
SliceCokernelTo i c =>
Slice 'To i c -> Cokernel N1 c
sliceCokernelTo Slice 'To (Free k') AbHom
h'SliceTo
    
    cSum :: Limes
  Mlt 'Injective 'Discrete N2 'N0 (SliceFactor 'To (Free k') AbHom)
cSum = Limits
  Mlt 'Injective 'Discrete N2 'N0 (SliceFactor 'To (Free k') AbHom)
-> Diagram 'Discrete N2 'N0 (SliceFactor 'To (Free k') AbHom)
-> Limes
     Mlt 'Injective 'Discrete N2 'N0 (SliceFactor 'To (Free k') AbHom)
forall s (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N')
       a.
Limits s p t n m a -> Diagram t n m a -> Limes s p t n m a
limes (Limits Mlt 'Injective 'Discrete N2 'N0 AbHom
-> Limits
     Mlt 'Injective 'Discrete N2 'N0 (SliceFactor 'To (Free k') AbHom)
forall c (i :: * -> *) (t :: DiagramType) (n :: N') (m :: N').
(Multiplicative c, Sliced i c) =>
Limits Mlt 'Injective t n m c
-> Limits Mlt 'Injective t n m (SliceFactor 'To i c)
slfLimitsInjective Limits Mlt 'Injective 'Discrete N2 'N0 AbHom
forall (n :: N'). Sums n AbHom
abhSums)
                 (FinList N2 (Point (SliceFactor 'To (Free k') AbHom))
-> Diagram 'Discrete N2 'N0 (SliceFactor 'To (Free k') AbHom)
forall (n :: N') a.
FinList n (Point a) -> Diagram 'Discrete n 'N0 a
DiagramDiscrete (Slice 'To (Free k') AbHom
h'SliceToSlice 'To (Free k') AbHom
-> FinList N1 (Slice 'To (Free k') AbHom)
-> FinList (N1 + 1) (Slice 'To (Free k') AbHom)
forall a (n1 :: N'). a -> FinList n1 a -> FinList (n1 + 1) a
:|Slice 'To (Free k') AbHom
q'SliceToSlice 'To (Free k') AbHom
-> FinList 'N0 (Slice 'To (Free k') AbHom)
-> FinList ('N0 + 1) (Slice 'To (Free k') AbHom)
forall a (n1 :: N'). a -> FinList n1 a -> FinList (n1 + 1) a
:|FinList 'N0 (Slice 'To (Free k') AbHom)
forall a. FinList 'N0 a
Nil))
           
    SliceFactor 'To (Free k') AbHom
_:|SliceFactor 'To (Free k') AbHom
w:|FinList n1 (SliceFactor 'To (Free k') AbHom)
Nil = Cone
  Mlt 'Injective 'Discrete N2 'N0 (SliceFactor 'To (Free k') AbHom)
-> FinList N2 (SliceFactor 'To (Free k') AbHom)
forall s (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N')
       a.
Cone s p t n m a -> FinList n a
shell (Cone
   Mlt 'Injective 'Discrete N2 'N0 (SliceFactor 'To (Free k') AbHom)
 -> FinList N2 (SliceFactor 'To (Free k') AbHom))
-> Cone
     Mlt 'Injective 'Discrete N2 'N0 (SliceFactor 'To (Free k') AbHom)
-> FinList N2 (SliceFactor 'To (Free k') AbHom)
forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ Limes
  Mlt 'Injective 'Discrete N2 'N0 (SliceFactor 'To (Free k') AbHom)
-> Cone
     Mlt 'Injective 'Discrete N2 'N0 (SliceFactor 'To (Free k') AbHom)
forall s (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N')
       a.
Limes s p t n m a -> Cone s p t n m a
universalCone Limes
  Mlt 'Injective 'Discrete N2 'N0 (SliceFactor 'To (Free k') AbHom)
cSum        

    -- the univesal cone
    w'Cn :: Cone Dst 'Injective ('Parallel 'RightToLeft) N2 N1 AbHom
w'Cn = Diagram ('Parallel 'RightToLeft) N2 N1 AbHom
-> AbHom
-> Cone Dst 'Injective ('Parallel 'RightToLeft) N2 N1 AbHom
forall a (m :: N').
Distributive a =>
Diagram ('Parallel 'RightToLeft) N2 m a
-> a -> Cone Dst 'Injective ('Parallel 'RightToLeft) N2 m a
ConeCokernel Diagram ('Parallel 'RightToLeft) N2 N1 AbHom
d AbHom
w'
    SliceFactor Slice 'From (Free k') AbHom
_ Slice 'From (Free k') AbHom
_ AbHom
w' = SliceCokernelKernel
  (Free k')
  AbHom
  (SliceFactor 'To (Free k') AbHom)
  (SliceFactor 'From (Free k') AbHom)
-> SliceFactor 'To (Free k') AbHom
-> SliceFactor 'From (Free k') AbHom
forall a b. SliceCokernelKernel (Free k') AbHom a b -> a -> b
forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
amap SliceCokernelKernel
  (Free k')
  AbHom
  (SliceFactor 'To (Free k') AbHom)
  (SliceFactor 'From (Free k') AbHom)
lAdj SliceFactor 'To (Free k') AbHom
w SliceFactor 'From (Free k') AbHom
-> SliceFactor 'From (Free k') AbHom
-> SliceFactor 'From (Free k') AbHom
forall c. Multiplicative c => c -> c -> c
* SliceFactor 'From (Free k') AbHom
qIso

    c'Sum :: Limes
  Mlt 'Injective 'Discrete N2 'N0 (SliceFactor 'From (Free k') AbHom)
c'Sum = Adjunction
  (SliceCokernelKernel (Free k') AbHom)
  (SliceFactor 'From (Free k') AbHom)
  (SliceFactor 'To (Free k') AbHom)
-> Limes
     Mlt 'Injective 'Discrete N2 'N0 (SliceFactor 'To (Free k') AbHom)
-> Limes
     Mlt 'Injective 'Discrete N2 'N0 (SliceFactor 'From (Free k') AbHom)
forall (h :: * -> * -> *) d c (t :: DiagramType) (n :: N')
       (m :: N').
Hom Mlt h =>
Adjunction h d c
-> Limes Mlt 'Injective t n m c -> Limes Mlt 'Injective t n m d
lmInjMap Adjunction
  (SliceCokernelKernel (Free k') AbHom)
  (SliceFactor 'From (Free k') AbHom)
  (SliceFactor 'To (Free k') AbHom)
adj Limes
  Mlt 'Injective 'Discrete N2 'N0 (SliceFactor 'To (Free k') AbHom)
cSum

    -- the universal factor
    w'Univ :: Cone Dst 'Injective ('Parallel 'RightToLeft) N2 N1 AbHom -> AbHom
w'Univ (ConeCokernel Diagram ('Parallel 'RightToLeft) N2 N1 AbHom
_ AbHom
x) = AbHom
f where
      SliceFactor Slice 'From (Free k') AbHom
_ Slice 'From (Free k') AbHom
_ AbHom
f = Limes
  Mlt 'Injective 'Discrete N2 'N0 (SliceFactor 'From (Free k') AbHom)
-> Cone
     Mlt 'Injective 'Discrete N2 'N0 (SliceFactor 'From (Free k') AbHom)
-> SliceFactor 'From (Free k') AbHom
forall s (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N')
       a.
Limes s p t n m a -> Cone s p t n m a -> a
universalFactor Limes
  Mlt 'Injective 'Discrete N2 'N0 (SliceFactor 'From (Free k') AbHom)
c'Sum
        (Diagram 'Discrete N2 'N0 (SliceFactor 'From (Free k') AbHom)
-> Point (SliceFactor 'From (Free k') AbHom)
-> FinList N2 (SliceFactor 'From (Free k') AbHom)
-> Cone
     Mlt 'Injective 'Discrete N2 'N0 (SliceFactor 'From (Free k') AbHom)
forall a (t :: DiagramType) (n :: N') (m :: N').
Multiplicative a =>
Diagram t n m a
-> Point a -> FinList n a -> Cone Mlt 'Injective t n m a
ConeInjective (Limes
  Mlt 'Injective 'Discrete N2 'N0 (SliceFactor 'From (Free k') AbHom)
-> Diagram 'Discrete N2 'N0 (SliceFactor 'From (Free k') AbHom)
forall s (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N')
       a.
Limes s p t n m a -> Diagram t n m a
diagram Limes
  Mlt 'Injective 'Discrete N2 'N0 (SliceFactor 'From (Free k') AbHom)
c'Sum) Point (SliceFactor 'From (Free k') AbHom)
Slice 'From (Free k') AbHom
t (SliceFactor 'From (Free k') AbHom
yFromSliceFactor 'From (Free k') AbHom
-> FinList N1 (SliceFactor 'From (Free k') AbHom)
-> FinList (N1 + 1) (SliceFactor 'From (Free k') AbHom)
forall a (n1 :: N'). a -> FinList n1 a -> FinList (n1 + 1) a
:|SliceFactor 'From (Free k') AbHom
xFrom SliceFactor 'From (Free k') AbHom
-> SliceFactor 'From (Free k') AbHom
-> SliceFactor 'From (Free k') AbHom
forall c. Multiplicative c => c -> c -> c
* SliceFactor 'From (Free k') AbHom
qIso'SliceFactor 'From (Free k') AbHom
-> FinList 'N0 (SliceFactor 'From (Free k') AbHom)
-> FinList ('N0 + 1) (SliceFactor 'From (Free k') AbHom)
forall a (n1 :: N'). a -> FinList n1 a -> FinList (n1 + 1) a
:|FinList 'N0 (SliceFactor 'From (Free k') AbHom)
forall a. FinList 'N0 a
Nil))

      xq :: AbHom
xq = AbHom
xAbHom -> AbHom -> AbHom
forall c. Multiplicative c => c -> c -> c
*AbHom
q
      t :: Slice 'From (Free k') AbHom
t = Free k' AbHom -> AbHom -> Slice 'From (Free k') AbHom
forall (i :: * -> *) c. i c -> c -> Slice 'From i c
SliceFrom Free k' AbHom
ne' AbHom
xq
      
      xFrom :: SliceFactor 'From (Free k') AbHom
xFrom = Slice 'From (Free k') AbHom
-> Slice 'From (Free k') AbHom
-> AbHom
-> SliceFactor 'From (Free k') AbHom
forall (s :: Site) (i :: * -> *) c.
Slice s i c -> Slice s i c -> c -> SliceFactor s i c
SliceFactor Slice 'From (Free k') AbHom
qSliceFrom Slice 'From (Free k') AbHom
t AbHom
x

      yFrom :: SliceFactor 'From (Free k') AbHom
yFrom = Slice 'From (Free k') AbHom
-> Slice 'From (Free k') AbHom
-> AbHom
-> SliceFactor 'From (Free k') AbHom
forall (s :: Site) (i :: * -> *) c.
Slice s i c -> Slice s i c -> c -> SliceFactor s i c
SliceFactor Point (SliceFactor 'From (Free k') AbHom)
Slice 'From (Free k') AbHom
h'L Slice 'From (Free k') AbHom
t AbHom
y

      y :: AbHom
y = Cokernel N1 AbHom
-> Cone Dst 'Injective ('Parallel 'RightToLeft) N2 N1 AbHom
-> AbHom
forall s (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N')
       a.
Limes s p t n m a -> Cone s p t n m a -> a
universalFactor Cokernel N1 AbHom
h'Coker (Diagram ('Parallel 'RightToLeft) N2 N1 AbHom
-> AbHom
-> Cone Dst 'Injective ('Parallel 'RightToLeft) N2 N1 AbHom
forall a (m :: N').
Distributive a =>
Diagram ('Parallel 'RightToLeft) N2 m a
-> a -> Cone Dst 'Injective ('Parallel 'RightToLeft) N2 m a
ConeCokernel (Cokernel N1 AbHom -> Diagram ('Parallel 'RightToLeft) N2 N1 AbHom
forall s (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N')
       a.
Limes s p t n m a -> Diagram t n m a
diagram Cokernel N1 AbHom
h'Coker) AbHom
xq)

--------------------------------------------------------------------------------
-- abhCokernels -

-- | cokernels for 'AbHom'. 
abhCokernels :: Cokernels N1 AbHom
abhCokernels :: Cokernels N1 AbHom
abhCokernels = (Diagram ('Parallel 'RightToLeft) N2 N1 AbHom -> Cokernel N1 AbHom)
-> Cokernels N1 AbHom
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 Diagram ('Parallel 'RightToLeft) N2 N1 AbHom -> Cokernel N1 AbHom
abhCokernel

--------------------------------------------------------------------------------
-- isoSmithNormal -

-- | isomorphism to its smith normal group.
--
-- __Properties__ Let @g@ be in 'AbGroup', then holds:
--
-- (1) @'start' ('isoSmithNormal' g) '==' g@.
--
-- (2) @'end' ('isoSmithNormal' g)@ is smith normal (see definition t'AbGroup').
isoSmithNormal :: AbGroup -> Inv AbHom
isoSmithNormal :: AbGroup -> Inv AbHom
isoSmithNormal AbGroup
g = AbHom -> AbHom -> Inv AbHom
forall c. c -> c -> Inv c
Inv AbHom
h AbHom
h' where
  c :: Cokernel N1 AbHom
c  = Cokernels N1 AbHom
-> Diagram ('Parallel 'RightToLeft) N2 N1 AbHom
-> Cokernel N1 AbHom
forall s (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N')
       a.
Limits s p t n m a -> Diagram t n m a -> Limes s p t n m a
limes Cokernels N1 AbHom
abhCokernels (AbHom -> Diagram ('Parallel 'RightToLeft) N2 N1 AbHom
forall c. Oriented c => c -> CokernelDiagram N1 c
cokernelDiagram (Root AbHom -> AbHom
forall a. Additive a => Root a -> a
zero (Point AbGroup -> AbGroup
forall c. Multiplicative c => Point c -> c
one ()AbGroup -> AbGroup -> Orientation AbGroup
forall p. p -> p -> Orientation p
:>AbGroup
g)))
  h :: AbHom
h  = Cone Dst 'Injective ('Parallel 'RightToLeft) N2 N1 AbHom -> AbHom
forall c. CokernelCone N1 c -> c
cokernelFactor (Cone Dst 'Injective ('Parallel 'RightToLeft) N2 N1 AbHom -> AbHom)
-> Cone Dst 'Injective ('Parallel 'RightToLeft) N2 N1 AbHom
-> AbHom
forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ Cokernel N1 AbHom
-> Cone Dst 'Injective ('Parallel 'RightToLeft) N2 N1 AbHom
forall s (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N')
       a.
Limes s p t n m a -> Cone s p t n m a
universalCone Cokernel N1 AbHom
c
  h' :: AbHom
h' = Cokernel N1 AbHom
-> Cone Dst 'Injective ('Parallel 'RightToLeft) N2 N1 AbHom
-> AbHom
forall s (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N')
       a.
Limes s p t n m a -> Cone s p t n m a -> a
universalFactor Cokernel N1 AbHom
c (Diagram ('Parallel 'RightToLeft) N2 N1 AbHom
-> AbHom
-> Cone Dst 'Injective ('Parallel 'RightToLeft) N2 N1 AbHom
forall a (m :: N').
Distributive a =>
Diagram ('Parallel 'RightToLeft) N2 m a
-> a -> Cone Dst 'Injective ('Parallel 'RightToLeft) N2 m a
ConeCokernel (Cokernel N1 AbHom -> Diagram ('Parallel 'RightToLeft) N2 N1 AbHom
forall s (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N')
       a.
Limes s p t n m a -> Diagram t n m a
diagram Cokernel N1 AbHom
c) (Point AbHom -> AbHom
forall c. Multiplicative c => Point c -> c
one Point AbHom
AbGroup
g))