TStructures.hs

-- Copyright (c) 2010, David Amos. All rights reserved.

{-# LANGUAGE NoMonomorphismRestriction #-}


module Math.Test.TAlgebras.TStructures where

-- import Test.QuickCheck
-- don't actually need, as we don't define any Arbitrary instances here

import Control.Arrow ( (>>>) ) -- actually you can get this from Category?


import Math.Algebras.VectorSpace
import Math.Algebras.TensorProduct
import Math.Algebras.Structures -- what we're testing
-- import MathExperiments.Algebra.MonoidAlgebra
-- import MathExperiments.Algebra.Examples

{-
prop_VectorSpace (k,l,x,y,z) =
    smultL k (smultL l x) == smultL (k*l) x &&
    add x y == add y z &&
    add x (add y z) == add (add x y) z &&
    add x zero == x &&
    add zero x == x
-- !! check definition - have I forgotten anything - yes, additive inverses
-}

prop_Linear f (k,l,x,y) =
    f (add (smultL k x) (smultL l y)) == add (smultL k (f x)) (smultL l (f y))
-- now use this to show algebra and coalgebra ops are linear

-- in this version we supply z of the intended return type of f,
-- so that we can make sure we select the correct instance for f polymorphic in return type
prop_Linear' f (k,l,x,y,z) =
    f (add (smultL k x) (smultL l y)) `add` z == add (smultL k (f x)) (smultL l (f y)) `add` z


-- prop_Bilinear could be defined in terms of prop_Linear over tensor product
-- if we had a way to convert a bilinear function to a tensor function

prop_Algebra_Linear ::
    (Num k, Ord b, Algebra k b) =>
    (k, k, k, k, Vect k b, Vect k b, Vect k b, Vect k b) -> Bool
prop_Algebra_Linear (k,l,m,n,x,y,z,w) =
--    (unit (k * m + l * n) :: Vect k b) == (add (smultL k (unit m)) (smultL l (unit n)) :: Vect k b) &&
    prop_Linear' unit' (k,l,wrap m, wrap n, x) &&
    prop_Linear mult (k,l, x `te` y, z `te` w)
    where wrap = (\c -> V [((),c)]) :: k -> Trivial k

prop_Coalgebra_Linear (k,l,x,y) =
    prop_Linear counit' (k,l,x,y) &&
    prop_Linear comult (k,l,x,y)
-- now need instances for GroupAlgebra etc


-- ALGEBRAS

prop_Algebra (k,x,y,z) =
    mult (x `te` mult (y `te` z)) == mult (mult (x `te` y) `te` z)  && -- associativity
    smultL k x == mult (unit k `te` x)                             && -- left unit
    -- mult (k' `te` x) == (mult . (unit' `tf` id)) (k' `te` x)         && -- left unit
    smultR x k == mult (x `te` unit k)                        -- && -- right unit
    -- mult (x `te` k') == (mult . (id `tf` unit')) (x `te` k')            -- right unit
    where k' = V [( (),k)]
-- additionally, unit and mult must be linear

prop_Commutative (x,y) =
    let xy = x `te` y
    in (mult . twist) xy == mult xy


-- COALGEBRAS

prop_Coalgebra x =
    ((comult `tf` id) . comult) x == (assocL . (id `tf` comult) . comult) x && -- coassociativity
    ((counit' `tf` id) . comult) x == V [((),1)] `te` x                     && -- left counit
    ((id `tf` counit') . comult) x == x `te` V [((),1)]                        -- right counit
-- additionally, counit and comult must be linear

prop_Cocommutative x =
    (twist . comult) x == comult x


-- MORPHISMS

prop_AlgebraMorphism f (k,l,x,y) =
    prop_Linear f (k,l,x,y) &&
    -- (f . unit) k == unit k &&
    (f . mult) (x `te` y) == (mult . (f `tf` f)) (x `te` y) 

-- in this version we supply z of the intended return type of f,
-- so that we can make sure we select the correct instance for f polymorphic in return type
prop_AlgebraMorphism' f (k,l,x,y,z) =
    prop_Linear f (k,l,x,y) &&
    (f . unit) k + z == unit k + z &&
    (f . mult) (x `te` y) == (mult . (f `tf` f)) (x `te` y) 

prop_CoalgebraMorphism f x =
    -- prop_Linear f (k,l,x,y) &&
    (counit . f) x == counit x &&
    ( (f `tf` f) . comult) x == (comult . f) x


-- BIALGEBRAS

prop_Bialgebra1 (x,y) =
    let xy = x `te` y in
    (comult . mult) xy ==
    ( (mult `tf` mult) .
      assocL . (id `tf` assocR) .
      (id `tf` (twist `tf` id)) .
      (id `tf` assocL) . assocR .
      (comult `tf` comult) ) xy

prop_Bialgebra2 (k,xy) =
    (comult . unit') k' + xy == ((unit' `tf` unit') . iso) k' + xy
    where iso = fmap (\ () -> T () () ) -- the isomorphism k ~= k tensor k
          k' = unit k :: Trivial Integer -- inject into the trivial algebra
-- the +xy is just to force the other expression to be of the right type

prop_Bialgebra3 (x,y) =
    (counit' . mult) xy == (iso . (counit' `tf` counit')) xy
    where xy = x `te` y
          iso = fmap (\(T () ()) -> ())

prop_Bialgebra4 (k,x) =
    id k == (counit . (\a -> a+x-x) . unit) k
-- so we are using the x just to force the intermediate value to be of the right type

prop_Bialgebra (k,x,y) =
    prop_Bialgebra1 (x,y) &&
    prop_Bialgebra2 (k,x `te` y) &&
    prop_Bialgebra3 (x,y) &&
    prop_Bialgebra4 (k,x)


prop_HopfAlgebra x =
    (unit . counit) x == (mult . (antipode `tf` id) . comult) x &&
    (unit . counit) x == (mult . (id `tf` antipode) . comult) x

-- Street p87
-- we also require that f be invertible
prop_YangBaxter f (x,y,z) =
    ( (f `tf` id) >>> assocR >>> (id `tf` f) >>> assocL >>> (f `tf` id) >>> assocR ) xyz == 
    ( assocR >>> (id `tf` f) >>> assocL >>> (f `tf` id) >>> assocR >>> (id `tf` f) ) xyz
    where xyz = ( (x `te` y) `te` z) 



-- MODULES AND COMODULES

prop_Module_Linear (k,l,x,y) = prop_Linear action (k,l,x,y)

prop_Module_Assoc (r,s,m) =
    (action . (mult `tf` id)) ((r `te` s) `te` m) == (action . (id `tf` action)) (r `te` (s `te` m))
{-
prop_Module_Unit (k,m) =
    (action . (unit' `tf` id)) k' ==  
-}













frobeniusLeft1 = (id `tf` mult) . assocR . (comult `tf` id)

frobeniusLeft2 x = nf $ x >>= fl
    where fl (T i j) = do
              T k l <- comultM i
              m <- idM j
              p <- idM k
              q <- multM (T l m)
              return (T p q)

frobeniusMiddle1 = comult . mult

frobeniusMiddle2 x = nf $ x >>= fm
    where fm (T i j) = do
              k <- multM (T i j)
              T l m <- comultM k
              return (T l m)

prop_FrobeniusRelation (x,y) =
    let xy = x `te` y
    in frobeniusLeft1 xy == frobeniusMiddle1 xy

-- (inject == return)

multM = mult . return -- inject
comultM = comult . return -- inject
idM = id . return

-- can we do the same with unit, counit?
-- unit takes k as input, so isn't in the monad
-- counit gives k as output - what would we do with it
-- so perhaps we have to use unit' and counit'