{-# 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
  , abgZero

    -- * Homomorphism

  , AbHom(..)
  , abh, abh'
  , abhz, zabh
  , abhDensity
  , abhSplitable
  
    -- * Adjunction

  , abhFreeAdjunction
  , AbHomFree(..)

    -- * Limes

  , abhProducts, abhSums


    -- * Finite Presentation

  , abgFinPres

    -- * Elements

  , AbElement(..), AbElementForm(..), abge
  , abhvecFree1, vecabhFree1
    -- * X

  , xAbHom, xAbHomTo, xAbHomFrom
  , stdMaxDim, xAbhSomeFreeSlice

    -- * Proposition

  , prpAbHom

  ) where

import Prelude(ceiling)

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

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

import OAlg.Prelude

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

import OAlg.Category.Path as C

import OAlg.Structure.Oriented
import OAlg.Structure.Multiplicative
import OAlg.Structure.Fibred
import OAlg.Structure.FibredOriented
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.FibredOriented
import OAlg.Hom.Additive
import OAlg.Hom.Distributive
import OAlg.Hom.Vectorial
import OAlg.Hom.Algebraic

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

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.Entity.Sum hiding (sy)

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,Oriented AbGroup
Point AbGroup -> AbGroup
Oriented AbGroup =>
(Point AbGroup -> AbGroup)
-> (AbGroup -> AbGroup -> AbGroup)
-> (AbGroup -> N -> AbGroup)
-> Multiplicative 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
"]"
    
type instance Point AbGroup = ()
instance ShowPoint AbGroup
instance EqPoint AbGroup
instance ValidablePoint AbGroup
instance TypeablePoint AbGroup
instance SingletonPoint AbGroup

instance Oriented AbGroup where
  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 (h :: * -> * -> *) (f :: * -> *) x y.
Applicative1 h f =>
h x y -> f x -> f y
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 a. Logical a => a -> a -> a
|| (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 a. Logical a => a -> a -> a
|| (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,Eq AbHom
Eq AbHom =>
(AbHom -> AbHom -> Ordering)
-> (AbHom -> AbHom -> Bool)
-> (AbHom -> AbHom -> Bool)
-> (AbHom -> AbHom -> Bool)
-> (AbHom -> AbHom -> Bool)
-> (AbHom -> AbHom -> AbHom)
-> (AbHom -> AbHom -> AbHom)
-> Ord AbHom
AbHom -> AbHom -> Bool
AbHom -> AbHom -> Ordering
AbHom -> AbHom -> AbHom
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 :: AbHom -> AbHom -> Ordering
compare :: AbHom -> AbHom -> Ordering
$c< :: AbHom -> AbHom -> Bool
< :: AbHom -> AbHom -> Bool
$c<= :: AbHom -> AbHom -> Bool
<= :: AbHom -> AbHom -> Bool
$c> :: AbHom -> AbHom -> Bool
> :: AbHom -> AbHom -> Bool
$c>= :: AbHom -> AbHom -> Bool
>= :: AbHom -> AbHom -> Bool
$cmax :: AbHom -> AbHom -> AbHom
max :: AbHom -> AbHom -> AbHom
$cmin :: AbHom -> AbHom -> AbHom
min :: AbHom -> AbHom -> AbHom
Ord,AbHom -> Statement
(AbHom -> Statement) -> Validable AbHom
forall a. (a -> Statement) -> Validable a
$cvalid :: AbHom -> Statement
valid :: AbHom -> Statement
Validable)

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

-- abgZero -


-- | the zero point for 'AbHom'.

abgZero :: ZeroPoint AbHom
abgZero :: ZeroPoint AbHom
abgZero = Point AbHom -> ZeroPoint AbHom
forall x. Point x -> ZeroPoint x
ZeroPoint (Point AbGroup -> AbGroup
forall c. Multiplicative c => Point c -> c
one ())

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

-- 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

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

-- abhDensity -


-- | the density of the abelian homomorphism, i. e. the density of the underlying matrix

-- (see: 'mtxDensity').

abhDensity :: N -> AbHom -> Maybe Q
abhDensity :: N -> AbHom -> Maybe Q
abhDensity N
n (AbHom Matrix ZModHom
h) = do
  Q
d <- Matrix ZModHom -> Maybe Q
forall x. Matrix x -> Maybe Q
mtxDensity Matrix ZModHom
h
  Q -> Maybe Q
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return (Q -> Z
forall b. Integral b => Q -> b
forall a b. (RealFrac a, Integral b) => a -> b
ceiling (N -> Q
forall a b. Embeddable a b => a -> b
inj N
n Q -> Q -> Q
forall c. Multiplicative c => c -> c -> c
* Q
d) Z -> N -> Q
% N
n)

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

-- 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 (h :: * -> * -> *) (f :: * -> *) x y.
Applicative1 h f =>
h x y -> f x -> f y
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 (h :: * -> * -> *) (f :: * -> *) x y.
Applicative1 h f =>
h x y -> f x -> f y
amap1 Z -> ZModHom
fromZ Entries N N Z
xs

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

-- AbHom - Algebraic -

type instance Point AbHom = AbGroup

instance ShowPoint AbHom
instance EqPoint AbHom
instance ValidablePoint AbHom
instance TypeablePoint AbHom

instance Oriented AbHom where
  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)

type instance Root AbHom = Orientation AbGroup
instance ShowRoot AbHom
instance EqRoot AbHom
instance ValidableRoot AbHom
instance TypeableRoot AbHom

instance Fibred AbHom

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 :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ 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 (h :: * -> * -> *) (f :: * -> *) x y.
Applicative1 h f =>
h x y -> f x -> f y
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 ApplicativeG Id AbHomMap (->) where
  amapG :: forall x y. AbHomMap x y -> Id x -> Id y
amapG AbHomMap x y
AbHomMatrix (Id (AbHom Matrix ZModHom
m)) = y -> Id y
forall x. x -> Id x
Id y
Matrix ZModHom
m
  amapG AbHomMap x y
MatrixAbHom (Id x
m) = y -> Id y
forall x. x -> Id x
Id (Matrix ZModHom -> AbHom
AbHom x
Matrix ZModHom
m)

instance TransformableObjectClassTyp AbHomMap

instance ApplicativeG Pnt AbHomMap (->) where
  amapG :: forall x y. AbHomMap x y -> Pnt x -> Pnt y
amapG AbHomMap x y
AbHomMatrix (Pnt (AbGroup ProductSymbol ZMod
g)) = Point y -> Pnt y
forall x. Point x -> Pnt x
Pnt (CSequence (Point ZModHom) -> Dim' ZModHom
forall x. CSequence (Point x) -> Dim x (Point x)
Dim CSequence (Point ZModHom)
ProductSymbol ZMod
g)
  amapG AbHomMap x y
MatrixAbHom (Pnt (Dim CSequence (Point ZModHom)
g)) = Point y -> Pnt y
forall x. Point x -> Pnt x
Pnt (ProductSymbol ZMod -> AbGroup
AbGroup CSequence (Point ZModHom)
ProductSymbol ZMod
g)

instance HomOriented AbHomMap

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)

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

-- 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'@.

abHomMatrix :: Variant2 Covariant (Inv2 IsoAbHomMap) AbHom (Matrix ZModHom)
abHomMatrix :: Variant2 'Covariant (Inv2 IsoAbHomMap) AbHom (Matrix ZModHom)
abHomMatrix = Inv2 IsoAbHomMap AbHom (Matrix ZModHom)
-> Variant2 'Covariant (Inv2 IsoAbHomMap) AbHom (Matrix ZModHom)
forall {k} {k1} (h :: k -> k1 -> *) (x :: k) (y :: k1).
h x y -> Variant2 'Covariant h x y
Covariant2 (IsoAbHomMap AbHom (Matrix ZModHom)
-> IsoAbHomMap (Matrix ZModHom) AbHom
-> Inv2 IsoAbHomMap AbHom (Matrix ZModHom)
forall (c :: * -> * -> *) x y. c x y -> c y x -> Inv2 c x y
Inv2 IsoAbHomMap AbHom (Matrix ZModHom)
t IsoAbHomMap (Matrix ZModHom) AbHom
f) where
  t :: IsoAbHomMap AbHom (Matrix ZModHom)
t = 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)
  f :: IsoAbHomMap (Matrix ZModHom) AbHom
f = 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) 

instance Disjunctive (IsoAbHomMap x y) where variant :: IsoAbHomMap x y -> Variant
variant = Variant -> IsoAbHomMap x y -> Variant
forall b a. b -> a -> b
const Variant
Covariant
instance Disjunctive2 IsoAbHomMap
  
instance CategoryDisjunctive IsoAbHomMap

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

-- IsoAbHomMap - Hom -


instance ApplicativeG Id IsoAbHomMap (->) where
  amapG :: forall x y. IsoAbHomMap x y -> Id x -> Id y
amapG IsoAbHomMap x y
i = Path AbHomMap x y -> Id x -> Id y
forall x y. Path AbHomMap x y -> Id x -> Id y
forall (t :: * -> *) (a :: * -> * -> *) (b :: * -> * -> *) x y.
ApplicativeG t a b =>
a x y -> b (t x) (t y)
amapG (IsoAbHomMap x y -> Form (IsoAbHomMap x y)
forall x. Exposable x => x -> Form x
form IsoAbHomMap x y
i)

instance ApplicativeG Pnt IsoAbHomMap (->) where
  amapG :: forall x y. IsoAbHomMap x y -> Pnt x -> Pnt y
amapG IsoAbHomMap x y
i = Path AbHomMap x y -> Pnt x -> Pnt y
forall x y. Path AbHomMap x y -> Pnt x -> Pnt y
forall (t :: * -> *) (a :: * -> * -> *) (b :: * -> * -> *) x y.
ApplicativeG t a b =>
a x y -> b (t x) (t y)
amapG (IsoAbHomMap x y -> Form (IsoAbHomMap x y)
forall x. Exposable x => x -> Form x
form IsoAbHomMap x y
i)
  
instance HomOriented IsoAbHomMap
instance HomOrientedDisjunctive IsoAbHomMap

instance HomMultiplicative IsoAbHomMap
instance HomMultiplicativeDisjunctive IsoAbHomMap

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

-- IsoAbHomMap - Functorial -


instance FunctorialG Id IsoAbHomMap (->)
instance FunctorialG Pnt IsoAbHomMap (->)

instance FunctorialOriented IsoAbHomMap

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

-- abhProducts -


-- | products for 'AbHom'.

abhProducts :: Products n AbHom
abhProducts :: forall (n :: N'). Products n AbHom
abhProducts = Variant2 'Covariant (Inv2 IsoAbHomMap) (Matrix ZModHom) AbHom
-> LimitsG
     Cone Mlt 'Projective Diagram 'Discrete n 'N0 (Matrix ZModHom)
-> LimitsG Cone Mlt 'Projective Diagram 'Discrete n 'N0 AbHom
forall (h :: * -> * -> *)
       (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       s (p :: Perspective) (d :: DiagramType -> N' -> N' -> * -> *)
       (t :: DiagramType) (n :: N') (m :: N') x y.
NaturalConicBi (Inv2 h) c s p d t n m =>
Variant2 'Covariant (Inv2 h) x y
-> LimitsG c s p d t n m x -> LimitsG c s p d t n m y
lmsMapCov (Inv2 IsoAbHomMap (Matrix ZModHom) AbHom
-> Variant2 'Covariant (Inv2 IsoAbHomMap) (Matrix ZModHom) AbHom
forall {k} {k1} (h :: k -> k1 -> *) (x :: k) (y :: k1).
h x y -> Variant2 'Covariant h x y
Covariant2 (Inv2 IsoAbHomMap AbHom (Matrix ZModHom)
-> Inv2 IsoAbHomMap (Matrix ZModHom) AbHom
forall (c :: * -> * -> *) x y. Inv2 c x y -> Inv2 c y x
inv2 Inv2 IsoAbHomMap AbHom (Matrix ZModHom)
i)) LimitsG
  Cone Mlt 'Projective Diagram 'Discrete n 'N0 (Matrix ZModHom)
forall x (n :: N'). Distributive x => Products n (Matrix x)
mtxProducts where Covariant2 Inv2 IsoAbHomMap AbHom (Matrix ZModHom)
i = Variant2 'Covariant (Inv2 IsoAbHomMap) AbHom (Matrix ZModHom)
abHomMatrix

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

-- abhSums -


-- | sums for 'AbHom'.

abhSums :: Sums n AbHom
abhSums :: forall (n :: N'). Sums n AbHom
abhSums = Variant2 'Covariant (Inv2 IsoAbHomMap) (Matrix ZModHom) AbHom
-> LimitsG
     Cone Mlt 'Injective Diagram 'Discrete n 'N0 (Matrix ZModHom)
-> LimitsG Cone Mlt 'Injective Diagram 'Discrete n 'N0 AbHom
forall (h :: * -> * -> *)
       (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       s (p :: Perspective) (d :: DiagramType -> N' -> N' -> * -> *)
       (t :: DiagramType) (n :: N') (m :: N') x y.
NaturalConicBi (Inv2 h) c s p d t n m =>
Variant2 'Covariant (Inv2 h) x y
-> LimitsG c s p d t n m x -> LimitsG c s p d t n m y
lmsMapCov (Inv2 IsoAbHomMap (Matrix ZModHom) AbHom
-> Variant2 'Covariant (Inv2 IsoAbHomMap) (Matrix ZModHom) AbHom
forall {k} {k1} (h :: k -> k1 -> *) (x :: k) (y :: k1).
h x y -> Variant2 'Covariant h x y
Covariant2 (Inv2 IsoAbHomMap AbHom (Matrix ZModHom)
-> Inv2 IsoAbHomMap (Matrix ZModHom) AbHom
forall (c :: * -> * -> *) x y. Inv2 c x y -> Inv2 c y x
inv2 Inv2 IsoAbHomMap AbHom (Matrix ZModHom)
i)) LimitsG
  Cone Mlt 'Injective Diagram 'Discrete n 'N0 (Matrix ZModHom)
forall x (n :: N'). Distributive x => Sums n (Matrix x)
mtxSums where Covariant2 Inv2 IsoAbHomMap AbHom (Matrix ZModHom)
i = Variant2 'Covariant (Inv2 IsoAbHomMap) AbHom (Matrix ZModHom)
abHomMatrix

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

-- 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

instance SlicedFree AbHom where slicedFree :: forall (k :: N'). Attestable k => Struct (Sld (Free k)) AbHom
slicedFree = Struct (Sld (Free k)) AbHom
forall s x. Structure s x => Struct s x
Struct

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

-- 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 :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ 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

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

-- abhSplit -


-- | splitable property for 'AbHom' with free start point of any finite dimension.

abhSplitable :: Splitable From Free AbHom
abhSplitable :: Splitable 'From Free AbHom
abhSplitable = (forall (k :: N').
 (Attestable k, Sliced (Free k) AbHom) =>
 Slice 'From (Free k) AbHom
 -> FinList k (Slice 'From (Free N1) AbHom))
-> Splitable 'From Free AbHom
forall (s :: Site) (i :: N' -> * -> *) d.
(forall (k :: N').
 (Attestable k, Sliced (i k) d) =>
 Slice s (i k) d -> FinList k (Slice s (i N1) d))
-> Splitable s i d
Splitable Slice 'From (Free k) AbHom
-> FinList k (Slice 'From (Free N1) AbHom)
forall (k :: N').
(Attestable k, Sliced (Free k) AbHom) =>
Slice 'From (Free k) AbHom
-> FinList k (Slice 'From (Free N1) AbHom)
forall (k :: N').
Slice 'From (Free k) AbHom
-> FinList k (Slice 'From (Free N1) AbHom)
abhSplit

abhSplit :: Slice From (Free k) AbHom -> FinList k (Slice From (Free N1) AbHom)
abhSplit :: forall (k :: N').
Slice 'From (Free k) AbHom
-> FinList k (Slice 'From (Free N1) AbHom)
abhSplit (SliceFrom (Free Any k
k) h :: AbHom
h@(AbHom Matrix ZModHom
h'))
  = case Any k
-> [Slice 'From (Free N1) AbHom]
-> Maybe (FinList k (Slice 'From (Free N1) AbHom))
forall (n :: N') a. Any n -> [a] -> Maybe (FinList n a)
maybeFinList Any k
k ([Slice 'From (Free N1) AbHom]
 -> Maybe (FinList k (Slice 'From (Free N1) AbHom)))
-> [Slice 'From (Free N1) AbHom]
-> Maybe (FinList k (Slice 'From (Free N1) AbHom))
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ Any k -> N -> [(Col N ZModHom, N)] -> [Slice 'From (Free N1) AbHom]
forall j i (k :: N').
(j ~ N, i ~ N) =>
Any k -> j -> [(Col i ZModHom, j)] -> [Slice 'From (Free N1) AbHom]
toAbHoms Any k
k N
0 ([(Col N ZModHom, N)] -> [Slice 'From (Free N1) AbHom])
-> [(Col N ZModHom, N)] -> [Slice 'From (Free N1) AbHom]
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ Row N (Col N ZModHom) -> [(Col N ZModHom, N)]
forall j x. Row j x -> [(x, j)]
rowxs (Row N (Col N ZModHom) -> [(Col N ZModHom, N)])
-> Row N (Col N ZModHom) -> [(Col N ZModHom, N)]
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ Matrix ZModHom -> Row N (Col N ZModHom)
forall x. Matrix x -> Row N (Col N x)
mtxRowCol Matrix ZModHom
h' of
      Just FinList k (Slice 'From (Free N1) AbHom)
xs -> FinList k (Slice 'From (Free N1) AbHom)
xs
      Maybe (FinList k (Slice 'From (Free N1) AbHom))
_       -> AlgebraicException -> FinList k (Slice 'From (Free N1) AbHom)
forall a e. Exception e => e -> a
throw (AlgebraicException -> FinList k (Slice 'From (Free N1) AbHom))
-> AlgebraicException -> FinList k (Slice 'From (Free N1) AbHom)
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ String -> AlgebraicException
ImplementationError String
"abhSplit.maybeFinList"
  where
    r :: Point AbHom
r  = AbHom -> Point AbHom
forall q. Oriented q => q -> Point q
end AbHom
h
    n1 :: Free N1 AbHom
n1 = Any N1 -> Free N1 AbHom
forall (k :: N') c. Any k -> Free k c
Free Any N1
forall (n :: N'). Attestable n => W n
attest :: Free N1 AbHom
    z1 :: AbGroup
z1 = N -> AbGroup
abg N
0 
    
    sZero :: Slice From (Free N1) AbHom
    sZero :: Slice 'From (Free N1) AbHom
sZero = Root (Slice 'From (Free N1) AbHom) -> Slice 'From (Free N1) AbHom
forall a. Additive a => Root a -> a
zero Point AbHom
Root (Slice 'From (Free N1) AbHom)
r

    toAbHoms :: (j ~ N, i ~ N) => Any k -> j -> [(Col i ZModHom,j)] -> [Slice From (Free N1) AbHom]
    toAbHoms :: forall j i (k :: N').
(j ~ N, i ~ N) =>
Any k -> j -> [(Col i ZModHom, j)] -> [Slice 'From (Free N1) AbHom]
toAbHoms W k
W0 j
_ [(Col i ZModHom, j)]
_                         = []
    toAbHoms (SW W n1
k') j
j []                   = Slice 'From (Free N1) AbHom
sZero Slice 'From (Free N1) AbHom
-> [Slice 'From (Free N1) AbHom] -> [Slice 'From (Free N1) AbHom]
forall a. a -> [a] -> [a]
: W n1 -> j -> [(Col N ZModHom, j)] -> [Slice 'From (Free N1) AbHom]
forall j i (k :: N').
(j ~ N, i ~ N) =>
Any k -> j -> [(Col i ZModHom, j)] -> [Slice 'From (Free N1) AbHom]
toAbHoms W n1
k' (j -> j
forall a. Enum a => a -> a
succ j
j) []
    toAbHoms (SW W n1
k') j
j cljs :: [(Col i ZModHom, j)]
cljs@((Col i ZModHom
cl,j
j'):[(Col i ZModHom, j)]
cljs') = case j
j j -> j -> Ordering
forall a. Ord a => a -> a -> Ordering
`compare` j
j' of
      Ordering
LT -> Slice 'From (Free N1) AbHom
sZero Slice 'From (Free N1) AbHom
-> [Slice 'From (Free N1) AbHom] -> [Slice 'From (Free N1) AbHom]
forall a. a -> [a] -> [a]
: W n1 -> j -> [(Col i ZModHom, j)] -> [Slice 'From (Free N1) AbHom]
forall j i (k :: N').
(j ~ N, i ~ N) =>
Any k -> j -> [(Col i ZModHom, j)] -> [Slice 'From (Free N1) AbHom]
toAbHoms W n1
k' (j -> j
forall a. Enum a => a -> a
succ j
j) [(Col i ZModHom, j)]
cljs
      Ordering
EQ -> Col i ZModHom -> Slice 'From (Free N1) AbHom
forall i. (i ~ N) => Col i ZModHom -> Slice 'From (Free N1) AbHom
toAbHom Col i ZModHom
cl Slice 'From (Free N1) AbHom
-> [Slice 'From (Free N1) AbHom] -> [Slice 'From (Free N1) AbHom]
forall a. a -> [a] -> [a]
: W n1 -> j -> [(Col i ZModHom, j)] -> [Slice 'From (Free N1) AbHom]
forall j i (k :: N').
(j ~ N, i ~ N) =>
Any k -> j -> [(Col i ZModHom, j)] -> [Slice 'From (Free N1) AbHom]
toAbHoms W n1
k' (j -> j
forall a. Enum a => a -> a
succ j
j) [(Col i ZModHom, j)]
cljs'
      Ordering
_  -> AlgebraicException -> [Slice 'From (Free N1) AbHom]
forall a e. Exception e => e -> a
throw (AlgebraicException -> [Slice 'From (Free N1) AbHom])
-> AlgebraicException -> [Slice 'From (Free N1) AbHom]
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ String -> AlgebraicException
ImplementationError String
"abhSplit.toAbHoms"


    toAbHom :: i ~  N => Col i ZModHom -> Slice From (Free N1) AbHom
    toAbHom :: forall i. (i ~ N) => Col i ZModHom -> Slice 'From (Free N1) AbHom
toAbHom Col i ZModHom
cl = Free N1 AbHom -> AbHom -> Slice 'From (Free N1) AbHom
forall (i :: * -> *) x. i x -> x -> Slice 'From i x
SliceFrom Free N1 AbHom
n1 AbHom
h where
      h :: AbHom
h = Orientation AbGroup -> [(ZModHom, N, N)] -> AbHom
abh (AbGroup
z1 AbGroup -> AbGroup -> Orientation AbGroup
forall p. p -> p -> Orientation p
:> Point AbHom
AbGroup
r) ([(ZModHom, N, N)] -> AbHom) -> [(ZModHom, N, N)] -> AbHom
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ ((ZModHom, N) -> (ZModHom, N, N))
-> [(ZModHom, N)] -> [(ZModHom, N, N)]
forall (h :: * -> * -> *) (f :: * -> *) x y.
Applicative1 h f =>
h x y -> f x -> f y
amap1 (\(ZModHom
x,N
i) -> (ZModHom
x,N
i,N
0)) ([(ZModHom, i)] -> [(ZModHom, N, N)])
-> [(ZModHom, i)] -> [(ZModHom, N, N)]
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ Col i ZModHom -> [(ZModHom, i)]
forall i x. Col i x -> [(x, i)]
colxs Col i ZModHom
cl

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

-- 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

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

-- abhzFree -


abhzFree :: AbHom -> Matrix Z
abhzFree :: AbHom -> Matrix Z
abhzFree h :: AbHom
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 AbHom
s :> Point AbHom
e = AbHom -> Orientation (Point AbHom)
forall q. Oriented q => q -> Orientation (Point q)
orientation AbHom
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 AbHom
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 AbHom
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 :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ 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 :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ [(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 :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ 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 AbHom
AbGroup
e) (AbGroup -> [(ZMod, N)]
abgxs Point AbHom
AbGroup
s) ([(Row N ZModHom, N)] -> [(Row N Z, N)])
-> [(Row N ZModHom, N)] -> [(Row N Z, N)]
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ 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 :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ 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 :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ [(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 :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ 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'

instance ApplicativeG Id AbHomFree (->) where
  amapG :: forall x y. AbHomFree x y -> Id x -> Id y
amapG AbHomFree x y
AbHomFree = (x -> y) -> Id x -> Id y
forall x y. (x -> y) -> Id x -> Id y
toIdG x -> y
AbHom -> Matrix Z
abhzFree
  amapG AbHomFree x y
FreeAbHom = (x -> y) -> Id x -> Id y
forall x y. (x -> y) -> Id x -> Id y
toIdG x -> y
Matrix Z -> AbHom
zabh

instance ApplicativeG Pnt AbHomFree (->) where
  amapG :: forall x y. AbHomFree x y -> Pnt x -> Pnt y
amapG AbHomFree x y
AbHomFree (Pnt Point x
g) = Point y -> Pnt y
forall x. Point x -> Pnt x
Pnt (() -> 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 x
AbGroup
g)
  amapG AbHomFree x y
FreeAbHom (Pnt Point x
n) = Point y -> Pnt y
forall x. Point x -> Pnt x
Pnt (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 x
Dim Z ()
n)

instance HomOriented AbHomFree
instance HomMultiplicative AbHomFree

instance ApplicativeG Rt AbHomFree (->) where
  amapG :: forall x y. AbHomFree x y -> Rt x -> Rt y
amapG h :: AbHomFree x y
h@AbHomFree x y
AbHomFree (Rt Root x
x) = Root y -> Rt y
forall x. Root x -> Rt x
Rt (AbHomFree x y -> Orientation (Point x) -> Orientation (Point y)
forall (h :: * -> * -> *) a b.
ApplicativePoint h =>
h a b -> Orientation (Point a) -> Orientation (Point b)
omap AbHomFree x y
h Orientation (Point x)
Root x
x)
  amapG h :: AbHomFree x y
h@AbHomFree x y
FreeAbHom (Rt Root x
x) = Root y -> Rt y
forall x. Root x -> Rt x
Rt (AbHomFree x y -> Orientation (Point x) -> Orientation (Point y)
forall (h :: * -> * -> *) a b.
ApplicativePoint h =>
h a b -> Orientation (Point a) -> Orientation (Point b)
omap AbHomFree x y
h Orientation (Point x)
Root x
x)

instance HomFibred AbHomFree
instance HomFibredOriented AbHomFree
instance HomAdditive AbHomFree
instance HomDistributive AbHomFree
instance HomVectorial Z AbHomFree
instance HomAlgebraic Z 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 :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ [(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 :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ 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 (h :: * -> * -> *) x y.
ApplicativePoint h =>
h x y -> Point x -> Point y
pmap AbHomFree (Matrix Z) AbHom
FreeAbHom (AbHomFree AbHom (Matrix Z) -> Point AbHom -> Point (Matrix Z)
forall (h :: * -> * -> *) x y.
ApplicativePoint h =>
h x y -> Point x -> Point y
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 @'GeneratorTo' ('DiagramChainTo' g _) _ _ _ _ = 'abgGeneratorTo' a@.  

abgGeneratorTo :: AbGroup -> FinitePresentation To Free AbHom
abgGeneratorTo :: AbGroup -> FinitePresentation 'To Free 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 -> Slice 'From (Free k) AbHom)
-> FinitePresentation 'To Free AbHom
forall (k' :: N') (i :: N' -> * -> *) a (k'' :: N').
(Attestable k', Sliced (i k') a, Attestable k'',
 Sliced (i k'') a) =>
Diagram ('Chain 'To) N3 N2 a
-> i k' a
-> i k'' a
-> Cokernel N1 a
-> Kernel N1 a
-> (forall (k :: N'). Slice 'From (i k) a -> Slice 'From (i k) a)
-> FinitePresentation 'To i 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 -> Slice 'From (Free k) AbHom
forall (k :: N').
Slice 'From (Free k) AbHom -> Slice 'From (Free k) 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 :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ (((ZMod, N), N) -> (ZModHom, N, N))
-> [((ZMod, N), N)] -> [(ZModHom, N, N)]
forall (h :: * -> * -> *) (f :: * -> *) x y.
Applicative1 h f =>
h x y -> f x -> f y
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 :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ 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 (h :: * -> * -> *) (f :: * -> *) x y.
Applicative1 h f =>
h x y -> f x -> f y
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 Diagram ('Parallel 'LeftToRight) N2 N1 AbHom
-> (Cone
      Dst 'Projective Diagram ('Parallel 'LeftToRight) N2 N1 AbHom
    -> AbHom)
-> Kernel N1 AbHom
forall (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       s (d :: DiagramType -> N' -> N' -> * -> *) (t :: DiagramType)
       (n :: N') (m :: N') x.
c s 'Projective d t n m x
-> (Cone s 'Projective d t n m x -> x)
-> LimesG c s 'Projective d t n m x
LimesProjective (Diagram ('Parallel 'LeftToRight) N2 N1 AbHom
-> AbHom
-> Cone
     Dst 'Projective Diagram ('Parallel 'LeftToRight) N2 N1 AbHom
forall a (d :: DiagramType -> N' -> N' -> * -> *) (m :: N').
Distributive a =>
d ('Parallel 'LeftToRight) N2 m a
-> a -> Cone Dst 'Projective d ('Parallel 'LeftToRight) N2 m a
ConeKernel Diagram ('Parallel 'LeftToRight) N2 N1 AbHom
dg AbHom
p') Cone Dst 'Projective Diagram ('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 Diagram ('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 :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ 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 :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ [(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 :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ 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 (h :: * -> * -> *) (f :: * -> *) x y.
Applicative1 h f =>
h x y -> f x -> f y
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 :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ 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 (h :: * -> * -> *) (f :: * -> *) x y.
Applicative1 h f =>
h x y -> f x -> f y
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 Diagram ('Parallel 'RightToLeft) N2 N1 AbHom
-> (Cone
      Dst 'Injective Diagram ('Parallel 'RightToLeft) N2 N1 AbHom
    -> AbHom)
-> Cokernel N1 AbHom
forall (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       s (d :: DiagramType -> N' -> N' -> * -> *) (t :: DiagramType)
       (n :: N') (m :: N') x.
c s 'Injective d t n m x
-> (Cone s 'Injective d t n m x -> x)
-> LimesG c s 'Injective d t n m x
LimesInjective (Diagram ('Parallel 'RightToLeft) N2 N1 AbHom
-> AbHom
-> Cone Dst 'Injective Diagram ('Parallel 'RightToLeft) N2 N1 AbHom
forall a (d :: DiagramType -> N' -> N' -> * -> *) (m :: N').
Distributive a =>
d ('Parallel 'RightToLeft) N2 m a
-> a -> Cone Dst 'Injective d ('Parallel 'RightToLeft) N2 m a
ConeCokernel Diagram ('Parallel 'RightToLeft) N2 N1 AbHom
dg AbHom
p) Cone Dst 'Injective Diagram ('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 Diagram ('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 :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ 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 :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ [(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 :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ 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 :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ 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 (h :: * -> * -> *) (f :: * -> *) x y.
Applicative1 h f =>
h x y -> f x -> f y
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 -> Slice From (Free k) AbHom
    lft :: forall (k :: N').
Slice 'From (Free k) AbHom -> Slice 'From (Free k) AbHom
lft (SliceFrom Free k AbHom
k (AbHom (Matrix Dim' ZModHom
_ Dim' ZModHom
c Entries N N ZModHom
xs))) = Free k AbHom -> AbHom -> Slice 'From (Free k) AbHom
forall (i :: * -> *) x. i x -> x -> Slice 'From i x
SliceFrom Free k AbHom
k (AbHom -> Slice 'From (Free k) AbHom)
-> AbHom -> Slice 'From (Free k) AbHom
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ 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 :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ 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 :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ [(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 :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ 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 :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ 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 (h :: * -> * -> *) (f :: * -> *) x y.
Applicative1 h f =>
h x y -> f x -> f y
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

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

-- abgFinPres -


-- | free finitely presentations for 'AbHom'. 

abgFinPres :: FinitelyPresentable To Free AbHom
abgFinPres :: FinitelyPresentable 'To Free AbHom
abgFinPres = (Point AbHom -> FinitePresentation 'To Free AbHom)
-> FinitelyPresentable 'To Free AbHom
forall (s :: Site) (i :: N' -> * -> *) a.
(Point a -> FinitePresentation s i a) -> FinitelyPresentable s i a
FinitelyPresentable Point AbHom -> FinitePresentation 'To Free AbHom
AbGroup -> FinitePresentation 'To Free AbHom
abgGeneratorTo

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

-- AbElementForm -


-- | form for a 'AbElement'.

data AbElementForm = AbElementForm AbGroup [(Z,N)] deriving (AbElementForm -> AbElementForm -> Bool
(AbElementForm -> AbElementForm -> Bool)
-> (AbElementForm -> AbElementForm -> Bool) -> Eq AbElementForm
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: AbElementForm -> AbElementForm -> Bool
== :: AbElementForm -> AbElementForm -> Bool
$c/= :: AbElementForm -> AbElementForm -> Bool
/= :: AbElementForm -> AbElementForm -> Bool
Eq)

instance Show AbElementForm where
  show :: AbElementForm -> String
show (AbElementForm AbGroup
a [(Z, N)]
zis) = [(Z, N)] -> String
forall {a} {a}. (Eq a, Num a, Show a, Show a) => [(a, a)] -> String
shs [(Z, N)]
zis String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" :: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ AbGroup -> String
forall a. Show a => a -> String
show AbGroup
a where
    shs :: [(a, a)] -> String
shs []       = String
"0"
    shs ((a, a)
zi:[(a, a)]
zis) = (a, a) -> String
forall {a} {a}. (Eq a, Num a, Show a, Show a) => (a, a) -> String
sh (a, a)
zi String -> ShowS
forall a. [a] -> [a] -> [a]
++ [(a, a)] -> String
forall {a} {a}. (Eq a, Num a, Show a, Show a) => [(a, a)] -> String
shs' [(a, a)]
zis

    shs' :: [(a, a)] -> String
shs' []       = String
""
    shs' ((a, a)
zi:[(a, a)]
zis) = String
" + " String -> ShowS
forall a. [a] -> [a] -> [a]
++ (a, a) -> String
forall {a} {a}. (Eq a, Num a, Show a, Show a) => (a, a) -> String
sh (a, a)
zi String -> ShowS
forall a. [a] -> [a] -> [a]
++ [(a, a)] -> String
shs' [(a, a)]
zis

    sh :: (a, a) -> String
sh (a
1,a
i) = String
"e" String -> ShowS
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show a
i
    sh (a
z,a
i) = a -> String
forall a. Show a => a -> String
show a
z String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"!e" String -> ShowS
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show a
i

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

-- AbElement -


-- | elements of an finitely generated abelian group. There 'root' - which is an element of 'AbGroup' -

--   gives there affiliated group. They are gererated via 'make'.

newtype AbElement = AbElement (Slice From (Free N1) AbHom) deriving (Int -> AbElement -> ShowS
[AbElement] -> ShowS
AbElement -> String
(Int -> AbElement -> ShowS)
-> (AbElement -> String)
-> ([AbElement] -> ShowS)
-> Show AbElement
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> AbElement -> ShowS
showsPrec :: Int -> AbElement -> ShowS
$cshow :: AbElement -> String
show :: AbElement -> String
$cshowList :: [AbElement] -> ShowS
showList :: [AbElement] -> ShowS
Show,AbElement -> AbElement -> Bool
(AbElement -> AbElement -> Bool)
-> (AbElement -> AbElement -> Bool) -> Eq AbElement
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: AbElement -> AbElement -> Bool
== :: AbElement -> AbElement -> Bool
$c/= :: AbElement -> AbElement -> Bool
/= :: AbElement -> AbElement -> Bool
Eq,Eq AbElement
Eq AbElement =>
(AbElement -> AbElement -> Ordering)
-> (AbElement -> AbElement -> Bool)
-> (AbElement -> AbElement -> Bool)
-> (AbElement -> AbElement -> Bool)
-> (AbElement -> AbElement -> Bool)
-> (AbElement -> AbElement -> AbElement)
-> (AbElement -> AbElement -> AbElement)
-> Ord AbElement
AbElement -> AbElement -> Bool
AbElement -> AbElement -> Ordering
AbElement -> AbElement -> AbElement
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 :: AbElement -> AbElement -> Ordering
compare :: AbElement -> AbElement -> Ordering
$c< :: AbElement -> AbElement -> Bool
< :: AbElement -> AbElement -> Bool
$c<= :: AbElement -> AbElement -> Bool
<= :: AbElement -> AbElement -> Bool
$c> :: AbElement -> AbElement -> Bool
> :: AbElement -> AbElement -> Bool
$c>= :: AbElement -> AbElement -> Bool
>= :: AbElement -> AbElement -> Bool
$cmax :: AbElement -> AbElement -> AbElement
max :: AbElement -> AbElement -> AbElement
$cmin :: AbElement -> AbElement -> AbElement
min :: AbElement -> AbElement -> AbElement
Ord,AbElement -> Statement
(AbElement -> Statement) -> Validable AbElement
forall a. (a -> Statement) -> Validable a
$cvalid :: AbElement -> Statement
valid :: AbElement -> Statement
Validable)

instance LengthN AbElement where
  lengthN :: AbElement -> N
lengthN (AbElement (SliceFrom Free N1 AbHom
_ AbHom
a)) = AbGroup -> N
forall x. LengthN x => x -> N
lengthN (AbGroup -> N) -> AbGroup -> N
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ AbHom -> Point AbHom
forall q. Oriented q => q -> Point q
end AbHom
a

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

-- AbElement - Constructable -


instance Exposable AbElement where
  type Form AbElement = AbElementForm
  form :: AbElement -> Form AbElement
form (AbElement (SliceFrom Free N1 AbHom
_ AbHom
a)) = AbGroup -> [(Z, N)] -> AbElementForm
AbElementForm (AbHom -> Point AbHom
forall q. Oriented q => q -> Point q
end AbHom
a) [(Z, N)]
zis where
    zis :: [(Z, N)]
zis = ((Z, N, N) -> (Z, N)) -> [(Z, N, N)] -> [(Z, N)]
forall (h :: * -> * -> *) (f :: * -> *) x y.
Applicative1 h f =>
h x y -> f x -> f y
amap1 (\(Z
z,N
i,N
_) -> (Z
z,N
i))
        ([(Z, N, N)] -> [(Z, N)]) -> [(Z, N, N)] -> [(Z, N)]
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ Entries N N Z -> [(Z, N, N)]
forall i j x. Entries i j x -> [(x, i, j)]
etsxs (Entries N N Z -> [(Z, N, N)]) -> Entries N N Z -> [(Z, N, N)]
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ Matrix Z -> Entries N N Z
forall x. Matrix x -> Entries N N x
mtxxs (Matrix Z -> Entries N N Z) -> Matrix Z -> Entries N N Z
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ AbHom -> Matrix Z
abhz AbHom
a
  
instance Constructable AbElement where
  make :: Form AbElement -> AbElement
make (AbElementForm AbGroup
a [(Z, N)]
zis)
    = Slice 'From (Free N1) AbHom -> AbElement
AbElement
    (Slice 'From (Free N1) AbHom -> AbElement)
-> Slice 'From (Free N1) AbHom -> AbElement
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ Free N1 AbHom -> AbHom -> Slice 'From (Free N1) AbHom
forall (i :: * -> *) x. i x -> x -> Slice 'From i x
SliceFrom (Any N1 -> Free N1 AbHom
forall (k :: N') c. Any k -> Free k c
Free (W 'N0 -> W ('N0 + 1)
forall (n1 :: N'). W n1 -> W (n1 + 1)
SW W 'N0
W0))
    (AbHom -> Slice 'From (Free N1) AbHom)
-> AbHom -> Slice 'From (Free N1) AbHom
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ Orientation AbGroup -> [(Z, N, N)] -> AbHom
abh' (N -> AbGroup
abg N
0 AbGroup -> AbGroup -> Orientation AbGroup
forall p. p -> p -> Orientation p
:> AbGroup
a)
    ([(Z, N, N)] -> AbHom) -> [(Z, N, N)] -> AbHom
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ ((Z, N) -> (Z, N, N)) -> [(Z, N)] -> [(Z, N, N)]
forall (h :: * -> * -> *) (f :: * -> *) x y.
Applicative1 h f =>
h x y -> f x -> f y
amap1 (\(Z
z,N
i) -> (Z
z,N
i,N
0))
    ([(Z, N)] -> [(Z, N, N)]) -> [(Z, N)] -> [(Z, N, N)]
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ LinearCombination Z N -> [(Z, N)]
forall r a. LinearCombination r a -> [(r, a)]
lcs
    (LinearCombination Z N -> [(Z, N)])
-> LinearCombination Z N -> [(Z, N)]
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ SumSymbol Z N -> LinearCombination Z N
forall r a. Semiring r => SumSymbol r a -> LinearCombination r a
ssylc
    (SumSymbol Z N -> LinearCombination Z N)
-> SumSymbol Z N -> LinearCombination Z N
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ [(Z, N)] -> SumSymbol Z N
forall r a.
(Semiring r, Commutative r, Entity a, Ord a) =>
[(r, a)] -> SumSymbol r a
sumSymbol
    ([(Z, N)] -> SumSymbol Z N) -> [(Z, N)] -> SumSymbol Z N
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ ((Z, N) -> Bool) -> [(Z, N)] -> [(Z, N)]
forall a. (a -> Bool) -> [a] -> [a]
filter ((N -> N -> Bool
forall a. Ord a => a -> a -> Bool
<N
n)(N -> Bool) -> ((Z, N) -> N) -> (Z, 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
.(Z, N) -> N
forall a b. (a, b) -> b
snd)
    ([(Z, N)] -> [(Z, N)]) -> [(Z, N)] -> [(Z, N)]
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ [(Z, N)]
zis
    where n :: N
n = AbGroup -> N
forall x. LengthN x => x -> N
lengthN AbGroup
a

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

-- abge -


-- | the @i@-th canonical generator of the given abelian group.

abge :: AbGroup -> N -> AbElement
abge :: AbGroup -> N -> AbElement
abge AbGroup
a N
i = Form AbElement -> AbElement
forall x. Constructable x => Form x -> x
make (AbGroup -> [(Z, N)] -> AbElementForm
AbElementForm AbGroup
a [(Z
1,N
i)])

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

-- vecabhFree1 -


-- | the abelian homomorphism with the free 'start' point of dimension @1@ and free

-- 'end' point of the given dimension according to the given vector.

vecabhFree1 :: N -> Vector Z -> Slice From (Free N1) AbHom
vecabhFree1 :: N -> Vector Z -> Slice 'From (Free N1) AbHom
vecabhFree1 N
r Vector Z
v = Free N1 AbHom -> AbHom -> Slice 'From (Free N1) AbHom
forall (i :: * -> *) x. i x -> x -> Slice 'From i x
SliceFrom (Any N1 -> Free N1 AbHom
forall (k :: N') c. Any k -> Free k c
Free Any N1
forall (n :: N'). Attestable n => W n
attest :: Free N1 AbHom) (Matrix Z -> AbHom
zabh Matrix Z
h) where
  h :: Matrix Z
h = N -> N -> [(Z, N, N)] -> Matrix Z
forall x.
(Additive x, FibredOriented x, Total x) =>
N -> N -> [(x, N, N)] -> Matrix x
matrixTtl N
r N
1 ([(Z, N, N)] -> Matrix Z) -> [(Z, N, N)] -> Matrix Z
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ ((Z, N) -> (Z, N, N)) -> [(Z, N)] -> [(Z, N, N)]
forall (h :: * -> * -> *) (f :: * -> *) x y.
Applicative1 h f =>
h x y -> f x -> f y
amap1 (\(Z
x,N
i) -> (Z
x,N
i,N
0)) ([(Z, N)] -> [(Z, N, N)]) -> [(Z, N)] -> [(Z, N, N)]
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ ((Z, N) -> Bool) -> [(Z, N)] -> [(Z, N)]
forall a. (a -> Bool) -> [a] -> [a]
filter ((N -> N -> Bool
forall a. Ord a => a -> a -> Bool
<N
r)(N -> Bool) -> ((Z, N) -> N) -> (Z, 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
.(Z, N) -> N
forall a b. (a, b) -> b
snd) ([(Z, N)] -> [(Z, N)]) -> [(Z, N)] -> [(Z, N)]
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ PSequence N Z -> [(Z, N)]
forall i x. PSequence i x -> [(x, i)]
psqxs (PSequence N Z -> [(Z, N)]) -> PSequence N Z -> [(Z, N)]
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ Vector Z -> PSequence N Z
forall r. Vector r -> PSequence N r
vecpsq Vector Z
v 

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

-- abhvecFree1 -


-- | the underlying 'Z'-vector.

abhvecFree1 :: Slice From (Free N1) AbHom -> Vector Z
abhvecFree1 :: Slice 'From (Free N1) AbHom -> Vector Z
abhvecFree1 (SliceFrom Free N1 AbHom
_ AbHom
h) = Row N (Col N Z) -> Vector Z
forall i j r. (i ~ N, j ~ N) => Row j (Col i r) -> Vector r
fstRow (Row N (Col N Z) -> Vector Z) -> Row N (Col N Z) -> Vector Z
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ Matrix Z -> Row N (Col N Z)
forall x. Matrix x -> Row N (Col N x)
mtxRowCol (Matrix Z -> Row N (Col N Z)) -> Matrix Z -> Row N (Col N Z)
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ AbHom -> Matrix Z
abhz AbHom
h where
  fstRow :: (i ~ N, j ~ N) => Row j (Col i r) -> Vector r
  fstRow :: forall i j r. (i ~ N, j ~ N) => Row j (Col i r) -> Vector r
fstRow (Row (PSequence [(Col i r, j)]
rs)) = case [(Col i r, j)]
rs of
    []            -> PSequence N r -> Vector r
forall r. PSequence N r -> Vector r
Vector PSequence N r
forall i x. PSequence i x
psqEmpty
    [(Col PSequence i r
ris,j
0)] -> PSequence N r -> Vector r
forall r. PSequence N r -> Vector r
Vector PSequence i r
PSequence N r
ris
    [(Col i r, j)]
_             -> AlgebraicException -> Vector r
forall a e. Exception e => e -> a
throw (AlgebraicException -> Vector r) -> AlgebraicException -> Vector r
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ String -> AlgebraicException
InvalidData String
"abhvecFree1"
    
--------------------------------------------------------------------------------

-- AbElement - Abelian -


type instance Root AbElement = AbGroup -- i.e. Root (Slice From (Free N1) AbHom)

instance ShowRoot AbElement
instance EqRoot AbElement
instance ValidableRoot AbElement
instance TypeableRoot AbElement

instance Fibred AbElement where  
  root :: AbElement -> Root AbElement
root (AbElement Slice 'From (Free N1) AbHom
a) = Slice 'From (Free N1) AbHom -> Root (Slice 'From (Free N1) AbHom)
forall f. Fibred f => f -> Root f
root Slice 'From (Free N1) AbHom
a

instance Additive AbElement where
  zero :: Root AbElement -> AbElement
zero Root AbElement
g = Slice 'From (Free N1) AbHom -> AbElement
AbElement (Root (Slice 'From (Free N1) AbHom) -> Slice 'From (Free N1) AbHom
forall a. Additive a => Root a -> a
zero Root (Slice 'From (Free N1) AbHom)
Root AbElement
g)

  AbElement Slice 'From (Free N1) AbHom
a + :: AbElement -> AbElement -> AbElement
+ AbElement Slice 'From (Free N1) AbHom
b = Slice 'From (Free N1) AbHom -> AbElement
AbElement (Slice 'From (Free N1) AbHom
aSlice 'From (Free N1) AbHom
-> Slice 'From (Free N1) AbHom -> Slice 'From (Free N1) AbHom
forall a. Additive a => a -> a -> a
+Slice 'From (Free N1) AbHom
b)

  ntimes :: N -> AbElement -> AbElement
ntimes N
n (AbElement Slice 'From (Free N1) AbHom
a) = Slice 'From (Free N1) AbHom -> AbElement
AbElement (Slice 'From (Free N1) AbHom -> AbElement)
-> Slice 'From (Free N1) AbHom -> AbElement
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ N -> Slice 'From (Free N1) AbHom -> Slice 'From (Free N1) AbHom
forall a. Additive a => N -> a -> a
ntimes N
n Slice 'From (Free N1) AbHom
a
    
instance Abelian AbElement where
  negate :: AbElement -> AbElement
negate (AbElement Slice 'From (Free N1) AbHom
a) = Slice 'From (Free N1) AbHom -> AbElement
AbElement (Slice 'From (Free N1) AbHom -> AbElement)
-> Slice 'From (Free N1) AbHom -> AbElement
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ Slice 'From (Free N1) AbHom -> Slice 'From (Free N1) AbHom
forall a. Abelian a => a -> a
negate Slice 'From (Free N1) AbHom
a

  AbElement Slice 'From (Free N1) AbHom
a - :: AbElement -> AbElement -> AbElement
- AbElement Slice 'From (Free N1) AbHom
b = Slice 'From (Free N1) AbHom -> AbElement
AbElement (Slice 'From (Free N1) AbHom
aSlice 'From (Free N1) AbHom
-> Slice 'From (Free N1) AbHom -> Slice 'From (Free N1) AbHom
forall a. Abelian a => a -> a -> a
-Slice 'From (Free N1) AbHom
b)

  ztimes :: Z -> AbElement -> AbElement
ztimes Z
z (AbElement Slice 'From (Free N1) AbHom
a) = Slice 'From (Free N1) AbHom -> AbElement
AbElement (Slice 'From (Free N1) AbHom -> AbElement)
-> Slice 'From (Free N1) AbHom -> AbElement
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ Z -> Slice 'From (Free N1) AbHom -> Slice 'From (Free N1) AbHom
forall a. Abelian a => Z -> a -> a
ztimes Z
z Slice 'From (Free N1) AbHom
a

instance Vectorial AbElement where
  type Scalar AbElement = Z
  Scalar AbElement
z ! :: Scalar AbElement -> AbElement -> AbElement
! AbElement Slice 'From (Free N1) AbHom
a = Slice 'From (Free N1) AbHom -> AbElement
AbElement (Scalar (Slice 'From (Free N1) AbHom)
Scalar AbElement
zScalar (Slice 'From (Free N1) AbHom)
-> Slice 'From (Free N1) AbHom -> Slice 'From (Free N1) AbHom
forall v. Vectorial v => Scalar v -> v -> v
!Slice 'From (Free N1) AbHom
a)

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

-- 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 :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ 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 :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ Free n AbHom -> AbHom -> Slice 'From (Free n) AbHom
forall (i :: * -> *) x. i x -> x -> Slice 'From i x
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 :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ [(Q, X AbGroup)] -> X (X AbGroup)
forall a. [(Q, a)] -> X a
xOneOfW [ (Q
99,([ZMod] -> AbGroup) -> X [ZMod] -> X AbGroup
forall (h :: * -> * -> *) (f :: * -> *) x y.
Applicative1 h f =>
h x y -> f x -> f y
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 :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ 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 :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ 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 :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ Matrix ZModHom -> AbHom
AbHom (Matrix ZModHom -> AbHom) -> Matrix ZModHom -> AbHom
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ 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 :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ 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 (h :: * -> * -> *) (f :: * -> *) x y.
Applicative1 h f =>
h x y -> f x -> f y
amap1 AbHom -> String
s (X AbHom -> X String) -> X AbHom -> X String
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ 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 (h :: * -> * -> *) (f :: * -> *) x y.
Applicative1 h f =>
h x y -> f x -> f y
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 (h :: * -> * -> *) (f :: * -> *) x y.
Applicative1 h f =>
h x y -> f x -> f y
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 (h :: * -> * -> *) (f :: * -> *) x y.
Applicative1 h f =>
h x y -> f x -> f y
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 :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ [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 x. GLT x -> RowTrafo x
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 (h :: * -> * -> *) (f :: * -> *) x y.
Applicative1 h f =>
h x y -> f x -> f y
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 :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ 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 :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ 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 :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ 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 (h :: * -> * -> *) (f :: * -> *) x y.
Applicative1 h f =>
h x y -> f x -> f y
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 :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ ((N, N) -> N) -> [(N, N)] -> [N]
forall (h :: * -> * -> *) (f :: * -> *) x y.
Applicative1 h f =>
h x y -> f x -> f y
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 :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ N -> ZMod
ZMod (N -> ZMod) -> N -> ZMod
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ (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 :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ (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 (h :: * -> * -> *) (f :: * -> *) x y.
Applicative1 h f =>
h x y -> f x -> f y
amap1 AbHom -> String
w (X AbHom -> X String) -> X AbHom -> X String
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ 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 :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ (Q
100Q -> Q -> Q
forall c. Multiplicative c => c -> c -> c
*) (Q -> Q) -> Q -> Q
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ (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 (h :: * -> * -> *) (f :: * -> *) x y.
Applicative1 h f =>
h x y -> f x -> f y
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 (h :: * -> * -> *) (f :: * -> *) x y.
Applicative1 h f =>
h x y -> f x -> f y
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 (h :: * -> * -> *) (f :: * -> *) x y.
Applicative1 h f =>
h x y -> f x -> f y
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 :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ [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 {x}. Distributive x => Dim x (Point x) -> X (RowTrafo x)
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 x (Point x) -> X (RowTrafo x)
xpr Dim x (Point x)
r = 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)
r)
    RowTrafo x -> X (RowTrafo x)
forall a. a -> X a
forall (m :: * -> *) a. Monad m => a -> m a
return (GLT x -> RowTrafo x
forall x. GLT x -> RowTrafo x
RowTrafo (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)
r Dim x (Point x) -> Permutation N -> Dim x (Point x)
forall f x. Opr f x => x -> f -> x
<* Permutation N
p) Dim x (Point x)
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 (h :: * -> * -> *) (f :: * -> *) x y.
Applicative1 h f =>
h x y -> f x -> f y
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 :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ 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 :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ 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 :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ 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 (h :: * -> * -> *) (f :: * -> *) x y.
Applicative1 h f =>
h x y -> f x -> f y
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 :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ ((N, N) -> N) -> [(N, N)] -> [N]
forall (h :: * -> * -> *) (f :: * -> *) x y.
Applicative1 h f =>
h x y -> f x -> f y
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 :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ N -> ZMod
ZMod (N -> ZMod) -> N -> ZMod
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ (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 :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ (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 (h :: * -> * -> *) (f :: * -> *) x y.
Applicative1 h f =>
h x y -> f x -> f y
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 (h :: * -> * -> *) (f :: * -> *) x y.
Applicative1 h f =>
h x y -> f x -> f y
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 (h :: * -> * -> *) (f :: * -> *) x y.
Applicative1 h f =>
h x y -> f x -> f y
amap1 AbHom -> Point AbHom
AbHom -> AbGroup
forall q. Oriented q => q -> Point q
end (X AbHom -> X AbGroup) -> X AbHom -> X AbGroup
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ 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
      
    
instance XStandardEligibleConeG Cone Dst Projective Diagram (Parallel LeftToRight) N2 N1 AbHom where
  xStandardEligibleConeG :: XEligibleConeG
  Cone Dst 'Projective Diagram ('Parallel 'LeftToRight) N2 N1 AbHom
xStandardEligibleConeG = XEligibleConeFactorG
  Cone Dst 'Projective Diagram ('Parallel 'LeftToRight) N2 N1 AbHom
-> XEligibleConeG
     Cone Dst 'Projective Diagram ('Parallel 'LeftToRight) N2 N1 AbHom
forall (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       s (p :: Perspective) (d :: DiagramType -> N' -> N' -> * -> *)
       (t :: DiagramType) (n :: N') (m :: N') x.
XEligibleConeFactorG c s p d t n m x
-> XEligibleConeG c s p d t n m x
xecfEligibleCone XEligibleConeFactorG
  Cone Dst 'Projective Diagram ('Parallel 'LeftToRight) N2 N1 AbHom
forall (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       s (p :: Perspective) (d :: DiagramType -> N' -> N' -> * -> *)
       (t :: DiagramType) (n :: N') (m :: N') x.
XStandardEligibleConeFactorG c s p d t n m x =>
XEligibleConeFactorG c s p d t n m x
xStandardEligibleConeFactorG
  
instance XStandardEligibleConeFactorG
           Cone Dst Projective Diagram (Parallel LeftToRight) N2 N1 AbHom where
  xStandardEligibleConeFactorG :: XEligibleConeFactorG
  Cone Dst 'Projective Diagram ('Parallel 'LeftToRight) N2 N1 AbHom
xStandardEligibleConeFactorG = XOrtSite 'To AbHom
-> XEligibleConeFactorG
     Cone
     Dst
     (ToPerspective 'To)
     Diagram
     ('Parallel 'LeftToRight)
     N2
     N1
     AbHom
forall (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       (r :: Site) x s (d :: DiagramType -> N' -> N' -> * -> *)
       (t :: DiagramType) (n :: N') (m :: N').
Conic c =>
XOrtSite r x
-> XEligibleConeFactorG c s (ToPerspective r) d t n m x
xecfOrtSite (XOrtSite 'To AbHom
forall (s :: Site) a. XStandardOrtSite s a => XOrtSite s a
xStandardOrtSite :: XOrtSite To AbHom)

instance XStandardEligibleConeG
           ConeLiftable Dst Injective Diagram (Parallel RightToLeft) N2 N1 AbHom where
  xStandardEligibleConeG :: XEligibleConeG
  ConeLiftable
  Dst
  'Injective
  Diagram
  ('Parallel 'RightToLeft)
  N2
  N1
  AbHom
xStandardEligibleConeG = XEligibleConeFactorG
  ConeLiftable
  Dst
  'Injective
  Diagram
  ('Parallel 'RightToLeft)
  N2
  N1
  AbHom
-> XEligibleConeG
     ConeLiftable
     Dst
     'Injective
     Diagram
     ('Parallel 'RightToLeft)
     N2
     N1
     AbHom
forall (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       s (p :: Perspective) (d :: DiagramType -> N' -> N' -> * -> *)
       (t :: DiagramType) (n :: N') (m :: N') x.
XEligibleConeFactorG c s p d t n m x
-> XEligibleConeG c s p d t n m x
xecfEligibleCone XEligibleConeFactorG
  ConeLiftable
  Dst
  'Injective
  Diagram
  ('Parallel 'RightToLeft)
  N2
  N1
  AbHom
forall (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       s (p :: Perspective) (d :: DiagramType -> N' -> N' -> * -> *)
       (t :: DiagramType) (n :: N') (m :: N') x.
XStandardEligibleConeFactorG c s p d t n m x =>
XEligibleConeFactorG c s p d t n m x
xStandardEligibleConeFactorG
  
instance XStandardEligibleConeFactorG
           ConeLiftable Dst Injective Diagram (Parallel RightToLeft) N2 N1 AbHom where
  xStandardEligibleConeFactorG :: XEligibleConeFactorG
  ConeLiftable
  Dst
  'Injective
  Diagram
  ('Parallel 'RightToLeft)
  N2
  N1
  AbHom
xStandardEligibleConeFactorG = XOrtSite 'From AbHom
-> XEligibleConeFactorG
     ConeLiftable
     Dst
     (ToPerspective 'From)
     Diagram
     ('Parallel 'RightToLeft)
     N2
     N1
     AbHom
forall (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       (r :: Site) x s (d :: DiagramType -> N' -> N' -> * -> *)
       (t :: DiagramType) (n :: N') (m :: N').
Conic c =>
XOrtSite r x
-> XEligibleConeFactorG c s (ToPerspective r) d t n m x
xecfOrtSite (XOrtSite 'From AbHom
forall (s :: Site) a. XStandardOrtSite s a => XOrtSite s a
xStandardOrtSite :: XOrtSite From AbHom)

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

-- 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 (h :: * -> * -> *) (f :: * -> *) x y.
Applicative1 h f =>
h x y -> f x -> f y
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 :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ 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 :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ 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)

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

-- xAbhSomeFreeSlice -


-- | random variable for some free slice from in 'AbHom'

xAbhSomeFreeSlice :: N -> X (SomeFreeSlice From AbHom)
xAbhSomeFreeSlice :: N -> X (SomeFreeSlice 'From AbHom)
xAbhSomeFreeSlice N
nMax = do
  N
n <- N -> N -> X N
xNB N
0 N
nMax
  AbGroup
g <- X AbGroup
forall x. XStandard x => X x
xStandard
  AbHom
h <- Q -> Orientation AbGroup -> X AbHom
xAbHom Q
0.8 ((AbGroup
z1 AbGroup -> Exponent AbGroup -> AbGroup
forall f. Exponential f => f -> Exponent f -> f
^ N
Exponent AbGroup
n) AbGroup -> AbGroup -> Orientation AbGroup
forall p. p -> p -> Orientation p
:> AbGroup
g)
  case N -> SomeNatural
someNatural N
n of
    SomeNatural W n
sn -> 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 :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ 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 (Free n AbHom -> AbHom -> Slice 'From (Free n) AbHom
forall (i :: * -> *) x. i x -> x -> Slice 'From i x
SliceFrom (W n -> Free n AbHom
forall (k :: N') c. Any k -> Free k c
Free W n
sn) AbHom
h)
  where z1 :: AbGroup
z1 = N -> AbGroup
abg N
0