{-# LANGUAGE NoImplicitPrelude #-}

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

-- |
-- Module      : OAlg.AbelianGroup.Definition
-- Description : homomorphisms between finitely generated abelian groups
-- Copyright   : (c) Erich Gut
-- License     : BSD3
-- Maintainer  : zerich.gut@gmail.com
--
-- homomorphisms between finitely generated abelian groups.
module OAlg.AbelianGroup.Definition
  ( -- * Abelian Group
    AbGroup(..), abg, isSmithNormal
  , abgDim

    -- * Homomorphism
  , AbHom(..)
  , abh, abh'
  , abhz, zabh

    -- * Adjunction
  , abhFreeAdjunction
  , AbHomFree(..)

    -- * Limes
  , abhProducts, abhSums

    -- * Generator
  , abgGeneratorTo

    -- * X
  , xAbHom, xAbHomTo, xAbHomFrom
  , stdMaxDim

    -- * Proposition
  , prpAbHom
  ) where

import Control.Monad
import Control.Applicative ((<|>))

import Data.List (foldl,(++),filter,takeWhile,zip)
import Data.Typeable

import OAlg.Prelude

import OAlg.Data.Canonical
import OAlg.Data.Reducible
import OAlg.Data.Constructable

import OAlg.Category.Path as C

import OAlg.Structure.Oriented
import OAlg.Structure.Multiplicative
import OAlg.Structure.Fibred
import OAlg.Structure.Additive
import OAlg.Structure.Vectorial
import OAlg.Structure.Distributive
import OAlg.Structure.Algebraic
import OAlg.Structure.Exponential
import OAlg.Structure.Number
import OAlg.Structure.Operational

import OAlg.Hom.Oriented
import OAlg.Hom.Multiplicative
import OAlg.Hom.Fibred
import OAlg.Hom.Additive
import OAlg.Hom.Distributive

import OAlg.Limes.Limits
import OAlg.Limes.Definition
import OAlg.Limes.Cone
import OAlg.Limes.ProductsAndSums as L
import OAlg.Limes.KernelsAndCokernels

import OAlg.Adjunction

import OAlg.Entity.Natural hiding ((++))
import OAlg.Entity.FinList hiding ((++),zip)
import OAlg.Entity.Diagram
import OAlg.Entity.Sequence
import OAlg.Entity.Matrix
import OAlg.Entity.Product
import OAlg.Entity.Slice

import OAlg.Data.Generator

import OAlg.AbelianGroup.ZMod
import OAlg.AbelianGroup.Euclid

--------------------------------------------------------------------------------
-- AbGroup -

-- | finitely generate abelian group, i.e. the cartesian product of cyclic groups @'Z'\/n@
--   and are represented as a formal product with symbols in t'ZMod'.
--
-- __Definition__ Let @g@ be in t'AbGroup'. We call @g@ __/smith normal/__ if and only if
-- there exists a sequence @n 0, n 1 .. n (k-1)@ in 'N' with length @k@ and a exponent
-- @r@ in 'N' such that:
--
-- (1) @2 '<=' n i@ for all @0 '<=' i < k@.
--
-- (2) @n (i v'+' 1) `mod` n i '==' 0@ for all @i@ in @0 '<=' i < k-1@.
--
-- (3) @g '==' 'abg' (n 0) v'*' 'abg' (n 1) v'*' .. v'*' 'abg' (n (k-1)) v'*' 'abg' 0 '^' r@.
--
-- __Theorem__ Every finitely generated abelian group is isomorphic to a group in
-- smith normal form. This isomorphism is given by
-- 'OAlg.AbelianGroup.KernelsAndCokernels.isoSmithNormal'.
--
--  __Examples__ Finitely generated abelian groups constructed via 'abg' and its
--  multiplicative structure:
--
-- >>> abg 12
-- AbGroup[Z/12]
--
-- represents the cyclic group @'Z'/12@.
--
-- >>> abg 2 * abg 3
-- AbGroup[Z/2*Z/3]
--
-- represents the cartesian product of the groups @'Z'\/2@ and @'Z'\/3@.
--
-- >>> abg 6 * abg 4 * abg 4
-- AbGroup[Z/6*Z/4^2]
--
-- represents the cartesian product of the groups @'Z'\/6@, @'Z'\/4@  and @'Z'\/4@.
--
-- >>> abg 0 ^ 6
-- AbGroup[Z^6]
-- 
-- represents the free abelian group  @'Z' '^' 6@ of /dimension/ 6.
--
-- >>> one () :: AbGroup
-- AbGroup[]
--
-- represents the cartesian product of zero cyclic groups and
--
-- >>> one () * abg 4 * abg 6 == abg 4 * abg 6
-- True
--
--
-- __Examples__ Checking for smith normal via 'isSmithNormal':
--
-- >>> isSmithNormal (abg 4)
-- True
--
-- >>> isSmithNormal (abg 2 * abg 2)
-- True
--
-- >>> isSmithNormal (abg 17 * abg 51)
-- True
--
-- >>> isSmithNormal (abg 2 * abg 4 * abg 0 ^ 3)
-- True
--
-- >>> isSmithNormal (abg 5 * abg 3)
-- False
--
-- >>> isSmithNormal (abg 0 * abg 3 * abg 6)
-- False
--
-- >>> isSmithNormal (abg 1 * abg 4)
-- False
--
-- >>> isSmithNormal (one ())
-- True
--
-- __Examples__ The associated isomorphism in 'AbHom' of a finitely generated abelian group
-- given by 'OAlg.AbelianGroup.KernelsAndCokernels.isoSmithNormal'.
--
-- >>> end (isoSmithNormal (abg 3 * abg 5))
-- AbGroup[Z/15]
--
-- >>> end (isoSmithNormal (abg 2 * abg 4 * abg 2))
-- AbGroup[Z/2^2*Z/4]
--
-- >>> end (isoSmithNormal (abg 4 * abg 6))
-- AbGroup[Z/2*Z/12]
--
-- >>> end (isoSmithNormal (abg 1))
-- AbGroup[]
newtype AbGroup = AbGroup (ProductSymbol ZMod)
  deriving (AbGroup -> AbGroup -> Bool
(AbGroup -> AbGroup -> Bool)
-> (AbGroup -> AbGroup -> Bool) -> Eq AbGroup
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: AbGroup -> AbGroup -> Bool
== :: AbGroup -> AbGroup -> Bool
$c/= :: AbGroup -> AbGroup -> Bool
/= :: AbGroup -> AbGroup -> Bool
Eq,Eq AbGroup
Eq AbGroup =>
(AbGroup -> AbGroup -> Ordering)
-> (AbGroup -> AbGroup -> Bool)
-> (AbGroup -> AbGroup -> Bool)
-> (AbGroup -> AbGroup -> Bool)
-> (AbGroup -> AbGroup -> Bool)
-> (AbGroup -> AbGroup -> AbGroup)
-> (AbGroup -> AbGroup -> AbGroup)
-> Ord AbGroup
AbGroup -> AbGroup -> Bool
AbGroup -> AbGroup -> Ordering
AbGroup -> AbGroup -> AbGroup
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: AbGroup -> AbGroup -> Ordering
compare :: AbGroup -> AbGroup -> Ordering
$c< :: AbGroup -> AbGroup -> Bool
< :: AbGroup -> AbGroup -> Bool
$c<= :: AbGroup -> AbGroup -> Bool
<= :: AbGroup -> AbGroup -> Bool
$c> :: AbGroup -> AbGroup -> Bool
> :: AbGroup -> AbGroup -> Bool
$c>= :: AbGroup -> AbGroup -> Bool
>= :: AbGroup -> AbGroup -> Bool
$cmax :: AbGroup -> AbGroup -> AbGroup
max :: AbGroup -> AbGroup -> AbGroup
$cmin :: AbGroup -> AbGroup -> AbGroup
min :: AbGroup -> AbGroup -> AbGroup
Ord,AbGroup -> N
(AbGroup -> N) -> LengthN AbGroup
forall x. (x -> N) -> LengthN x
$clengthN :: AbGroup -> N
lengthN :: AbGroup -> N
LengthN,AbGroup -> Statement
(AbGroup -> Statement) -> Validable AbGroup
forall a. (a -> Statement) -> Validable a
$cvalid :: AbGroup -> Statement
valid :: AbGroup -> Statement
Validable,Eq AbGroup
Show AbGroup
Typeable AbGroup
Validable AbGroup
(Show AbGroup, Eq AbGroup, Validable AbGroup, Typeable AbGroup) =>
Entity AbGroup
forall a. (Show a, Eq a, Validable a, Typeable a) => Entity a
Entity,Oriented AbGroup
Oriented AbGroup =>
(Point AbGroup -> AbGroup)
-> (AbGroup -> AbGroup -> AbGroup)
-> (AbGroup -> N -> AbGroup)
-> Multiplicative AbGroup
Point AbGroup -> AbGroup
AbGroup -> N -> AbGroup
AbGroup -> AbGroup -> AbGroup
forall c.
Oriented c =>
(Point c -> c)
-> (c -> c -> c) -> (c -> N -> c) -> Multiplicative c
$cone :: Point AbGroup -> AbGroup
one :: Point AbGroup -> AbGroup
$c* :: AbGroup -> AbGroup -> AbGroup
* :: AbGroup -> AbGroup -> AbGroup
$cnpower :: AbGroup -> N -> AbGroup
npower :: AbGroup -> N -> AbGroup
Multiplicative)

instance Show AbGroup where
  show :: AbGroup -> String
show (AbGroup ProductSymbol ZMod
g) = String
"AbGroup[" String -> ShowS
forall a. [a] -> [a] -> [a]
++ ProductSymbol ZMod -> String
forall x. Entity x => ProductSymbol x -> String
psyShow ProductSymbol ZMod
g String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"]"
    

instance Oriented AbGroup where
  type Point AbGroup = ()
  orientation :: AbGroup -> Orientation (Point AbGroup)
orientation (AbGroup ProductSymbol ZMod
g) = ProductSymbol ZMod -> Orientation (Point (ProductSymbol ZMod))
forall q. Oriented q => q -> Orientation (Point q)
orientation ProductSymbol ZMod
g

instance Exponential AbGroup where
  type Exponent AbGroup = N
  ^ :: AbGroup -> Exponent AbGroup -> AbGroup
(^) = AbGroup -> N -> AbGroup
AbGroup -> Exponent AbGroup -> AbGroup
forall c. Multiplicative c => c -> N -> c
npower

--------------------------------------------------------------------------------
-- abg -

-- | the cyclic group of the given order as a finitely generated abelian group.
abg :: N -> AbGroup
abg :: N -> AbGroup
abg = ProductSymbol ZMod -> AbGroup
AbGroup (ProductSymbol ZMod -> AbGroup)
-> (N -> ProductSymbol ZMod) -> N -> AbGroup
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
. ZMod -> ProductSymbol ZMod
forall x. Entity x => x -> ProductSymbol x
sy (ZMod -> ProductSymbol ZMod)
-> (N -> ZMod) -> N -> ProductSymbol 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
. N -> ZMod
ZMod

--------------------------------------------------------------------------------
-- abgxs -

-- | the indexed listing of the 'ZMod's.
abgxs :: AbGroup -> [(ZMod,N)]
abgxs :: AbGroup -> [(ZMod, N)]
abgxs (AbGroup ProductSymbol ZMod
g) = ProductSymbol ZMod -> [(ZMod, N)]
forall x. ProductSymbol x -> [(x, N)]
psyxs ProductSymbol ZMod
g

--------------------------------------------------------------------------------
-- isSmithNormal -

-- | checks if the given group is smith normal (see definition 'AbGroup').
isSmithNormal :: AbGroup -> Bool
isSmithNormal :: AbGroup -> Bool
isSmithNormal (AbGroup ProductSymbol ZMod
g) = [ZMod] -> Bool
sn (((ZMod, N) -> ZMod) -> [(ZMod, N)] -> [ZMod]
forall a b. (a -> b) -> [a] -> [b]
forall (h :: * -> * -> *) (f :: * -> *) a b.
Applicative1 h f =>
h a b -> f a -> f b
amap1 (ZMod, N) -> ZMod
forall a b. (a, b) -> a
fst [(ZMod, N)]
ws) where
  Word [(ZMod, N)]
ws = ProductSymbol ZMod -> Word N ZMod
forall x. Entity x => ProductSymbol x -> Word N x
psywrd ProductSymbol ZMod
g

  sn :: [ZMod] -> Bool
sn [ZMod N
n,ZMod N
n']    = [Bool] -> Bool
forall b. Boolean b => [b] -> b
and [N
2 N -> N -> Bool
forall a. Ord a => a -> a -> Bool
<= N
n,(N
n' N -> N -> Bool
forall a. Eq a => a -> a -> Bool
== N
0) Bool -> Bool -> Bool
forall b. Boolean b => b -> b -> b
|| (N
n' N -> N -> N
forall a. Integral a => a -> a -> a
`mod` N
n N -> N -> Bool
forall a. Eq a => a -> a -> Bool
== N
0)]
  sn (ZMod N
n:ZMod N
n':[ZMod]
ws) = [Bool] -> Bool
forall b. Boolean b => [b] -> b
and [N
2 N -> N -> Bool
forall a. Ord a => a -> a -> Bool
<= N
n,N
n' N -> N -> N
forall a. Integral a => a -> a -> a
`mod` N
n N -> N -> Bool
forall a. Eq a => a -> a -> Bool
== N
0,[ZMod] -> Bool
sn (N -> ZMod
ZMod N
n'ZMod -> [ZMod] -> [ZMod]
forall a. a -> [a] -> [a]
:[ZMod]
ws)]
  sn [ZMod N
n]            = (N
2 N -> N -> Bool
forall a. Ord a => a -> a -> Bool
<= N
n) Bool -> Bool -> Bool
forall b. Boolean b => b -> b -> b
|| (N
n N -> N -> Bool
forall a. Eq a => a -> a -> Bool
== N
0)
  sn [ZMod]
_                   = Bool
True


--------------------------------------------------------------------------------
-- AbHom -

-- | additive homomorphism between finitely generated abelian groups which are
-- represented by matrices over 'ZModHom'.
newtype AbHom = AbHom (Matrix ZModHom)
  deriving (Int -> AbHom -> ShowS
[AbHom] -> ShowS
AbHom -> String
(Int -> AbHom -> ShowS)
-> (AbHom -> String) -> ([AbHom] -> ShowS) -> Show AbHom
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> AbHom -> ShowS
showsPrec :: Int -> AbHom -> ShowS
$cshow :: AbHom -> String
show :: AbHom -> String
$cshowList :: [AbHom] -> ShowS
showList :: [AbHom] -> ShowS
Show,AbHom -> AbHom -> Bool
(AbHom -> AbHom -> Bool) -> (AbHom -> AbHom -> Bool) -> Eq AbHom
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: AbHom -> AbHom -> Bool
== :: AbHom -> AbHom -> Bool
$c/= :: AbHom -> AbHom -> Bool
/= :: AbHom -> AbHom -> Bool
Eq,AbHom -> Statement
(AbHom -> Statement) -> Validable AbHom
forall a. (a -> Statement) -> Validable a
$cvalid :: AbHom -> Statement
valid :: AbHom -> Statement
Validable,Eq AbHom
Show AbHom
Typeable AbHom
Validable AbHom
(Show AbHom, Eq AbHom, Validable AbHom, Typeable AbHom) =>
Entity AbHom
forall a. (Show a, Eq a, Validable a, Typeable a) => Entity a
Entity)

--------------------------------------------------------------------------------
-- abgDim -

-- | the associated dimension for matrices of 'ZModHom'.
abgDim :: AbGroup -> Dim' ZModHom
abgDim :: AbGroup -> Dim' ZModHom
abgDim (AbGroup ProductSymbol ZMod
g) = CSequence (Point ZModHom) -> Dim' ZModHom
forall x. CSequence (Point x) -> Dim x (Point x)
Dim CSequence (Point ZModHom)
ProductSymbol ZMod
g

--------------------------------------------------------------------------------
-- abhz -

-- | the underlying 'Z'-matrix.
abhz :: AbHom -> Matrix Z
abhz :: AbHom -> Matrix Z
abhz (AbHom (Matrix Dim' ZModHom
r Dim' ZModHom
c Entries N N ZModHom
xs)) = Dim' Z -> Dim' Z -> Entries N N Z -> Matrix Z
forall x. Dim' x -> Dim' x -> Entries N N x -> Matrix x
Matrix Dim Z ()
Dim' Z
r' Dim Z ()
Dim' Z
c' Entries N N Z
xs' where
  u :: Dim Z ()
u = () -> Dim Z ()
forall p x. (Entity p, p ~ Point x) => p -> Dim x p
dim ()
  r' :: Dim Z ()
r' = Dim Z ()
u Dim Z () -> Exponent (Dim Z ()) -> Dim Z ()
forall f. Exponential f => f -> Exponent f -> f
^ Dim ZModHom ZMod -> N
forall x. LengthN x => x -> N
lengthN Dim' ZModHom
Dim ZModHom ZMod
r
  c' :: Dim Z ()
c' = Dim Z ()
u Dim Z () -> Exponent (Dim Z ()) -> Dim Z ()
forall f. Exponential f => f -> Exponent f -> f
^ Dim ZModHom ZMod -> N
forall x. LengthN x => x -> N
lengthN Dim' ZModHom
Dim ZModHom ZMod
c

  xs' :: Entries N N Z
xs' = (ZModHom -> Z) -> Entries N N ZModHom -> Entries N N Z
forall a b. (a -> b) -> Entries N N a -> Entries N N b
forall (h :: * -> * -> *) (f :: * -> *) a b.
Applicative1 h f =>
h a b -> f a -> f b
amap1 ZModHom -> Z
toZ Entries N N ZModHom
xs

--------------------------------------------------------------------------------
-- zabh -

-- | the associated homomorphism between products of @'abg' 0@ given by the column
-- - respectively row - length.
zabh :: Matrix Z -> AbHom
zabh :: Matrix Z -> AbHom
zabh (Matrix Dim' Z
r Dim' Z
c Entries N N Z
xs) = Matrix ZModHom -> AbHom
AbHom (Dim' ZModHom
-> Dim' ZModHom -> Entries N N ZModHom -> Matrix ZModHom
forall x. Dim' x -> Dim' x -> Entries N N x -> Matrix x
Matrix Dim' ZModHom
Dim ZModHom ZMod
r' Dim' ZModHom
Dim ZModHom ZMod
c' Entries N N ZModHom
xs') where
  u :: Dim ZModHom ZMod
u = ZMod -> Dim ZModHom ZMod
forall p x. (Entity p, p ~ Point x) => p -> Dim x p
dim (N -> ZMod
ZMod N
0)
  r' :: Dim ZModHom ZMod
r' = Dim ZModHom ZMod
u Dim ZModHom ZMod -> Exponent (Dim ZModHom ZMod) -> Dim ZModHom ZMod
forall f. Exponential f => f -> Exponent f -> f
^ Dim Z () -> N
forall x. LengthN x => x -> N
lengthN Dim Z ()
Dim' Z
r
  c' :: Dim ZModHom ZMod
c' = Dim ZModHom ZMod
u Dim ZModHom ZMod -> Exponent (Dim ZModHom ZMod) -> Dim ZModHom ZMod
forall f. Exponential f => f -> Exponent f -> f
^ Dim Z () -> N
forall x. LengthN x => x -> N
lengthN Dim Z ()
Dim' Z
c

  xs' :: Entries N N ZModHom
xs' = (Z -> ZModHom) -> Entries N N Z -> Entries N N ZModHom
forall a b. (a -> b) -> Entries N N a -> Entries N N b
forall (h :: * -> * -> *) (f :: * -> *) a b.
Applicative1 h f =>
h a b -> f a -> f b
amap1 Z -> ZModHom
fromZ Entries N N Z
xs

--------------------------------------------------------------------------------
-- AbHom - Algebraic -

instance Oriented AbHom where
  type Point AbHom = AbGroup
  orientation :: AbHom -> Orientation (Point AbHom)
orientation (AbHom Matrix ZModHom
h) = ProductSymbol ZMod -> AbGroup
AbGroup ProductSymbol ZMod
s AbGroup -> AbGroup -> Orientation AbGroup
forall p. p -> p -> Orientation p
:> ProductSymbol ZMod -> AbGroup
AbGroup ProductSymbol ZMod
e where
    Dim CSequence (Point ZModHom)
ProductSymbol ZMod
s :> Dim CSequence (Point ZModHom)
ProductSymbol ZMod
e = Matrix ZModHom -> Orientation (Point (Matrix ZModHom))
forall q. Oriented q => q -> Orientation (Point q)
orientation Matrix ZModHom
h

instance Multiplicative AbHom where
  one :: Point AbHom -> AbHom
one = Matrix ZModHom -> AbHom
AbHom (Matrix ZModHom -> AbHom)
-> (AbGroup -> Matrix ZModHom) -> AbGroup -> 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
. Point (Matrix ZModHom) -> Matrix ZModHom
Dim ZModHom ZMod -> Matrix ZModHom
forall c. Multiplicative c => Point c -> c
one (Dim ZModHom ZMod -> Matrix ZModHom)
-> (AbGroup -> Dim ZModHom ZMod) -> AbGroup -> Matrix 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
. AbGroup -> Dim' ZModHom
AbGroup -> Dim ZModHom ZMod
abgDim
  AbHom Matrix ZModHom
f * :: AbHom -> AbHom -> AbHom
* AbHom Matrix ZModHom
g = Matrix ZModHom -> AbHom
AbHom (Matrix ZModHom
fMatrix ZModHom -> Matrix ZModHom -> Matrix ZModHom
forall c. Multiplicative c => c -> c -> c
*Matrix ZModHom
g)
  npower :: AbHom -> N -> AbHom
npower (AbHom Matrix ZModHom
h) N
n = Matrix ZModHom -> AbHom
AbHom (Matrix ZModHom -> N -> Matrix ZModHom
forall c. Multiplicative c => c -> N -> c
npower Matrix ZModHom
h N
n)

instance Fibred AbHom where
  type Root AbHom = Orientation AbGroup

instance Additive AbHom where
  zero :: Root AbHom -> AbHom
zero (AbGroup
s :> AbGroup
e) = Matrix ZModHom -> AbHom
AbHom (Root (Matrix ZModHom) -> Matrix ZModHom
forall a. Additive a => Root a -> a
zero (AbGroup -> Dim' ZModHom
abgDim AbGroup
s Dim ZModHom ZMod
-> Dim ZModHom ZMod -> Orientation (Dim ZModHom ZMod)
forall p. p -> p -> Orientation p
:> AbGroup -> Dim' ZModHom
abgDim AbGroup
e))
  AbHom Matrix ZModHom
a + :: AbHom -> AbHom -> AbHom
+ AbHom Matrix ZModHom
b = Matrix ZModHom -> AbHom
AbHom (Matrix ZModHom
aMatrix ZModHom -> Matrix ZModHom -> Matrix ZModHom
forall a. Additive a => a -> a -> a
+Matrix ZModHom
b)
  ntimes :: N -> AbHom -> AbHom
ntimes N
n (AbHom Matrix ZModHom
a) = Matrix ZModHom -> AbHom
AbHom (N -> Matrix ZModHom -> Matrix ZModHom
forall a. Additive a => N -> a -> a
ntimes N
n Matrix ZModHom
a)

instance Abelian AbHom where
  negate :: AbHom -> AbHom
negate (AbHom Matrix ZModHom
a) = Matrix ZModHom -> AbHom
AbHom (Matrix ZModHom -> Matrix ZModHom
forall a. Abelian a => a -> a
negate Matrix ZModHom
a)
  AbHom Matrix ZModHom
a - :: AbHom -> AbHom -> AbHom
- AbHom Matrix ZModHom
b = Matrix ZModHom -> AbHom
AbHom (Matrix ZModHom
aMatrix ZModHom -> Matrix ZModHom -> Matrix ZModHom
forall a. Abelian a => a -> a -> a
-Matrix ZModHom
b)
  ztimes :: Z -> AbHom -> AbHom
ztimes Z
z (AbHom Matrix ZModHom
a) = Matrix ZModHom -> AbHom
AbHom (Z -> Matrix ZModHom -> Matrix ZModHom
forall a. Abelian a => Z -> a -> a
ztimes Z
z Matrix ZModHom
a)
  
instance Vectorial AbHom where
  type Scalar AbHom = Z
  ! :: Scalar AbHom -> AbHom -> AbHom
(!) = Z -> AbHom -> AbHom
Scalar AbHom -> AbHom -> AbHom
forall a. Abelian a => Z -> a -> a
ztimes

instance FibredOriented AbHom
instance Distributive AbHom
instance Algebraic AbHom

--------------------------------------------------------------------------------
-- abh -

-- | the additive homomorphism with the given orientation and 'ZModHom'-entries.
abh :: Orientation AbGroup -> [(ZModHom,N,N)] -> AbHom
abh :: Orientation AbGroup -> [(ZModHom, N, N)] -> AbHom
abh (AbGroup
s :> AbGroup
e) [(ZModHom, N, N)]
xs = Matrix ZModHom -> AbHom
AbHom (Matrix ZModHom -> AbHom) -> Matrix ZModHom -> AbHom
forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ 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 (AbGroup -> Dim' ZModHom
abgDim AbGroup
e) (AbGroup -> Dim' ZModHom
abgDim AbGroup
s) [(ZModHom, N, N)]
xs 

-- | the additive homomorphism with the given orientation and 'Z'-entries.
abh' :: Orientation AbGroup -> [(Z,N,N)] -> AbHom
abh' :: Orientation AbGroup -> [(Z, N, N)] -> AbHom
abh' o :: Orientation AbGroup
o@(AbGroup
s :> AbGroup
e) [(Z, N, N)]
xs = Orientation AbGroup -> [(ZModHom, N, N)] -> AbHom
abh Orientation AbGroup
o [(ZModHom, N, N)]
xs' where
  xs' :: [(ZModHom, N, N)]
xs' = ((Z, N, N) -> (ZModHom, N, N)) -> [(Z, N, N)] -> [(ZModHom, N, N)]
forall a b. (a -> b) -> [a] -> [b]
forall (h :: * -> * -> *) (f :: * -> *) a b.
Applicative1 h f =>
h a b -> f a -> f b
amap1 (\(Z
r,N
i,N
j) -> (Orientation ZMod -> Z -> ZModHom
zmh (N -> ZMod
s' N
j ZMod -> ZMod -> Orientation ZMod
forall p. p -> p -> Orientation p
:> N -> ZMod
e' N
i) Z
r,N
i,N
j)) [(Z, N, N)]
xs
  s' :: N -> ZMod
s' N
j = Maybe ZMod -> ZMod
forall a. HasCallStack => Maybe a -> a
fromJust (ProductSymbol ZMod
sp ProductSymbol ZMod -> N -> Maybe ZMod
forall (s :: * -> *) i x. Sequence s i x => s x -> i -> Maybe x
?? N
j)
  e' :: N -> ZMod
e' N
i = Maybe ZMod -> ZMod
forall a. HasCallStack => Maybe a -> a
fromJust (ProductSymbol ZMod
ep ProductSymbol ZMod -> N -> Maybe ZMod
forall (s :: * -> *) i x. Sequence s i x => s x -> i -> Maybe x
?? N
i)
  AbGroup ProductSymbol ZMod
sp = AbGroup
s
  AbGroup ProductSymbol ZMod
ep = AbGroup
e

--------------------------------------------------------------------------------
-- AbHomMap -

-- | morphisms between 'AbHom' and the underlying @'Matrix' 'ZModHom'@ which constitute
-- isomorphisms (see 'IsoAbHomMap').
data AbHomMap x y where
  AbHomMatrix :: AbHomMap AbHom (Matrix ZModHom)
  MatrixAbHom :: AbHomMap (Matrix ZModHom) AbHom

--------------------------------------------------------------------------------
-- AbHomMap - Entity -

deriving instance Show (AbHomMap x y)
instance Show2 AbHomMap
deriving instance Eq (AbHomMap x y)
instance Eq2 AbHomMap

instance Validable (AbHomMap x y) where
  valid :: AbHomMap x y -> Statement
valid AbHomMap x y
AbHomMatrix = Statement
SValid
  valid AbHomMap x y
MatrixAbHom = Statement
SValid

instance Validable2 AbHomMap

instance (Typeable x, Typeable y) => Entity (AbHomMap x y)
instance Entity2 AbHomMap

--------------------------------------------------------------------------------
-- invAbHomMap -

-- | the inverse.
invAbHomMap :: AbHomMap x y -> AbHomMap y x
invAbHomMap :: forall x y. AbHomMap x y -> AbHomMap y x
invAbHomMap AbHomMap x y
AbHomMatrix = AbHomMap y x
AbHomMap (Matrix ZModHom) AbHom
MatrixAbHom
invAbHomMap AbHomMap x y
MatrixAbHom = AbHomMap y x
AbHomMap AbHom (Matrix ZModHom)
AbHomMatrix

--------------------------------------------------------------------------------
-- AbHomMap - HomAlgebraic -

instance Morphism AbHomMap where
  type ObjectClass AbHomMap = Alg Z
  homomorphous :: forall x y. AbHomMap x y -> Homomorphous (ObjectClass AbHomMap) x y
homomorphous AbHomMap x y
AbHomMatrix = Struct (Alg Z) x
forall s x. Structure s x => Struct s x
Struct Struct (Alg Z) x -> Struct (Alg Z) y -> Homomorphous (Alg Z) x y
forall s x y. Struct s x -> Struct s y -> Homomorphous s x y
:>: Struct (Alg Z) y
forall s x. Structure s x => Struct s x
Struct
  homomorphous AbHomMap x y
MatrixAbHom = Struct (Alg Z) x
forall s x. Structure s x => Struct s x
Struct Struct (Alg Z) x -> Struct (Alg Z) y -> Homomorphous (Alg Z) x y
forall s x y. Struct s x -> Struct s y -> Homomorphous s x y
:>: Struct (Alg Z) y
forall s x. Structure s x => Struct s x
Struct

instance EmbeddableMorphism AbHomMap Ort
instance EmbeddableMorphism AbHomMap Typ
instance EmbeddableMorphismTyp AbHomMap

instance Applicative AbHomMap where
  amap :: forall a b. AbHomMap a b -> a -> b
amap AbHomMap a b
AbHomMatrix (AbHom Matrix ZModHom
m) = b
Matrix ZModHom
m
  amap AbHomMap a b
MatrixAbHom a
m = Matrix ZModHom -> AbHom
AbHom a
Matrix ZModHom
m

instance HomOriented AbHomMap where
  pmap :: forall a b. AbHomMap a b -> Point a -> Point b
pmap AbHomMap a b
AbHomMatrix (AbGroup ProductSymbol ZMod
g) = CSequence (Point ZModHom) -> Dim' ZModHom
forall x. CSequence (Point x) -> Dim x (Point x)
Dim CSequence (Point ZModHom)
ProductSymbol ZMod
g
  pmap AbHomMap a b
MatrixAbHom (Dim CSequence (Point ZModHom)
g) = ProductSymbol ZMod -> AbGroup
AbGroup CSequence (Point ZModHom)
ProductSymbol ZMod
g

instance EmbeddableMorphism AbHomMap Mlt
instance HomMultiplicative AbHomMap

--------------------------------------------------------------------------------
-- PathAbHomMap -

-- | paths of 'AbHomMap'.
type PathAbHomMap = C.Path AbHomMap

--------------------------------------------------------------------------------
-- IsoAbHomMap -

-- | isomorphisms between 'AbHom' and @'Matrix' 'ZModHom'@.
newtype IsoAbHomMap x y = IsoAbHomMap (PathAbHomMap x y)
  deriving (Int -> IsoAbHomMap x y -> ShowS
[IsoAbHomMap x y] -> ShowS
IsoAbHomMap x y -> String
(Int -> IsoAbHomMap x y -> ShowS)
-> (IsoAbHomMap x y -> String)
-> ([IsoAbHomMap x y] -> ShowS)
-> Show (IsoAbHomMap x y)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall x y. Int -> IsoAbHomMap x y -> ShowS
forall x y. [IsoAbHomMap x y] -> ShowS
forall x y. IsoAbHomMap x y -> String
$cshowsPrec :: forall x y. Int -> IsoAbHomMap x y -> ShowS
showsPrec :: Int -> IsoAbHomMap x y -> ShowS
$cshow :: forall x y. IsoAbHomMap x y -> String
show :: IsoAbHomMap x y -> String
$cshowList :: forall x y. [IsoAbHomMap x y] -> ShowS
showList :: [IsoAbHomMap x y] -> ShowS
Show,(forall x y. IsoAbHomMap x y -> String) -> Show2 IsoAbHomMap
forall x y. IsoAbHomMap x y -> String
forall (h :: * -> * -> *). (forall a b. h a b -> String) -> Show2 h
$cshow2 :: forall x y. IsoAbHomMap x y -> String
show2 :: forall x y. IsoAbHomMap x y -> String
Show2,IsoAbHomMap x y -> Statement
(IsoAbHomMap x y -> Statement) -> Validable (IsoAbHomMap x y)
forall a. (a -> Statement) -> Validable a
forall x y. IsoAbHomMap x y -> Statement
$cvalid :: forall x y. IsoAbHomMap x y -> Statement
valid :: IsoAbHomMap x y -> Statement
Validable,(forall x y. IsoAbHomMap x y -> Statement)
-> Validable2 IsoAbHomMap
forall x y. IsoAbHomMap x y -> Statement
forall (h :: * -> * -> *).
(forall x y. h x y -> Statement) -> Validable2 h
$cvalid2 :: forall x y. IsoAbHomMap x y -> Statement
valid2 :: forall x y. IsoAbHomMap x y -> Statement
Validable2,IsoAbHomMap x y -> IsoAbHomMap x y -> Bool
(IsoAbHomMap x y -> IsoAbHomMap x y -> Bool)
-> (IsoAbHomMap x y -> IsoAbHomMap x y -> Bool)
-> Eq (IsoAbHomMap x y)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall x y. IsoAbHomMap x y -> IsoAbHomMap x y -> Bool
$c== :: forall x y. IsoAbHomMap x y -> IsoAbHomMap x y -> Bool
== :: IsoAbHomMap x y -> IsoAbHomMap x y -> Bool
$c/= :: forall x y. IsoAbHomMap x y -> IsoAbHomMap x y -> Bool
/= :: IsoAbHomMap x y -> IsoAbHomMap x y -> Bool
Eq,(forall x y. IsoAbHomMap x y -> IsoAbHomMap x y -> Bool)
-> Eq2 IsoAbHomMap
forall x y. IsoAbHomMap x y -> IsoAbHomMap x y -> Bool
forall (h :: * -> * -> *).
(forall x y. h x y -> h x y -> Bool) -> Eq2 h
$ceq2 :: forall x y. IsoAbHomMap x y -> IsoAbHomMap x y -> Bool
eq2 :: forall x y. IsoAbHomMap x y -> IsoAbHomMap x y -> Bool
Eq2,Eq (IsoAbHomMap x y)
Show (IsoAbHomMap x y)
Typeable (IsoAbHomMap x y)
Validable (IsoAbHomMap x y)
(Show (IsoAbHomMap x y), Eq (IsoAbHomMap x y),
 Validable (IsoAbHomMap x y), Typeable (IsoAbHomMap x y)) =>
Entity (IsoAbHomMap x y)
forall a. (Show a, Eq a, Validable a, Typeable a) => Entity a
forall x y. (Typeable x, Typeable y) => Eq (IsoAbHomMap x y)
forall x y. (Typeable x, Typeable y) => Show (IsoAbHomMap x y)
forall x y. (Typeable x, Typeable y) => Typeable (IsoAbHomMap x y)
forall x y. (Typeable x, Typeable y) => Validable (IsoAbHomMap x y)
Entity,Typeable IsoAbHomMap
Eq2 IsoAbHomMap
Show2 IsoAbHomMap
Validable2 IsoAbHomMap
(Show2 IsoAbHomMap, Eq2 IsoAbHomMap, Validable2 IsoAbHomMap,
 Typeable IsoAbHomMap) =>
Entity2 IsoAbHomMap
forall (h :: * -> * -> *).
(Show2 h, Eq2 h, Validable2 h, Typeable h) =>
Entity2 h
Entity2)

--------------------------------------------------------------------------------
-- IsoAbHomMap - Constructable -

-- | reducing paths of 'AbHomMap'.
rdcPathAbHomMap :: PathAbHomMap x y -> Rdc (PathAbHomMap x y)
rdcPathAbHomMap :: forall x y. PathAbHomMap x y -> Rdc (PathAbHomMap x y)
rdcPathAbHomMap PathAbHomMap x y
pth = case PathAbHomMap x y
pth of
  AbHomMap y1 y
AbHomMatrix :. AbHomMap y1 y1
MatrixAbHom :. Path AbHomMap x y1
p -> Path AbHomMap x y1 -> Rdc (Path AbHomMap x y1)
forall x. x -> Rdc x
reducesTo Path AbHomMap x y1
p Rdc (Path AbHomMap x y1)
-> (Path AbHomMap x y1 -> Rdc (PathAbHomMap x y))
-> Rdc (PathAbHomMap x y)
forall a b.
Action RdcState a -> (a -> Action RdcState b) -> Action RdcState b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Path AbHomMap x y1 -> Rdc (PathAbHomMap x y)
Path AbHomMap x y1 -> Rdc (Path AbHomMap x y1)
forall x y. PathAbHomMap x y -> Rdc (PathAbHomMap x y)
rdcPathAbHomMap
  AbHomMap y1 y
MatrixAbHom :. AbHomMap y1 y1
AbHomMatrix :. Path AbHomMap x y1
p -> Path AbHomMap x y1 -> Rdc (Path AbHomMap x y1)
forall x. x -> Rdc x
reducesTo Path AbHomMap x y1
p Rdc (Path AbHomMap x y1)
-> (Path AbHomMap x y1 -> Rdc (PathAbHomMap x y))
-> Rdc (PathAbHomMap x y)
forall a b.
Action RdcState a -> (a -> Action RdcState b) -> Action RdcState b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Path AbHomMap x y1 -> Rdc (PathAbHomMap x y)
Path AbHomMap x y1 -> Rdc (Path AbHomMap x y1)
forall x y. PathAbHomMap x y -> Rdc (PathAbHomMap x y)
rdcPathAbHomMap
  AbHomMap y1 y
h :. Path AbHomMap x y1
p                          -> Path AbHomMap x y1 -> Rdc (Path AbHomMap x y1)
forall x y. PathAbHomMap x y -> Rdc (PathAbHomMap x y)
rdcPathAbHomMap Path AbHomMap x y1
p Rdc (Path AbHomMap x y1)
-> (Path AbHomMap x y1 -> Rdc (PathAbHomMap x y))
-> Rdc (PathAbHomMap x y)
forall a b.
Action RdcState a -> (a -> Action RdcState b) -> Action RdcState b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= PathAbHomMap x y -> Rdc (PathAbHomMap x y)
forall x. x -> Rdc x
forall (m :: * -> *) a. Monad m => a -> m a
return (PathAbHomMap x y -> Rdc (PathAbHomMap x y))
-> (Path AbHomMap x y1 -> PathAbHomMap x y)
-> Path AbHomMap x y1
-> Rdc (PathAbHomMap x y)
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
. (AbHomMap y1 y
hAbHomMap y1 y -> Path AbHomMap x y1 -> PathAbHomMap x y
forall (m :: * -> * -> *) y1 y x.
m y1 y -> Path m x y1 -> Path m x y
:.)
  PathAbHomMap x y
p                               -> PathAbHomMap x y -> Rdc (PathAbHomMap x y)
forall x. x -> Rdc x
forall (m :: * -> *) a. Monad m => a -> m a
return PathAbHomMap x y
p

instance Reducible (PathAbHomMap x y) where
  reduce :: PathAbHomMap x y -> PathAbHomMap x y
reduce = (PathAbHomMap x y -> Rdc (PathAbHomMap x y))
-> PathAbHomMap x y -> PathAbHomMap x y
forall x. (x -> Rdc x) -> x -> x
reduceWith PathAbHomMap x y -> Rdc (PathAbHomMap x y)
forall x y. PathAbHomMap x y -> Rdc (PathAbHomMap x y)
rdcPathAbHomMap

instance Exposable (IsoAbHomMap x y) where
  type Form (IsoAbHomMap x y) = PathAbHomMap x y
  form :: IsoAbHomMap x y -> Form (IsoAbHomMap x y)
form (IsoAbHomMap PathAbHomMap x y
p) = Form (IsoAbHomMap x y)
PathAbHomMap x y
p

instance Constructable (IsoAbHomMap x y) where
  make :: Form (IsoAbHomMap x y) -> IsoAbHomMap x y
make Form (IsoAbHomMap x y)
p = PathAbHomMap x y -> IsoAbHomMap x y
forall x y. PathAbHomMap x y -> IsoAbHomMap x y
IsoAbHomMap (PathAbHomMap x y -> PathAbHomMap x y
forall e. Reducible e => e -> e
reduce Form (IsoAbHomMap x y)
PathAbHomMap x y
p)

--------------------------------------------------------------------------------
-- abHomMatrix -

-- | the induced isomorphism from 'AbHom' to @'Matrix' 'ZModHom'@ with inverse 'matrixAbHom'.
abHomMatrix :: IsoAbHomMap AbHom (Matrix ZModHom)
abHomMatrix :: IsoAbHomMap AbHom (Matrix ZModHom)
abHomMatrix = PathAbHomMap AbHom (Matrix ZModHom)
-> IsoAbHomMap AbHom (Matrix ZModHom)
forall x y. PathAbHomMap x y -> IsoAbHomMap x y
IsoAbHomMap (AbHomMap AbHom (Matrix ZModHom)
AbHomMatrix AbHomMap AbHom (Matrix ZModHom)
-> Path AbHomMap AbHom AbHom -> PathAbHomMap AbHom (Matrix ZModHom)
forall (m :: * -> * -> *) y1 y x.
m y1 y -> Path m x y1 -> Path m x y
:. Struct (ObjectClass AbHomMap) AbHom -> Path AbHomMap AbHom AbHom
forall (m :: * -> * -> *) x. Struct (ObjectClass m) x -> Path m x x
IdPath Struct (ObjectClass AbHomMap) AbHom
Struct (Alg Z) AbHom
forall s x. Structure s x => Struct s x
Struct)

--------------------------------------------------------------------------------
-- matrixAbHom -

-- | the induced isomorphism from @'Matrix' 'ZModHom'@ to 'AbHom' with inverse 'abHomMatrix'.
matrixAbHom :: IsoAbHomMap (Matrix ZModHom) AbHom
matrixAbHom :: IsoAbHomMap (Matrix ZModHom) AbHom
matrixAbHom = PathAbHomMap (Matrix ZModHom) AbHom
-> IsoAbHomMap (Matrix ZModHom) AbHom
forall x y. PathAbHomMap x y -> IsoAbHomMap x y
IsoAbHomMap (AbHomMap (Matrix ZModHom) AbHom
MatrixAbHom AbHomMap (Matrix ZModHom) AbHom
-> Path AbHomMap (Matrix ZModHom) (Matrix ZModHom)
-> PathAbHomMap (Matrix ZModHom) AbHom
forall (m :: * -> * -> *) y1 y x.
m y1 y -> Path m x y1 -> Path m x y
:. Struct (ObjectClass AbHomMap) (Matrix ZModHom)
-> Path AbHomMap (Matrix ZModHom) (Matrix ZModHom)
forall (m :: * -> * -> *) x. Struct (ObjectClass m) x -> Path m x x
IdPath Struct (ObjectClass AbHomMap) (Matrix ZModHom)
Struct (Alg Z) (Matrix ZModHom)
forall s x. Structure s x => Struct s x
Struct)

--------------------------------------------------------------------------------
-- IsoAbHomMap - Cayleyan2 -

instance Morphism IsoAbHomMap where
  type ObjectClass IsoAbHomMap = Alg Z
  homomorphous :: forall x y.
IsoAbHomMap x y -> Homomorphous (ObjectClass IsoAbHomMap) x y
homomorphous = (Form (IsoAbHomMap x y) -> Homomorphous (Alg Z) x y)
-> IsoAbHomMap x y -> Homomorphous (Alg Z) x y
forall x y. Exposable x => (Form x -> y) -> x -> y
restrict Form (IsoAbHomMap x y) -> Homomorphous (Alg Z) x y
Path AbHomMap x y -> Homomorphous (ObjectClass (Path AbHomMap)) x y
forall x y.
Path AbHomMap x y -> Homomorphous (ObjectClass (Path AbHomMap)) x y
forall (m :: * -> * -> *) x y.
Morphism m =>
m x y -> Homomorphous (ObjectClass m) x y
homomorphous

instance Category IsoAbHomMap where
  cOne :: forall x. Struct (ObjectClass IsoAbHomMap) x -> IsoAbHomMap x x
cOne Struct (ObjectClass IsoAbHomMap) x
o = PathAbHomMap x x -> IsoAbHomMap x x
forall x y. PathAbHomMap x y -> IsoAbHomMap x y
IsoAbHomMap (Struct (ObjectClass AbHomMap) x -> PathAbHomMap x x
forall (m :: * -> * -> *) x. Struct (ObjectClass m) x -> Path m x x
IdPath Struct (ObjectClass IsoAbHomMap) x
Struct (ObjectClass AbHomMap) x
o)
  IsoAbHomMap PathAbHomMap y z
f . :: forall y z x. IsoAbHomMap y z -> IsoAbHomMap x y -> IsoAbHomMap x z
. IsoAbHomMap PathAbHomMap x y
g = Form (IsoAbHomMap x z) -> IsoAbHomMap x z
forall x. Constructable x => Form x -> x
make (PathAbHomMap y z
f PathAbHomMap y z -> PathAbHomMap x y -> Path AbHomMap x z
forall y z x.
Path AbHomMap y z -> Path AbHomMap x y -> Path AbHomMap x z
forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. PathAbHomMap x y
g)

instance Cayleyan2 IsoAbHomMap where
  invert2 :: forall x y. IsoAbHomMap x y -> IsoAbHomMap y x
invert2 (IsoAbHomMap PathAbHomMap x y
f) = PathAbHomMap y x -> IsoAbHomMap y x
forall x y. PathAbHomMap x y -> IsoAbHomMap x y
IsoAbHomMap ((forall u.
 Struct (ObjectClass AbHomMap) u -> Struct (ObjectClass AbHomMap) u)
-> (forall x y. AbHomMap x y -> AbHomMap y x)
-> PathAbHomMap x y
-> PathAbHomMap y x
forall (m :: * -> * -> *) (f :: * -> * -> *) x y.
(Morphism m, Morphism f) =>
(forall u. Struct (ObjectClass m) u -> Struct (ObjectClass f) u)
-> (forall u v. m u v -> f v u) -> Path m x y -> Path f y x
reverse Struct (ObjectClass AbHomMap) u -> Struct (ObjectClass AbHomMap) u
Struct (Alg Z) u -> Struct (Alg Z) u
forall x. x -> x
forall u.
Struct (ObjectClass AbHomMap) u -> Struct (ObjectClass AbHomMap) u
id AbHomMap u v -> AbHomMap v u
forall x y. AbHomMap x y -> AbHomMap y x
invAbHomMap PathAbHomMap x y
f) 

--------------------------------------------------------------------------------
-- IsoAbHomMap - Hom -

instance Applicative IsoAbHomMap where
  amap :: forall a b. IsoAbHomMap a b -> a -> b
amap = (Form (IsoAbHomMap a b) -> a -> b) -> IsoAbHomMap a b -> a -> b
forall x y. Exposable x => (Form x -> y) -> x -> y
restrict Form (IsoAbHomMap a b) -> a -> b
Path AbHomMap a b -> a -> b
forall a b. Path AbHomMap a b -> a -> b
forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
amap

instance EmbeddableMorphism IsoAbHomMap Ort
instance EmbeddableMorphism IsoAbHomMap Typ
instance EmbeddableMorphismTyp IsoAbHomMap

instance HomOriented IsoAbHomMap where
  pmap :: forall a b. IsoAbHomMap a b -> Point a -> Point b
pmap = (Form (IsoAbHomMap a b) -> Point a -> Point b)
-> IsoAbHomMap a b -> Point a -> Point b
forall x y. Exposable x => (Form x -> y) -> x -> y
restrict Form (IsoAbHomMap a b) -> Point a -> Point b
Path AbHomMap a b -> Point a -> Point b
forall a b. Path AbHomMap a b -> Point a -> Point b
forall (h :: * -> * -> *) a b.
HomOriented h =>
h a b -> Point a -> Point b
pmap

instance EmbeddableMorphism IsoAbHomMap Mlt
instance HomMultiplicative IsoAbHomMap

--------------------------------------------------------------------------------
-- IsoAbHomMap - Functorial -

instance Functorial IsoAbHomMap
instance FunctorialHomOriented IsoAbHomMap

--------------------------------------------------------------------------------
-- abhProducts -

-- | products for 'AbHom'.
abhProducts :: Products n AbHom
abhProducts :: forall (n :: N'). Products n AbHom
abhProducts = IsoAbHomMap (Matrix ZModHom) AbHom
-> Limits Mlt 'Projective 'Discrete n N0 (Matrix ZModHom)
-> Limits Mlt 'Projective 'Discrete n N0 AbHom
forall s (h :: * -> * -> *) a b (p :: Perspective)
       (t :: DiagramType) (n :: N') (m :: N').
IsoOrt s h =>
h a b -> Limits s p t n m a -> Limits s p t n m b
lmsMap IsoAbHomMap (Matrix ZModHom) AbHom
matrixAbHom Limits Mlt 'Projective 'Discrete n N0 (Matrix ZModHom)
forall x (n :: N'). Distributive x => Products n (Matrix x)
mtxProducts

--------------------------------------------------------------------------------
-- abhSums -

-- | sums for 'AbHom'.
abhSums :: Sums n AbHom
abhSums :: forall (n :: N'). Sums n AbHom
abhSums = IsoAbHomMap (Matrix ZModHom) AbHom
-> Limits Mlt 'Injective 'Discrete n N0 (Matrix ZModHom)
-> Limits Mlt 'Injective 'Discrete n N0 AbHom
forall s (h :: * -> * -> *) a b (p :: Perspective)
       (t :: DiagramType) (n :: N') (m :: N').
IsoOrt s h =>
h a b -> Limits s p t n m a -> Limits s p t n m b
lmsMap IsoAbHomMap (Matrix ZModHom) AbHom
matrixAbHom Limits Mlt 'Injective 'Discrete n N0 (Matrix ZModHom)
forall x (n :: N'). Distributive x => Sums n (Matrix x)
mtxSums

--------------------------------------------------------------------------------
-- abgFree -

-- | the free abelian group of the given dimension.
--
-- >>> abgFree (Free attest :: Free N6 AbGroup)
-- AbGroup ProductSymbol[Z^6]
abgFree :: Free k x -> AbGroup
abgFree :: forall (k :: N') x. Free k x -> AbGroup
abgFree Free k x
n = N -> AbGroup
abg N
0 AbGroup -> Exponent AbGroup -> AbGroup
forall f. Exponential f => f -> Exponent f -> f
^ (Free k x -> N
forall (k :: N') c. Free k c -> N
freeN Free k x
n)

--------------------------------------------------------------------------------
-- Sliced (Free k) -

instance Attestable k => Sliced (Free k) AbHom where
  slicePoint :: Free k AbHom -> Point AbHom
slicePoint = Free k AbHom -> Point AbHom
Free k AbHom -> AbGroup
forall (k :: N') x. Free k x -> AbGroup
abgFree

--------------------------------------------------------------------------------
-- abgMaybeFree -

-- | check of being free of some length.
--
-- >>> abgMaybeFree (abg 0 ^ 5)
-- Just (SomeFree (Free 5))
--
-- >>> abgMaybeFree (abg 0 ^ 5 * abg 3)
-- Nothing
--
-- >>> abgMaybeFree (abg 0 ^ 5 * abg 3 ^ 0)
-- Just (SomeFree (Free 5))
abgMaybeFree :: AbGroup -> Maybe (SomeFree AbHom)
abgMaybeFree :: AbGroup -> Maybe (SomeFree AbHom)
abgMaybeFree AbGroup
g = case N -> SomeNatural
someNatural (N -> SomeNatural) -> N -> SomeNatural
forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ AbGroup -> N
forall x. LengthN x => x -> N
lengthN AbGroup
g of
  SomeNatural W n
k -> if AbGroup
g AbGroup -> AbGroup -> Bool
forall a. Eq a => a -> a -> Bool
== Free n AbHom -> AbGroup
forall (k :: N') x. Free k x -> AbGroup
abgFree Free n AbHom
k' then SomeFree AbHom -> Maybe (SomeFree AbHom)
forall a. a -> Maybe a
Just (Free n AbHom -> SomeFree AbHom
forall (k :: N') c.
(Attestable k, Sliced (Free k) c) =>
Free k c -> SomeFree c
SomeFree Free n AbHom
k') else Maybe (SomeFree AbHom)
forall a. Maybe a
Nothing where k' :: Free n AbHom
k' = W n -> Free n AbHom
forall (k :: N') c. Any k -> Free k c
Free W n
k

--------------------------------------------------------------------------------
-- abgFrees -

-- | number of free components.
abgFrees :: AbGroup -> N
abgFrees :: AbGroup -> N
abgFrees = [(ZMod, N)] -> N
forall x. LengthN x => x -> N
lengthN ([(ZMod, N)] -> N) -> (AbGroup -> [(ZMod, N)]) -> AbGroup -> N
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
. ((ZMod, N) -> Bool) -> [(ZMod, N)] -> [(ZMod, N)]
forall a. (a -> Bool) -> [a] -> [a]
filter ((ZMod -> ZMod -> Bool
forall a. Eq a => a -> a -> Bool
== N -> ZMod
ZMod N
0) (ZMod -> Bool) -> ((ZMod, N) -> ZMod) -> (ZMod, N) -> Bool
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
. (ZMod, N) -> ZMod
forall a b. (a, b) -> a
fst) ([(ZMod, N)] -> [(ZMod, N)])
-> (AbGroup -> [(ZMod, N)]) -> AbGroup -> [(ZMod, N)]
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
. AbGroup -> [(ZMod, N)]
abgxs
  
--------------------------------------------------------------------------------
-- AbHomFree -

-- | projection homomorphisms to @'Matrix' 'Z'@.
data AbHomFree x y where
  AbHomFree :: AbHomFree AbHom (Matrix Z)
  FreeAbHom :: AbHomFree (Matrix Z) AbHom

--------------------------------------------------------------------------------
-- AbHomFree - Entity -

deriving instance Show (AbHomFree x y)
instance Show2 AbHomFree
deriving instance Eq (AbHomFree x y)
instance Eq2 AbHomFree

instance Validable (AbHomFree x y) where
  valid :: AbHomFree x y -> Statement
valid AbHomFree x y
AbHomFree = Statement
SValid
  valid AbHomFree x y
_         = Statement
SValid

instance Validable2 AbHomFree

instance (Typeable x, Typeable y) => Entity (AbHomFree x y)
instance Entity2 AbHomFree

--------------------------------------------------------------------------------
-- AbHomFree - HomAlgebraic -

instance Morphism AbHomFree where
  type ObjectClass AbHomFree = Alg Z
  homomorphous :: forall x y.
AbHomFree x y -> Homomorphous (ObjectClass AbHomFree) x y
homomorphous AbHomFree x y
AbHomFree = Struct (Alg Z) x
forall s x. Structure s x => Struct s x
Struct Struct (Alg Z) x -> Struct (Alg Z) y -> Homomorphous (Alg Z) x y
forall s x y. Struct s x -> Struct s y -> Homomorphous s x y
:>: Struct (Alg Z) y
forall s x. Structure s x => Struct s x
Struct
  homomorphous AbHomFree x y
FreeAbHom = Struct (Alg Z) x
forall s x. Structure s x => Struct s x
Struct Struct (Alg Z) x -> Struct (Alg Z) y -> Homomorphous (Alg Z) x y
forall s x y. Struct s x -> Struct s y -> Homomorphous s x y
:>: Struct (Alg Z) y
forall s x. Structure s x => Struct s x
Struct

instance EmbeddableMorphism AbHomFree Ort
instance EmbeddableMorphism AbHomFree Typ
instance EmbeddableMorphismTyp AbHomFree

instance Applicative AbHomFree where
  amap :: forall a b. AbHomFree a b -> a -> b
amap AbHomFree a b
AbHomFree h :: a
h@(AbHom (Matrix Dim' ZModHom
_ Dim' ZModHom
_ Entries N N ZModHom
xs)) = Dim' Z -> Dim' Z -> Entries N N Z -> Matrix Z
forall x. Dim' x -> Dim' x -> Entries N N x -> Matrix x
Matrix Dim Z ()
Dim' Z
n Dim Z ()
Dim' Z
m Entries N N Z
xs' where
    Point a
s :> Point a
e = a -> Orientation (Point a)
forall q. Oriented q => q -> Orientation (Point q)
orientation a
h
    u :: Dim Z ()
u = () -> Dim Z ()
forall p x. (Entity p, p ~ Point x) => p -> Dim x p
dim ()
    n :: Dim Z ()
n = Dim Z ()
u Dim Z () -> Exponent (Dim Z ()) -> Dim Z ()
forall f. Exponential f => f -> Exponent f -> f
^ AbGroup -> N
abgFrees Point a
AbGroup
e
    m :: Dim Z ()
m = Dim Z ()
u Dim Z () -> Exponent (Dim Z ()) -> Dim Z ()
forall f. Exponential f => f -> Exponent f -> f
^ AbGroup -> N
abgFrees Point a
AbGroup
s
    
    xs' :: Entries N N Z
xs' = Col N (Row N Z) -> Entries N N Z
forall i j x. Col i (Row j x) -> Entries i j x
crets (Col N (Row N Z) -> Entries N N Z)
-> Col N (Row N Z) -> Entries N N Z
forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ PSequence N (Row N Z) -> Col N (Row N Z)
forall i x. PSequence i x -> Col i x
Col (PSequence N (Row N Z) -> Col N (Row N Z))
-> PSequence N (Row N Z) -> Col N (Row N Z)
forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ [(Row N Z, N)] -> PSequence N (Row N Z)
forall i x. [(x, i)] -> PSequence i x
PSequence ([(Row N Z, N)] -> PSequence N (Row N Z))
-> [(Row N Z, N)] -> PSequence N (Row N Z)
forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ N
-> [(ZMod, N)]
-> [(ZMod, N)]
-> [(Row N ZModHom, N)]
-> [(Row N Z, N)]
forall i j.
(i ~ N, j ~ N) =>
i
-> [(ZMod, i)]
-> [(ZMod, j)]
-> [(Row j ZModHom, i)]
-> [(Row j Z, i)]
frees N
0 (AbGroup -> [(ZMod, N)]
abgxs Point a
AbGroup
e) (AbGroup -> [(ZMod, N)]
abgxs Point a
AbGroup
s) ([(Row N ZModHom, N)] -> [(Row N Z, N)])
-> [(Row N ZModHom, N)] -> [(Row N Z, N)]
forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ Col N (Row N ZModHom) -> [(Row N ZModHom, N)]
forall i x. Col i x -> [(x, i)]
colxs (Col N (Row N ZModHom) -> [(Row N ZModHom, N)])
-> Col N (Row N ZModHom) -> [(Row N ZModHom, N)]
forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ Entries N N ZModHom -> Col N (Row N ZModHom)
forall i j x. Eq i => Entries i j x -> Col i (Row j x)
etscr Entries N N ZModHom
xs

    frees :: (i ~ N,j ~ N)
      => i -> [(ZMod,i)] -> [(ZMod,j)] -> [(Row j ZModHom,i)] -> [(Row j Z,i)]
    frees :: forall i j.
(i ~ N, j ~ N) =>
i
-> [(ZMod, i)]
-> [(ZMod, j)]
-> [(Row j ZModHom, i)]
-> [(Row j Z, i)]
frees i
_ [] [(ZMod, j)]
_ [(Row j ZModHom, i)]
_ = []
    frees i
_ [(ZMod, i)]
_ [(ZMod, j)]
_ [] = []
    frees i
i'' ((ZMod N
0,i
i):[(ZMod, i)]
is') [(ZMod, j)]
js rws :: [(Row j ZModHom, i)]
rws@((Row j ZModHom
rw,i
i'):[(Row j ZModHom, i)]
rws') = if i
i i -> i -> Bool
forall a. Ord a => a -> a -> Bool
< i
i'
      then i
-> [(ZMod, i)]
-> [(ZMod, j)]
-> [(Row j ZModHom, i)]
-> [(Row j Z, i)]
forall i j.
(i ~ N, j ~ N) =>
i
-> [(ZMod, i)]
-> [(ZMod, j)]
-> [(Row j ZModHom, i)]
-> [(Row j Z, i)]
frees (i -> i
forall a. Enum a => a -> a
succ i
i'') [(ZMod, i)]
is' [(ZMod, j)]
js [(Row j ZModHom, i)]
rws
      else ((PSequence N Z -> Row j Z
PSequence N Z -> Row N Z
forall j x. PSequence j x -> Row j x
Row (PSequence N Z -> Row j Z) -> PSequence N Z -> Row j Z
forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ [(Z, j)] -> PSequence N Z
[(Z, N)] -> PSequence N Z
forall i x. [(x, i)] -> PSequence i x
PSequence ([(Z, j)] -> PSequence N Z) -> [(Z, j)] -> PSequence N Z
forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ j -> [(ZMod, j)] -> [(ZModHom, j)] -> [(Z, j)]
forall j. (j ~ N) => j -> [(ZMod, j)] -> [(ZModHom, j)] -> [(Z, j)]
rwFrees j
0 [(ZMod, j)]
js (Row j ZModHom -> [(ZModHom, j)]
forall j x. Row j x -> [(x, j)]
rowxs Row j ZModHom
rw),i
i'')(Row j Z, i) -> [(Row j Z, i)] -> [(Row j Z, i)]
forall a. a -> [a] -> [a]
:i
-> [(ZMod, i)]
-> [(ZMod, j)]
-> [(Row j ZModHom, i)]
-> [(Row j Z, i)]
forall i j.
(i ~ N, j ~ N) =>
i
-> [(ZMod, i)]
-> [(ZMod, j)]
-> [(Row j ZModHom, i)]
-> [(Row j Z, i)]
frees (i -> i
forall a. Enum a => a -> a
succ i
i'') [(ZMod, i)]
is' [(ZMod, j)]
js [(Row j ZModHom, i)]
rws')
    frees i
i'' ((ZMod N
_,i
i):[(ZMod, i)]
is') [(ZMod, j)]
js rws :: [(Row j ZModHom, i)]
rws@((Row j ZModHom
_,i
i'):[(Row j ZModHom, i)]
rws') = if i
i i -> i -> Bool
forall a. Ord a => a -> a -> Bool
< i
i'
      then i
-> [(ZMod, i)]
-> [(ZMod, j)]
-> [(Row j ZModHom, i)]
-> [(Row j Z, i)]
forall i j.
(i ~ N, j ~ N) =>
i
-> [(ZMod, i)]
-> [(ZMod, j)]
-> [(Row j ZModHom, i)]
-> [(Row j Z, i)]
frees i
i'' [(ZMod, i)]
is' [(ZMod, j)]
js [(Row j ZModHom, i)]
rws
      else i
-> [(ZMod, i)]
-> [(ZMod, j)]
-> [(Row j ZModHom, i)]
-> [(Row j Z, i)]
forall i j.
(i ~ N, j ~ N) =>
i
-> [(ZMod, i)]
-> [(ZMod, j)]
-> [(Row j ZModHom, i)]
-> [(Row j Z, i)]
frees i
i'' [(ZMod, i)]
is' [(ZMod, j)]
js [(Row j ZModHom, i)]
rws'

    rwFrees :: j ~ N => j -> [(ZMod,j)] -> [(ZModHom,j)] -> [(Z,j)]
    rwFrees :: forall j. (j ~ N) => j -> [(ZMod, j)] -> [(ZModHom, j)] -> [(Z, j)]
rwFrees j
_ [] [(ZModHom, j)]
_ = []
    rwFrees j
_ [(ZMod, j)]
_ [] = []
    rwFrees j
j'' ((ZMod N
0,j
j):[(ZMod, j)]
js') hs :: [(ZModHom, j)]
hs@((ZModHom
h,j
j'):[(ZModHom, j)]
hs') = if j
j j -> j -> Bool
forall a. Ord a => a -> a -> Bool
< j
j'
      then j -> [(ZMod, j)] -> [(ZModHom, j)] -> [(Z, j)]
forall j. (j ~ N) => j -> [(ZMod, j)] -> [(ZModHom, j)] -> [(Z, j)]
rwFrees (j -> j
forall a. Enum a => a -> a
succ j
j'') [(ZMod, j)]
js' [(ZModHom, j)]
hs
      else ((ZModHom -> Z
toZ ZModHom
h,j
j'')(Z, j) -> [(Z, j)] -> [(Z, j)]
forall a. a -> [a] -> [a]
:j -> [(ZMod, j)] -> [(ZModHom, j)] -> [(Z, j)]
forall j. (j ~ N) => j -> [(ZMod, j)] -> [(ZModHom, j)] -> [(Z, j)]
rwFrees (j -> j
forall a. Enum a => a -> a
succ j
j'') [(ZMod, j)]
js' [(ZModHom, j)]
hs')
    rwFrees j
j'' ((ZMod N
_,j
j):[(ZMod, j)]
js') hs :: [(ZModHom, j)]
hs@((ZModHom
_,j
j'):[(ZModHom, j)]
hs') = if j
j j -> j -> Bool
forall a. Ord a => a -> a -> Bool
< j
j'
      then j -> [(ZMod, j)] -> [(ZModHom, j)] -> [(Z, j)]
forall j. (j ~ N) => j -> [(ZMod, j)] -> [(ZModHom, j)] -> [(Z, j)]
rwFrees j
j'' [(ZMod, j)]
js' [(ZModHom, j)]
hs
      else j -> [(ZMod, j)] -> [(ZModHom, j)] -> [(Z, j)]
forall j. (j ~ N) => j -> [(ZMod, j)] -> [(ZModHom, j)] -> [(Z, j)]
rwFrees j
j'' [(ZMod, j)]
js' [(ZModHom, j)]
hs'
    
  amap AbHomFree a b
FreeAbHom a
m = Matrix Z -> AbHom
zabh a
Matrix Z
m

instance HomOriented AbHomFree where
  pmap :: forall a b. AbHomFree a b -> Point a -> Point b
pmap AbHomFree a b
AbHomFree Point a
g = () -> 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
^ AbGroup -> N
abgFrees Point a
AbGroup
g
  pmap AbHomFree a b
FreeAbHom Point a
n = N -> AbGroup
abg N
0 AbGroup -> Exponent AbGroup -> AbGroup
forall f. Exponential f => f -> Exponent f -> f
^ Dim Z () -> N
forall x. LengthN x => x -> N
lengthN Point a
Dim Z ()
n

instance EmbeddableMorphism AbHomFree Mlt
instance HomMultiplicative AbHomFree

instance EmbeddableMorphism AbHomFree Fbr
instance EmbeddableMorphism AbHomFree FbrOrt
instance HomFibred AbHomFree

instance HomFibredOriented AbHomFree

instance EmbeddableMorphism AbHomFree Add
instance HomAdditive AbHomFree

instance EmbeddableMorphism AbHomFree Dst
instance HomDistributive AbHomFree

--------------------------------------------------------------------------------
-- abhFreeAdjucntion -

-- | the projection 'AbHomFree' as left adjoint.
abhFreeAdjunction :: Adjunction AbHomFree (Matrix Z) AbHom
abhFreeAdjunction :: Adjunction AbHomFree (Matrix Z) AbHom
abhFreeAdjunction = AbHomFree AbHom (Matrix Z)
-> AbHomFree (Matrix Z) AbHom
-> (Point AbHom -> AbHom)
-> (Point (Matrix Z) -> Matrix Z)
-> Adjunction AbHomFree (Matrix Z) AbHom
forall (h :: * -> * -> *) c d.
h c d
-> h d c -> (Point c -> c) -> (Point d -> d) -> Adjunction h d c
Adjunction AbHomFree AbHom (Matrix Z)
AbHomFree AbHomFree (Matrix Z) AbHom
FreeAbHom Point AbHom -> AbHom
AbGroup -> AbHom
u Point (Matrix Z) -> Matrix Z
forall c. Multiplicative c => Point c -> c
one where
  u :: AbGroup -> AbHom
  u :: AbGroup -> AbHom
u AbGroup
g = Matrix ZModHom -> AbHom
AbHom (Dim' ZModHom
-> Dim' ZModHom -> Entries N N ZModHom -> Matrix ZModHom
forall x. Dim' x -> Dim' x -> Entries N N x -> Matrix x
Matrix (AbGroup -> Dim' ZModHom
abgDim Point AbHom
AbGroup
g') (AbGroup -> Dim' ZModHom
abgDim AbGroup
g) (PSequence (N, N) ZModHom -> Entries N N ZModHom
forall i j x. PSequence (i, j) x -> Entries i j x
Entries (PSequence (N, N) ZModHom -> Entries N N ZModHom)
-> PSequence (N, N) ZModHom -> Entries N N ZModHom
forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ [(ZModHom, (N, N))] -> PSequence (N, N) ZModHom
forall i x. [(x, i)] -> PSequence i x
PSequence ([(ZModHom, (N, N))] -> PSequence (N, N) ZModHom)
-> [(ZModHom, (N, N))] -> PSequence (N, N) ZModHom
forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ N -> [(ZMod, N)] -> [(ZModHom, (N, N))]
forall i j. Enum i => i -> [(ZMod, j)] -> [(ZModHom, (i, j))]
xs N
0 (AbGroup -> [(ZMod, N)]
abgxs AbGroup
g))) where
    g' :: Point AbHom
g' = AbHomFree (Matrix Z) AbHom -> Point (Matrix Z) -> Point AbHom
forall a b. AbHomFree a b -> Point a -> Point b
forall (h :: * -> * -> *) a b.
HomOriented h =>
h a b -> Point a -> Point b
pmap AbHomFree (Matrix Z) AbHom
FreeAbHom (AbHomFree AbHom (Matrix Z) -> Point AbHom -> Point (Matrix Z)
forall a b. AbHomFree a b -> Point a -> Point b
forall (h :: * -> * -> *) a b.
HomOriented h =>
h a b -> Point a -> Point b
pmap AbHomFree AbHom (Matrix Z)
AbHomFree Point AbHom
AbGroup
g)
    o :: ZModHom
o = Point ZModHom -> ZModHom
forall c. Multiplicative c => Point c -> c
one (N -> ZMod
ZMod N
0) :: ZModHom
    
    xs :: Enum i => i -> [(ZMod,j)] -> [(ZModHom,(i,j))]
    xs :: forall i j. Enum i => i -> [(ZMod, j)] -> [(ZModHom, (i, j))]
xs i
_ []              = []
    xs i
i ((ZMod N
n,j
j):[(ZMod, j)]
js) = if N
n N -> N -> Bool
forall a. Eq a => a -> a -> Bool
/= N
0
      then i -> [(ZMod, j)] -> [(ZModHom, (i, j))]
forall i j. Enum i => i -> [(ZMod, j)] -> [(ZModHom, (i, j))]
xs i
i [(ZMod, j)]
js
      else ((ZModHom
o,(i
i,j
j))(ZModHom, (i, j)) -> [(ZModHom, (i, j))] -> [(ZModHom, (i, j))]
forall a. a -> [a] -> [a]
: i -> [(ZMod, j)] -> [(ZModHom, (i, j))]
forall i j. Enum i => i -> [(ZMod, j)] -> [(ZModHom, (i, j))]
xs (i -> i
forall a. Enum a => a -> a
succ i
i) [(ZMod, j)]
js)

--------------------------------------------------------------------------------
-- abgGeneratorTo -

-- | the generator for a finitely generated abelian group.
--
-- __Property__ Let @a@ be in 'AbGroup', then holds
-- @a '==' g@ where @'Generator' ('DiagramChainTo' g _) _ _ _ _ = 'abgGeneratorTo' a@.  
abgGeneratorTo :: AbGroup -> Generator To AbHom
abgGeneratorTo :: AbGroup -> Generator 'To AbHom
abgGeneratorTo g :: AbGroup
g@(AbGroup ProductSymbol ZMod
pg) = case (N -> SomeNatural
someNatural N
ng',N -> SomeNatural
someNatural N
ng'') of
  (SomeNatural W n
k',SomeNatural W n
k'') -> Diagram ('Chain 'To) N3 N2 AbHom
-> Free n AbHom
-> Free n AbHom
-> Cokernel N1 AbHom
-> Kernel N1 AbHom
-> (forall (k :: N'). Slice 'From (Free k) AbHom -> AbHom)
-> Generator 'To AbHom
forall (k' :: N') a (k'' :: N').
(Attestable k', Sliced (Free k') a, Attestable k'',
 Sliced (Free k'') a) =>
Diagram ('Chain 'To) N3 N2 a
-> Free k' a
-> Free k'' a
-> Cokernel N1 a
-> Kernel N1 a
-> (forall (k :: N'). Slice 'From (Free k) a -> a)
-> Generator 'To a
GeneratorTo Diagram ('Chain 'To) (N2 + 1) N2 AbHom
Diagram ('Chain 'To) N3 N2 AbHom
chn (W n -> Free n AbHom
forall (k :: N') c. Any k -> Free k c
Free W n
k') (W n -> Free n AbHom
forall (k :: N') c. Any k -> Free k c
Free W n
k'') Cokernel N1 AbHom
coker Kernel N1 AbHom
ker Slice 'From (Free k) AbHom -> AbHom
forall (k :: N'). Slice 'From (Free k) AbHom -> AbHom
lft
  where
    gs :: [(ZMod, N)]
gs   = ProductSymbol ZMod -> [(ZMod, N)]
forall (s :: * -> *) x. Sequence s N x => s x -> [(x, N)]
listN ProductSymbol ZMod
pg
    g's :: [(ZMod, N)]
g's  = ((ZMod, N) -> Bool) -> [(ZMod, N)] -> [(ZMod, N)]
forall a. (a -> Bool) -> [a] -> [a]
filter ((ZMod -> ZMod -> Bool
forall a. Eq a => a -> a -> Bool
/=N -> ZMod
ZMod N
1) (ZMod -> Bool) -> ((ZMod, N) -> ZMod) -> (ZMod, N) -> Bool
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
. (ZMod, N) -> ZMod
forall a b. (a, b) -> a
fst) [(ZMod, N)]
gs
    g''s :: [(ZMod, N)]
g''s = ((ZMod, N) -> Bool) -> [(ZMod, N)] -> [(ZMod, N)]
forall a. (a -> Bool) -> [a] -> [a]
filter ((ZMod -> ZMod -> Bool
forall a. Eq a => a -> a -> Bool
/=N -> ZMod
ZMod N
0) (ZMod -> Bool) -> ((ZMod, N) -> ZMod) -> (ZMod, N) -> Bool
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
. (ZMod, N) -> ZMod
forall a b. (a, b) -> a
fst) [(ZMod, N)]
g's

    ng' :: N
ng' = [(ZMod, N)] -> N
forall x. LengthN x => x -> N
lengthN [(ZMod, N)]
g's
    g' :: AbGroup
g'  = N -> AbGroup
abg N
0 AbGroup -> Exponent AbGroup -> AbGroup
forall f. Exponential f => f -> Exponent f -> f
^ N
Exponent AbGroup
ng'

    ng'' :: N
ng'' = [(ZMod, N)] -> N
forall x. LengthN x => x -> N
lengthN [(ZMod, N)]
g''s
    g'' :: AbGroup
g'' = N -> AbGroup
abg N
0 AbGroup -> Exponent AbGroup -> AbGroup
forall f. Exponential f => f -> Exponent f -> f
^ N
Exponent AbGroup
ng''
    
    p :: AbHom
p  = Orientation AbGroup -> [(ZModHom, N, N)] -> AbHom
abh (AbGroup
g' AbGroup -> AbGroup -> Orientation AbGroup
forall p. p -> p -> Orientation p
:> AbGroup
g) ([(ZModHom, N, N)] -> AbHom) -> [(ZModHom, N, N)] -> AbHom
forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ (((ZMod, N), N) -> (ZModHom, N, N))
-> [((ZMod, N), N)] -> [(ZModHom, N, N)]
forall a b. (a -> b) -> [a] -> [b]
forall (h :: * -> * -> *) (f :: * -> *) a b.
Applicative1 h f =>
h a b -> f a -> f b
amap1 (\((ZMod
z,N
i),N
j) -> (Orientation ZMod -> Z -> ZModHom
zmh (N -> ZMod
ZMod N
0ZMod -> ZMod -> Orientation ZMod
forall p. p -> p -> Orientation p
:>ZMod
z) Z
1,N
i,N
j)) ([(ZMod, N)]
g's [(ZMod, N)] -> [N] -> [((ZMod, N), N)]
forall a b. [a] -> [b] -> [(a, b)]
`zip` [N
0..])
    p' :: AbHom
p' = Orientation AbGroup -> [(ZModHom, N, N)] -> AbHom
abh (AbGroup
g'' AbGroup -> AbGroup -> Orientation AbGroup
forall p. p -> p -> Orientation p
:> AbGroup
g') ([(ZModHom, N, N)] -> AbHom) -> [(ZModHom, N, N)] -> AbHom
forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ N -> [(ZMod, N)] -> [(ZModHom, N, N)]
forall {t} {b}. Enum t => t -> [(ZMod, b)] -> [(ZModHom, b, t)]
zs N
0 (((ZMod, N) -> ZMod) -> [(ZMod, N)] -> [ZMod]
forall a b. (a -> b) -> [a] -> [b]
forall (h :: * -> * -> *) (f :: * -> *) a b.
Applicative1 h f =>
h a b -> f a -> f b
amap1 (ZMod, N) -> ZMod
forall a b. (a, b) -> a
fst [(ZMod, N)]
g's [ZMod] -> [N] -> [(ZMod, N)]
forall a b. [a] -> [b] -> [(a, b)]
`zip` [N
0..]) where
      z0 :: ZMod
z0 = N -> ZMod
ZMod N
0
      zs :: t -> [(ZMod, b)] -> [(ZModHom, b, t)]
zs t
_ [] = []
      zs t
j ((ZMod N
n,b
i):[(ZMod, b)]
g's) = if N
n N -> N -> Bool
forall a. Eq a => a -> a -> Bool
/= N
0
        then (Orientation ZMod -> Z -> ZModHom
zmh (ZMod
z0ZMod -> ZMod -> Orientation ZMod
forall p. p -> p -> Orientation p
:>ZMod
z0) (N -> Z
forall a b. Embeddable a b => a -> b
inj N
n),b
i,t
j)(ZModHom, b, t) -> [(ZModHom, b, t)] -> [(ZModHom, b, t)]
forall a. a -> [a] -> [a]
:t -> [(ZMod, b)] -> [(ZModHom, b, t)]
zs (t -> t
forall a. Enum a => a -> a
succ t
j) [(ZMod, b)]
g's
        else t -> [(ZMod, b)] -> [(ZModHom, b, t)]
zs t
j [(ZMod, b)]
g's 

    chn :: Diagram ('Chain 'To) (N2 + 1) N2 AbHom
chn = Point AbHom
-> FinList N2 AbHom -> Diagram ('Chain 'To) (N2 + 1) N2 AbHom
forall a (m :: N').
Point a -> FinList m a -> Diagram ('Chain 'To) (m + 1) m a
DiagramChainTo Point AbHom
AbGroup
g (AbHom
pAbHom -> 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)
    
    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 (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
dg AbHom
p') Cone Dst 'Projective ('Parallel 'LeftToRight) N2 N1 AbHom -> AbHom
univ where
      dg :: Diagram ('Parallel 'LeftToRight) N2 N1 AbHom
dg = 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
p) (AbHom -> Point AbHom
forall q. Oriented q => q -> Point q
end AbHom
p) (AbHom
pAbHom -> 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)
      univ :: KernelCone N1 AbHom -> AbHom
      univ :: Cone Dst 'Projective ('Parallel 'LeftToRight) N2 N1 AbHom -> AbHom
univ (ConeKernel Diagram ('Parallel 'LeftToRight) N2 N1 AbHom
_ (AbHom (Matrix Dim' ZModHom
_ Dim' ZModHom
c Entries N N ZModHom
xs))) = Matrix ZModHom -> AbHom
AbHom (Dim' ZModHom
-> Dim' ZModHom -> Entries N N ZModHom -> Matrix ZModHom
forall x. Dim' x -> Dim' x -> Entries N N x -> Matrix x
Matrix (AbGroup -> Dim' ZModHom
abgDim AbGroup
g'') Dim' ZModHom
c Entries N N ZModHom
xs') where
        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
$ N -> [(ZMod, N)] -> [(Row N ZModHom, N)] -> [(Row N ZModHom, N)]
forall i j.
(Enum i, Ord i) =>
i -> [(ZMod, i)] -> [(Row j ZModHom, i)] -> [(Row j ZModHom, i)]
divRows N
0 (((ZMod, N) -> ZMod) -> [(ZMod, N)] -> [ZMod]
forall a b. (a -> b) -> [a] -> [b]
forall (h :: * -> * -> *) (f :: * -> *) a b.
Applicative1 h f =>
h a b -> f a -> f b
amap1 (ZMod, N) -> ZMod
forall a b. (a, b) -> a
fst [(ZMod, N)]
g's [ZMod] -> [N] -> [(ZMod, N)]
forall a b. [a] -> [b] -> [(a, b)]
`zip` [N
0..]) (Col N (Row N ZModHom) -> [(Row N ZModHom, N)]
forall (s :: * -> *) x. Sequence s N x => s x -> [(x, N)]
listN (Col N (Row N ZModHom) -> [(Row N ZModHom, N)])
-> Col N (Row N ZModHom) -> [(Row N ZModHom, N)]
forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ Entries N N ZModHom -> Col N (Row N ZModHom)
forall i j x. Eq i => Entries i j x -> Col i (Row j x)
etscr Entries N N ZModHom
xs)
        
        divRows :: (Enum i, Ord i)
          => i -> [(ZMod,i)] -> [(Row j ZModHom,i)] -> [(Row j ZModHom,i)]
        divRows :: forall i j.
(Enum i, Ord i) =>
i -> [(ZMod, i)] -> [(Row j ZModHom, i)] -> [(Row j ZModHom, i)]
divRows i
_ [] [(Row j ZModHom, i)]
_   = []
        divRows i
_ [(ZMod, i)]
_ []   = []
        divRows i
i'' ((ZMod N
n,i
i):[(ZMod, i)]
zis') rws :: [(Row j ZModHom, i)]
rws@((Row j ZModHom
rw,i
i'):[(Row j ZModHom, i)]
rws')
          | N
n N -> N -> Bool
forall a. Eq a => a -> a -> Bool
== N
0    = i -> [(ZMod, i)] -> [(Row j ZModHom, i)] -> [(Row j ZModHom, i)]
forall i j.
(Enum i, Ord i) =>
i -> [(ZMod, i)] -> [(Row j ZModHom, i)] -> [(Row j ZModHom, i)]
divRows i
i'' [(ZMod, i)]
zis' [(Row j ZModHom, i)]
rws
          | i
i i -> i -> Bool
forall a. Eq a => a -> a -> Bool
== i
i'   = ((ZModHom -> ZModHom) -> Row j ZModHom -> 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 -> ZModHom
divZHom (N -> Z
forall a b. Embeddable a b => a -> b
inj N
n)) Row j ZModHom
rw,i
i'')(Row j ZModHom, i) -> [(Row j ZModHom, i)] -> [(Row j ZModHom, i)]
forall a. a -> [a] -> [a]
:i -> [(ZMod, i)] -> [(Row j ZModHom, i)] -> [(Row j ZModHom, i)]
forall i j.
(Enum i, Ord i) =>
i -> [(ZMod, i)] -> [(Row j ZModHom, i)] -> [(Row j ZModHom, i)]
divRows (i -> i
forall a. Enum a => a -> a
succ i
i'') [(ZMod, i)]
zis' [(Row j ZModHom, i)]
rws'
          | Bool
otherwise = i -> [(ZMod, i)] -> [(Row j ZModHom, i)] -> [(Row j ZModHom, i)]
forall i j.
(Enum i, Ord i) =>
i -> [(ZMod, i)] -> [(Row j ZModHom, i)] -> [(Row j ZModHom, i)]
divRows (i -> i
forall a. Enum a => a -> a
succ i
i'') [(ZMod, i)]
zis' [(Row j ZModHom, i)]
rws

        divZHom :: Z -> ZModHom -> ZModHom
        divZHom :: Z -> ZModHom -> ZModHom
divZHom Z
q ZModHom
h = Orientation ZMod -> Z -> ZModHom
zmh (ZModHom -> Orientation (Point ZModHom)
forall q. Oriented q => q -> Orientation (Point q)
orientation ZModHom
h) (Z -> Z -> Z
forall a. Integral a => a -> a -> a
div (ZModHom -> Z
toZ ZModHom
h) Z
q)
    
    coker :: Cokernel N1 AbHom
coker = 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
dg AbHom
p) Cone Dst 'Injective ('Parallel 'RightToLeft) N2 N1 AbHom -> AbHom
univ where
      dg :: Diagram ('Parallel 'RightToLeft) N2 N1 AbHom
dg = Point AbHom
-> Point AbHom
-> FinList N1 AbHom
-> Diagram ('Parallel 'RightToLeft) N2 N1 AbHom
forall a (m :: N').
Point a
-> Point a
-> FinList m a
-> Diagram ('Parallel 'RightToLeft) N2 m a
DiagramParallelRL (AbHom -> Point AbHom
forall q. Oriented q => q -> Point q
end AbHom
p') (AbHom -> Point AbHom
forall q. Oriented q => q -> Point q
start AbHom
p') (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)
      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 Dim' ZModHom
r Dim' ZModHom
_ Entries N N ZModHom
xs))) = Matrix ZModHom -> AbHom
AbHom (Dim' ZModHom
-> Dim' ZModHom -> Entries N N ZModHom -> Matrix ZModHom
forall x. Dim' x -> Dim' x -> Entries N N x -> Matrix x
Matrix Dim' ZModHom
r (AbGroup -> Dim' ZModHom
abgDim AbGroup
g) Entries N N ZModHom
xs') where
        xs' :: Entries N N ZModHom
xs' = 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
$ N -> [(ZMod, N)] -> [(Col N ZModHom, N)] -> [(Col N ZModHom, N)]
forall j i.
(Ord j, Enum j) =>
j -> [(ZMod, j)] -> [(Col i ZModHom, j)] -> [(Col i ZModHom, j)]
castCols N
0 [(ZMod, N)]
gs (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
xs)

        castCols :: (Ord j, Enum j)
          => j -> [(ZMod,j)] -> [(Col i ZModHom,j)] -> [(Col i ZModHom,j)]
        castCols :: forall j i.
(Ord j, Enum j) =>
j -> [(ZMod, j)] -> [(Col i ZModHom, j)] -> [(Col i ZModHom, j)]
castCols j
_ [] [(Col i ZModHom, j)]
_  = []
        castCols j
_ [(ZMod, j)]
_ []  = []
        castCols j
j'' ((g :: ZMod
g@(ZMod N
n),j
j):[(ZMod, j)]
gs) cls :: [(Col i ZModHom, j)]
cls@((Col i ZModHom
cl,j
j'):[(Col i ZModHom, j)]
cls')
          | N
n N -> N -> Bool
forall a. Eq a => a -> a -> Bool
== N
1    = j -> [(ZMod, j)] -> [(Col i ZModHom, j)] -> [(Col i ZModHom, j)]
forall j i.
(Ord j, Enum j) =>
j -> [(ZMod, j)] -> [(Col i ZModHom, j)] -> [(Col i ZModHom, j)]
castCols j
j'' [(ZMod, j)]
gs [(Col i ZModHom, j)]
cls
          | j
j'' j -> j -> Bool
forall a. Eq a => a -> a -> Bool
== j
j' = ((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
castZHom ZMod
g) 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, j)] -> [(Col i ZModHom, j)] -> [(Col i ZModHom, j)]
forall j i.
(Ord j, Enum j) =>
j -> [(ZMod, j)] -> [(Col i ZModHom, j)] -> [(Col i ZModHom, j)]
castCols (j -> j
forall a. Enum a => a -> a
succ j
j'') [(ZMod, j)]
gs [(Col i ZModHom, j)]
cls'
          | Bool
otherwise = j -> [(ZMod, j)] -> [(Col i ZModHom, j)] -> [(Col i ZModHom, j)]
forall j i.
(Ord j, Enum j) =>
j -> [(ZMod, j)] -> [(Col i ZModHom, j)] -> [(Col i ZModHom, j)]
castCols (j -> j
forall a. Enum a => a -> a
succ j
j'') [(ZMod, j)]
gs [(Col i ZModHom, j)]
cls

        castZHom :: ZMod -> ZModHom -> ZModHom
        castZHom :: ZMod -> ZModHom -> ZModHom
castZHom ZMod
g ZModHom
h = Orientation ZMod -> Z -> ZModHom
zmh (ZMod
g ZMod -> 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)

    lft :: Slice From (Free k) AbHom -> AbHom
    lft :: forall (k :: N'). Slice 'From (Free k) AbHom -> AbHom
lft (SliceFrom Free k AbHom
_ (AbHom (Matrix Dim' ZModHom
_ Dim' ZModHom
c Entries N N ZModHom
xs))) = Matrix ZModHom -> AbHom
AbHom (Dim' ZModHom
-> Dim' ZModHom -> Entries N N ZModHom -> Matrix ZModHom
forall x. Dim' x -> Dim' x -> Entries N N x -> Matrix x
Matrix (AbGroup -> Dim' ZModHom
abgDim AbGroup
g') Dim' ZModHom
c Entries N N ZModHom
xs') where
      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
$ N -> [(ZMod, N)] -> [(Row N ZModHom, N)] -> [(Row N ZModHom, N)]
forall i j.
(Ord i, Enum i) =>
i -> [(ZMod, i)] -> [(Row j ZModHom, i)] -> [(Row j ZModHom, i)]
lftRows N
0 [(ZMod, N)]
gs (Col N (Row N ZModHom) -> [(Row N ZModHom, N)]
forall (s :: * -> *) x. Sequence s N x => s x -> [(x, N)]
listN (Col N (Row N ZModHom) -> [(Row N ZModHom, N)])
-> Col N (Row N ZModHom) -> [(Row N ZModHom, N)]
forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ Entries N N ZModHom -> Col N (Row N ZModHom)
forall i j x. Eq i => Entries i j x -> Col i (Row j x)
etscr Entries N N ZModHom
xs)

      lftRows :: (Ord i, Enum i)
        => i -> [(ZMod,i)] -> [(Row j ZModHom,i)] -> [(Row j ZModHom,i)]
      lftRows :: forall i j.
(Ord i, Enum i) =>
i -> [(ZMod, i)] -> [(Row j ZModHom, i)] -> [(Row j ZModHom, i)]
lftRows i
_ [] [(Row j ZModHom, i)]
_ = []
      lftRows i
_ [(ZMod, i)]
_ [] = []
      lftRows i
i'' ((ZMod N
n,i
i):[(ZMod, i)]
gs) rws :: [(Row j ZModHom, i)]
rws@((Row j ZModHom
rw,i
i'):[(Row j ZModHom, i)]
rws')
        | N
n N -> N -> Bool
forall a. Eq a => a -> a -> Bool
== N
1    = i -> [(ZMod, i)] -> [(Row j ZModHom, i)] -> [(Row j ZModHom, i)]
forall i j.
(Ord i, Enum i) =>
i -> [(ZMod, i)] -> [(Row j ZModHom, i)] -> [(Row j ZModHom, i)]
lftRows i
i'' [(ZMod, i)]
gs [(Row j ZModHom, i)]
rws
        | i
i i -> i -> Bool
forall a. Eq a => a -> a -> Bool
== i
i'   = ((ZModHom -> ZModHom) -> Row j ZModHom -> 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) -> (ZModHom -> Z) -> ZModHom -> 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
. ZModHom -> Z
toZ) Row j ZModHom
rw,i
i'')(Row j ZModHom, i) -> [(Row j ZModHom, i)] -> [(Row j ZModHom, i)]
forall a. a -> [a] -> [a]
:i -> [(ZMod, i)] -> [(Row j ZModHom, i)] -> [(Row j ZModHom, i)]
forall i j.
(Ord i, Enum i) =>
i -> [(ZMod, i)] -> [(Row j ZModHom, i)] -> [(Row j ZModHom, i)]
lftRows (i -> i
forall a. Enum a => a -> a
succ i
i'') [(ZMod, i)]
gs [(Row j ZModHom, i)]
rws'
        | Bool
otherwise = i -> [(ZMod, i)] -> [(Row j ZModHom, i)] -> [(Row j ZModHom, i)]
forall i j.
(Ord i, Enum i) =>
i -> [(ZMod, i)] -> [(Row j ZModHom, i)] -> [(Row j ZModHom, i)]
lftRows (i -> i
forall a. Enum a => a -> a
succ i
i'') [(ZMod, i)]
gs [(Row j ZModHom, i)]
rws

--------------------------------------------------------------------------------
-- XSomeFreeSliceFromLiftable -

-- | random variable for 'AbHom'.
xsfsflAbHom :: XSomeFreeSliceFromLiftable AbHom
xsfsflAbHom :: XSomeFreeSliceFromLiftable AbHom
xsfsflAbHom = (Point AbHom -> X (SomeFreeSlice 'From AbHom))
-> XSomeFreeSliceFromLiftable AbHom
forall a.
(Point a -> X (SomeFreeSlice 'From a))
-> XSomeFreeSliceFromLiftable a
XSomeFreeSliceFromLiftable Point AbHom -> X (SomeFreeSlice 'From AbHom)
AbGroup -> X (SomeFreeSlice 'From AbHom)
xsf where
  q :: Q
q = Q
0.1
  xsf :: AbGroup -> X (SomeFreeSlice 'From AbHom)
xsf AbGroup
g = do
    SomeNatural W n
k <- X N -> X SomeNatural
xSomeNatural (N -> N -> X N
xNB N
0 N
stdMaxDim)
    N
d <- N -> N -> X N
xNB N
1 N
10
    AbHom
h <- Q -> N -> N -> N -> AbGroup -> X AbHom
xAbHomTo (N -> Q
forall a b. Embeddable a b => a -> b
inj N
d Q -> Q -> Q
forall c. Multiplicative c => c -> c -> c
* Q
q) (W n -> N
forall x. LengthN x => x -> N
lengthN W n
k) N
0 N
0 AbGroup
g
    SomeFreeSlice 'From AbHom -> X (SomeFreeSlice 'From AbHom)
forall a. a -> X a
forall (m :: * -> *) a. Monad m => a -> m a
return (SomeFreeSlice 'From AbHom -> X (SomeFreeSlice 'From AbHom))
-> SomeFreeSlice 'From AbHom -> X (SomeFreeSlice 'From AbHom)
forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ Slice 'From (Free n) AbHom -> SomeFreeSlice 'From AbHom
forall (k :: N') c (s :: Site).
(Attestable k, Sliced (Free k) c) =>
Slice s (Free k) c -> SomeFreeSlice s c
SomeFreeSlice (Slice 'From (Free n) AbHom -> SomeFreeSlice 'From AbHom)
-> Slice 'From (Free n) AbHom -> SomeFreeSlice 'From AbHom
forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ Free n AbHom -> AbHom -> Slice 'From (Free n) AbHom
forall (i :: * -> *) c. i c -> c -> Slice 'From i c
SliceFrom (W n -> Free n AbHom
forall (k :: N') c. Any k -> Free k c
Free W n
k) AbHom
h
    
instance XStandardSomeFreeSliceFromLiftable AbHom where
  xStandardSomeFreeSliceFromLiftable :: XSomeFreeSliceFromLiftable AbHom
xStandardSomeFreeSliceFromLiftable = XSomeFreeSliceFromLiftable AbHom
xsfsflAbHom
  
--------------------------------------------------------------------------------
-- AbGroup - XStandard -

-- | the maximal length of abelian groups for the standard random variable of type
-- @'X' 'AbGroup'@.
--
-- __Property__ @1 '<=' 'stdMaxDim'@.
stdMaxDim :: N
stdMaxDim :: N
stdMaxDim = N
10

stdMaxPrime :: N
stdMaxPrime :: N
stdMaxPrime = N
1000

stdPrimes :: [N]
stdPrimes :: [N]
stdPrimes = (N -> Bool) -> [N] -> [N]
forall a. (a -> Bool) -> [a] -> [a]
takeWhile (N -> N -> Bool
forall a. Ord a => a -> a -> Bool
<=N
stdMaxPrime) [N]
primes

instance XStandard AbGroup where
  xStandard :: X AbGroup
xStandard = X (X AbGroup) -> X AbGroup
forall (m :: * -> *) a. Monad m => m (m a) -> m a
join
            (X (X AbGroup) -> X AbGroup) -> X (X AbGroup) -> X AbGroup
forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ [(Q, X AbGroup)] -> X (X AbGroup)
forall a. [(Q, a)] -> X a
xOneOfW [ (Q
99,([ZMod] -> AbGroup) -> X [ZMod] -> X AbGroup
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 (ProductSymbol ZMod -> AbGroup
AbGroup (ProductSymbol ZMod -> AbGroup)
-> ([ZMod] -> ProductSymbol ZMod) -> [ZMod] -> AbGroup
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
. [ZMod] -> ProductSymbol ZMod
forall x. Entity x => [x] -> ProductSymbol x
productSymbol) (X [ZMod] -> X AbGroup) -> X [ZMod] -> X AbGroup
forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ N -> N -> X ZMod -> X [ZMod]
forall x. N -> N -> X x -> X [x]
xTakeB N
1 N
stdMaxDim X ZMod
forall x. XStandard x => X x
xStandard)
                      , ( Q
1,AbGroup -> X AbGroup
forall a. a -> X a
forall (m :: * -> *) a. Monad m => a -> m a
return (AbGroup -> X AbGroup) -> AbGroup -> X AbGroup
forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ Point AbGroup -> AbGroup
forall c. Multiplicative c => Point c -> c
one ())
                      ]

instance XStandardPoint AbHom

--------------------------------------------------------------------------------
-- xAbHom -

-- | random variable for 'AbHom' given by a density and an orientation.
xAbHom :: Q -> Orientation AbGroup -> X AbHom
xAbHom :: Q -> Orientation AbGroup -> X AbHom
xAbHom Q
q = Q -> X Z -> Orientation AbGroup -> X AbHom
xAbHom' Q
q (Z -> Z -> X Z
xZB (-Z
100) Z
100)

-- | random variable of homomorphism of the given 'Orientation.
xAbHom'
  :: Q -- ^ density @d@.
  -> X Z
  -> Orientation AbGroup -> X AbHom
xAbHom' :: Q -> X Z -> Orientation AbGroup -> X AbHom
xAbHom' Q
d X Z
xz (AbGroup ProductSymbol ZMod
a :> AbGroup ProductSymbol ZMod
b)
  | N
dab N -> N -> Bool
forall a. Eq a => a -> a -> Bool
== N
0 = AbHom -> X AbHom
forall a. a -> X a
forall (m :: * -> *) a. Monad m => a -> m a
return (AbHom -> X AbHom) -> AbHom -> X AbHom
forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ Matrix ZModHom -> AbHom
AbHom (Matrix ZModHom -> AbHom) -> Matrix ZModHom -> AbHom
forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ Root (Matrix ZModHom) -> Matrix ZModHom
forall a. Additive a => Root a -> a
zero (CSequence (Point ZModHom) -> Dim' ZModHom
forall x. CSequence (Point x) -> Dim x (Point x)
Dim CSequence (Point ZModHom)
ProductSymbol ZMod
a Dim ZModHom ZMod
-> Dim ZModHom ZMod -> Orientation (Dim ZModHom ZMod)
forall p. p -> p -> Orientation p
:> CSequence (Point ZModHom) -> Dim' ZModHom
forall x. CSequence (Point x) -> Dim x (Point x)
Dim CSequence (Point ZModHom)
ProductSymbol ZMod
b)
  | Bool
otherwise = X [(ZModHom, N, N)]
xxs X [(ZModHom, N, N)] -> ([(ZModHom, N, N)] -> X AbHom) -> X AbHom
forall a b. X a -> (a -> X b) -> X b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= AbHom -> X AbHom
forall a. a -> X a
forall (m :: * -> *) a. Monad m => a -> m a
return (AbHom -> X AbHom)
-> ([(ZModHom, N, N)] -> AbHom) -> [(ZModHom, N, N)] -> X 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
. Matrix ZModHom -> AbHom
AbHom (Matrix ZModHom -> AbHom)
-> ([(ZModHom, N, N)] -> Matrix ZModHom)
-> [(ZModHom, N, N)]
-> 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' ZModHom -> Dim' ZModHom -> [(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 (CSequence (Point ZModHom) -> Dim' ZModHom
forall x. CSequence (Point x) -> Dim x (Point x)
Dim CSequence (Point ZModHom)
ProductSymbol ZMod
b) (CSequence (Point ZModHom) -> Dim' ZModHom
forall x. CSequence (Point x) -> Dim x (Point x)
Dim CSequence (Point ZModHom)
ProductSymbol ZMod
a)
  where
    as :: [(ZMod, N)]
as = ProductSymbol ZMod -> [(ZMod, N)]
forall x. ProductSymbol x -> [(x, N)]
psyxs ProductSymbol ZMod
a
    bs :: [(ZMod, N)]
bs = ProductSymbol ZMod -> [(ZMod, N)]
forall x. ProductSymbol x -> [(x, N)]
psyxs ProductSymbol ZMod
b
    da :: N
da = [(ZMod, N)] -> N
forall x. LengthN x => x -> N
lengthN [(ZMod, N)]
as
    db :: N
db = [(ZMod, N)] -> N
forall x. LengthN x => x -> N
lengthN [(ZMod, N)]
bs
        
    dab :: N
dab = N
daN -> N -> N
forall c. Multiplicative c => c -> c -> c
*N
db
    n :: N
n = Z -> N
forall a b. Projectible a b => b -> a
prj (Z -> N) -> Z -> N
forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ Q -> Z
forall r. Number r => r -> Z
zFloor (Q
dQ -> Q -> Q
forall c. Multiplicative c => c -> c -> c
*N -> Q
forall a b. Embeddable a b => a -> b
inj N
dab) :: N

    xs :: [((ZModHom, N), N, N)]
xs = (((ZModHom, N), N, N) -> Bool)
-> [((ZModHom, N), N, N)] -> [((ZModHom, N), N, N)]
forall a. (a -> Bool) -> [a] -> [a]
filter (\((ZModHom
h,N
_),N
_,N
_) -> Bool -> Bool
forall b. Boolean b => b -> b
not (ZModHom -> Bool
forall a. Additive a => a -> Bool
isZero ZModHom
h))
       [(Orientation ZMod -> (ZModHom, N)
zmhGenOrd (ZMod
a ZMod -> ZMod -> Orientation ZMod
forall p. p -> p -> Orientation p
:> ZMod
b),N
i,N
j) | (ZMod
a,N
j) <- [(ZMod, N)]
as, (ZMod
b,N
i) <- [(ZMod, N)]
bs] 
         
    xxs :: X [(ZModHom, N, N)]
xxs = do
      Permutation N
p <- N -> N -> X (Permutation N)
forall i. (Ord i, Enum i) => i -> i -> X (Permutation i)
xPermutationB N
0 (N -> N
forall a. Enum a => a -> a
pred N
dab) -- 0 < dba
      [((ZModHom, N), N, N)] -> X [(ZModHom, N, N)]
xets (N -> [((ZModHom, N), N, N)] -> [((ZModHom, N), N, N)]
forall a. N -> [a] -> [a]
takeN N
n ([((ZModHom, N), N, N)]
xs [((ZModHom, N), N, N)] -> Permutation N -> [((ZModHom, N), N, N)]
forall f x. Opr f x => x -> f -> x
<* Permutation N
p))

    xets :: [((ZModHom, N), N, N)] -> X [(ZModHom, N, N)]
xets []            = [(ZModHom, N, N)] -> X [(ZModHom, N, N)]
forall a. a -> X a
forall (m :: * -> *) a. Monad m => a -> m a
return []
    xets (((ZModHom, N)
ho,N
i,N
j):[((ZModHom, N), N, N)]
xs) = do
      [(ZModHom, N, N)]
xs' <- [((ZModHom, N), N, N)] -> X [(ZModHom, N, N)]
xets [((ZModHom, N), N, N)]
xs
      ZModHom
h' <- (ZModHom, N) -> X ZModHom
xh (ZModHom, N)
ho
      [(ZModHom, N, N)] -> X [(ZModHom, N, N)]
forall a. a -> X a
forall (m :: * -> *) a. Monad m => a -> m a
return ((ZModHom
h',N
i,N
j)(ZModHom, N, N) -> [(ZModHom, N, N)] -> [(ZModHom, N, N)]
forall a. a -> [a] -> [a]
:[(ZModHom, N, N)]
xs')

    xh :: (ZModHom, N) -> X ZModHom
xh (ZModHom
h,N
0) = X Z
xz X Z -> (Z -> X ZModHom) -> X ZModHom
forall a b. X a -> (a -> X b) -> X b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= ZModHom -> X ZModHom
forall a. a -> X a
forall (m :: * -> *) a. Monad m => a -> m a
return (ZModHom -> X ZModHom) -> (Z -> ZModHom) -> Z -> X 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
. (Scalar ZModHom -> ZModHom -> ZModHom
forall v. Vectorial v => Scalar v -> v -> v
! ZModHom
h)
    xh (ZModHom
h,N
1) = ZModHom -> X ZModHom
forall a. a -> X a
forall (m :: * -> *) a. Monad m => a -> m a
return ZModHom
h
    xh (ZModHom
h,N
o) = do
      Z
z <- Z -> Z -> X Z
xZB Z
1 (Z -> Z
forall a. Enum a => a -> a
pred (N -> Z
forall a b. Embeddable a b => a -> b
inj N
o))
      ZModHom -> X ZModHom
forall a. a -> X a
forall (m :: * -> *) a. Monad m => a -> m a
return (Z
Scalar ZModHom
z Scalar ZModHom -> ZModHom -> ZModHom
forall v. Vectorial v => Scalar v -> v -> v
! ZModHom
h)

dstXAbHom :: (AbHom -> String) -> Int -> Q -> Orientation AbGroup -> IO ()
dstXAbHom :: (AbHom -> String) -> Int -> Q -> Orientation AbGroup -> IO ()
dstXAbHom AbHom -> String
s Int
n Q
q Orientation AbGroup
r = IO Omega
getOmega IO Omega -> (Omega -> IO ()) -> IO ()
forall a b. IO a -> (a -> IO b) -> IO b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Int -> X String -> Omega -> IO ()
forall x. (Show x, Ord x) => Int -> X x -> Omega -> IO ()
putDistribution Int
n ((AbHom -> String) -> X AbHom -> X String
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 AbHom -> String
s (X AbHom -> X String) -> X AbHom -> X String
forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ Q -> Orientation AbGroup -> X AbHom
xAbHom Q
q Orientation AbGroup
r) 

--------------------------------------------------------------------------------
-- xAbHomTo -

-- | random variable of homomorphisms between abelian groups with 'end' equal to the given
-- one.
--
-- @
--    r s t
--   [f    ] a
--   [     ] b
--   [g h  ] c
-- @
xAbHomTo :: Q -> N -> N -> N -> AbGroup -> X AbHom
xAbHomTo :: Q -> N -> N -> N -> AbGroup -> X AbHom
xAbHomTo Q
d N
r N
s N
t (AbGroup ProductSymbol ZMod
g) = (Matrix ZModHom -> AbHom) -> X (Matrix ZModHom) -> X 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 Matrix ZModHom -> AbHom
AbHom X (Matrix ZModHom)
xm where

  xm :: X (Matrix ZModHom)
  xm :: X (Matrix ZModHom)
xm = do
    ProductSymbol ZMod
dr <- ProductSymbol ZMod -> X (ProductSymbol ZMod)
forall a. a -> X a
forall (m :: * -> *) a. Monad m => a -> m a
return (ZMod -> ProductSymbol ZMod
forall x. Entity x => x -> ProductSymbol x
sy (N -> ZMod
ZMod N
0) ProductSymbol ZMod
-> Exponent (ProductSymbol ZMod) -> ProductSymbol ZMod
forall f. Exponential f => f -> Exponent f -> f
^ N
Exponent (ProductSymbol ZMod)
r) 
    ProductSymbol ZMod
ds <- X (ProductSymbol ZMod)
xds
    ProductSymbol ZMod
dt <- X (ProductSymbol ZMod)
xdt
    AbHom Matrix ZModHom
f <- Q -> Orientation AbGroup -> X AbHom
xAbHom Q
d (ProductSymbol ZMod -> AbGroup
AbGroup ProductSymbol ZMod
dr AbGroup -> AbGroup -> Orientation AbGroup
forall p. p -> p -> Orientation p
:> ProductSymbol ZMod -> AbGroup
AbGroup ProductSymbol ZMod
da)
    AbHom Matrix ZModHom
g <- Q -> Orientation AbGroup -> X AbHom
xAbHom Q
d (ProductSymbol ZMod -> AbGroup
AbGroup ProductSymbol ZMod
dr AbGroup -> AbGroup -> Orientation AbGroup
forall p. p -> p -> Orientation p
:> ProductSymbol ZMod -> AbGroup
AbGroup ProductSymbol ZMod
dc)
    AbHom Matrix ZModHom
h <- Q -> Orientation AbGroup -> X AbHom
xAbHom Q
d (ProductSymbol ZMod -> AbGroup
AbGroup ProductSymbol ZMod
ds AbGroup -> AbGroup -> Orientation AbGroup
forall p. p -> p -> Orientation p
:> ProductSymbol ZMod -> AbGroup
AbGroup ProductSymbol ZMod
dc)
    let cl :: [Dim' ZModHom]
cl = (ProductSymbol ZMod -> Dim' ZModHom)
-> [ProductSymbol ZMod] -> [Dim' ZModHom]
forall a b. (a -> b) -> [a] -> [b]
forall (h :: * -> * -> *) (f :: * -> *) a b.
Applicative1 h f =>
h a b -> f a -> f b
amap1 CSequence (Point ZModHom) -> Dim' ZModHom
ProductSymbol ZMod -> Dim' ZModHom
forall x. CSequence (Point x) -> Dim x (Point x)
Dim [ProductSymbol ZMod
dr,ProductSymbol ZMod
ds,ProductSymbol ZMod
dt]
        rw :: [Dim' ZModHom]
rw = (ProductSymbol ZMod -> Dim' ZModHom)
-> [ProductSymbol ZMod] -> [Dim' ZModHom]
forall a b. (a -> b) -> [a] -> [b]
forall (h :: * -> * -> *) (f :: * -> *) a b.
Applicative1 h f =>
h a b -> f a -> f b
amap1 CSequence (Point ZModHom) -> Dim' ZModHom
ProductSymbol ZMod -> Dim' ZModHom
forall x. CSequence (Point x) -> Dim x (Point x)
Dim [ProductSymbol ZMod
da,ProductSymbol ZMod
db,ProductSymbol ZMod
dc]
        m :: Matrix ZModHom
m  = 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]
-> [Dim' 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]
rw [Dim' ZModHom]
cl [(Matrix ZModHom
f,N
0,N
0),(Matrix ZModHom
g,N
2,N
0),(Matrix ZModHom
h,N
2,N
1)]
     in do
      ColTrafo ZModHom
pc <- Dim' ZModHom -> X (ColTrafo ZModHom)
forall {x}. Distributive x => Dim x (Point x) -> X (ColTrafo x)
xpc (Matrix ZModHom -> Point (Matrix ZModHom)
forall q. Oriented q => q -> Point q
start Matrix ZModHom
m)
      Matrix ZModHom -> X (Matrix ZModHom)
forall a. a -> X a
forall (m :: * -> *) a. Monad m => a -> m a
return ((RowTrafo ZModHom
pr RowTrafo ZModHom -> Matrix ZModHom -> Matrix ZModHom
forall f x. Opl f x => f -> x -> x
*> Matrix ZModHom
m) Matrix ZModHom -> ColTrafo ZModHom -> Matrix ZModHom
forall f x. Opr f x => x -> f -> x
<* ColTrafo ZModHom
pc)

  (ProductSymbol ZMod
g',Permutation N
p) = (ZMod -> ZMod -> Ordering)
-> (ZMod -> ZMod)
-> ProductSymbol ZMod
-> (ProductSymbol ZMod, Permutation N)
forall (s :: * -> *) x w.
PermutableSequence s N x =>
(w -> w -> Ordering) -> (x -> w) -> s x -> (s x, Permutation N)
permuteByN ZMod -> ZMod -> Ordering
forall a. Ord a => a -> a -> Ordering
compare ZMod -> ZMod
forall x. x -> x
id ProductSymbol ZMod
g

  pr :: RowTrafo ZModHom
  pr :: RowTrafo ZModHom
pr = GLT ZModHom -> RowTrafo ZModHom
forall a. GLT a -> RowTrafo a
RowTrafo (Dim' ZModHom -> Dim' ZModHom -> Permutation N -> GLT ZModHom
forall x.
Distributive x =>
Dim' x -> Dim' x -> Permutation N -> GLT x
permute (CSequence (Point ZModHom) -> Dim' ZModHom
forall x. CSequence (Point x) -> Dim x (Point x)
Dim CSequence (Point ZModHom)
ProductSymbol ZMod
g) (CSequence (Point ZModHom) -> Dim' ZModHom
forall x. CSequence (Point x) -> Dim x (Point x)
Dim CSequence (Point ZModHom)
ProductSymbol ZMod
g') (Permutation N -> Permutation N
forall c. Invertible c => c -> c
invert Permutation N
p))

  xpc :: Dim x (Point x) -> X (ColTrafo x)
xpc Dim x (Point x)
c = do
    Permutation N
p <- N -> X (Permutation N)
xPermutationN (Dim x (Point x) -> N
forall x. LengthN x => x -> N
lengthN Dim x (Point x)
c)
    ColTrafo x -> X (ColTrafo x)
forall a. a -> X a
forall (m :: * -> *) a. Monad m => a -> m a
return (GLT x -> ColTrafo x
forall x. GLT x -> ColTrafo x
ColTrafo (Dim x (Point x) -> Dim x (Point x) -> Permutation N -> GLT x
forall x.
Distributive x =>
Dim' x -> Dim' x -> Permutation N -> GLT x
permute Dim x (Point x)
c (Dim x (Point x)
c Dim x (Point x) -> Permutation N -> Dim x (Point x)
forall f x. Opr f x => x -> f -> x
<* Permutation N -> Permutation N
forall c. Invertible c => c -> c
invert Permutation N
p) Permutation N
p))
      
  expAt :: N -> Word r ZMod -> (r, Word r ZMod)
expAt N
n Word r ZMod
w = case Word r ZMod
w of
    Word ((ZMod N
m,r
r):[(ZMod, r)]
w') | N
n N -> N -> Bool
forall a. Eq a => a -> a -> Bool
== N
m -> (r
r,[(ZMod, r)] -> Word r ZMod
forall r a. [(a, r)] -> Word r a
Word [(ZMod, r)]
w')
    Word r ZMod
_                             -> (r
0,Word r ZMod
w)

  w' :: Word N ZMod
w' = ProductSymbol ZMod -> Word N ZMod
forall x. Entity x => ProductSymbol x -> Word N x
psywrd ProductSymbol ZMod
g'

  da :: ProductSymbol ZMod
da = ZMod -> ProductSymbol ZMod
forall x. Entity x => x -> ProductSymbol x
sy (N -> ZMod
ZMod N
0) ProductSymbol ZMod
-> Exponent (ProductSymbol ZMod) -> ProductSymbol ZMod
forall f. Exponential f => f -> Exponent f -> f
^ N
Exponent (ProductSymbol ZMod)
a
  (N
a,Word N ZMod
w'') = N -> Word N ZMod -> (N, Word N ZMod)
forall {r}. Num r => N -> Word r ZMod -> (r, Word r ZMod)
expAt N
0 Word N ZMod
w'
  
  db :: ProductSymbol ZMod
db = ZMod -> ProductSymbol ZMod
forall x. Entity x => x -> ProductSymbol x
sy (N -> ZMod
ZMod N
1) ProductSymbol ZMod
-> Exponent (ProductSymbol ZMod) -> ProductSymbol ZMod
forall f. Exponential f => f -> Exponent f -> f
^ N
Exponent (ProductSymbol ZMod)
b
  (N
b,Word N ZMod
w''') = N -> Word N ZMod -> (N, Word N ZMod)
forall {r}. Num r => N -> Word r ZMod -> (r, Word r ZMod)
expAt N
1 Word N ZMod
w''
  -- for all ((ZMod n),_) in w''' holds: 2 <= n
    
  dc :: ProductSymbol ZMod
dc = Word N ZMod -> ProductSymbol ZMod
forall x. Entity x => Word N x -> ProductSymbol x
wrdpsy Word N ZMod
w'''

  ms :: [N]
ms = ((ZMod, N) -> N) -> [(ZMod, N)] -> [N]
forall a b. (a -> b) -> [a] -> [b]
forall (h :: * -> * -> *) (f :: * -> *) a b.
Applicative1 h f =>
h a b -> f a -> f b
amap1 ((\(ZMod N
m) -> N
m) (ZMod -> N) -> ((ZMod, N) -> ZMod) -> (ZMod, N) -> N
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
. (ZMod, N) -> ZMod
forall a b. (a, b) -> a
fst) ([(ZMod, N)] -> [N]) -> [(ZMod, N)] -> [N]
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
w'''
  gms :: N
gms  = [N] -> N
gcds [N]
ms  
  lms :: N
lms  = [N] -> N
lcms [N]
ms
  -- 1 <= lms, because 2 <= m for all m in ms
  
  xsl :: X ZMod
xsl = do
    N
n <- N -> N -> X N
xNB N
1 N
10
    ZMod -> X ZMod
forall a. a -> X a
forall (m :: * -> *) a. Monad m => a -> m a
return (ZMod -> X ZMod) -> ZMod -> X ZMod
forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ N -> ZMod
ZMod (N
nN -> N -> N
forall c. Multiplicative c => c -> c -> c
*N
lms)

  xsg :: X ZMod
xsg | N
gms N -> N -> Bool
forall a. Ord a => a -> a -> Bool
< N
2   = X ZMod
forall x. X x
XEmpty
      | [(N, N)]
ws [(N, N)] -> [(N, N)] -> Bool
forall a. Eq a => a -> a -> Bool
== []  = X ZMod
forall x. X x
XEmpty
      | Bool
otherwise = do
          N
r  <- N -> N -> X N
xNB N
1 N
rMax
          [N]
ps <- N -> X N -> X [N]
forall x. N -> X x -> X [x]
xTakeN N
r ([N] -> X N
forall a. [a] -> X a
xOneOf [N]
fs)
          N
n  <- N -> N -> X N
xNB N
1 N
10
          ZMod -> X ZMod
forall a. a -> X a
forall (m :: * -> *) a. Monad m => a -> m a
return (ZMod -> X ZMod) -> ZMod -> X ZMod
forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ N -> ZMod
ZMod (N
n N -> N -> N
forall c. Multiplicative c => c -> c -> c
* (N -> N -> N) -> N -> [N] -> N
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl N -> N -> N
forall c. Multiplicative c => c -> c -> c
(*) N
1 [N]
ps)
    where Word [(N, N)]
ws  = N -> N -> Word N N
nFactorize' N
stdMaxPrime N
gms
          fs :: [N]
fs = ((N, N) -> N) -> [(N, N)] -> [N]
forall a b. (a -> b) -> [a] -> [b]
forall (h :: * -> * -> *) (f :: * -> *) a b.
Applicative1 h f =>
h a b -> f a -> f b
amap1 (N, N) -> N
forall a b. (a, b) -> a
fst [(N, N)]
ws
          rMax :: N
rMax = (N -> N -> N) -> N -> [N] -> N
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl N -> N -> N
forall a. Additive a => a -> a -> a
(+) N
0 ([N] -> N) -> [N] -> N
forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ ((N, N) -> N) -> [(N, N)] -> [N]
forall a b. (a -> b) -> [a] -> [b]
forall (h :: * -> * -> *) (f :: * -> *) a b.
Applicative1 h f =>
h a b -> f a -> f b
amap1 (N, N) -> N
forall a b. (a, b) -> b
snd [(N, N)]
ws
          -- 0 < nMax, because ws is not empty
          
  xds :: X (ProductSymbol ZMod)
xds = N -> X ZMod -> X [ZMod]
forall x. N -> X x -> X [x]
xTakeN N
s (X ZMod
xsg X ZMod -> X ZMod -> X ZMod
forall a. X a -> X a -> X a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> X ZMod
xsl) X [ZMod]
-> ([ZMod] -> X (ProductSymbol ZMod)) -> X (ProductSymbol ZMod)
forall a b. X a -> (a -> X b) -> X b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= ProductSymbol ZMod -> X (ProductSymbol ZMod)
forall a. a -> X a
forall (m :: * -> *) a. Monad m => a -> m a
return (ProductSymbol ZMod -> X (ProductSymbol ZMod))
-> ([ZMod] -> ProductSymbol ZMod)
-> [ZMod]
-> X (ProductSymbol 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
. [ZMod] -> ProductSymbol ZMod
forall x. Entity x => [x] -> ProductSymbol x
productSymbol

  xt :: X ZMod
xt | [N]
fs [N] -> [N] -> Bool
forall a. Eq a => a -> a -> Bool
== []  = X ZMod
forall x. X x
XEmpty
     | Bool
otherwise = do
    N
n <- N -> N -> X N
xNB N
1 N
5
    [N]
ps <- N -> X N -> X [N]
forall x. N -> X x -> X [x]
xTakeN N
n ([N] -> X N
forall a. [a] -> X a
xOneOf [N]
fs)
    ZMod -> X ZMod
forall a. a -> X a
forall (m :: * -> *) a. Monad m => a -> m a
return (ZMod -> X ZMod) -> ZMod -> X ZMod
forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ N -> ZMod
ZMod (N -> ZMod) -> N -> ZMod
forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ (N -> N -> N) -> N -> [N] -> N
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl N -> N -> N
forall c. Multiplicative c => c -> c -> c
(*) N
1 [N]
ps
    where fs :: [N]
fs = N -> [N] -> [N]
forall a. N -> [a] -> [a]
takeN N
10 ([N] -> [N]) -> [N] -> [N]
forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ (N -> Bool) -> [N] -> [N]
forall a. (a -> Bool) -> [a] -> [a]
filter ((N -> N -> Bool
forall a. Eq a => a -> a -> Bool
/=N
0) (N -> Bool) -> (N -> N) -> N -> Bool
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
. N -> N -> N
forall a. Integral a => a -> a -> a
mod N
lms) ([N]
stdPrimes)
    
  xdt :: X (ProductSymbol ZMod)
xdt = case X ZMod
xt of
    X ZMod
XEmpty -> ProductSymbol ZMod -> X (ProductSymbol ZMod)
forall a. a -> X a
forall (m :: * -> *) a. Monad m => a -> m a
return ([ZMod] -> ProductSymbol ZMod
forall x. Entity x => [x] -> ProductSymbol x
productSymbol [])
    X ZMod
_      -> N -> X ZMod -> X [ZMod]
forall x. N -> X x -> X [x]
xTakeN N
t X ZMod
xt X [ZMod]
-> ([ZMod] -> X (ProductSymbol ZMod)) -> X (ProductSymbol ZMod)
forall a b. X a -> (a -> X b) -> X b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= ProductSymbol ZMod -> X (ProductSymbol ZMod)
forall a. a -> X a
forall (m :: * -> *) a. Monad m => a -> m a
return (ProductSymbol ZMod -> X (ProductSymbol ZMod))
-> ([ZMod] -> ProductSymbol ZMod)
-> [ZMod]
-> X (ProductSymbol 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
. [ZMod] -> ProductSymbol ZMod
forall x. Entity x => [x] -> ProductSymbol x
productSymbol


dstXAbHomTo :: (AbHom -> String) -> Int -> Q -> N -> N -> N -> X AbGroup -> IO ()
dstXAbHomTo :: (AbHom -> String) -> Int -> Q -> N -> N -> N -> X AbGroup -> IO ()
dstXAbHomTo AbHom -> String
w Int
n Q
q N
r N
s N
t X AbGroup
xg = IO Omega
getOmega IO Omega -> (Omega -> IO ()) -> IO ()
forall a b. IO a -> (a -> IO b) -> IO b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Int -> X String -> Omega -> IO ()
forall x. (Show x, Ord x) => Int -> X x -> Omega -> IO ()
putDistribution Int
n ((AbHom -> String) -> X AbHom -> X String
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 AbHom -> String
w (X AbHom -> X String) -> X AbHom -> X String
forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ X AbHom
xh)
  where xh :: X AbHom
xh = X AbGroup
xg X AbGroup -> (AbGroup -> X AbHom) -> X AbHom
forall a b. X a -> (a -> X b) -> X b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Q -> N -> N -> N -> AbGroup -> X AbHom
xAbHomTo Q
q N
r N
s N
t

dns :: AbHom -> String
dns :: AbHom -> String
dns (AbHom (Matrix Dim' ZModHom
r Dim' ZModHom
c Entries N N ZModHom
xs))
  | N
rc N -> N -> Bool
forall a. Eq a => a -> a -> Bool
== N
0   = String
"empty"
  | Z
p Z -> Z -> Bool
forall a. Eq a => a -> a -> Bool
== Z
0    = String
"(" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Z -> String
forall a. Show a => a -> String
show Z
p String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"," String -> ShowS
forall a. [a] -> [a] -> [a]
++ Z -> String
forall a. Show a => a -> String
show (Z
pZ -> Z -> Z
forall a. Additive a => a -> a -> a
+Z
1) String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"%)"
  | Z
p Z -> Z -> Bool
forall a. Eq a => a -> a -> Bool
== Z
100  = String
"full"
  | Bool
otherwise = String
"[" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Z -> String
forall a. Show a => a -> String
show Z
p String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"," String -> ShowS
forall a. [a] -> [a] -> [a]
++ Z -> String
forall a. Show a => a -> String
show (Z
pZ -> Z -> Z
forall a. Additive a => a -> a -> a
+Z
1) String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"%)"
  
  where p :: Z
p = Q -> Z
forall r. Number r => r -> Z
zFloor (Q -> Z) -> Q -> Z
forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ (Q
100Q -> Q -> Q
forall c. Multiplicative c => c -> c -> c
*) (Q -> Q) -> Q -> Q
forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ (N -> Z
forall a b. Embeddable a b => a -> b
inj (Entries N N ZModHom -> N
forall x. LengthN x => x -> N
lengthN Entries N N ZModHom
xs) Z -> N -> Q
% N
rc)
        rc :: N
rc = Dim ZModHom ZMod -> N
forall x. LengthN x => x -> N
lengthN Dim' ZModHom
Dim ZModHom ZMod
r N -> N -> N
forall c. Multiplicative c => c -> c -> c
* Dim ZModHom ZMod -> N
forall x. LengthN x => x -> N
lengthN Dim' ZModHom
Dim ZModHom ZMod
c

lng :: AbHom -> String
lng :: AbHom -> String
lng (AbHom (Matrix Dim' ZModHom
r Dim' ZModHom
c Entries N N ZModHom
_)) = (N, N) -> String
forall a. Show a => a -> String
show (Dim ZModHom ZMod -> N
forall x. LengthN x => x -> N
lengthN Dim' ZModHom
Dim ZModHom ZMod
r,Dim ZModHom ZMod -> N
forall x. LengthN x => x -> N
lengthN Dim' ZModHom
Dim ZModHom ZMod
c)

lngMax :: AbHom -> String
lngMax :: AbHom -> String
lngMax (AbHom (Matrix Dim' ZModHom
r Dim' ZModHom
c Entries N N ZModHom
_)) = N -> String
forall a. Show a => a -> String
show (Dim ZModHom ZMod -> N
forall x. LengthN x => x -> N
lengthN Dim' ZModHom
Dim ZModHom ZMod
r N -> N -> N
forall a. Ord a => a -> a -> a
`max` Dim ZModHom ZMod -> N
forall x. LengthN x => x -> N
lengthN Dim' ZModHom
Dim ZModHom ZMod
c)

--------------------------------------------------------------------------------
-- xAbHomFrom -

-- | random variable of homomorphisms between abelian groups with 'start' equal to the given
-- one.
--
-- @
--    a b c
--   [f    ] r
--   [g   l] s
--   [h    ] t
-- @
xAbHomFrom :: Q -> N -> N -> N -> AbGroup -> X AbHom
xAbHomFrom :: Q -> N -> N -> N -> AbGroup -> X AbHom
xAbHomFrom Q
d N
r N
s N
t (AbGroup ProductSymbol ZMod
g) = (Matrix ZModHom -> AbHom) -> X (Matrix ZModHom) -> X 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 Matrix ZModHom -> AbHom
AbHom X (Matrix ZModHom)
xm where

  xm :: X (Matrix ZModHom)
  xm :: X (Matrix ZModHom)
xm = do
    ProductSymbol ZMod
dr <- ProductSymbol ZMod -> X (ProductSymbol ZMod)
forall a. a -> X a
forall (m :: * -> *) a. Monad m => a -> m a
return (ZMod -> ProductSymbol ZMod
forall x. Entity x => x -> ProductSymbol x
sy (N -> ZMod
ZMod N
0) ProductSymbol ZMod
-> Exponent (ProductSymbol ZMod) -> ProductSymbol ZMod
forall f. Exponential f => f -> Exponent f -> f
^ N
Exponent (ProductSymbol ZMod)
r)
    ProductSymbol ZMod
ds <- X (ProductSymbol ZMod)
xds
    ProductSymbol ZMod
dt <- X (ProductSymbol ZMod)
xdt
    AbHom Matrix ZModHom
f <- Q -> Orientation AbGroup -> X AbHom
xAbHom Q
d (ProductSymbol ZMod -> AbGroup
AbGroup ProductSymbol ZMod
da AbGroup -> AbGroup -> Orientation AbGroup
forall p. p -> p -> Orientation p
:> ProductSymbol ZMod -> AbGroup
AbGroup ProductSymbol ZMod
dr)
    AbHom Matrix ZModHom
g <- Q -> Orientation AbGroup -> X AbHom
xAbHom Q
d (ProductSymbol ZMod -> AbGroup
AbGroup ProductSymbol ZMod
da AbGroup -> AbGroup -> Orientation AbGroup
forall p. p -> p -> Orientation p
:> ProductSymbol ZMod -> AbGroup
AbGroup ProductSymbol ZMod
ds)
    AbHom Matrix ZModHom
h <- Q -> Orientation AbGroup -> X AbHom
xAbHom Q
d (ProductSymbol ZMod -> AbGroup
AbGroup ProductSymbol ZMod
da AbGroup -> AbGroup -> Orientation AbGroup
forall p. p -> p -> Orientation p
:> ProductSymbol ZMod -> AbGroup
AbGroup ProductSymbol ZMod
dt)
    AbHom Matrix ZModHom
l <- Q -> Orientation AbGroup -> X AbHom
xAbHom Q
d (ProductSymbol ZMod -> AbGroup
AbGroup ProductSymbol ZMod
dc AbGroup -> AbGroup -> Orientation AbGroup
forall p. p -> p -> Orientation p
:> ProductSymbol ZMod -> AbGroup
AbGroup ProductSymbol ZMod
ds)
    let cl :: [Dim' ZModHom]
cl = (ProductSymbol ZMod -> Dim' ZModHom)
-> [ProductSymbol ZMod] -> [Dim' ZModHom]
forall a b. (a -> b) -> [a] -> [b]
forall (h :: * -> * -> *) (f :: * -> *) a b.
Applicative1 h f =>
h a b -> f a -> f b
amap1 CSequence (Point ZModHom) -> Dim' ZModHom
ProductSymbol ZMod -> Dim' ZModHom
forall x. CSequence (Point x) -> Dim x (Point x)
Dim [ProductSymbol ZMod
da,ProductSymbol ZMod
db,ProductSymbol ZMod
dc]
        rw :: [Dim' ZModHom]
rw = (ProductSymbol ZMod -> Dim' ZModHom)
-> [ProductSymbol ZMod] -> [Dim' ZModHom]
forall a b. (a -> b) -> [a] -> [b]
forall (h :: * -> * -> *) (f :: * -> *) a b.
Applicative1 h f =>
h a b -> f a -> f b
amap1 CSequence (Point ZModHom) -> Dim' ZModHom
ProductSymbol ZMod -> Dim' ZModHom
forall x. CSequence (Point x) -> Dim x (Point x)
Dim [ProductSymbol ZMod
dr,ProductSymbol ZMod
ds,ProductSymbol ZMod
dt]
        m :: Matrix ZModHom
m  = 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]
-> [Dim' 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]
rw [Dim' ZModHom]
cl [(Matrix ZModHom
f,N
0,N
0),(Matrix ZModHom
g,N
1,N
0),(Matrix ZModHom
h,N
2,N
0),(Matrix ZModHom
l,N
1,N
2)]
     in do
      RowTrafo ZModHom
pr <- Dim' ZModHom -> X (RowTrafo ZModHom)
forall {a}. Distributive a => Dim a (Point a) -> X (RowTrafo a)
xpr (Matrix ZModHom -> Point (Matrix ZModHom)
forall q. Oriented q => q -> Point q
end Matrix ZModHom
m)
      Matrix ZModHom -> X (Matrix ZModHom)
forall a. a -> X a
forall (m :: * -> *) a. Monad m => a -> m a
return ((RowTrafo ZModHom
pr RowTrafo ZModHom -> Matrix ZModHom -> Matrix ZModHom
forall f x. Opl f x => f -> x -> x
*> Matrix ZModHom
m) Matrix ZModHom -> ColTrafo ZModHom -> Matrix ZModHom
forall f x. Opr f x => x -> f -> x
<* ColTrafo ZModHom
pc)

  (ProductSymbol ZMod
g',Permutation N
p) = (ZMod -> ZMod -> Ordering)
-> (ZMod -> ZMod)
-> ProductSymbol ZMod
-> (ProductSymbol ZMod, Permutation N)
forall (s :: * -> *) x w.
PermutableSequence s N x =>
(w -> w -> Ordering) -> (x -> w) -> s x -> (s x, Permutation N)
permuteByN ZMod -> ZMod -> Ordering
forall a. Ord a => a -> a -> Ordering
compare ZMod -> ZMod
forall x. x -> x
id ProductSymbol ZMod
g

  pc :: ColTrafo ZModHom
  pc :: ColTrafo ZModHom
pc = GLT ZModHom -> ColTrafo ZModHom
forall x. GLT x -> ColTrafo x
ColTrafo (Dim' ZModHom -> Dim' ZModHom -> Permutation N -> GLT ZModHom
forall x.
Distributive x =>
Dim' x -> Dim' x -> Permutation N -> GLT x
permute (CSequence (Point ZModHom) -> Dim' ZModHom
forall x. CSequence (Point x) -> Dim x (Point x)
Dim CSequence (Point ZModHom)
ProductSymbol ZMod
g') (CSequence (Point ZModHom) -> Dim' ZModHom
forall x. CSequence (Point x) -> Dim x (Point x)
Dim CSequence (Point ZModHom)
ProductSymbol ZMod
g) Permutation N
p)

  xpr :: Dim a (Point a) -> X (RowTrafo a)
xpr Dim a (Point a)
r = do
    Permutation N
p <- N -> X (Permutation N)
xPermutationN (Dim a (Point a) -> N
forall x. LengthN x => x -> N
lengthN Dim a (Point a)
r)
    RowTrafo a -> X (RowTrafo a)
forall a. a -> X a
forall (m :: * -> *) a. Monad m => a -> m a
return (GLT a -> RowTrafo a
forall a. GLT a -> RowTrafo a
RowTrafo (Dim a (Point a) -> Dim a (Point a) -> Permutation N -> GLT a
forall x.
Distributive x =>
Dim' x -> Dim' x -> Permutation N -> GLT x
permute (Dim a (Point a)
r Dim a (Point a) -> Permutation N -> Dim a (Point a)
forall f x. Opr f x => x -> f -> x
<* Permutation N
p) Dim a (Point a)
r Permutation N
p))

  expAt :: N -> Word r ZMod -> (r, Word r ZMod)
expAt N
n Word r ZMod
w = case Word r ZMod
w of
    Word ((ZMod N
m,r
r):[(ZMod, r)]
w') | N
n N -> N -> Bool
forall a. Eq a => a -> a -> Bool
== N
m -> (r
r,[(ZMod, r)] -> Word r ZMod
forall r a. [(a, r)] -> Word r a
Word [(ZMod, r)]
w')
    Word r ZMod
_                             -> (r
0,Word r ZMod
w)

  w' :: Word N ZMod
w' = ProductSymbol ZMod -> Word N ZMod
forall x. Entity x => ProductSymbol x -> Word N x
psywrd ProductSymbol ZMod
g'

  da :: ProductSymbol ZMod
da = ZMod -> ProductSymbol ZMod
forall x. Entity x => x -> ProductSymbol x
sy (N -> ZMod
ZMod N
0) ProductSymbol ZMod
-> Exponent (ProductSymbol ZMod) -> ProductSymbol ZMod
forall f. Exponential f => f -> Exponent f -> f
^ N
Exponent (ProductSymbol ZMod)
a
  (N
a,Word N ZMod
w'') = N -> Word N ZMod -> (N, Word N ZMod)
forall {r}. Num r => N -> Word r ZMod -> (r, Word r ZMod)
expAt N
0 Word N ZMod
w'
  
  db :: ProductSymbol ZMod
db = ZMod -> ProductSymbol ZMod
forall x. Entity x => x -> ProductSymbol x
sy (N -> ZMod
ZMod N
1) ProductSymbol ZMod
-> Exponent (ProductSymbol ZMod) -> ProductSymbol ZMod
forall f. Exponential f => f -> Exponent f -> f
^ N
Exponent (ProductSymbol ZMod)
b
  (N
b,Word N ZMod
w''') = N -> Word N ZMod -> (N, Word N ZMod)
forall {r}. Num r => N -> Word r ZMod -> (r, Word r ZMod)
expAt N
1 Word N ZMod
w''
  -- for all ((ZMod n),_) in w''' holds: 2 <= n
    
  dc :: ProductSymbol ZMod
dc = Word N ZMod -> ProductSymbol ZMod
forall x. Entity x => Word N x -> ProductSymbol x
wrdpsy Word N ZMod
w'''

  ms :: [N]
ms = ((ZMod, N) -> N) -> [(ZMod, N)] -> [N]
forall a b. (a -> b) -> [a] -> [b]
forall (h :: * -> * -> *) (f :: * -> *) a b.
Applicative1 h f =>
h a b -> f a -> f b
amap1 ((\(ZMod N
m) -> N
m) (ZMod -> N) -> ((ZMod, N) -> ZMod) -> (ZMod, N) -> N
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
. (ZMod, N) -> ZMod
forall a b. (a, b) -> a
fst) ([(ZMod, N)] -> [N]) -> [(ZMod, N)] -> [N]
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
w'''
  gms :: N
gms  = [N] -> N
gcds [N]
ms  
  lms :: N
lms  = [N] -> N
lcms [N]
ms
  -- 1 <= lms, because 2 <= m for all m in ms
  
  xsl :: X ZMod
xsl = do
    N
n <- N -> N -> X N
xNB N
1 N
10
    ZMod -> X ZMod
forall a. a -> X a
forall (m :: * -> *) a. Monad m => a -> m a
return (ZMod -> X ZMod) -> ZMod -> X ZMod
forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ N -> ZMod
ZMod (N
nN -> N -> N
forall c. Multiplicative c => c -> c -> c
*N
lms)

  xsg :: X ZMod
xsg | N
gms N -> N -> Bool
forall a. Ord a => a -> a -> Bool
< N
2   = X ZMod
forall x. X x
XEmpty
      | [(N, N)]
ws [(N, N)] -> [(N, N)] -> Bool
forall a. Eq a => a -> a -> Bool
== []  = X ZMod
forall x. X x
XEmpty
      | Bool
otherwise = do
          N
r  <- N -> N -> X N
xNB N
1 N
rMax
          [N]
ps <- N -> X N -> X [N]
forall x. N -> X x -> X [x]
xTakeN N
r ([N] -> X N
forall a. [a] -> X a
xOneOf [N]
fs)
          N
n  <- N -> N -> X N
xNB N
1 N
10
          ZMod -> X ZMod
forall a. a -> X a
forall (m :: * -> *) a. Monad m => a -> m a
return (ZMod -> X ZMod) -> ZMod -> X ZMod
forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ N -> ZMod
ZMod (N
n N -> N -> N
forall c. Multiplicative c => c -> c -> c
* (N -> N -> N) -> N -> [N] -> N
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl N -> N -> N
forall c. Multiplicative c => c -> c -> c
(*) N
1 [N]
ps)
    where Word [(N, N)]
ws  = N -> N -> Word N N
nFactorize' N
stdMaxPrime N
gms
          fs :: [N]
fs = ((N, N) -> N) -> [(N, N)] -> [N]
forall a b. (a -> b) -> [a] -> [b]
forall (h :: * -> * -> *) (f :: * -> *) a b.
Applicative1 h f =>
h a b -> f a -> f b
amap1 (N, N) -> N
forall a b. (a, b) -> a
fst [(N, N)]
ws
          rMax :: N
rMax = (N -> N -> N) -> N -> [N] -> N
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl N -> N -> N
forall a. Additive a => a -> a -> a
(+) N
0 ([N] -> N) -> [N] -> N
forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ ((N, N) -> N) -> [(N, N)] -> [N]
forall a b. (a -> b) -> [a] -> [b]
forall (h :: * -> * -> *) (f :: * -> *) a b.
Applicative1 h f =>
h a b -> f a -> f b
amap1 (N, N) -> N
forall a b. (a, b) -> b
snd [(N, N)]
ws
          -- 0 < nMax, because ws is not empty
          
  xds :: X (ProductSymbol ZMod)
xds = N -> X ZMod -> X [ZMod]
forall x. N -> X x -> X [x]
xTakeN N
s (X ZMod
xsg X ZMod -> X ZMod -> X ZMod
forall a. X a -> X a -> X a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> X ZMod
xsl) X [ZMod]
-> ([ZMod] -> X (ProductSymbol ZMod)) -> X (ProductSymbol ZMod)
forall a b. X a -> (a -> X b) -> X b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= ProductSymbol ZMod -> X (ProductSymbol ZMod)
forall a. a -> X a
forall (m :: * -> *) a. Monad m => a -> m a
return (ProductSymbol ZMod -> X (ProductSymbol ZMod))
-> ([ZMod] -> ProductSymbol ZMod)
-> [ZMod]
-> X (ProductSymbol 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
. [ZMod] -> ProductSymbol ZMod
forall x. Entity x => [x] -> ProductSymbol x
productSymbol

  xt :: X ZMod
xt | [N]
fs [N] -> [N] -> Bool
forall a. Eq a => a -> a -> Bool
== []  = X ZMod
forall x. X x
XEmpty
     | Bool
otherwise = do
    N
n <- N -> N -> X N
xNB N
1 N
5
    [N]
ps <- N -> X N -> X [N]
forall x. N -> X x -> X [x]
xTakeN N
n ([N] -> X N
forall a. [a] -> X a
xOneOf [N]
fs)
    ZMod -> X ZMod
forall a. a -> X a
forall (m :: * -> *) a. Monad m => a -> m a
return (ZMod -> X ZMod) -> ZMod -> X ZMod
forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ N -> ZMod
ZMod (N -> ZMod) -> N -> ZMod
forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ (N -> N -> N) -> N -> [N] -> N
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl N -> N -> N
forall c. Multiplicative c => c -> c -> c
(*) N
1 [N]
ps
    where fs :: [N]
fs = N -> [N] -> [N]
forall a. N -> [a] -> [a]
takeN N
10 ([N] -> [N]) -> [N] -> [N]
forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ (N -> Bool) -> [N] -> [N]
forall a. (a -> Bool) -> [a] -> [a]
filter ((N -> N -> Bool
forall a. Eq a => a -> a -> Bool
/=N
0) (N -> Bool) -> (N -> N) -> N -> Bool
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
. N -> N -> N
forall a. Integral a => a -> a -> a
mod N
lms) ([N]
stdPrimes)
    
  xdt :: X (ProductSymbol ZMod)
xdt = case X ZMod
xt of
    X ZMod
XEmpty -> ProductSymbol ZMod -> X (ProductSymbol ZMod)
forall a. a -> X a
forall (m :: * -> *) a. Monad m => a -> m a
return ([ZMod] -> ProductSymbol ZMod
forall x. Entity x => [x] -> ProductSymbol x
productSymbol [])
    X ZMod
_      -> N -> X ZMod -> X [ZMod]
forall x. N -> X x -> X [x]
xTakeN N
t X ZMod
xt X [ZMod]
-> ([ZMod] -> X (ProductSymbol ZMod)) -> X (ProductSymbol ZMod)
forall a b. X a -> (a -> X b) -> X b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= ProductSymbol ZMod -> X (ProductSymbol ZMod)
forall a. a -> X a
forall (m :: * -> *) a. Monad m => a -> m a
return (ProductSymbol ZMod -> X (ProductSymbol ZMod))
-> ([ZMod] -> ProductSymbol ZMod)
-> [ZMod]
-> X (ProductSymbol 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
. [ZMod] -> ProductSymbol ZMod
forall x. Entity x => [x] -> ProductSymbol x
productSymbol
 
--------------------------------------------------------------------------------
-- AbHom - XStandardOrtSite -

instance XStandardOrtSite To AbHom where
  xStandardOrtSite :: XOrtSite 'To AbHom
xStandardOrtSite = X (Point AbHom) -> (Point AbHom -> X AbHom) -> XOrtSite 'To AbHom
forall q. X (Point q) -> (Point q -> X q) -> XOrtSite 'To q
XEnd X (Point AbHom)
X AbGroup
forall x. XStandard x => X x
xStandard Point AbHom -> X AbHom
AbGroup -> X AbHom
xTo where
    q :: Q
q = Q
0.1
    d3 :: N
d3 = N
stdMaxDim N -> N -> N
forall a. Integral a => a -> a -> a
`div` N
3
    xTo :: AbGroup -> X AbHom
xTo AbGroup
g = do
      N
r <- N -> N -> X N
xNB N
0 (N
stdMaxDim N -> N -> N
>- N
2N -> N -> N
forall c. Multiplicative c => c -> c -> c
*N
d3)
      N
s <- N -> N -> X N
xNB N
0 N
d3
      N
t <- N -> N -> X N
xNB N
0 N
d3
      N
n <- N -> N -> X N
xNB N
1 N
10
      Q -> N -> N -> N -> AbGroup -> X AbHom
xAbHomTo (N -> Q
forall a b. Embeddable a b => a -> b
inj N
n Q -> Q -> Q
forall c. Multiplicative c => c -> c -> c
* Q
q) N
r N
s N
t AbGroup
g

-- | distribution of the density of the random variable of @'X' 'AbHom'@, induced by the
-- standard random variable of type @'XOrtSite' 'To' 'AbHom'@.
dstXStdOrtSiteToAbHom :: Int -> (AbHom -> String) -> IO ()
dstXStdOrtSiteToAbHom :: Int -> (AbHom -> String) -> IO ()
dstXStdOrtSiteToAbHom Int
n AbHom -> String
f = IO Omega
getOmega IO Omega -> (Omega -> IO ()) -> IO ()
forall a b. IO a -> (a -> IO b) -> IO b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Int -> X String -> Omega -> IO ()
forall x. (Show x, Ord x) => Int -> X x -> Omega -> IO ()
putDistribution Int
n ((AbHom -> String) -> X AbHom -> X String
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 AbHom -> String
f X AbHom
xh) where
  XEnd X (Point AbHom)
X AbGroup
xg Point AbHom -> X AbHom
AbGroup -> X AbHom
xt = XOrtSite 'To AbHom
forall (s :: Site) a. XStandardOrtSite s a => XOrtSite s a
xStandardOrtSite :: XOrtSite To AbHom
  xh :: X AbHom
xh = X AbGroup
xg X AbGroup -> (AbGroup -> X AbHom) -> X AbHom
forall a b. X a -> (a -> X b) -> X b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= AbGroup -> X AbHom
xt

instance XStandardOrtSiteTo AbHom

instance XStandardOrtSite From AbHom where
  xStandardOrtSite :: XOrtSite 'From AbHom
xStandardOrtSite = X (Point AbHom) -> (Point AbHom -> X AbHom) -> XOrtSite 'From AbHom
forall q. X (Point q) -> (Point q -> X q) -> XOrtSite 'From q
XStart X (Point AbHom)
X AbGroup
forall x. XStandard x => X x
xStandard Point AbHom -> X AbHom
AbGroup -> X AbHom
xFrom where
    q :: Q
q = Q
0.1
    d3 :: N
d3 = N
stdMaxDim N -> N -> N
forall a. Integral a => a -> a -> a
`div` N
3
    xFrom :: AbGroup -> X AbHom
xFrom AbGroup
g = do
      N
r <- N -> N -> X N
xNB N
0 (N
stdMaxDim N -> N -> N
>- N
2N -> N -> N
forall c. Multiplicative c => c -> c -> c
*N
d3)
      N
s <- N -> N -> X N
xNB N
0 N
d3
      N
t <- N -> N -> X N
xNB N
0 N
d3
      N
n <- N -> N -> X N
xNB N
1 N
10
      Q -> N -> N -> N -> AbGroup -> X AbHom
xAbHomFrom (N -> Q
forall a b. Embeddable a b => a -> b
inj N
n Q -> Q -> Q
forall c. Multiplicative c => c -> c -> c
* Q
q) N
r N
s N
t AbGroup
g

-- | distribution of the density of the random variable of @'X' 'AbHom'@, induced by the
-- standard random variable of type @'XOrtSite' 'From' 'AbHom'@.
dstXStdOrtSiteFromAbHom :: Int -> (AbHom -> String) -> IO ()
dstXStdOrtSiteFromAbHom :: Int -> (AbHom -> String) -> IO ()
dstXStdOrtSiteFromAbHom Int
n AbHom -> String
f = IO Omega
getOmega IO Omega -> (Omega -> IO ()) -> IO ()
forall a b. IO a -> (a -> IO b) -> IO b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Int -> X String -> Omega -> IO ()
forall x. (Show x, Ord x) => Int -> X x -> Omega -> IO ()
putDistribution Int
n ((AbHom -> String) -> X AbHom -> X String
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 AbHom -> String
f X AbHom
xh) where
  XStart X (Point AbHom)
X AbGroup
xg Point AbHom -> X AbHom
AbGroup -> X AbHom
xs = XOrtSite 'From AbHom
forall (s :: Site) a. XStandardOrtSite s a => XOrtSite s a
xStandardOrtSite :: XOrtSite From AbHom
  xh :: X AbHom
xh = X AbGroup
xg X AbGroup -> (AbGroup -> X AbHom) -> X AbHom
forall a b. X a -> (a -> X b) -> X b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= AbGroup -> X AbHom
xs

instance XStandardOrtSiteFrom AbHom

instance XStandardOrtOrientation AbHom where
  xStandardOrtOrientation :: XOrtOrientation AbHom
xStandardOrtOrientation = X (Orientation (Point AbHom))
-> (Orientation (Point AbHom) -> X AbHom) -> XOrtOrientation AbHom
forall q.
X (Orientation (Point q))
-> (Orientation (Point q) -> X q) -> XOrtOrientation q
XOrtOrientation X (Orientation (Point AbHom))
X (Orientation AbGroup)
xo Orientation (Point AbHom) -> X AbHom
Orientation AbGroup -> X AbHom
xh where
    q :: Q
q = Q
0.1
    XStart X (Point AbHom)
X AbGroup
xg Point AbHom -> X AbHom
AbGroup -> X AbHom
xFrom = XOrtSite 'From AbHom
forall (s :: Site) a. XStandardOrtSite s a => XOrtSite s a
xStandardOrtSite :: XOrtSite From AbHom
    
    xo :: X (Orientation AbGroup)
xo = do
      AbGroup
s <- X AbGroup
xg
      AbGroup
e <- (AbHom -> AbGroup) -> X AbHom -> X AbGroup
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 AbHom -> Point AbHom
AbHom -> AbGroup
forall q. Oriented q => q -> Point q
end (X AbHom -> X AbGroup) -> X AbHom -> X AbGroup
forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ AbGroup -> X AbHom
xFrom AbGroup
s
      Orientation AbGroup -> X (Orientation AbGroup)
forall a. a -> X a
forall (m :: * -> *) a. Monad m => a -> m a
return (AbGroup
sAbGroup -> AbGroup -> Orientation AbGroup
forall p. p -> p -> Orientation p
:>AbGroup
e)
      
    xh :: Orientation AbGroup -> X AbHom
xh Orientation AbGroup
o = do
      N
n <- N -> N -> X N
xNB N
0 N
10
      Q -> Orientation AbGroup -> X AbHom
xAbHom (N -> Q
forall a b. Embeddable a b => a -> b
inj N
n Q -> Q -> Q
forall c. Multiplicative c => c -> c -> c
* Q
q) Orientation AbGroup
o
      
    

--------------------------------------------------------------------------------
-- AbHom - XStandard -

instance XStandard AbHom where
  xStandard :: X AbHom
xStandard = XOrtSite 'From AbHom -> X AbHom
forall q (s :: Site). Oriented q => XOrtSite s q -> XOrt q
xosOrt (XOrtSite 'From AbHom
forall (s :: Site) a. XStandardOrtSite s a => XOrtSite s a
xStandardOrtSite :: XOrtSite From AbHom)

dstXStdAbHom :: Int -> (AbHom -> String) -> IO ()
dstXStdAbHom :: Int -> (AbHom -> String) -> IO ()
dstXStdAbHom Int
n AbHom -> String
f = IO Omega
getOmega IO Omega -> (Omega -> IO ()) -> IO ()
forall a b. IO a -> (a -> IO b) -> IO b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Int -> X String -> Omega -> IO ()
forall x. (Show x, Ord x) => Int -> X x -> Omega -> IO ()
putDistribution Int
n ((AbHom -> String) -> X AbHom -> X String
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 AbHom -> String
f X AbHom
forall x. XStandard x => X x
xStandard)

--------------------------------------------------------------------------------
-- prpAbHom -

-- | validity of the algebraic structure of 'AbHom'.
prpAbHom :: Statement
prpAbHom :: Statement
prpAbHom = String -> Label
Prp String
"AbHom" Label -> Statement -> Statement
:<=>:
  [Statement] -> Statement
And [ X AbHom -> Statement
forall q. Oriented q => XOrt q -> Statement
prpOrt X AbHom
xOrt
      , XMlt AbHom -> Statement
forall c. Multiplicative c => XMlt c -> Statement
prpMlt XMlt AbHom
xMlt
      , X AbHom -> Statement
forall f. Fibred f => XFbr f -> Statement
prpFbr X AbHom
xFbr
      , XAdd AbHom -> Statement
forall a. Additive a => XAdd a -> Statement
prpAdd XAdd AbHom
xAdd
      , XAbl AbHom -> Statement
forall a. Abelian a => XAbl a -> Statement
prpAbl XAbl AbHom
xAbl
      ] where

  xHomTo :: XOrtSite 'To AbHom
xHomTo@(XEnd X (Point AbHom)
X AbGroup
xG Point AbHom -> X AbHom
AbGroup -> X AbHom
xTo)  = XOrtSite 'To AbHom
forall (s :: Site) a. XStandardOrtSite s a => XOrtSite s a
xStandardOrtSite :: XOrtSite To AbHom

  xOrt :: X AbHom
xOrt = XOrtSite 'To AbHom -> X AbHom
forall q (s :: Site). Oriented q => XOrtSite s q -> XOrt q
xosOrt XOrtSite 'To AbHom
xHomTo

  xMlt :: XMlt AbHom
xMlt = X N
-> X (Point AbHom)
-> X AbHom
-> X (Endo AbHom)
-> X (Mltp2 AbHom)
-> X (Mltp3 AbHom)
-> XMlt AbHom
forall c.
X N
-> X (Point c)
-> X c
-> X (Endo c)
-> X (Mltp2 c)
-> X (Mltp3 c)
-> XMlt c
XMlt X N
xn X (Point AbHom)
X AbGroup
xG X AbHom
xOrt X (Endo AbHom)
xe X (Mltp2 AbHom)
xh2 X (Mltp3 AbHom)
xh3 where
    xn :: X N
xn = N -> N -> X N
xNB N
0 N
10
    xe :: X (Endo AbHom)
xe = do
      AbGroup
g <- X AbGroup
xG
      AbHom
h <- Q -> Orientation AbGroup -> X AbHom
xAbHom Q
0.8 (AbGroup
gAbGroup -> AbGroup -> Orientation AbGroup
forall p. p -> p -> Orientation p
:>AbGroup
g)
      Endo AbHom -> X (Endo AbHom)
forall a. a -> X a
forall (m :: * -> *) a. Monad m => a -> m a
return (Endo AbHom -> X (Endo AbHom)) -> Endo AbHom -> X (Endo AbHom)
forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ AbHom -> Endo AbHom
forall q. q -> Endo q
Endo AbHom
h
    xh2 :: X (Mltp2 AbHom)
xh2 = XOrtSite 'To AbHom -> X (Mltp2 AbHom)
forall c (d :: Site).
Multiplicative c =>
XOrtSite d c -> X (Mltp2 c)
xMltp2 XOrtSite 'To AbHom
xHomTo
    xh3 :: X (Mltp3 AbHom)
xh3 = XOrtSite 'To AbHom -> X (Mltp3 AbHom)
forall c (d :: Site).
Multiplicative c =>
XOrtSite d c -> X (Mltp3 c)
xMltp3 XOrtSite 'To AbHom
xHomTo

  xFbr :: X AbHom
xFbr = X AbHom
xOrt

  xRoot :: X (Orientation AbGroup)
xRoot = do
    AbGroup
t <- X AbGroup
xG
    AbHom
h <- AbGroup -> X AbHom
xTo AbGroup
t
    Orientation AbGroup -> X (Orientation AbGroup)
forall a. a -> X a
forall (m :: * -> *) a. Monad m => a -> m a
return (Orientation AbGroup -> X (Orientation AbGroup))
-> Orientation AbGroup -> X (Orientation AbGroup)
forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ AbHom -> Orientation (Point AbHom)
forall q. Oriented q => q -> Orientation (Point q)
orientation AbHom
h

  xStalk :: XStalk AbHom
xStalk = X (Root AbHom) -> (Root AbHom -> X AbHom) -> XStalk AbHom
forall x. X (Root x) -> (Root x -> X x) -> XStalk x
XStalk X (Orientation AbGroup)
X (Root AbHom)
xRoot (Q -> Orientation AbGroup -> X AbHom
xAbHom Q
0.8)
  xAdd :: XAdd AbHom
xAdd = XStalk AbHom -> X N -> XAdd AbHom
forall a. Additive a => XStalk a -> X N -> XAdd a
xAddStalk XStalk AbHom
xStalk (N -> N -> X N
xNB N
0 N
1000)
  xAbl :: XAbl AbHom
xAbl = X Z -> X AbHom -> X (Adbl2 AbHom) -> XAbl AbHom
forall a. X Z -> X a -> X (Adbl2 a) -> XAbl a
XAbl X Z
forall x. XStandard x => X x
xStandard X AbHom
xFbr X (Adbl2 AbHom)
xa2 where
    xa2 :: X (Adbl2 AbHom)
xa2 = X (Orientation AbGroup)
xRoot X (Orientation AbGroup)
-> (Orientation AbGroup -> X (Adbl2 AbHom)) -> X (Adbl2 AbHom)
forall a b. X a -> (a -> X b) -> X b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= XStalk AbHom -> Root AbHom -> X (Adbl2 AbHom)
forall a. Additive a => XStalk a -> Root a -> X (Adbl2 a)
xStalkAdbl2 XStalk AbHom
xStalk

xMltAbh :: XMlt AbHom
xMltAbh :: XMlt AbHom
xMltAbh = X N -> XOrtOrientation AbHom -> XMlt AbHom
forall c. Multiplicative c => X N -> XOrtOrientation c -> XMlt c
xoMlt X N
xN (XOrtOrientation AbHom
forall q. XStandardOrtOrientation q => XOrtOrientation q
xStandardOrtOrientation :: XOrtOrientation AbHom)