{-# LANGUAGE NoImplicitPrelude #-}

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

-- |
-- Module      : OAlg.Entity.Matrix.GeneralLinearGroup
-- Description : general linear group and elementary transformations
-- Copyright   : (c) Erich Gut
-- License     : BSD3
-- Maintainer  : zerich.gut@gmail.com
-- 
-- general linear group 'GL' and elementary transformations over a 'Galoisian' structure.
module OAlg.Entity.Matrix.GeneralLinearGroup
  (
    -- * Transformation
    Transformation(..)

    -- * GL
  , GL, GL2(..)

    -- * GLT
  , GLT()
  , permute, permuteFT
  , scale, shear
  , rdcGLTForm
  
  , GLTForm, gltfTrsp

    -- * FT
  , FT
  
    -- * Homomorphism
    
    -- ** Ort
  , TrApp(..)
  , trGLT
  
    -- ** Mlt
  , GLApp(..)

  )

  where

import Control.Monad hiding (sequence)

import Data.Typeable
import Data.List ((++))

import OAlg.Prelude hiding (T)

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

import OAlg.Structure.Exception
import OAlg.Structure.Oriented
import OAlg.Structure.Multiplicative
import OAlg.Structure.Additive
import OAlg.Structure.Distributive
import OAlg.Structure.Ring
import OAlg.Structure.Number
import OAlg.Structure.Exponential
import OAlg.Structure.Operational

import OAlg.Hom.Oriented
import OAlg.Hom.Multiplicative

import OAlg.Entity.Product
import OAlg.Entity.Sequence

import OAlg.Entity.Matrix.Dim
import OAlg.Entity.Matrix.Entries
import OAlg.Entity.Matrix.Definition

--------------------------------------------------------------------------------
-- GL -

-- | general linear groupoid of matrices.
type GL x = Inv (Matrix x)

--------------------------------------------------------------------------------
-- GL2 -

-- | the general linear group of @2x2@ matrices for a 'Galoisian' structure @__x__@.
--
--  __Property__ Let @'GL2' s t u v@ be in @t'GL2' __x__@ for a 'Galoisian' structure
--  @__x__@, then holds: @s'*'v '-' u'*'t@ is invertible.
--
--  __Example__ Let @g = 'GL2' 3 5 4 7 :: 'GL2' 'Z'@:
--
--  >>> invert g
-- GL2 7 -5 -4 3
--
-- >>> g * invert g
-- GL2 1 0 0 1
--
-- which is the 'one' in @'GL2' 'Z'@.
--
--  __Note__
--
--  @'GL2' (s t u v)@ represents the @2x2@-matrix
--
-- @
--    [s t]
--    [u v]
-- @
--
-- and is obtained by 'GL2GL'.
data GL2 x = GL2 x x x x deriving (Int -> GL2 x -> ShowS
forall x. Show x => Int -> GL2 x -> ShowS
forall x. Show x => [GL2 x] -> ShowS
forall x. Show x => GL2 x -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [GL2 x] -> ShowS
$cshowList :: forall x. Show x => [GL2 x] -> ShowS
show :: GL2 x -> String
$cshow :: forall x. Show x => GL2 x -> String
showsPrec :: Int -> GL2 x -> ShowS
$cshowsPrec :: forall x. Show x => Int -> GL2 x -> ShowS
Show,GL2 x -> GL2 x -> Bool
forall x. Eq x => GL2 x -> GL2 x -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: GL2 x -> GL2 x -> Bool
$c/= :: forall x. Eq x => GL2 x -> GL2 x -> Bool
== :: GL2 x -> GL2 x -> Bool
$c== :: forall x. Eq x => GL2 x -> GL2 x -> Bool
Eq,GL2 x -> GL2 x -> Bool
GL2 x -> GL2 x -> Ordering
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
forall {x}. Ord x => Eq (GL2 x)
forall x. Ord x => GL2 x -> GL2 x -> Bool
forall x. Ord x => GL2 x -> GL2 x -> Ordering
forall x. Ord x => GL2 x -> GL2 x -> GL2 x
min :: GL2 x -> GL2 x -> GL2 x
$cmin :: forall x. Ord x => GL2 x -> GL2 x -> GL2 x
max :: GL2 x -> GL2 x -> GL2 x
$cmax :: forall x. Ord x => GL2 x -> GL2 x -> GL2 x
>= :: GL2 x -> GL2 x -> Bool
$c>= :: forall x. Ord x => GL2 x -> GL2 x -> Bool
> :: GL2 x -> GL2 x -> Bool
$c> :: forall x. Ord x => GL2 x -> GL2 x -> Bool
<= :: GL2 x -> GL2 x -> Bool
$c<= :: forall x. Ord x => GL2 x -> GL2 x -> Bool
< :: GL2 x -> GL2 x -> Bool
$c< :: forall x. Ord x => GL2 x -> GL2 x -> Bool
compare :: GL2 x -> GL2 x -> Ordering
$ccompare :: forall x. Ord x => GL2 x -> GL2 x -> Ordering
Ord)

--------------------------------------------------------------------------------
-- gl2Det -

-- | the determinate of a galoisian matrix.
gl2Det :: Galoisian x => GL2 x -> x
gl2Det :: forall x. Galoisian x => GL2 x -> x
gl2Det (GL2 x
s x
t x
u x
v) = x
sforall c. Multiplicative c => c -> c -> c
*x
v forall a. Abelian a => a -> a -> a
- x
uforall c. Multiplicative c => c -> c -> c
*x
t

--------------------------------------------------------------------------------
-- gl2GL -

-- | the associate invertible @2x2@-matrix.
gl2GL :: Galoisian x => GL2 x -> GL x
gl2GL :: forall x. Galoisian x => GL2 x -> GL x
gl2GL GL2 x
g = forall c. c -> c -> Inv c
Inv (forall {x}. (Oriented x, Singleton (Point x)) => GL2 x -> Matrix x
gl GL2 x
g) (forall {x}. (Oriented x, Singleton (Point x)) => GL2 x -> Matrix x
gl forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall c. Invertible c => c -> c
invert GL2 x
g) where
  gl :: GL2 x -> Matrix x
gl (GL2 x
s x
t x
u x
v) = forall x. Dim' x -> Dim' x -> Entries N N x -> Matrix x
Matrix Dim x (Point x)
d Dim x (Point x)
d (forall i j x. PSequence (i, j) x -> Entries i j x
Entries (forall i x. [(x, i)] -> PSequence i x
PSequence [(x, (N, N))]
xs)) where
    d :: Dim x (Point x)
d = forall p x. (Entity p, p ~ Point x) => p -> Dim x p
dim forall s. Singleton s => s
unit forall f. Exponential f => f -> Exponent f -> f
^ N
2
    xs :: [(x, (N, N))]
xs = [(x
s,(N
0,N
0)),(x
t,(N
0,N
1)),(x
u,(N
1,N
0)),(x
v,(N
1,N
1))]

--------------------------------------------------------------------------------
-- GL2 - Cayleyan -

instance Galoisian x => Validable (GL2 x) where
  valid :: GL2 x -> Statement
valid g :: GL2 x
g@(GL2 x
s x
t x
u x
v)
    = [Statement] -> Statement
And [ forall a. Validable a => a -> Statement
valid (x
s,x
t,x
u,x
v)
          , String -> Label
Label String
"det" Label -> Statement -> Statement
:<=>: forall c. Invertible c => c -> Bool
isInvertible (forall x. Galoisian x => GL2 x -> x
gl2Det GL2 x
g) Bool -> Message -> Statement
:?> [Parameter] -> Message
Params [String
"g"String -> String -> Parameter
:=forall a. Show a => a -> String
show GL2 x
g] 
          ]

instance Galoisian x => Entity (GL2 x)

instance Galoisian x => Oriented (GL2 x) where
  type Point (GL2 x) = Point x
  orientation :: GL2 x -> Orientation (Point (GL2 x))
orientation GL2 x
_ = forall s. Singleton s => s
unit forall p. p -> p -> Orientation p
:> forall s. Singleton s => s
unit

instance Galoisian x => Total (GL2 x)

instance Galoisian x => Multiplicative (GL2 x) where
  one :: Point (GL2 x) -> GL2 x
one Point (GL2 x)
p = forall x. x -> x -> x -> x -> GL2 x
GL2 x
o x
z x
z x
o where
    o :: x
o = forall c. Multiplicative c => Point c -> c
one Point (GL2 x)
p
    z :: x
z = forall a. Additive a => Root a -> a
zero (Point (GL2 x)
pforall p. p -> p -> Orientation p
:>Point (GL2 x)
p)

  GL2 x
s x
t x
u x
v * :: GL2 x -> GL2 x -> GL2 x
* GL2 x
s' x
t' x
u' x
v' = forall x. x -> x -> x -> x -> GL2 x
GL2 (x
sforall c. Multiplicative c => c -> c -> c
*x
s' forall a. Additive a => a -> a -> a
+ x
tforall c. Multiplicative c => c -> c -> c
*x
u') (x
sforall c. Multiplicative c => c -> c -> c
*x
t' forall a. Additive a => a -> a -> a
+ x
tforall c. Multiplicative c => c -> c -> c
*x
v')
                                      (x
uforall c. Multiplicative c => c -> c -> c
*x
s' forall a. Additive a => a -> a -> a
+ x
vforall c. Multiplicative c => c -> c -> c
*x
u') (x
uforall c. Multiplicative c => c -> c -> c
*x
t' forall a. Additive a => a -> a -> a
+ x
vforall c. Multiplicative c => c -> c -> c
*x
v')

instance Galoisian x => Invertible (GL2 x) where
  tryToInvert :: GL2 x -> Solver (GL2 x)
tryToInvert g :: GL2 x
g@(GL2 x
s x
t x
u x
v) = do
    x
r <- forall c. Invertible c => c -> Solver c
tryToInvert (forall x. Galoisian x => GL2 x -> x
gl2Det GL2 x
g)
    forall (m :: * -> *) a. Monad m => a -> m a
return (forall x. x -> x -> x -> x -> GL2 x
GL2 (x
rforall c. Multiplicative c => c -> c -> c
*x
v) (forall a. Abelian a => a -> a
negate (x
rforall c. Multiplicative c => c -> c -> c
*x
t)) (forall a. Abelian a => a -> a
negate (x
rforall c. Multiplicative c => c -> c -> c
*x
u)) (x
rforall c. Multiplicative c => c -> c -> c
*x
s))

instance Galoisian x => Cayleyan (GL2 x)

instance Galoisian x => Exponential (GL2 x) where
  type Exponent (GL2 x) = Z
  ^ :: GL2 x -> Exponent (GL2 x) -> GL2 x
(^) = forall c. Invertible c => c -> Z -> c
zpower

instance (Galoisian x, TransposableDistributive x) => Transposable (GL2 x) where
  transpose :: GL2 x -> GL2 x
transpose (GL2 x
s x
t x
u x
v) = forall x. x -> x -> x -> x -> GL2 x
GL2 (x -> x
trs x
s) (x -> x
trs x
u) (x -> x
trs x
t) (x -> x
trs x
v) where trs :: x -> x
trs = forall x. Transposable x => x -> x
transpose

instance (Galoisian x, TransposableDistributive x) => TransposableOriented (GL2 x)
instance (Galoisian x, TransposableDistributive x) => TransposableMultiplicative (GL2 x)

--------------------------------------------------------------------------------
-- gl2ScaleRow1 -

-- | scaling the first row.
gl2ScaleRow1 :: Galoisian x => Inv x -> GL2 x -> GL2 x
gl2ScaleRow1 :: forall x. Galoisian x => Inv x -> GL2 x -> GL2 x
gl2ScaleRow1 (Inv x
x x
_) (GL2 x
s x
t x
u x
v) = forall x. x -> x -> x -> x -> GL2 x
GL2 (x
xforall c. Multiplicative c => c -> c -> c
*x
s) (x
xforall c. Multiplicative c => c -> c -> c
*x
t) x
u x
v

--------------------------------------------------------------------------------
-- gl2ScaleRow2 -

-- | scaling the second row.
gl2ScaleRow2 :: Galoisian x => Inv x -> GL2 x -> GL2 x
gl2ScaleRow2 :: forall x. Galoisian x => Inv x -> GL2 x -> GL2 x
gl2ScaleRow2 (Inv x
x x
_) (GL2 x
s x
t x
u x
v) = forall x. x -> x -> x -> x -> GL2 x
GL2 x
s x
t (x
xforall c. Multiplicative c => c -> c -> c
*x
u) (x
xforall c. Multiplicative c => c -> c -> c
*x
v)

--------------------------------------------------------------------------------
-- gl2ScaleCol1 -

-- | scaling the first column.
gl2ScaleCol1 :: Galoisian x => GL2 x -> Inv x -> GL2 x
gl2ScaleCol1 :: forall x. Galoisian x => GL2 x -> Inv x -> GL2 x
gl2ScaleCol1 (GL2 x
s x
t x
u x
v) (Inv x
x x
_) = forall x. x -> x -> x -> x -> GL2 x
GL2 (x
sforall c. Multiplicative c => c -> c -> c
*x
x) x
t (x
uforall c. Multiplicative c => c -> c -> c
*x
x) x
v

--------------------------------------------------------------------------------
-- gl2ScaleCol2 -

-- | scaling the second column.
gl2ScaleCol2 :: Galoisian x => GL2 x -> Inv x -> GL2 x
gl2ScaleCol2 :: forall x. Galoisian x => GL2 x -> Inv x -> GL2 x
gl2ScaleCol2 (GL2 x
s x
t x
u x
v) (Inv x
x x
_) = forall x. x -> x -> x -> x -> GL2 x
GL2 x
s (x
tforall c. Multiplicative c => c -> c -> c
*x
x) x
u (x
vforall c. Multiplicative c => c -> c -> c
*x
x)


--------------------------------------------------------------------------------
-- Transformation -

-- | elementary linear transformation over a 'Distributive' structure @__x__@.
--
-- __Property__ Let @f@ be in @'Transformation' __x__@ then holds:
--
-- (1) If @f@ matches @'Permute' r c p@ then holds:
--
--         (1) @h '<=' 'It' n@ where @(_,h) = 'span' 'nProxy' p@ and @n = 'lengthN' c@.
--
--         (2) @r '==' c '<*' p@.
--
-- (2) If @f@ matches @'Scale' d k s@ then holds:
--
--     (1) @k '<' 'lengthN' d@.
--
--     (2) @s@ is an endo at @d '?' k@.
--
--     (3) @s@ is 'valid'.
--
-- (3) If @f@ matches @'Shear' d k l g@ then holds:
--
--     (1) @k '<' 'lengthN' d@ and @l '<' 'lengthN' d@.
--
--     (2) @k '<' l@.
--
--     (3) @g@ is 'valid'.
--
--
-- __Note__ @'Shear' d k l ('GL2' s t u v)@ represents the square matrix @m@ of dimension @d@
-- where @m k k '==' s@, @m k l '==' t@, @m l k '==' u@, @m l l '==' v@ and
-- for all @i, j@ not in @[k,l]@ holds: If @i '/=' j@ then @m i j@ is 'zero' else @m i i@
-- is 'one'.
data Transformation x where
  Permute :: Distributive x
    => Dim x (Point x) -> Dim x (Point x) -> Permutation N -> Transformation x
  Scale :: Distributive x => Dim x (Point x) -> N -> Inv x -> Transformation x
  Shear :: Galoisian x => Dim x (Point x) -> N -> N -> GL2 x -> Transformation x

--------------------------------------------------------------------------------
-- Transformation - Entity -

deriving instance Eq (Transformation x)
deriving instance Show (Transformation x)

instance Validable (Transformation x) where
  valid :: Transformation x -> Statement
valid (Permute Dim x (Point x)
r Dim x (Point x)
c Permutation N
p) = String -> Label
Label String
"Permute" Label -> Statement -> Statement
:<=>:
    [Statement] -> Statement
And [ forall a. Validable a => a -> Statement
valid (Dim x (Point x)
r,Dim x (Point x)
c,Permutation N
p)
        , String -> Label
Label String
"1.1" Label -> Statement -> Statement
:<=>: let {(Closer N
_,Closer N
h) = forall (s :: * -> *) i x (p :: * -> *).
Sequence s i x =>
p i -> s x -> Span i
span Proxy N
nProxy Permutation N
p; n :: N
n = forall x. LengthN x => x -> N
lengthN Dim x (Point x)
c} in
            (Closer N
h forall a. Ord a => a -> a -> Bool
<= forall x. x -> Closer x
It N
n) Bool -> Message -> Statement
:?> [Parameter] -> Message
Params[String
"h"String -> String -> Parameter
:=forall a. Show a => a -> String
show Closer N
h,String
"n"String -> String -> Parameter
:=forall a. Show a => a -> String
show N
n]
        , String -> Label
Label String
"1.2" Label -> Statement -> Statement
:<=>: (Dim x (Point x)
r forall a. Eq a => a -> a -> Bool
== Dim x (Point x)
c forall f x. Opr f x => x -> f -> x
<* Permutation N
p) Bool -> Message -> Statement
:?> [Parameter] -> Message
Params[String
"r"String -> String -> Parameter
:=forall a. Show a => a -> String
show Dim x (Point x)
r,String
"c"String -> String -> Parameter
:=forall a. Show a => a -> String
show Dim x (Point x)
c,String
"p"String -> String -> Parameter
:=forall a. Show a => a -> String
show Permutation N
p]
        ]
  valid (Scale Dim x (Point x)
d N
k Inv x
s) = String -> Label
Label String
"Scale" Label -> Statement -> Statement
:<=>:
    [Statement] -> Statement
And [ forall a. Validable a => a -> Statement
valid (Dim x (Point x)
d,N
k)
        , String -> Label
Label String
"2,1" Label -> Statement -> Statement
:<=>: let n :: N
n = forall x. LengthN x => x -> N
lengthN Dim x (Point x)
d in
            (N
k forall a. Ord a => a -> a -> Bool
< N
n)Bool -> Message -> Statement
:?>[Parameter] -> Message
Params[String
"d"String -> String -> Parameter
:=forall a. Show a => a -> String
show Dim x (Point x)
d,String
"lengthN d"String -> String -> Parameter
:=forall a. Show a => a -> String
show N
n]
        , String -> Label
Label String
"2.2" Label -> Statement -> Statement
:<=>: forall a. Oriented a => Point a -> a -> Bool
isEndoAt (Dim x (Point x)
dforall (s :: * -> *) i x. Sequence s i x => s x -> i -> x
?N
k) Inv x
s Bool -> Message -> Statement
:?>[Parameter] -> Message
Params [String
"s"String -> String -> Parameter
:=forall a. Show a => a -> String
show Inv x
s]
        , String -> Label
Label String
"2.3" Label -> Statement -> Statement
:<=>: forall a. Validable a => a -> Statement
valid Inv x
s
        ]
  valid (Shear Dim x (Point x)
d N
k N
l GL2 x
g) = String -> Label
Label String
"Shear" Label -> Statement -> Statement
:<=>:
    [Statement] -> Statement
And [ forall a. Validable a => a -> Statement
valid (Dim x (Point x)
d,N
k,N
l)
        , String -> Label
Label String
"3.1" Label -> Statement -> Statement
:<=>: let n :: N
n = forall x. LengthN x => x -> N
lengthN Dim x (Point x)
d in
            [Statement] -> Statement
And [ (N
k forall a. Ord a => a -> a -> Bool
< N
n)Bool -> Message -> Statement
:?>[Parameter] -> Message
Params[String
"d"String -> String -> Parameter
:=forall a. Show a => a -> String
show Dim x (Point x)
d,String
"lengthN d"String -> String -> Parameter
:=forall a. Show a => a -> String
show N
n]
                , (N
l forall a. Ord a => a -> a -> Bool
< N
n)Bool -> Message -> Statement
:?>[Parameter] -> Message
Params[String
"l"String -> String -> Parameter
:=forall a. Show a => a -> String
show N
l,String
"lengthN d"String -> String -> Parameter
:=forall a. Show a => a -> String
show N
n]
                ]
        , String -> Label
Label String
"3.2"Label -> Statement -> Statement
:<=>: (N
k forall a. Ord a => a -> a -> Bool
< N
l)Bool -> Message -> Statement
:?>[Parameter] -> Message
Params[String
"(k,l"String -> String -> Parameter
:=forall a. Show a => a -> String
show (N
k,N
l)]
        , String -> Label
Label String
"3.3" Label -> Statement -> Statement
:<=>: forall a. Validable a => a -> Statement
valid GL2 x
g
        ]

instance Typeable x => Entity (Transformation x)

--------------------------------------------------------------------------------
-- Transformation - Oriented -

instance Oriented x => Oriented (Transformation x) where
  type Point (Transformation x) = Dim x (Point x)
  orientation :: Transformation x -> Orientation (Point (Transformation x))
orientation Transformation x
tr = case Transformation x
tr of
    Permute Dim x (Point x)
r Dim x (Point x)
c Permutation N
_ -> Dim x (Point x)
c forall p. p -> p -> Orientation p
:> Dim x (Point x)
r
    Scale Dim x (Point x)
d N
_ Inv x
_   -> Dim x (Point x)
d forall p. p -> p -> Orientation p
:> Dim x (Point x)
d
    Shear Dim x (Point x)
d N
_ N
_ GL2 x
_ -> Dim x (Point x)
d forall p. p -> p -> Orientation p
:> Dim x (Point x)
d

--------------------------------------------------------------------------------
-- trmtx -

-- | associated matrix of a transformation.
trmtx :: Transformation x -> Matrix x

trmtx :: forall x. Transformation x -> Matrix x
trmtx (Permute Dim x (Point x)
r Dim x (Point x)
c Permutation N
p) = forall x. Dim' x -> Dim' x -> Entries N N x -> Matrix x
Matrix Dim x (Point x)
r Dim x (Point x)
c Entries N N x
os where
  os :: Entries N N x
os = forall i j x. Col i (Row j x) -> Entries i j x
crets ((forall x. Matrix x -> Col N (Row N x)
mtxColRow forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall c. Multiplicative c => Point c -> c
one Dim x (Point x)
c) forall f x. Opr f x => x -> f -> x
<* Permutation N
p)

trmtx (Scale Dim x (Point x)
d N
k Inv x
s) = forall x p.
(Additive x, p ~ Point x) =>
Dim x p -> Dim x p -> [(x, N, N)] -> Matrix x
matrix Dim x (Point x)
d Dim x (Point x)
d ((forall a b. Embeddable a b => a -> b
inj Inv x
s,N
k,N
k)forall a. a -> [a] -> [a]
:[(x, N, N)]
os) where
  os :: [(x, N, N)]
os = [(forall c. Multiplicative c => Point c -> c
one Point x
p,N
i,N
i) | (Point x
p,N
i) <- forall p x. (p ~ Point x) => Dim x p -> [(p, N)]
dimxs Dim x (Point x)
d, N
i forall a. Eq a => a -> a -> Bool
/= N
k]

trmtx (Shear Dim x (Point x)
d N
k N
l (GL2 x
s x
t x
u x
v))= forall x p.
(Additive x, p ~ Point x) =>
Dim x p -> Dim x p -> [(x, N, N)] -> Matrix x
matrix Dim x (Point x)
d Dim x (Point x)
d ([(x, N, N)]
xs forall a. [a] -> [a] -> [a]
++ [(x, N, N)]
os) where
  xs :: [(x, N, N)]
xs = [(x
s,N
k,N
k),(x
t,N
k,N
l),(x
u,N
l,N
k),(x
v,N
l,N
l)]
  os :: [(x, N, N)]
os = [(forall c. Multiplicative c => Point c -> c
one Point x
p,N
i,N
i) | (Point x
p,N
i) <- forall p x. (p ~ Point x) => Dim x p -> [(p, N)]
dimxs Dim x (Point x)
d, N
i forall a. Eq a => a -> a -> Bool
/= N
k, N
i forall a. Eq a => a -> a -> Bool
/= N
l]

--------------------------------------------------------------------------------
-- trInverse -

-- | the formal inverse of a transformation.
trInverse :: Transformation x -> Transformation x
trInverse :: forall x. Transformation x -> Transformation x
trInverse (Permute Dim x (Point x)
r Dim x (Point x)
c Permutation N
p) = forall x.
Distributive x =>
Dim x (Point x)
-> Dim x (Point x) -> Permutation N -> Transformation x
Permute Dim x (Point x)
c Dim x (Point x)
r (forall c. Invertible c => c -> c
invert Permutation N
p)
trInverse (Scale Dim x (Point x)
d N
k Inv x
s)   = forall x.
Distributive x =>
Dim x (Point x) -> N -> Inv x -> Transformation x
Scale Dim x (Point x)
d N
k (forall c. Invertible c => c -> c
invert Inv x
s)
trInverse (Shear Dim x (Point x)
d N
k N
l GL2 x
g) = forall x.
Galoisian x =>
Dim x (Point x) -> N -> N -> GL2 x -> Transformation x
Shear Dim x (Point x)
d N
k N
l (forall c. Invertible c => c -> c
invert GL2 x
g)

--------------------------------------------------------------------------------
-- trGL -

-- | the associated invertible matrix.
trGL :: Transformation x -> GL x
trGL :: forall x. Transformation x -> GL x
trGL Transformation x
t = forall c. c -> c -> Inv c
Inv (forall x. Transformation x -> Matrix x
trmtx Transformation x
t) (forall x. Transformation x -> Matrix x
trmtx forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall x. Transformation x -> Transformation x
trInverse Transformation x
t)

--------------------------------------------------------------------------------
-- rdcPower -

-- | pre: if z /= 1 then f is an endo.
rdcPower :: Transformation x -> Z -> Rdc (Transformation x)
rdcPower :: forall x. Transformation x -> Z -> Rdc (Transformation x)
rdcPower Transformation x
f Z
1         = forall (m :: * -> *) a. Monad m => a -> m a
return Transformation x
f
rdcPower Transformation x
f Z
z | Z
z forall a. Ord a => a -> a -> Bool
< Z
0 = forall x. Transformation x -> Z -> Rdc (Transformation x)
rdcPower (forall x. Transformation x -> Transformation x
trInverse Transformation x
f) (forall r. Number r => r -> r
abs Z
z)
rdcPower Transformation x
f Z
z         = let n :: N
n = forall a b. Projectible a b => b -> a
prj Z
z :: N in case Transformation x
f of
  Permute Dim x (Point x)
r Dim x (Point x)
c Permutation N
p -> forall x. x -> Rdc x
reducesTo forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall x.
Distributive x =>
Dim x (Point x)
-> Dim x (Point x) -> Permutation N -> Transformation x
Permute Dim x (Point x)
r Dim x (Point x)
c (forall c. Multiplicative c => c -> N -> c
npower Permutation N
p N
n)
  Scale Dim x (Point x)
d N
k Inv x
s   -> forall x. x -> Rdc x
reducesTo forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall x.
Distributive x =>
Dim x (Point x) -> N -> Inv x -> Transformation x
Scale Dim x (Point x)
d N
k (forall c. Multiplicative c => c -> N -> c
npower Inv x
s N
n)
  Shear Dim x (Point x)
d N
k N
l GL2 x
g -> forall x. x -> Rdc x
reducesTo forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall x.
Galoisian x =>
Dim x (Point x) -> N -> N -> GL2 x -> Transformation x
Shear Dim x (Point x)
d N
k N
l (forall c. Multiplicative c => c -> N -> c
npower GL2 x
g N
n)

--------------------------------------------------------------------------------
-- rdcTransformations -

-- | reducing transformations.
rdcTransformations :: Word Z (Transformation x) -> Rdc (Word Z (Transformation x))
rdcTransformations :: forall x.
Word Z (Transformation x) -> Rdc (Word Z (Transformation x))
rdcTransformations (Word [(Transformation x, Z)]
fs) = forall {x}.
[(Transformation x, Z)] -> Action RdcState [(Transformation x, Z)]
rdcTrafos [(Transformation x, Z)]
fs forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall (m :: * -> *) a. Monad m => a -> m a
return forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. forall r a. [(a, r)] -> Word r a
Word where
  rdcTrafos :: [(Transformation x, Z)] -> Action RdcState [(Transformation x, Z)]
rdcTrafos [(Transformation x, Z)]
fs = case [(Transformation x, Z)]
fs of
    (Transformation x
_,Z
0):[(Transformation x, Z)]
fs' -> forall x. x -> Rdc x
reducesTo [(Transformation x, Z)]
fs' forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= [(Transformation x, Z)] -> Action RdcState [(Transformation x, Z)]
rdcTrafos
  
    (Transformation x
f,Z
z):[(Transformation x, Z)]
fs' | Z
z forall a. Eq a => a -> a -> Bool
/= Z
1 -> do
      [(Transformation x, Z)]
fs'' <- [(Transformation x, Z)] -> Action RdcState [(Transformation x, Z)]
rdcTrafos [(Transformation x, Z)]
fs'
      Transformation x
f'   <- forall x. Transformation x -> Z -> Rdc (Transformation x)
rdcPower Transformation x
f Z
z
      [(Transformation x, Z)] -> Action RdcState [(Transformation x, Z)]
rdcTrafos ((Transformation x
f',Z
1)forall a. a -> [a] -> [a]
:[(Transformation x, Z)]
fs'')

    (Permute Dim x (Point x)
_ Dim x (Point x)
_ Permutation N
p,Z
_):[(Transformation x, Z)]
fs' | Permutation N
p forall a. Eq a => a -> a -> Bool
== forall c. Multiplicative c => Point c -> c
one () -> forall x. x -> Rdc x
reducesTo [(Transformation x, Z)]
fs' forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= [(Transformation x, Z)] -> Action RdcState [(Transformation x, Z)]
rdcTrafos
    (Permute Dim x (Point x)
r Dim x (Point x)
_ Permutation N
p,Z
1):(Permute Dim x (Point x)
_ Dim x (Point x)
c Permutation N
q,Z
1):[(Transformation x, Z)]
fs'
      -> forall x. x -> Rdc x
reducesTo (forall x.
Distributive x =>
Dim x (Point x)
-> Dim x (Point x) -> Permutation N -> Transformation x
Permute Dim x (Point x)
r Dim x (Point x)
c (Permutation N
q forall c. Multiplicative c => c -> c -> c
* Permutation N
p))
         forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \Transformation x
f -> [(Transformation x, Z)] -> Action RdcState [(Transformation x, Z)]
rdcTrafos ((Transformation x
f,Z
1)forall a. a -> [a] -> [a]
:[(Transformation x, Z)]
fs')
  
    (Scale Dim x (Point x)
d N
k Inv x
s,Z
_):[(Transformation x, Z)]
fs' | Inv x
s forall a. Eq a => a -> a -> Bool
== forall c. Multiplicative c => Point c -> c
one (Dim x (Point x)
dforall (s :: * -> *) i x. Sequence s i x => s x -> i -> x
?N
k) -> forall x. x -> Rdc x
reducesTo [(Transformation x, Z)]
fs' forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= [(Transformation x, Z)] -> Action RdcState [(Transformation x, Z)]
rdcTrafos
    (Scale Dim x (Point x)
d N
k Inv x
s,Z
1):(Scale Dim x (Point x)
_ N
k' Inv x
t,Z
1):[(Transformation x, Z)]
fs' | N
k forall a. Eq a => a -> a -> Bool
== N
k'
      -> forall x. x -> Rdc x
reducesTo (forall x.
Distributive x =>
Dim x (Point x) -> N -> Inv x -> Transformation x
Scale Dim x (Point x)
d N
k (Inv x
s forall c. Multiplicative c => c -> c -> c
* Inv x
t))
         forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \Transformation x
f -> [(Transformation x, Z)] -> Action RdcState [(Transformation x, Z)]
rdcTrafos ((Transformation x
f,Z
1)forall a. a -> [a] -> [a]
:[(Transformation x, Z)]
fs')

    (Shear Dim x (Point x)
_ N
_ N
_ GL2 x
g,Z
_):[(Transformation x, Z)]
fs' | forall c. Multiplicative c => c -> Bool
isOne GL2 x
g -> forall x. x -> Rdc x
reducesTo [(Transformation x, Z)]
fs' forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= [(Transformation x, Z)] -> Action RdcState [(Transformation x, Z)]
rdcTrafos
    (Shear Dim x (Point x)
d N
k N
l GL2 x
g,Z
1):(Shear Dim x (Point x)
_ N
k' N
l' GL2 x
h,Z
1):[(Transformation x, Z)]
fs' | (N
k,N
l) forall a. Eq a => a -> a -> Bool
== (N
k',N
l')
      -> forall x. x -> Rdc x
reducesTo (forall x.
Galoisian x =>
Dim x (Point x) -> N -> N -> GL2 x -> Transformation x
Shear Dim x (Point x)
d N
k N
l (GL2 x
g forall c. Multiplicative c => c -> c -> c
* GL2 x
h))
         forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \Transformation x
f -> [(Transformation x, Z)] -> Action RdcState [(Transformation x, Z)]
rdcTrafos ((Transformation x
f,Z
1)forall a. a -> [a] -> [a]
:[(Transformation x, Z)]
fs')

    (Scale Dim x (Point x)
_ N
k' Inv x
r,Z
1):(Shear Dim x (Point x)
d N
k N
l GL2 x
g,Z
1):[(Transformation x, Z)]
fs'
      | N
k' forall a. Eq a => a -> a -> Bool
== N
k -> forall x. x -> Rdc x
reducesTo (forall x.
Galoisian x =>
Dim x (Point x) -> N -> N -> GL2 x -> Transformation x
Shear Dim x (Point x)
d N
k N
l forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall x. Galoisian x => Inv x -> GL2 x -> GL2 x
gl2ScaleRow1 Inv x
r GL2 x
g)
                   forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \Transformation x
f -> [(Transformation x, Z)] -> Action RdcState [(Transformation x, Z)]
rdcTrafos ((Transformation x
f,Z
1)forall a. a -> [a] -> [a]
:[(Transformation x, Z)]
fs')
      | N
k' forall a. Eq a => a -> a -> Bool
== N
l -> forall x. x -> Rdc x
reducesTo (forall x.
Galoisian x =>
Dim x (Point x) -> N -> N -> GL2 x -> Transformation x
Shear Dim x (Point x)
d N
k N
l forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall x. Galoisian x => Inv x -> GL2 x -> GL2 x
gl2ScaleRow2 Inv x
r GL2 x
g)
                   forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \Transformation x
f -> [(Transformation x, Z)] -> Action RdcState [(Transformation x, Z)]
rdcTrafos ((Transformation x
f,Z
1)forall a. a -> [a] -> [a]
:[(Transformation x, Z)]
fs')

    (Shear Dim x (Point x)
d N
k N
l GL2 x
g,Z
1):(Scale Dim x (Point x)
_ N
k' Inv x
r,Z
1):[(Transformation x, Z)]
fs'
      | N
k forall a. Eq a => a -> a -> Bool
== N
k' -> forall x. x -> Rdc x
reducesTo (forall x.
Galoisian x =>
Dim x (Point x) -> N -> N -> GL2 x -> Transformation x
Shear Dim x (Point x)
d N
k N
l forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall x. Galoisian x => GL2 x -> Inv x -> GL2 x
gl2ScaleCol1 GL2 x
g Inv x
r)
                   forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \Transformation x
f -> [(Transformation x, Z)] -> Action RdcState [(Transformation x, Z)]
rdcTrafos ((Transformation x
f,Z
1)forall a. a -> [a] -> [a]
:[(Transformation x, Z)]
fs')
      | N
l forall a. Eq a => a -> a -> Bool
== N
k' -> forall x. x -> Rdc x
reducesTo (forall x.
Galoisian x =>
Dim x (Point x) -> N -> N -> GL2 x -> Transformation x
Shear Dim x (Point x)
d N
k N
l forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall x. Galoisian x => GL2 x -> Inv x -> GL2 x
gl2ScaleCol2 GL2 x
g Inv x
r)
                   forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \Transformation x
f -> [(Transformation x, Z)] -> Action RdcState [(Transformation x, Z)]
rdcTrafos ((Transformation x
f,Z
1)forall a. a -> [a] -> [a]
:[(Transformation x, Z)]
fs')

    (Transformation x, Z)
fz:[(Transformation x, Z)]
fs' -> [(Transformation x, Z)] -> Action RdcState [(Transformation x, Z)]
rdcTrafos [(Transformation x, Z)]
fs' forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall (m :: * -> *) a. Monad m => a -> m a
return forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. ((Transformation x, Z)
fzforall a. a -> [a] -> [a]
:)
       
    [(Transformation x, Z)]
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return [(Transformation x, Z)]
fs

--------------------------------------------------------------------------------
-- trTrsp -

-- | transposition of a elementary transformation.
trTrsp :: TransposableDistributive r => Transformation r -> Transformation r
trTrsp :: forall r.
TransposableDistributive r =>
Transformation r -> Transformation r
trTrsp Transformation r
tr = case Transformation r
tr of
  Permute Dim r (Point r)
r Dim r (Point r)
c Permutation N
p       -> forall x.
Distributive x =>
Dim x (Point x)
-> Dim x (Point x) -> Permutation N -> Transformation x
Permute Dim r (Point r)
c Dim r (Point r)
r (forall c. Invertible c => c -> c
invert Permutation N
p)
  Scale Dim r (Point r)
d N
k Inv r
s         -> forall x.
Distributive x =>
Dim x (Point x) -> N -> Inv x -> Transformation x
Scale Dim r (Point r)
d N
k (forall x. Transposable x => x -> x
transpose Inv r
s)
  Shear Dim r (Point r)
d N
k N
l GL2 r
g       -> forall x.
Galoisian x =>
Dim x (Point x) -> N -> N -> GL2 x -> Transformation x
Shear Dim r (Point r)
d N
k N
l (forall x. Transposable x => x -> x
transpose GL2 r
g)

--------------------------------------------------------------------------------
-- GLTForm -

-- | form of 'GLT'.
type GLTForm x = ProductForm Z (Transformation x)

--------------------------------------------------------------------------------
-- rdcGLTForm -

-- | reduces a @'GLTForm' __x__@ to its normal form.
--
--  __Property__ Let @f@ be in @'GLTForm' __x__@ for a 'Oriented' structure @__x__@,
--  then holds:
--
--  (1) @'rdcGLTForm' ('rdcGLTForm' f) '==' 'rdcGLTForm' f@.
--
--  (2) For all exponents @z@ in @'rdcGLTForm' f@ holds: @0 '<' z@.
rdcGLTForm :: Oriented x => GLTForm x -> GLTForm x
rdcGLTForm :: forall x. Oriented x => GLTForm x -> GLTForm x
rdcGLTForm = forall a r.
(Oriented a, Integral r) =>
(Word r a -> Rdc (Word r a)) -> ProductForm r a -> ProductForm r a
prfReduceWith forall x.
Word Z (Transformation x) -> Rdc (Word Z (Transformation x))
rdcTransformations

--------------------------------------------------------------------------------
-- FT -

-- | the free groupoid of 'Transformation's.
type FT x = Product Z (Transformation x)

--------------------------------------------------------------------------------
-- GLT -

-- | quotient groupoid of the free groupoid of 'Transformation' (see 'FTGLT') given by the
-- relations:
--
-- * @'permuteFT' d c p '*' 'permuteFT' b a q ~ 'permuteFT' d a (q'*'p)@ where @b '==' c@
-- and @'Permute' d c p@, @'Permute' b a q@ are 'valid' (Note: the permutations @p@ and
-- @q@ are switched on the right side of the equation).
--
-- * ...
--
-- __Property__ Let @g@ be in 'GLT', then holds:
--
-- (1) For all exponents @z@ in @'form' g@ holds: @0 '<' z@.
--
-- __Example__ Let @d = 'dim' [()] '^' 10 :: t'Dim'' t'Z'@,
-- @a = 'permuteFT' d d ('swap' 2 8)@, @b = 'permuteFT' d d ('swap' 2 3)@ and
-- @c = 'permuteFT' d d ('swap' 2 3 * 'swap' 2 8)@ then:
--
-- >>> a * b == c
-- False
--
-- but in 'GLT' holds: let @a' = 'amap' 'FTGLT' a@, @b' = 'amap' 'FTGLT' b@ and
-- @c' = 'amap' 'FTGLT' c@ in
--
-- >>> a' * b' == c'
-- True
--
-- and 
--
-- >>> amap GLTGL (a' * b') == amap GLTGL a' * amap GLTGL b'
-- True
--
-- __Note__: As a consequence of the property (1.), 'GLT' can be canonically embedded
-- via @'prj' '.' 'form'@ - in to @'ProductForm' 'N' ('Transformation' x)@. 
newtype GLT x = GLT (GLTForm x) deriving (GLT x -> GLT x -> Bool
forall x. Oriented x => GLT x -> GLT x -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: GLT x -> GLT x -> Bool
$c/= :: forall x. Oriented x => GLT x -> GLT x -> Bool
== :: GLT x -> GLT x -> Bool
$c== :: forall x. Oriented x => GLT x -> GLT x -> Bool
Eq,Int -> GLT x -> ShowS
forall x. Oriented x => Int -> GLT x -> ShowS
forall x. Oriented x => [GLT x] -> ShowS
forall x. Oriented x => GLT x -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [GLT x] -> ShowS
$cshowList :: forall x. Oriented x => [GLT x] -> ShowS
show :: GLT x -> String
$cshow :: forall x. Oriented x => GLT x -> String
showsPrec :: Int -> GLT x -> ShowS
$cshowsPrec :: forall x. Oriented x => Int -> GLT x -> ShowS
Show,GLT x -> Statement
forall x. Oriented x => GLT x -> Statement
forall a. (a -> Statement) -> Validable a
valid :: GLT x -> Statement
$cvalid :: forall x. Oriented x => GLT x -> Statement
Validable,forall a. Show a -> Eq a -> Validable a -> Typeable a -> Entity a
forall x. Oriented x => Eq (GLT x)
forall x. Oriented x => Show (GLT x)
forall {x}. Oriented x => Typeable (GLT x)
forall x. Oriented x => Validable (GLT x)
Entity)

--------------------------------------------------------------------------------
-- GLT - Constructable -

instance Exposable (GLT x) where
  type Form (GLT x) = GLTForm x
  form :: GLT x -> Form (GLT x)
form (GLT GLTForm x
f) = GLTForm x
f
  
instance Oriented x => Constructable (GLT x) where
  make :: Form (GLT x) -> GLT x
make = forall x. GLTForm x -> GLT x
GLT forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. forall x. Oriented x => GLTForm x -> GLTForm x
rdcGLTForm

instance Embeddable (GLT x) (ProductForm N (Transformation x)) where
  inj :: GLT x -> ProductForm N (Transformation x)
inj = forall a b. Projectible a b => b -> a
prj forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. forall x. Exposable x => x -> Form x
form
  
--------------------------------------------------------------------------------
-- trGLT -

-- | the induced element of the groupoid 'GLT'.
trGLT :: Oriented x => Transformation x -> GLT x
trGLT :: forall x. Oriented x => Transformation x -> GLT x
trGLT = forall x. Constructable x => Form x -> x
make forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. forall r a. a -> ProductForm r a
P

--------------------------------------------------------------------------------
-- GLT - Multiplictive -

instance Oriented x => Oriented (GLT x) where
  type Point (GLT x) = Dim x (Point x)
  orientation :: GLT x -> Orientation (Point (GLT x))
orientation = forall x y. Exposable x => (Form x -> y) -> x -> y
restrict forall q. Oriented q => q -> Orientation (Point q)
orientation

instance Oriented x => Multiplicative (GLT x) where
  one :: Point (GLT x) -> GLT x
one Point (GLT x)
d = forall x. GLTForm x -> GLT x
GLT (forall r a. Point a -> ProductForm r a
One Point (GLT x)
d)
  GLT GLTForm x
f * :: GLT x -> GLT x -> GLT x
* GLT GLTForm x
g | forall q. Oriented q => q -> Point q
start GLTForm x
f forall a. Eq a => a -> a -> Bool
== forall q. Oriented q => q -> Point q
end GLTForm x
g = forall x. Constructable x => Form x -> x
make (GLTForm x
fforall r a. ProductForm r a -> ProductForm r a -> ProductForm r a
:*GLTForm x
g)
                | Bool
otherwise = forall a e. Exception e => e -> a
throw ArithmeticException
NotMultiplicable

--------------------------------------------------------------------------------
-- gltfTrsp -

-- | transposition of a product of elementary transformation.
gltfTrsp :: TransposableDistributive r => GLTForm r -> GLTForm r
gltfTrsp :: forall r. TransposableDistributive r => GLTForm r -> GLTForm r
gltfTrsp (One Point (Transformation r)
d)  = forall r a. Point a -> ProductForm r a
One Point (Transformation r)
d
gltfTrsp (P Transformation r
tr)   = forall r a. a -> ProductForm r a
P (forall r.
TransposableDistributive r =>
Transformation r -> Transformation r
trTrsp Transformation r
tr)
gltfTrsp (ProductForm Z (Transformation r)
a :^ Z
n) = forall r. TransposableDistributive r => GLTForm r -> GLTForm r
gltfTrsp ProductForm Z (Transformation r)
a forall r a. ProductForm r a -> r -> ProductForm r a
:^ Z
n
gltfTrsp (ProductForm Z (Transformation r)
a :* ProductForm Z (Transformation r)
b) = forall r. TransposableDistributive r => GLTForm r -> GLTForm r
gltfTrsp ProductForm Z (Transformation r)
b forall r a. ProductForm r a -> ProductForm r a -> ProductForm r a
:* forall r. TransposableDistributive r => GLTForm r -> GLTForm r
gltfTrsp ProductForm Z (Transformation r)
a

--------------------------------------------------------------------------------
-- gltfInverse -

-- | inverse of a product of elementary transformation.
gltfInverse :: GLTForm x -> GLTForm x
gltfInverse :: forall x. GLTForm x -> GLTForm x
gltfInverse o :: GLTForm x
o@(One Point (Transformation x)
_) = GLTForm x
o
gltfInverse (P Transformation x
t)     = forall r a. a -> ProductForm r a
P (forall x. Transformation x -> Transformation x
trInverse Transformation x
t)
gltfInverse (GLTForm x
a :^ Z
n)  = forall x. GLTForm x -> GLTForm x
gltfInverse GLTForm x
a forall r a. ProductForm r a -> r -> ProductForm r a
:^ Z
n
gltfInverse (GLTForm x
a :* GLTForm x
b)  = forall x. GLTForm x -> GLTForm x
gltfInverse GLTForm x
b forall r a. ProductForm r a -> ProductForm r a -> ProductForm r a
:* forall x. GLTForm x -> GLTForm x
gltfInverse GLTForm x
a

--------------------------------------------------------------------------------
-- GLT - Cayleyan -

instance Oriented x => Invertible (GLT x) where
  tryToInvert :: GLT x -> Solver (GLT x)
tryToInvert (GLT GLTForm x
f) = forall (m :: * -> *) a. Monad m => a -> m a
return forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall x. Constructable x => Form x -> x
make (forall x. GLTForm x -> GLTForm x
gltfInverse GLTForm x
f)

instance Oriented x => Exponential (GLT x) where
  type Exponent (GLT x) = Z
  ^ :: GLT x -> Exponent (GLT x) -> GLT x
(^) = forall c. Invertible c => c -> Z -> c
zpower

instance Oriented x => Cayleyan (GLT x)

--------------------------------------------------------------------------------
-- TrApp -

-- | 'Oriented' homomorphisms.
data TrApp x y where
  TrFT  :: Oriented x => TrApp (Transformation x) (FT x)
  TrGL  :: Distributive x => TrApp (Transformation x) (GL x)
  TrGLT :: Oriented x => TrApp (Transformation x) (GLT x) 

--------------------------------------------------------------------------------
-- TrApp - Entity -

deriving instance Show (TrApp x y)
instance Show2 TrApp

deriving instance Eq (TrApp x y)
instance Eq2 TrApp

instance Validable (TrApp x y) where
  valid :: TrApp x y -> Statement
valid TrApp x y
TrFT  = Statement
SValid
  valid TrApp x y
TrGL  = Statement
SValid
  valid TrApp x y
TrGLT = Statement
SValid
  
instance Validable2 TrApp

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

--------------------------------------------------------------------------------
-- TrApp - HomOriented -

instance Morphism TrApp where
  type ObjectClass TrApp = Ort
  homomorphous :: forall x y. TrApp x y -> Homomorphous (ObjectClass TrApp) x y
homomorphous TrApp x y
TrFT  = forall s x. Structure s x => Struct s x
Struct forall s x y. Struct s x -> Struct s y -> Homomorphous s x y
:>: forall s x. Structure s x => Struct s x
Struct
  homomorphous TrApp x y
TrGL  = forall s x. Structure s x => Struct s x
Struct forall s x y. Struct s x -> Struct s y -> Homomorphous s x y
:>: forall s x. Structure s x => Struct s x
Struct
  homomorphous TrApp x y
TrGLT = forall s x. Structure s x => Struct s x
Struct forall s x y. Struct s x -> Struct s y -> Homomorphous s x y
:>: forall s x. Structure s x => Struct s x
Struct

instance EmbeddableMorphism TrApp Ort
instance EmbeddableMorphism TrApp Typ
instance EmbeddableMorphismTyp TrApp

instance Applicative TrApp where
  amap :: forall a b. TrApp a b -> a -> b
amap TrApp a b
TrFT  = forall x. Constructable x => Form x -> x
make forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. forall r a. a -> ProductForm r a
P
  amap TrApp a b
TrGL  = forall x. Transformation x -> GL x
trGL
  amap TrApp a b
TrGLT = forall x. Oriented x => Transformation x -> GLT x
trGLT

instance HomOriented TrApp where
  pmap :: forall a b. TrApp a b -> Point a -> Point b
pmap TrApp a b
TrFT  = forall x. x -> x
id
  pmap TrApp a b
TrGL  = forall x. x -> x
id
  pmap TrApp a b
TrGLT = forall x. x -> x
id

--------------------------------------------------------------------------------
-- GLApp -

-- | 'Multiplicative' homomorphisms.
data GLApp x y where
  FTGL  :: Distributive x => GLApp (FT x) (GL x)
  FTGLT :: Oriented x => GLApp (FT x) (GLT x)
  GLTGL :: Distributive x => GLApp (GLT x) (GL x)
  GL2GL :: Galoisian x => GLApp (GL2 x) (GL x)

deriving instance Show (GLApp x y)
instance Show2 GLApp

deriving instance Eq (GLApp x y)
instance Eq2 GLApp

instance Validable (GLApp x y) where
  valid :: GLApp x y -> Statement
valid GLApp x y
FTGL  = Statement
SValid
  valid GLApp x y
FTGLT = Statement
SValid
  valid GLApp x y
GLTGL = Statement
SValid
  valid GLApp x y
GL2GL = Statement
SValid
  
instance Validable2 GLApp

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

--------------------------------------------------------------------------------
-- GLApp - HomMultiplicative -

instance Morphism GLApp where
  type ObjectClass GLApp = Mlt
  homomorphous :: forall x y. GLApp x y -> Homomorphous (ObjectClass GLApp) x y
homomorphous GLApp x y
FTGL = forall s x. Structure s x => Struct s x
Struct forall s x y. Struct s x -> Struct s y -> Homomorphous s x y
:>: forall s x. Structure s x => Struct s x
Struct
  homomorphous GLApp x y
FTGLT = forall s x. Structure s x => Struct s x
Struct forall s x y. Struct s x -> Struct s y -> Homomorphous s x y
:>: forall s x. Structure s x => Struct s x
Struct
  homomorphous GLApp x y
GLTGL = forall s x. Structure s x => Struct s x
Struct forall s x y. Struct s x -> Struct s y -> Homomorphous s x y
:>: forall s x. Structure s x => Struct s x
Struct
  homomorphous GLApp x y
GL2GL = forall s x. Structure s x => Struct s x
Struct forall s x y. Struct s x -> Struct s y -> Homomorphous s x y
:>: forall s x. Structure s x => Struct s x
Struct

instance EmbeddableMorphism GLApp Ort
instance EmbeddableMorphism GLApp Typ
instance EmbeddableMorphismTyp GLApp

instance Applicative GLApp where
  amap :: forall a b. GLApp a b -> a -> b
amap GLApp a b
FTGL  = forall (h :: * -> * -> *) x a.
(Hom Ort h, Cayleyan x) =>
h a x -> Product Z a -> x
zProduct forall x. Distributive x => TrApp (Transformation x) (GL x)
TrGL
  amap GLApp a b
FTGLT = forall (h :: * -> * -> *) x a.
(Hom Ort h, Cayleyan x) =>
h a x -> Product Z a -> x
zProduct forall x. Oriented x => TrApp (Transformation x) (GLT x)
TrGLT 
  amap GLApp a b
GLTGL = forall (h :: * -> * -> *) x a.
(Hom Ort h, Cayleyan x) =>
h a x -> ProductForm Z a -> x
zProductForm forall x. Distributive x => TrApp (Transformation x) (GL x)
TrGL forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. forall x. Exposable x => x -> Form x
form
  amap GLApp a b
GL2GL = forall x. Galoisian x => GL2 x -> GL x
gl2GL
  
instance HomOriented GLApp where
  pmap :: forall a b. GLApp a b -> Point a -> Point b
pmap GLApp a b
FTGL  = forall x. x -> x
id
  pmap GLApp a b
FTGLT = forall x. x -> x
id
  pmap GLApp a b
GLTGL = forall x. x -> x
id
  pmap GLApp a b
GL2GL = \Point a
p -> forall p x. (Entity p, p ~ Point x) => [p] -> Dim x p
productDim [Point a
p,Point a
p]

instance EmbeddableMorphism GLApp Mlt
instance HomMultiplicative GLApp

--------------------------------------------------------------------------------
-- permute -

-- | permutation of the given dimensions.
--
-- __Property__ Let @r@, @c@ be in @'Dim'' __x__@ and @p@ in @'Permutation' 'N'@ for
-- a 'Distributive' structure @__x__@, then holds:
-- If @'Permute' r c p@ is 'valid' then @'permute' r c p@ is 'valid'.
--
-- __Example__ Let @t = 'permute' r c p@ with @'Permute' r c p@ is 'valid' then its
-- associated matrix (see 'GLTGL') has the orientation @c ':>' r@ and the form
--
-- @
--
--            k         l
--   [1                          ]
--   [  .                        ]
--   [    .                      ]
--   [     1                     ]
--   [                 1         ] k
--   [         1                 ]
--   [           .               ]
--   [             .             ]
--   [               1           ]
--   [       1                   ] l
--   [                    1      ]
--   [                      .    ]
--   [                        .  ]
--   [                          1]
--
-- @
--
-- __Note__ @r@ dose not have to be equal to @c@, but from @r '==' c '<*' p@ follows that
-- both have the same length.
permute :: Distributive x => Dim' x -> Dim' x -> Permutation N -> GLT x
permute :: forall x.
Distributive x =>
Dim' x -> Dim' x -> Permutation N -> GLT x
permute Dim' x
r Dim' x
c Permutation N
p = forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
amap forall x. Oriented x => TrApp (Transformation x) (GLT x)
TrGLT (forall x.
Distributive x =>
Dim x (Point x)
-> Dim x (Point x) -> Permutation N -> Transformation x
Permute Dim' x
r Dim' x
c Permutation N
p)

--------------------------------------------------------------------------------
-- permutFT -

-- | the induce element in the free groupoid of transformations.
permuteFT :: Distributive x
  => Dim' x -> Dim' x -> Permutation N -> FT x
permuteFT :: forall x.
Distributive x =>
Dim' x -> Dim' x -> Permutation N -> FT x
permuteFT Dim' x
r Dim' x
c Permutation N
p = forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
amap forall x. Oriented x => TrApp (Transformation x) (FT x)
TrFT (forall x.
Distributive x =>
Dim x (Point x)
-> Dim x (Point x) -> Permutation N -> Transformation x
Permute Dim' x
r Dim' x
c Permutation N
p)

--------------------------------------------------------------------------------
-- scale -

-- | scaling.
--
-- __Property__ Let @d@ be in @'Dim'' __x__@, @k@ in 'N' and @s@ in @'Inv' __x__@, then
-- holds: If @'Scale' d k s@ is 'valid' then @'scale' d k s@ is 'valid'.
--
-- __Example__ Let @t = 'scale' d k s@ with @'Scale' d k s@ is 'valid' then its associated
-- matrix (see 'GLTGL') is an endo with dimension @d@ and has the form 
--
-- @
--
--           k         
--   [1               ]
--   [  .             ]
--   [    .           ]
--   [     1          ]
--   [      s'        ] k
--   [         1      ]
--   [           .    ]
--   [             .  ]
--   [               1]
--
-- @
-- where @s' = ('inj' :: 'Inv' __x__ -> __x__) s@.
scale :: Distributive x => Dim' x -> N -> Inv x -> GLT x
scale :: forall x. Distributive x => Dim' x -> N -> Inv x -> GLT x
scale Dim' x
d N
k Inv x
s = forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
amap forall x. Oriented x => TrApp (Transformation x) (GLT x)
TrGLT (forall x.
Distributive x =>
Dim x (Point x) -> N -> Inv x -> Transformation x
Scale Dim' x
d N
k Inv x
s)

--------------------------------------------------------------------------------
-- shear -

-- | shearing.
--
--  __Property__ Let @d@ be in @'Dim'' __x__@, @k@, @l@ in 'N' and @g@ in @'GL2' __x__@
-- then holds: If @'Shear' d k l g@ is 'valid' then @'shear' d k l g@ is 'valid'.
--
--  __Example__ Let @t = 'shear' d k l g@ where @'Shear' d k l g@ is 'valid' then its
--  associated matrix (see 'GLTGL') is an endo with dimension @d@ and has the form
--
-- @
--
--            k         l
--   [1                          ]
--   [  .                        ]
--   [    .                      ]
--   [     1                     ]
--   [       s         t         ] k
--   [         1                 ]
--   [           .               ]
--   [             .             ]
--   [               1           ]
--   [       u         v         ] l
--   [                    1      ]
--   [                      .    ]
--   [                        .  ]
--   [                          1]
--
-- @
shear :: Galoisian x  => Dim' x -> N -> N -> GL2 x -> GLT x
shear :: forall x. Galoisian x => Dim' x -> N -> N -> GL2 x -> GLT x
shear Dim' x
d N
k N
l GL2 x
g = forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
amap forall x. Oriented x => TrApp (Transformation x) (GLT x)
TrGLT (forall x.
Galoisian x =>
Dim x (Point x) -> N -> N -> GL2 x -> Transformation x
Shear Dim' x
d N
k N
l GL2 x
g)