{-# 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.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
[GL2 x] -> ShowS
GL2 x -> String
(Int -> GL2 x -> ShowS)
-> (GL2 x -> String) -> ([GL2 x] -> ShowS) -> Show (GL2 x)
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
$cshowsPrec :: forall x. Show x => Int -> GL2 x -> ShowS
showsPrec :: Int -> GL2 x -> ShowS
$cshow :: forall x. Show x => GL2 x -> String
show :: GL2 x -> String
$cshowList :: forall x. Show x => [GL2 x] -> ShowS
showList :: [GL2 x] -> ShowS
Show,GL2 x -> GL2 x -> Bool
(GL2 x -> GL2 x -> Bool) -> (GL2 x -> GL2 x -> Bool) -> Eq (GL2 x)
forall x. Eq x => GL2 x -> GL2 x -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$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
/= :: GL2 x -> GL2 x -> Bool
Eq,Eq (GL2 x)
Eq (GL2 x) =>
(GL2 x -> GL2 x -> Ordering)
-> (GL2 x -> GL2 x -> Bool)
-> (GL2 x -> GL2 x -> Bool)
-> (GL2 x -> GL2 x -> Bool)
-> (GL2 x -> GL2 x -> Bool)
-> (GL2 x -> GL2 x -> GL2 x)
-> (GL2 x -> GL2 x -> GL2 x)
-> Ord (GL2 x)
GL2 x -> GL2 x -> Bool
GL2 x -> GL2 x -> Ordering
GL2 x -> GL2 x -> GL2 x
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
$ccompare :: forall x. Ord x => GL2 x -> GL2 x -> Ordering
compare :: GL2 x -> GL2 x -> Ordering
$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
>= :: GL2 x -> GL2 x -> Bool
$cmax :: forall x. Ord x => GL2 x -> GL2 x -> GL2 x
max :: GL2 x -> GL2 x -> GL2 x
$cmin :: forall x. Ord x => GL2 x -> GL2 x -> GL2 x
min :: GL2 x -> GL2 x -> GL2 x
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
sx -> x -> x
forall c. Multiplicative c => c -> c -> c
*x
v x -> x -> x
forall a. Abelian a => a -> a -> a
- x
ux -> x -> x
forall 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 = Matrix x -> Matrix x -> Inv (Matrix x)
forall c. c -> c -> Inv c
Inv (GL2 x -> Matrix x
forall {x}. (Oriented x, Singleton (Point x)) => GL2 x -> Matrix x
gl GL2 x
g) (GL2 x -> Matrix x
forall {x}. (Oriented x, Singleton (Point x)) => GL2 x -> Matrix x
gl (GL2 x -> Matrix x) -> GL2 x -> Matrix x
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ GL2 x -> GL2 x
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) = Dim' x -> Dim' x -> Entries N N x -> Matrix x
forall x. Dim' x -> Dim' x -> Entries N N x -> Matrix x
Matrix Dim' x
d Dim' x
d (PSequence (N, N) x -> Entries N N x
forall i j x. PSequence (i, j) x -> Entries i j x
Entries ([(x, (N, N))] -> PSequence (N, N) x
forall i x. [(x, i)] -> PSequence i x
PSequence [(x, (N, N))]
xs)) where
    d :: Dim' x
d = Point x -> Dim' x
forall p x. (Entity p, p ~ Point x) => p -> Dim x p
dim Point x
forall s. Singleton s => s
unit Dim' x -> Exponent (Dim' x) -> Dim' x
forall f. Exponential f => f -> Exponent f -> f
^ N
Exponent (Dim' x)
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 => Entity (GL2 x)


type instance Point (GL2 x) = Point x

instance ShowPoint x => ShowPoint (GL2 x)
instance EqPoint x => EqPoint (GL2 x)
instance ValidablePoint x => ValidablePoint (GL2 x)
instance TypeablePoint x => TypeablePoint (GL2 x)
instance SingletonPoint x => SingletonPoint (GL2 x)

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

instance Galoisian x => Multiplicative (GL2 x) where
  one :: Point (GL2 x) -> GL2 x
one Point (GL2 x)
p = x -> x -> x -> x -> GL2 x
forall x. x -> x -> x -> x -> GL2 x
GL2 x
o x
z x
z x
o where
    o :: x
o = Point x -> x
forall c. Multiplicative c => Point c -> c
one Point x
Point (GL2 x)
p
    z :: x
z = Root x -> x
forall a. Additive a => Root a -> a
zero (Point x
Point (GL2 x)
pPoint x -> Point x -> Orientation (Point x)
forall p. p -> p -> Orientation p
:>Point x
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' = x -> x -> x -> x -> GL2 x
forall x. x -> x -> x -> x -> GL2 x
GL2 (x
sx -> x -> x
forall c. Multiplicative c => c -> c -> c
*x
s' x -> x -> x
forall a. Additive a => a -> a -> a
+ x
tx -> x -> x
forall c. Multiplicative c => c -> c -> c
*x
u') (x
sx -> x -> x
forall c. Multiplicative c => c -> c -> c
*x
t' x -> x -> x
forall a. Additive a => a -> a -> a
+ x
tx -> x -> x
forall c. Multiplicative c => c -> c -> c
*x
v')
                                      (x
ux -> x -> x
forall c. Multiplicative c => c -> c -> c
*x
s' x -> x -> x
forall a. Additive a => a -> a -> a
+ x
vx -> x -> x
forall c. Multiplicative c => c -> c -> c
*x
u') (x
ux -> x -> x
forall c. Multiplicative c => c -> c -> c
*x
t' x -> x -> x
forall a. Additive a => a -> a -> a
+ x
vx -> x -> x
forall 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 <- x -> Solver x
forall c. Invertible c => c -> Solver c
tryToInvert (GL2 x -> x
forall x. Galoisian x => GL2 x -> x
gl2Det GL2 x
g)
    GL2 x -> Solver (GL2 x)
forall a. a -> Solver a
forall (m :: * -> *) a. Monad m => a -> m a
return (x -> x -> x -> x -> GL2 x
forall x. x -> x -> x -> x -> GL2 x
GL2 (x
rx -> x -> x
forall c. Multiplicative c => c -> c -> c
*x
v) (x -> x
forall a. Abelian a => a -> a
negate (x
rx -> x -> x
forall c. Multiplicative c => c -> c -> c
*x
t)) (x -> x
forall a. Abelian a => a -> a
negate (x
rx -> x -> x
forall c. Multiplicative c => c -> c -> c
*x
u)) (x
rx -> x -> x
forall c. Multiplicative c => c -> c -> c
*x
s))

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

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
(^) = GL2 x -> Z -> GL2 x
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) = x -> x -> x -> x -> GL2 x
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 = x -> x
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) = x -> x -> x -> x -> GL2 x
forall x. x -> x -> x -> x -> GL2 x
GL2 (x
xx -> x -> x
forall c. Multiplicative c => c -> c -> c
*x
s) (x
xx -> x -> x
forall 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) = x -> x -> x -> x -> GL2 x
forall x. x -> x -> x -> x -> GL2 x
GL2 x
s x
t (x
xx -> x -> x
forall c. Multiplicative c => c -> c -> c
*x
u) (x
xx -> x -> x
forall 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
_) = x -> x -> x -> x -> GL2 x
forall x. x -> x -> x -> x -> GL2 x
GL2 (x
sx -> x -> x
forall c. Multiplicative c => c -> c -> c
*x
x) x
t (x
ux -> x -> x
forall 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
_) = x -> x -> x -> x -> GL2 x
forall x. x -> x -> x -> x -> GL2 x
GL2 x
s (x
tx -> x -> x
forall c. Multiplicative c => c -> c -> c
*x
x) x
u (x
vx -> x -> x
forall 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 [ (Dim x (Point x), Dim x (Point x), Permutation N) -> Statement
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 {(Closure N
_,Closure N
h) = Proxy N -> Permutation N -> (Closure N, Closure N)
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 = Dim x (Point x) -> N
forall x. LengthN x => x -> N
lengthN Dim x (Point x)
c} in
            (Closure N
h Closure N -> Closure N -> Bool
forall a. Ord a => a -> a -> Bool
<= N -> Closure N
forall x. x -> Closure x
It N
n) Bool -> Message -> Statement
:?> [Parameter] -> Message
Params[String
"h"String -> String -> Parameter
:=Closure N -> String
forall a. Show a => a -> String
show Closure N
h,String
"n"String -> String -> Parameter
:=N -> String
forall a. Show a => a -> String
show N
n]
        , String -> Label
Label String
"1.2" Label -> Statement -> Statement
:<=>: (Dim x (Point x)
r Dim x (Point x) -> Dim x (Point x) -> Bool
forall a. Eq a => a -> a -> Bool
== 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
p) Bool -> Message -> Statement
:?> [Parameter] -> Message
Params[String
"r"String -> String -> Parameter
:=Dim x (Point x) -> String
forall a. Show a => a -> String
show Dim x (Point x)
r,String
"c"String -> String -> Parameter
:=Dim x (Point x) -> String
forall a. Show a => a -> String
show Dim x (Point x)
c,String
"p"String -> String -> Parameter
:=Permutation N -> String
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 [ (Dim x (Point x), N) -> Statement
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 = Dim x (Point x) -> N
forall x. LengthN x => x -> N
lengthN Dim x (Point x)
d in
            (N
k N -> N -> Bool
forall a. Ord a => a -> a -> Bool
< N
n)Bool -> Message -> Statement
:?>[Parameter] -> Message
Params[String
"d"String -> String -> Parameter
:=Dim x (Point x) -> String
forall a. Show a => a -> String
show Dim x (Point x)
d,String
"lengthN d"String -> String -> Parameter
:=N -> String
forall a. Show a => a -> String
show N
n]
        , String -> Label
Label String
"2.2" Label -> Statement -> Statement
:<=>: Point (Inv x) -> Inv x -> Bool
forall a. Oriented a => Point a -> a -> Bool
isEndoAt (Dim x (Point x)
dDim x (Point x) -> N -> Point x
forall (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
:=Inv x -> String
forall a. Show a => a -> String
show Inv x
s]
        , String -> Label
Label String
"2.3" Label -> Statement -> Statement
:<=>: Inv x -> 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 [ (Dim x (Point x), N, N) -> Statement
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 = Dim x (Point x) -> N
forall x. LengthN x => x -> N
lengthN Dim x (Point x)
d in
            [Statement] -> Statement
And [ (N
k N -> N -> Bool
forall a. Ord a => a -> a -> Bool
< N
n)Bool -> Message -> Statement
:?>[Parameter] -> Message
Params[String
"d"String -> String -> Parameter
:=Dim x (Point x) -> String
forall a. Show a => a -> String
show Dim x (Point x)
d,String
"lengthN d"String -> String -> Parameter
:=N -> String
forall a. Show a => a -> String
show N
n]
                , (N
l N -> N -> Bool
forall a. Ord a => a -> a -> Bool
< N
n)Bool -> Message -> Statement
:?>[Parameter] -> Message
Params[String
"l"String -> String -> Parameter
:=N -> String
forall a. Show a => a -> String
show N
l,String
"lengthN d"String -> String -> Parameter
:=N -> String
forall a. Show a => a -> String
show N
n]
                ]
        , String -> Label
Label String
"3.2"Label -> Statement -> Statement
:<=>: (N
k N -> N -> Bool
forall a. Ord a => a -> a -> Bool
< N
l)Bool -> Message -> Statement
:?>[Parameter] -> Message
Params[String
"(k,l"String -> String -> Parameter
:=(N, N) -> String
forall a. Show a => a -> String
show (N
k,N
l)]
        , String -> Label
Label String
"3.3" Label -> Statement -> Statement
:<=>: GL2 x -> Statement
forall a. Validable a => a -> Statement
valid GL2 x
g
        ]

-- instance Typeable x => Entity (Transformation x)


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

-- Transformation - Oriented -


type instance Point (Transformation x) = Dim x (Point x)
instance Oriented x => ShowPoint (Transformation x)
instance Oriented x => EqPoint (Transformation x)
instance Oriented x => ValidablePoint (Transformation x)
instance Oriented x => TypeablePoint (Transformation x)

instance Oriented x => Oriented (Transformation x) where
  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 Dim x (Point x) -> Dim x (Point x) -> Orientation (Dim x (Point x))
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 Dim x (Point x) -> Dim x (Point x) -> Orientation (Dim x (Point x))
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 Dim x (Point x) -> Dim x (Point x) -> Orientation (Dim x (Point x))
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) = Dim x (Point x) -> Dim x (Point x) -> Entries N N x -> Matrix x
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 = Col N (Row N x) -> Entries N N x
forall i j x. Col i (Row j x) -> Entries i j x
crets ((Matrix x -> Col N (Row N x)
forall x. Matrix x -> Col N (Row N x)
mtxColRow (Matrix x -> Col N (Row N x)) -> Matrix x -> Col N (Row N x)
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ Point (Matrix x) -> Matrix x
forall c. Multiplicative c => Point c -> c
one Point (Matrix x)
Dim x (Point x)
c) Col N (Row N x) -> Permutation N -> Col N (Row N x)
forall f x. Opr f x => x -> f -> x
<* Permutation N
p)

trmtx (Scale Dim x (Point x)
d N
k Inv x
s) = Dim x (Point x) -> Dim x (Point x) -> [(x, N, N)] -> Matrix x
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 ((Inv x -> x
forall a b. Embeddable a b => a -> b
inj Inv x
s,N
k,N
k)(x, N, N) -> [(x, N, N)] -> [(x, N, N)]
forall a. a -> [a] -> [a]
:[(x, N, N)]
os) where
  os :: [(x, N, N)]
os = [(Point x -> x
forall c. Multiplicative c => Point c -> c
one Point x
p,N
i,N
i) | (Point x
p,N
i) <- Dim x (Point x) -> [(Point x, N)]
forall p x. (p ~ Point x) => Dim x p -> [(p, N)]
dimxs Dim x (Point x)
d, N
i N -> N -> Bool
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))= Dim x (Point x) -> Dim x (Point x) -> [(x, N, N)] -> Matrix x
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 [(x, N, N)] -> [(x, N, N)] -> [(x, N, N)]
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 = [(Point x -> x
forall c. Multiplicative c => Point c -> c
one Point x
p,N
i,N
i) | (Point x
p,N
i) <- Dim x (Point x) -> [(Point x, N)]
forall p x. (p ~ Point x) => Dim x p -> [(p, N)]
dimxs Dim x (Point x)
d, N
i N -> N -> Bool
forall a. Eq a => a -> a -> Bool
/= N
k, N
i N -> N -> Bool
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) = Dim x (Point x)
-> Dim x (Point x) -> Permutation N -> Transformation x
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 (Permutation N -> Permutation N
forall c. Invertible c => c -> c
invert Permutation N
p)
trInverse (Scale Dim x (Point x)
d N
k Inv x
s)   = Dim x (Point x) -> N -> Inv x -> Transformation x
forall x.
Distributive x =>
Dim x (Point x) -> N -> Inv x -> Transformation x
Scale Dim x (Point x)
d N
k (Inv x -> Inv x
forall c. Invertible c => c -> c
invert Inv x
s)
trInverse (Shear Dim x (Point x)
d N
k N
l GL2 x
g) = Dim x (Point x) -> N -> N -> GL2 x -> Transformation x
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 -> GL2 x
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 = Matrix x -> Matrix x -> Inv (Matrix x)
forall c. c -> c -> Inv c
Inv (Transformation x -> Matrix x
forall x. Transformation x -> Matrix x
trmtx Transformation x
t) (Transformation x -> Matrix x
forall x. Transformation x -> Matrix x
trmtx (Transformation x -> Matrix x) -> Transformation x -> Matrix x
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ Transformation x -> Transformation x
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         = Transformation x -> Action RdcState (Transformation x)
forall a. a -> Action RdcState a
forall (m :: * -> *) a. Monad m => a -> m a
return Transformation x
f
rdcPower Transformation x
f Z
z | Z
z Z -> Z -> Bool
forall a. Ord a => a -> a -> Bool
< Z
0 = Transformation x -> Z -> Action RdcState (Transformation x)
forall x. Transformation x -> Z -> Rdc (Transformation x)
rdcPower (Transformation x -> Transformation x
forall x. Transformation x -> Transformation x
trInverse Transformation x
f) (Z -> Z
forall r. Number r => r -> r
abs Z
z)
rdcPower Transformation x
f Z
z         = let n :: N
n = Z -> 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 -> Transformation x -> Action RdcState (Transformation x)
forall a. a -> Action RdcState a
reducesTo (Transformation x -> Action RdcState (Transformation x))
-> Transformation x -> Action RdcState (Transformation x)
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ Dim x (Point x)
-> Dim x (Point x) -> Permutation N -> Transformation x
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 -> N -> Permutation N
forall c. Multiplicative c => c -> N -> c
npower Permutation N
p N
n)
  Scale Dim x (Point x)
d N
k Inv x
s   -> Transformation x -> Action RdcState (Transformation x)
forall a. a -> Action RdcState a
reducesTo (Transformation x -> Action RdcState (Transformation x))
-> Transformation x -> Action RdcState (Transformation x)
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ Dim x (Point x) -> N -> Inv x -> Transformation x
forall x.
Distributive x =>
Dim x (Point x) -> N -> Inv x -> Transformation x
Scale Dim x (Point x)
d N
k (Inv x -> N -> Inv x
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 -> Transformation x -> Action RdcState (Transformation x)
forall a. a -> Action RdcState a
reducesTo (Transformation x -> Action RdcState (Transformation x))
-> Transformation x -> Action RdcState (Transformation x)
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ Dim x (Point x) -> N -> N -> GL2 x -> Transformation x
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 -> N -> GL2 x
forall c. Multiplicative c => c -> N -> c
npower GL2 x
g N
n)

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

-- rdcTransformations -


-- | reducing transformations.

rdcTransformations :: Eq x => Word Z (Transformation x) -> Rdc (Word Z (Transformation x))
rdcTransformations :: forall x.
Eq x =>
Word Z (Transformation x) -> Rdc (Word Z (Transformation x))
rdcTransformations (Word [(Transformation x, Z)]
fs) = [(Transformation x, Z)] -> Action RdcState [(Transformation x, Z)]
forall {x}.
Eq x =>
[(Transformation x, Z)] -> Action RdcState [(Transformation x, Z)]
rdcTrafos [(Transformation x, Z)]
fs Action RdcState [(Transformation x, Z)]
-> ([(Transformation x, Z)]
    -> Action RdcState (Word Z (Transformation x)))
-> Action RdcState (Word Z (Transformation x))
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
>>= Word Z (Transformation x)
-> Action RdcState (Word Z (Transformation x))
forall a. a -> Action RdcState a
forall (m :: * -> *) a. Monad m => a -> m a
return (Word Z (Transformation x)
 -> Action RdcState (Word Z (Transformation x)))
-> ([(Transformation x, Z)] -> Word Z (Transformation x))
-> [(Transformation x, Z)]
-> Action RdcState (Word Z (Transformation x))
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
. [(Transformation x, Z)] -> Word Z (Transformation x)
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' -> [(Transformation x, Z)] -> Action RdcState [(Transformation x, Z)]
forall a. a -> Action RdcState a
reducesTo [(Transformation x, Z)]
fs' Action RdcState [(Transformation x, Z)]
-> ([(Transformation x, Z)]
    -> Action RdcState [(Transformation x, Z)])
-> Action RdcState [(Transformation x, Z)]
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
>>= [(Transformation x, Z)] -> Action RdcState [(Transformation x, Z)]
rdcTrafos
  
    (Transformation x
f,Z
z):[(Transformation x, Z)]
fs' | Z
z Z -> Z -> Bool
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'   <- Transformation x -> Z -> Rdc (Transformation x)
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)(Transformation x, Z)
-> [(Transformation x, Z)] -> [(Transformation x, Z)]
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 Permutation N -> Permutation N -> Bool
forall a. Eq a => a -> a -> Bool
== Point (Permutation N) -> Permutation N
forall c. Multiplicative c => Point c -> c
one () -> [(Transformation x, Z)] -> Action RdcState [(Transformation x, Z)]
forall a. a -> Action RdcState a
reducesTo [(Transformation x, Z)]
fs' Action RdcState [(Transformation x, Z)]
-> ([(Transformation x, Z)]
    -> Action RdcState [(Transformation x, Z)])
-> Action RdcState [(Transformation x, Z)]
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
>>= [(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'
      -> Transformation x -> Rdc (Transformation x)
forall a. a -> Action RdcState a
reducesTo (Dim x (Point x)
-> Dim x (Point x) -> Permutation N -> Transformation x
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 Permutation N -> Permutation N -> Permutation N
forall c. Multiplicative c => c -> c -> c
* Permutation N
p))
         Rdc (Transformation x)
-> (Transformation x -> Action RdcState [(Transformation x, Z)])
-> Action RdcState [(Transformation x, Z)]
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
>>= \Transformation x
f -> [(Transformation x, Z)] -> Action RdcState [(Transformation x, Z)]
rdcTrafos ((Transformation x
f,Z
1)(Transformation x, Z)
-> [(Transformation x, Z)] -> [(Transformation x, Z)]
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 Inv x -> Inv x -> Bool
forall a. Eq a => a -> a -> Bool
== Point (Inv x) -> Inv x
forall c. Multiplicative c => Point c -> c
one (Dim x (Point x)
dDim x (Point x) -> N -> Point x
forall (s :: * -> *) i x. Sequence s i x => s x -> i -> x
?N
k) -> [(Transformation x, Z)] -> Action RdcState [(Transformation x, Z)]
forall a. a -> Action RdcState a
reducesTo [(Transformation x, Z)]
fs' Action RdcState [(Transformation x, Z)]
-> ([(Transformation x, Z)]
    -> Action RdcState [(Transformation x, Z)])
-> Action RdcState [(Transformation x, Z)]
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
>>= [(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 N -> N -> Bool
forall a. Eq a => a -> a -> Bool
== N
k'
      -> Transformation x -> Rdc (Transformation x)
forall a. a -> Action RdcState a
reducesTo (Dim x (Point x) -> N -> Inv x -> Transformation x
forall x.
Distributive x =>
Dim x (Point x) -> N -> Inv x -> Transformation x
Scale Dim x (Point x)
d N
k (Inv x
s Inv x -> Inv x -> Inv x
forall c. Multiplicative c => c -> c -> c
* Inv x
t))
         Rdc (Transformation x)
-> (Transformation x -> Action RdcState [(Transformation x, Z)])
-> Action RdcState [(Transformation x, Z)]
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
>>= \Transformation x
f -> [(Transformation x, Z)] -> Action RdcState [(Transformation x, Z)]
rdcTrafos ((Transformation x
f,Z
1)(Transformation x, Z)
-> [(Transformation x, Z)] -> [(Transformation x, Z)]
forall a. a -> [a] -> [a]
:[(Transformation x, Z)]
fs')

    (Shear Dim x (Point x)
_ N
_ N
_ GL2 x
g,Z
_):[(Transformation x, Z)]
fs' | GL2 x -> Bool
forall c. Multiplicative c => c -> Bool
isOne GL2 x
g -> [(Transformation x, Z)] -> Action RdcState [(Transformation x, Z)]
forall a. a -> Action RdcState a
reducesTo [(Transformation x, Z)]
fs' Action RdcState [(Transformation x, Z)]
-> ([(Transformation x, Z)]
    -> Action RdcState [(Transformation x, Z)])
-> Action RdcState [(Transformation x, Z)]
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
>>= [(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) (N, N) -> (N, N) -> Bool
forall a. Eq a => a -> a -> Bool
== (N
k',N
l')
      -> Transformation x -> Rdc (Transformation x)
forall a. a -> Action RdcState a
reducesTo (Dim x (Point x) -> N -> N -> GL2 x -> Transformation x
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 GL2 x -> GL2 x -> GL2 x
forall c. Multiplicative c => c -> c -> c
* GL2 x
h))
         Rdc (Transformation x)
-> (Transformation x -> Action RdcState [(Transformation x, Z)])
-> Action RdcState [(Transformation x, Z)]
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
>>= \Transformation x
f -> [(Transformation x, Z)] -> Action RdcState [(Transformation x, Z)]
rdcTrafos ((Transformation x
f,Z
1)(Transformation x, Z)
-> [(Transformation x, Z)] -> [(Transformation x, Z)]
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' N -> N -> Bool
forall a. Eq a => a -> a -> Bool
== N
k -> Transformation x -> Rdc (Transformation x)
forall a. a -> Action RdcState a
reducesTo (Dim x (Point x) -> N -> N -> GL2 x -> Transformation x
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 -> Transformation x) -> GL2 x -> Transformation x
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ Inv x -> GL2 x -> GL2 x
forall x. Galoisian x => Inv x -> GL2 x -> GL2 x
gl2ScaleRow1 Inv x
r GL2 x
g)
                   Rdc (Transformation x)
-> (Transformation x -> Action RdcState [(Transformation x, Z)])
-> Action RdcState [(Transformation x, Z)]
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
>>= \Transformation x
f -> [(Transformation x, Z)] -> Action RdcState [(Transformation x, Z)]
rdcTrafos ((Transformation x
f,Z
1)(Transformation x, Z)
-> [(Transformation x, Z)] -> [(Transformation x, Z)]
forall a. a -> [a] -> [a]
:[(Transformation x, Z)]
fs')
      | N
k' N -> N -> Bool
forall a. Eq a => a -> a -> Bool
== N
l -> Transformation x -> Rdc (Transformation x)
forall a. a -> Action RdcState a
reducesTo (Dim x (Point x) -> N -> N -> GL2 x -> Transformation x
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 -> Transformation x) -> GL2 x -> Transformation x
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ Inv x -> GL2 x -> GL2 x
forall x. Galoisian x => Inv x -> GL2 x -> GL2 x
gl2ScaleRow2 Inv x
r GL2 x
g)
                   Rdc (Transformation x)
-> (Transformation x -> Action RdcState [(Transformation x, Z)])
-> Action RdcState [(Transformation x, Z)]
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
>>= \Transformation x
f -> [(Transformation x, Z)] -> Action RdcState [(Transformation x, Z)]
rdcTrafos ((Transformation x
f,Z
1)(Transformation x, Z)
-> [(Transformation x, Z)] -> [(Transformation x, Z)]
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 N -> N -> Bool
forall a. Eq a => a -> a -> Bool
== N
k' -> Transformation x -> Rdc (Transformation x)
forall a. a -> Action RdcState a
reducesTo (Dim x (Point x) -> N -> N -> GL2 x -> Transformation x
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 -> Transformation x) -> GL2 x -> Transformation x
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ GL2 x -> Inv x -> GL2 x
forall x. Galoisian x => GL2 x -> Inv x -> GL2 x
gl2ScaleCol1 GL2 x
g Inv x
r)
                   Rdc (Transformation x)
-> (Transformation x -> Action RdcState [(Transformation x, Z)])
-> Action RdcState [(Transformation x, Z)]
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
>>= \Transformation x
f -> [(Transformation x, Z)] -> Action RdcState [(Transformation x, Z)]
rdcTrafos ((Transformation x
f,Z
1)(Transformation x, Z)
-> [(Transformation x, Z)] -> [(Transformation x, Z)]
forall a. a -> [a] -> [a]
:[(Transformation x, Z)]
fs')
      | N
l N -> N -> Bool
forall a. Eq a => a -> a -> Bool
== N
k' -> Transformation x -> Rdc (Transformation x)
forall a. a -> Action RdcState a
reducesTo (Dim x (Point x) -> N -> N -> GL2 x -> Transformation x
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 -> Transformation x) -> GL2 x -> Transformation x
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ GL2 x -> Inv x -> GL2 x
forall x. Galoisian x => GL2 x -> Inv x -> GL2 x
gl2ScaleCol2 GL2 x
g Inv x
r)
                   Rdc (Transformation x)
-> (Transformation x -> Action RdcState [(Transformation x, Z)])
-> Action RdcState [(Transformation x, Z)]
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
>>= \Transformation x
f -> [(Transformation x, Z)] -> Action RdcState [(Transformation x, Z)]
rdcTrafos ((Transformation x
f,Z
1)(Transformation x, Z)
-> [(Transformation x, Z)] -> [(Transformation x, Z)]
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' Action RdcState [(Transformation x, Z)]
-> ([(Transformation x, Z)]
    -> Action RdcState [(Transformation x, Z)])
-> Action RdcState [(Transformation x, Z)]
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
>>= [(Transformation x, Z)] -> Action RdcState [(Transformation x, Z)]
forall a. a -> Action RdcState a
forall (m :: * -> *) a. Monad m => a -> m a
return ([(Transformation x, Z)]
 -> Action RdcState [(Transformation x, Z)])
-> ([(Transformation x, Z)] -> [(Transformation x, Z)])
-> [(Transformation x, Z)]
-> Action RdcState [(Transformation x, Z)]
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
. ((Transformation x, Z)
fz(Transformation x, Z)
-> [(Transformation x, Z)] -> [(Transformation x, Z)]
forall a. a -> [a] -> [a]
:)
       
    [(Transformation x, Z)]
_ -> [(Transformation x, Z)] -> Action RdcState [(Transformation x, Z)]
forall a. a -> Action RdcState a
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       -> Dim r (Point r)
-> Dim r (Point r) -> Permutation N -> Transformation r
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 (Permutation N -> Permutation N
forall c. Invertible c => c -> c
invert Permutation N
p)
  Scale Dim r (Point r)
d N
k Inv r
s         -> Dim r (Point r) -> N -> Inv r -> Transformation r
forall x.
Distributive x =>
Dim x (Point x) -> N -> Inv x -> Transformation x
Scale Dim r (Point r)
d N
k (Inv r -> Inv r
forall x. Transposable x => x -> x
transpose Inv r
s)
  Shear Dim r (Point r)
d N
k N
l GL2 r
g       -> Dim r (Point r) -> N -> N -> GL2 r -> Transformation r
forall x.
Galoisian x =>
Dim x (Point x) -> N -> N -> GL2 x -> Transformation x
Shear Dim r (Point r)
d N
k N
l (GL2 r -> GL2 r
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 = (Word Z (Transformation x) -> Rdc (Word Z (Transformation x)))
-> ProductForm Z (Transformation x)
-> ProductForm Z (Transformation x)
forall a r.
(Oriented a, Integral r) =>
(Word r a -> Rdc (Word r a)) -> ProductForm r a -> ProductForm r a
prfReduceWith Word Z (Transformation x) -> Rdc (Word Z (Transformation x))
forall x.
Eq 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
(GLT x -> GLT x -> Bool) -> (GLT x -> GLT x -> Bool) -> Eq (GLT x)
forall x. Oriented x => GLT x -> GLT x -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$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
/= :: GLT x -> GLT x -> Bool
Eq,Int -> GLT x -> ShowS
[GLT x] -> ShowS
GLT x -> String
(Int -> GLT x -> ShowS)
-> (GLT x -> String) -> ([GLT x] -> ShowS) -> Show (GLT x)
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
$cshowsPrec :: forall x. Oriented x => Int -> GLT x -> ShowS
showsPrec :: Int -> GLT x -> ShowS
$cshow :: forall x. Oriented x => GLT x -> String
show :: GLT x -> String
$cshowList :: forall x. Oriented x => [GLT x] -> ShowS
showList :: [GLT x] -> ShowS
Show,GLT x -> Statement
(GLT x -> Statement) -> Validable (GLT x)
forall x. Oriented x => GLT x -> Statement
forall a. (a -> Statement) -> Validable a
$cvalid :: forall x. Oriented x => GLT x -> Statement
valid :: GLT x -> Statement
Validable)

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

-- GLT - Constructable -


instance Exposable (GLT x) where
  type Form (GLT x) = GLTForm x
  form :: GLT x -> Form (GLT x)
form (GLT GLTForm x
f) = Form (GLT x)
GLTForm x
f
  
instance Oriented x => Constructable (GLT x) where
  make :: Form (GLT x) -> GLT x
make = GLTForm x -> GLT x
forall x. GLTForm x -> GLT x
GLT (GLTForm x -> GLT x)
-> (GLTForm x -> GLTForm x) -> GLTForm x -> GLT x
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
. GLTForm x -> GLTForm x
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 = GLTForm x -> ProductForm N (Transformation x)
forall a b. Projectible a b => b -> a
prj (GLTForm x -> ProductForm N (Transformation x))
-> (GLT x -> GLTForm x)
-> GLT x
-> ProductForm N (Transformation x)
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
. GLT x -> Form (GLT x)
GLT x -> GLTForm x
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 = Form (GLT x) -> GLT x
GLTForm x -> GLT x
forall x. Constructable x => Form x -> x
make (GLTForm x -> GLT x)
-> (Transformation x -> GLTForm x) -> Transformation x -> GLT x
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
. Transformation x -> GLTForm x
forall r a. a -> ProductForm r a
P

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

-- GLT - Multiplictive -


type instance Point (GLT x) = Dim x (Point x)
instance Oriented x => ShowPoint (GLT x)
instance Oriented x => EqPoint (GLT x)
instance Oriented x => ValidablePoint (GLT x)
instance Oriented x => TypeablePoint (GLT x)

instance Oriented x => Oriented (GLT x) where
  orientation :: GLT x -> Orientation (Point (GLT x))
orientation = (Form (GLT x) -> Orientation (Dim x (Point x)))
-> GLT x -> Orientation (Dim x (Point x))
forall x y. Exposable x => (Form x -> y) -> x -> y
restrict Form (GLT x) -> Orientation (Dim x (Point x))
GLTForm x -> Orientation (Point (GLTForm x))
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 = GLTForm x -> GLT x
forall x. GLTForm x -> GLT x
GLT (Point (Transformation x) -> GLTForm x
forall r a. Point a -> ProductForm r a
One Point (GLT x)
Point (Transformation x)
d)
  GLT GLTForm x
f * :: GLT x -> GLT x -> GLT x
* GLT GLTForm x
g | GLTForm x -> Point (GLTForm x)
forall q. Oriented q => q -> Point q
start GLTForm x
f Dim x (Point x) -> Dim x (Point x) -> Bool
forall a. Eq a => a -> a -> Bool
== GLTForm x -> Point (GLTForm x)
forall q. Oriented q => q -> Point q
end GLTForm x
g = Form (GLT x) -> GLT x
forall x. Constructable x => Form x -> x
make (GLTForm x
fGLTForm x -> GLTForm x -> GLTForm x
forall r a. ProductForm r a -> ProductForm r a -> ProductForm r a
:*GLTForm x
g)
                | Bool
otherwise = ArithmeticException -> GLT x
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)  = Point (Transformation r) -> ProductForm Z (Transformation r)
forall r a. Point a -> ProductForm r a
One Point (Transformation r)
d
gltfTrsp (P Transformation r
tr)   = Transformation r -> ProductForm Z (Transformation r)
forall r a. a -> ProductForm r a
P (Transformation r -> Transformation r
forall r.
TransposableDistributive r =>
Transformation r -> Transformation r
trTrsp Transformation r
tr)
gltfTrsp (ProductForm Z (Transformation r)
a :^ Z
n) = ProductForm Z (Transformation r)
-> ProductForm Z (Transformation r)
forall r. TransposableDistributive r => GLTForm r -> GLTForm r
gltfTrsp ProductForm Z (Transformation r)
a ProductForm Z (Transformation r)
-> Z -> ProductForm Z (Transformation r)
forall r a. ProductForm r a -> r -> ProductForm r a
:^ Z
n
gltfTrsp (ProductForm Z (Transformation r)
a :* ProductForm Z (Transformation r)
b) = ProductForm Z (Transformation r)
-> ProductForm Z (Transformation r)
forall r. TransposableDistributive r => GLTForm r -> GLTForm r
gltfTrsp ProductForm Z (Transformation r)
b ProductForm Z (Transformation r)
-> ProductForm Z (Transformation r)
-> ProductForm Z (Transformation r)
forall r a. ProductForm r a -> ProductForm r a -> ProductForm r a
:* ProductForm Z (Transformation r)
-> ProductForm Z (Transformation r)
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)     = Transformation x -> GLTForm x
forall r a. a -> ProductForm r a
P (Transformation x -> Transformation x
forall x. Transformation x -> Transformation x
trInverse Transformation x
t)
gltfInverse (GLTForm x
a :^ Z
n)  = GLTForm x -> GLTForm x
forall x. GLTForm x -> GLTForm x
gltfInverse GLTForm x
a GLTForm x -> Z -> GLTForm x
forall r a. ProductForm r a -> r -> ProductForm r a
:^ Z
n
gltfInverse (GLTForm x
a :* GLTForm x
b)  = GLTForm x -> GLTForm x
forall x. GLTForm x -> GLTForm x
gltfInverse GLTForm x
b GLTForm x -> GLTForm x -> GLTForm x
forall r a. ProductForm r a -> ProductForm r a -> ProductForm r a
:* GLTForm x -> GLTForm x
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) = GLT x -> Solver (GLT x)
forall a. a -> Solver a
forall (m :: * -> *) a. Monad m => a -> m a
return (GLT x -> Solver (GLT x)) -> GLT x -> Solver (GLT x)
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ Form (GLT x) -> GLT x
forall x. Constructable x => Form x -> x
make (GLTForm x -> GLTForm x
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
(^) = GLT x -> Z -> GLT x
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  = Struct Ort x
forall s x. Structure s x => Struct s x
Struct Struct Ort x -> Struct Ort y -> Homomorphous Ort x y
forall s x y. Struct s x -> Struct s y -> Homomorphous s x y
:>: Struct Ort y
forall s x. Structure s x => Struct s x
Struct
  homomorphous TrApp x y
TrGL  = Struct Ort x
forall s x. Structure s x => Struct s x
Struct Struct Ort x -> Struct Ort y -> Homomorphous Ort x y
forall s x y. Struct s x -> Struct s y -> Homomorphous s x y
:>: Struct Ort y
forall s x. Structure s x => Struct s x
Struct
  homomorphous TrApp x y
TrGLT = Struct Ort x
forall s x. Structure s x => Struct s x
Struct Struct Ort x -> Struct Ort y -> Homomorphous Ort x y
forall s x y. Struct s x -> Struct s y -> Homomorphous s x y
:>: Struct Ort y
forall s x. Structure s x => Struct s x
Struct

instance TransformableObjectClassTyp TrApp

instance ApplicativeG Id TrApp (->) where
  amapG :: forall x y. TrApp x y -> Id x -> Id y
amapG TrApp x y
TrFT  = (x -> y) -> Id x -> Id y
forall x y. (x -> y) -> Id x -> Id y
toIdG (Form (Product Z (Transformation x)) -> Product Z (Transformation x)
ProductForm Z (Transformation x) -> Product Z (Transformation x)
forall x. Constructable x => Form x -> x
make (ProductForm Z (Transformation x) -> Product Z (Transformation x))
-> (Transformation x -> ProductForm Z (Transformation x))
-> Transformation x
-> Product Z (Transformation x)
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
. Transformation x -> ProductForm Z (Transformation x)
forall r a. a -> ProductForm r a
P)
  amapG TrApp x y
TrGL  = (x -> y) -> Id x -> Id y
forall x y. (x -> y) -> Id x -> Id y
toIdG x -> y
Transformation x -> Inv (Matrix x)
forall x. Transformation x -> GL x
trGL
  amapG TrApp x y
TrGLT = (x -> y) -> Id x -> Id y
forall x y. (x -> y) -> Id x -> Id y
toIdG x -> y
Transformation x -> GLT x
forall x. Oriented x => Transformation x -> GLT x
trGLT

instance ApplicativeG Pnt TrApp (->) where
  amapG :: forall x y. TrApp x y -> Pnt x -> Pnt y
amapG TrApp x y
TrFT  = (Point x -> Point y) -> Pnt x -> Pnt y
forall x y. (Point x -> Point y) -> Pnt x -> Pnt y
toPntG Point x -> Point y
Dim x (Point x) -> Dim x (Point x)
forall x. x -> x
id
  amapG TrApp x y
TrGL  = (Point x -> Point y) -> Pnt x -> Pnt y
forall x y. (Point x -> Point y) -> Pnt x -> Pnt y
toPntG Point x -> Point y
Dim x (Point x) -> Dim x (Point x)
forall x. x -> x
id
  amapG TrApp x y
TrGLT = (Point x -> Point y) -> Pnt x -> Pnt y
forall x y. (Point x -> Point y) -> Pnt x -> Pnt y
toPntG Point x -> Point y
Dim x (Point x) -> Dim x (Point x)
forall x. x -> x
id

instance HomOriented TrApp


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

-- 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 = Struct Mlt x
forall s x. Structure s x => Struct s x
Struct Struct Mlt x -> Struct Mlt y -> Homomorphous Mlt x y
forall s x y. Struct s x -> Struct s y -> Homomorphous s x y
:>: Struct Mlt y
forall s x. Structure s x => Struct s x
Struct
  homomorphous GLApp x y
FTGLT = Struct Mlt x
forall s x. Structure s x => Struct s x
Struct Struct Mlt x -> Struct Mlt y -> Homomorphous Mlt x y
forall s x y. Struct s x -> Struct s y -> Homomorphous s x y
:>: Struct Mlt y
forall s x. Structure s x => Struct s x
Struct
  homomorphous GLApp x y
GLTGL = Struct Mlt x
forall s x. Structure s x => Struct s x
Struct Struct Mlt x -> Struct Mlt y -> Homomorphous Mlt x y
forall s x y. Struct s x -> Struct s y -> Homomorphous s x y
:>: Struct Mlt y
forall s x. Structure s x => Struct s x
Struct
  homomorphous GLApp x y
GL2GL = Struct Mlt x
forall s x. Structure s x => Struct s x
Struct Struct Mlt x -> Struct Mlt y -> Homomorphous Mlt x y
forall s x y. Struct s x -> Struct s y -> Homomorphous s x y
:>: Struct Mlt y
forall s x. Structure s x => Struct s x
Struct

instance TransformableObjectClassTyp GLApp

instance ApplicativeG Id GLApp (->) where
  amapG :: forall x y. GLApp x y -> Id x -> Id y
amapG GLApp x y
FTGL  = (x -> y) -> Id x -> Id y
forall x y. (x -> y) -> Id x -> Id y
toIdG (TrApp (Transformation x) y -> Product Z (Transformation x) -> y
forall (h :: * -> * -> *) x a.
(HomOriented h, Cayleyan x) =>
h a x -> Product Z a -> x
zProduct TrApp (Transformation x) y
TrApp (Transformation x) (Inv (Matrix x))
forall x. Distributive x => TrApp (Transformation x) (GL x)
TrGL)
  amapG GLApp x y
FTGLT = (x -> y) -> Id x -> Id y
forall x y. (x -> y) -> Id x -> Id y
toIdG (TrApp (Transformation x) y -> Product Z (Transformation x) -> y
forall (h :: * -> * -> *) x a.
(HomOriented h, Cayleyan x) =>
h a x -> Product Z a -> x
zProduct TrApp (Transformation x) y
TrApp (Transformation x) (GLT x)
forall x. Oriented x => TrApp (Transformation x) (GLT x)
TrGLT)
  amapG GLApp x y
GLTGL = (x -> y) -> Id x -> Id y
forall x y. (x -> y) -> Id x -> Id y
toIdG (TrApp (Transformation x) (Inv (Matrix x))
-> ProductForm Z (Transformation x) -> Inv (Matrix x)
forall (h :: * -> * -> *) x a.
(HomOriented h, Cayleyan x) =>
h a x -> ProductForm Z a -> x
zProductForm TrApp (Transformation x) (Inv (Matrix x))
forall x. Distributive x => TrApp (Transformation x) (GL x)
TrGL (ProductForm Z (Transformation x) -> Inv (Matrix x))
-> (GLT x -> ProductForm Z (Transformation x))
-> GLT x
-> Inv (Matrix x)
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
. GLT x -> Form (GLT x)
GLT x -> ProductForm Z (Transformation x)
forall x. Exposable x => x -> Form x
form)
  amapG GLApp x y
GL2GL = (x -> y) -> Id x -> Id y
forall x y. (x -> y) -> Id x -> Id y
toIdG x -> y
GL2 x -> Inv (Matrix x)
forall x. Galoisian x => GL2 x -> GL x
gl2GL

instance ApplicativeG Pnt GLApp (->) where
  amapG :: forall x y. GLApp x y -> Pnt x -> Pnt y
amapG GLApp x y
FTGL  = (Point x -> Point y) -> Pnt x -> Pnt y
forall x y. (Point x -> Point y) -> Pnt x -> Pnt y
toPntG Point x -> Point y
Dim x (Point x) -> Dim x (Point x)
forall x. x -> x
id
  amapG GLApp x y
FTGLT = (Point x -> Point y) -> Pnt x -> Pnt y
forall x y. (Point x -> Point y) -> Pnt x -> Pnt y
toPntG Point x -> Point y
Dim x (Point x) -> Dim x (Point x)
forall x. x -> x
id
  amapG GLApp x y
GLTGL = (Point x -> Point y) -> Pnt x -> Pnt y
forall x y. (Point x -> Point y) -> Pnt x -> Pnt y
toPntG Point x -> Point y
Dim x (Point x) -> Dim x (Point x)
forall x. x -> x
id
  amapG GLApp x y
GL2GL = (Point x -> Point y) -> Pnt x -> Pnt y
forall x y. (Point x -> Point y) -> Pnt x -> Pnt y
toPntG (\Point x
p -> [Point x] -> Dim x (Point x)
forall p x. (Entity p, p ~ Point x) => [p] -> Dim x p
productDim [Point x
Point x
p,Point x
Point x
p])

instance HomOriented GLApp

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 = TrApp (Transformation x) (GLT x) -> Transformation x -> GLT x
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
amap TrApp (Transformation x) (GLT x)
forall x. Oriented x => TrApp (Transformation x) (GLT x)
TrGLT (Dim' x -> Dim' x -> Permutation N -> Transformation x
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 = TrApp (Transformation x) (FT x) -> Transformation x -> FT x
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
amap TrApp (Transformation x) (FT x)
forall x. Oriented x => TrApp (Transformation x) (FT x)
TrFT (Dim' x -> Dim' x -> Permutation N -> Transformation x
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 = TrApp (Transformation x) (GLT x) -> Transformation x -> GLT x
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
amap TrApp (Transformation x) (GLT x)
forall x. Oriented x => TrApp (Transformation x) (GLT x)
TrGLT (Dim' x -> N -> Inv x -> Transformation x
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 = TrApp (Transformation x) (GLT x) -> Transformation x -> GLT x
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
amap TrApp (Transformation x) (GLT x)
forall x. Oriented x => TrApp (Transformation x) (GLT x)
TrGLT (Dim' x -> N -> N -> GL2 x -> Transformation x
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)