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

{-# LANGUAGE MultiParamTypeClasses, NoMonomorphismRestriction #-}
{-# LANGUAGE FlexibleInstances, TypeSynonymInstances #-}
{-# LANGUAGE IncoherentInstances #-}

-- |A module defining various algebraic structures that can be defined on vector spaces
-- - specifically algebra, coalgebra, bialgebra, Hopf algebra, module, comodule
module Math.Algebras.Structures where

import Prelude hiding ( (*>) )

import Math.Algebras.VectorSpace
import Math.Algebras.TensorProduct


-- MONOID

-- |Monoid
class Mon m where
    munit :: m
    mmult :: m -> m -> m


-- ALGEBRAS, COALGEBRAS, BIALGEBRAS, HOPF ALGEBRAS

-- |Caution: If we declare an instance Algebra k b, then we are saying that the vector space Vect k b is a k-algebra.
-- In other words, we are saying that b is the basis for a k-algebra. So a more accurate name for this class
-- would have been AlgebraBasis.
class Algebra k b where
    unit :: k -> Vect k b
    mult :: Vect k (Tensor b b) -> Vect k b

-- |Sometimes it is more convenient to work with this version of unit.
unit' :: (Eq k, Num k, Algebra k b) => Vect k () -> Vect k b
unit' :: Vect k () -> Vect k b
unit' = k -> Vect k b
forall k b. Algebra k b => k -> Vect k b
unit (k -> Vect k b) -> (Vect k () -> k) -> Vect k () -> Vect k b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Vect k () -> k
forall k. Num k => Vect k () -> k
unwrap -- where unwrap = counit :: Num k => Trivial k -> k

-- |An instance declaration for Coalgebra k b is saying that the vector space Vect k b is a k-coalgebra.
class Coalgebra k b where
    counit :: Vect k b -> k
    comult :: Vect k b -> Vect k (Tensor b b)

-- |Sometimes it is more convenient to work with this version of counit.
counit' :: (Eq k, Num k, Coalgebra k b) => Vect k b -> Vect k ()
counit' :: Vect k b -> Vect k ()
counit' = k -> Vect k ()
forall k. (Eq k, Num k) => k -> Vect k ()
wrap (k -> Vect k ()) -> (Vect k b -> k) -> Vect k b -> Vect k ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Vect k b -> k
forall k b. Coalgebra k b => Vect k b -> k
counit -- where wrap = unit :: Num k => k -> Trivial k

-- unit' and counit' enable us to form tensors of these functions

-- |A bialgebra is an algebra which is also a coalgebra, subject to the compatibility conditions
-- that counit and comult must be algebra morphisms (or equivalently, that unit and mult must be coalgebra morphisms)
class (Algebra k b, Coalgebra k b) => Bialgebra k b where {}

class Bialgebra k b => HopfAlgebra k b where
    antipode :: Vect k b -> Vect k b


instance (Eq k, Num k, Eq b, Ord b, Show b, Algebra k b) => Num (Vect k b) where
    x :: Vect k b
x+ :: Vect k b -> Vect k b -> Vect k b
+y :: Vect k b
y = Vect k b
x Vect k b -> Vect k b -> Vect k b
forall k b.
(Eq k, Num k, Ord b) =>
Vect k b -> Vect k b -> Vect k b
<+> Vect k b
y
    negate :: Vect k b -> Vect k b
negate x :: Vect k b
x = Vect k b -> Vect k b
forall k b. (Eq k, Num k) => Vect k b -> Vect k b
negatev Vect k b
x
    -- negate (V ts) = V $ map (\(b,x) -> (b, negate x)) ts
    x :: Vect k b
x* :: Vect k b -> Vect k b -> Vect k b
*y :: Vect k b
y = Vect k (Tensor b b) -> Vect k b
forall k b. Algebra k b => Vect k (Tensor b b) -> Vect k b
mult (Vect k b
x Vect k b -> Vect k b -> Vect k (Tensor b b)
forall k a b. Num k => Vect k a -> Vect k b -> Vect k (Tensor a b)
`te` Vect k b
y)
    fromInteger :: Integer -> Vect k b
fromInteger n :: Integer
n = k -> Vect k b
forall k b. Algebra k b => k -> Vect k b
unit (Integer -> k
forall a. Num a => Integer -> a
fromInteger Integer
n)
    abs :: Vect k b -> Vect k b
abs _ = [Char] -> Vect k b
forall a. HasCallStack => [Char] -> a
error "Prelude.Num.abs: inappropriate abstraction"
    signum :: Vect k b -> Vect k b
signum _ = [Char] -> Vect k b
forall a. HasCallStack => [Char] -> a
error "Prelude.Num.signum: inappropriate abstraction"


-- This is the Frobenius form, provided some conditions are met
-- pairing = counit . mult

{-
-- A class to be used to declare that a type b should be given the set coalgebra structure
class SetCoalgebra b where {}

instance (Num k, SetCoalgebra b) => Coalgebra k b where
    counit (V ts) = sum [x | (m,x) <- ts] -- trace
    comult = fmap (\m -> T m m) -- diagonal
-}


instance (Eq k, Num k) => Algebra k () where
    unit :: k -> Vect k ()
unit = k -> Vect k ()
forall k. (Eq k, Num k) => k -> Vect k ()
wrap
    -- unit 0 = zero -- V []
    -- unit x = V [( (),x)]
    mult :: Vect k (Tensor () ()) -> Vect k ()
mult = (Tensor () () -> ()) -> Vect k (Tensor () ()) -> Vect k ()
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\((),())->())
    -- mult = linear mult' where mult' ((),()) = return ()
    -- mult (V [( ((),()), x)]) = V [( (),x)]
    -- mult (V []) = zerov

instance (Eq k, Num k) => Coalgebra k () where
    counit :: Vect k () -> k
counit = Vect k () -> k
forall k. Num k => Vect k () -> k
unwrap
    -- counit (V []) = 0
    -- counit (V [( (),x)]) = x
    comult :: Vect k () -> Vect k (Tensor () ())
comult = (() -> Tensor () ()) -> Vect k () -> Vect k (Tensor () ())
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\()->((),()))
    -- comult = linear comult' where comult' () = return ((),())
    -- comult (V [( (),x)]) = V [( ((),()), x)]
    -- comult (V []) = zerov


-- Kassel p4
-- |The direct sum of k-algebras can itself be given the structure of a k-algebra.
-- This is the product object in the category of k-algebras.
instance (Eq k, Num k, Ord a, Ord b, Algebra k a, Algebra k b) => Algebra k (DSum a b) where
    unit :: k -> Vect k (DSum a b)
unit k :: k
k = Vect k a -> Vect k (DSum a b)
forall k a b. Vect k a -> Vect k (DSum a b)
i1 (k -> Vect k a
forall k b. Algebra k b => k -> Vect k b
unit k
k) Vect k (DSum a b) -> Vect k (DSum a b) -> Vect k (DSum a b)
forall k b.
(Eq k, Num k, Ord b) =>
Vect k b -> Vect k b -> Vect k b
<+> Vect k b -> Vect k (DSum a b)
forall k b a. Vect k b -> Vect k (DSum a b)
i2 (k -> Vect k b
forall k b. Algebra k b => k -> Vect k b
unit k
k)
    -- unit == (i1 . unit) <<+>> (i2 . unit)
    mult :: Vect k (Tensor (DSum a b) (DSum a b)) -> Vect k (DSum a b)
mult = (Tensor (DSum a b) (DSum a b) -> Vect k (DSum a b))
-> Vect k (Tensor (DSum a b) (DSum a b)) -> Vect k (DSum a b)
forall k b a.
(Eq k, Num k, Ord b) =>
(a -> Vect k b) -> Vect k a -> Vect k b
linear Tensor (DSum a b) (DSum a b) -> Vect k (DSum a b)
forall k a b.
(Num k, Algebra k a, Algebra k b) =>
(Either a b, Either a b) -> Vect k (Either a b)
mult'
        where mult' :: (Either a b, Either a b) -> Vect k (Either a b)
mult' (Left a1 :: a
a1, Left a2 :: a
a2) = Vect k a -> Vect k (Either a b)
forall k a b. Vect k a -> Vect k (DSum a b)
i1 (Vect k a -> Vect k (Either a b))
-> Vect k a -> Vect k (Either a b)
forall a b. (a -> b) -> a -> b
$ Vect k (Tensor a a) -> Vect k a
forall k b. Algebra k b => Vect k (Tensor b b) -> Vect k b
mult (Vect k (Tensor a a) -> Vect k a)
-> Vect k (Tensor a a) -> Vect k a
forall a b. (a -> b) -> a -> b
$ Tensor a a -> Vect k (Tensor a a)
forall (m :: * -> *) a. Monad m => a -> m a
return (a
a1,a
a2)
              mult' (Right b1 :: b
b1, Right b2 :: b
b2) = Vect k b -> Vect k (Either a b)
forall k b a. Vect k b -> Vect k (DSum a b)
i2 (Vect k b -> Vect k (Either a b))
-> Vect k b -> Vect k (Either a b)
forall a b. (a -> b) -> a -> b
$ Vect k (Tensor b b) -> Vect k b
forall k b. Algebra k b => Vect k (Tensor b b) -> Vect k b
mult (Vect k (Tensor b b) -> Vect k b)
-> Vect k (Tensor b b) -> Vect k b
forall a b. (a -> b) -> a -> b
$ Tensor b b -> Vect k (Tensor b b)
forall (m :: * -> *) a. Monad m => a -> m a
return (b
b1,b
b2)
              mult' _ = Vect k (Either a b)
forall k b. Vect k b
zerov
-- This is the product algebra, which is the product in the category of algebras
-- 1 = (1,1)
-- (a1,b1) * (a2,b2) = (a1*a2, b1*b2)
-- It's not a coproduct, because i1, i2 aren't algebra morphisms (they violate Unit axiom)

-- |The direct sum of k-coalgebras can itself be given the structure of a k-coalgebra.
-- This is the coproduct object in the category of k-coalgebras.
instance (Eq k, Num k, Ord a, Ord b, Coalgebra k a, Coalgebra k b) => Coalgebra k (DSum a b) where
    counit :: Vect k (DSum a b) -> k
counit = Vect k () -> k
forall k. Num k => Vect k () -> k
unwrap (Vect k () -> k)
-> (Vect k (DSum a b) -> Vect k ()) -> Vect k (DSum a b) -> k
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (DSum a b -> Vect k ()) -> Vect k (DSum a b) -> Vect k ()
forall k b a.
(Eq k, Num k, Ord b) =>
(a -> Vect k b) -> Vect k a -> Vect k b
linear DSum a b -> Vect k ()
forall k b b.
(Eq k, Num k, Coalgebra k b, Coalgebra k b) =>
Either b b -> Vect k ()
counit'
        where counit' :: Either b b -> Vect k ()
counit' (Left a :: b
a) = (k -> Vect k ()
forall k. (Eq k, Num k) => k -> Vect k ()
wrap (k -> Vect k ()) -> (Vect k b -> k) -> Vect k b -> Vect k ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Vect k b -> k
forall k b. Coalgebra k b => Vect k b -> k
counit) (b -> Vect k b
forall (m :: * -> *) a. Monad m => a -> m a
return b
a)
              counit' (Right b :: b
b) = (k -> Vect k ()
forall k. (Eq k, Num k) => k -> Vect k ()
wrap (k -> Vect k ()) -> (Vect k b -> k) -> Vect k b -> Vect k ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Vect k b -> k
forall k b. Coalgebra k b => Vect k b -> k
counit) (b -> Vect k b
forall (m :: * -> *) a. Monad m => a -> m a
return b
b)
    -- counit = counit . p1 <<+>> counit . p2
    comult :: Vect k (DSum a b) -> Vect k (Tensor (DSum a b) (DSum a b))
comult = (DSum a b -> Vect k (Tensor (DSum a b) (DSum a b)))
-> Vect k (DSum a b) -> Vect k (Tensor (DSum a b) (DSum a b))
forall k b a.
(Eq k, Num k, Ord b) =>
(a -> Vect k b) -> Vect k a -> Vect k b
linear DSum a b -> Vect k (Tensor (DSum a b) (DSum a b))
forall k a b.
(Num k, Coalgebra k a, Coalgebra k b) =>
Either a b -> Vect k (Either a b, Either a b)
comult' where
        comult' :: Either a b -> Vect k (Either a b, Either a b)
comult' (Left a :: a
a) = ((a, a) -> (Either a b, Either a b))
-> Vect k (a, a) -> Vect k (Either a b, Either a b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\(a1 :: a
a1,a2 :: a
a2) -> (a -> Either a b
forall a b. a -> Either a b
Left a
a1, a -> Either a b
forall a b. a -> Either a b
Left a
a2)) (Vect k (a, a) -> Vect k (Either a b, Either a b))
-> Vect k (a, a) -> Vect k (Either a b, Either a b)
forall a b. (a -> b) -> a -> b
$ Vect k a -> Vect k (a, a)
forall k b. Coalgebra k b => Vect k b -> Vect k (Tensor b b)
comult (Vect k a -> Vect k (a, a)) -> Vect k a -> Vect k (a, a)
forall a b. (a -> b) -> a -> b
$ a -> Vect k a
forall (m :: * -> *) a. Monad m => a -> m a
return a
a
        comult' (Right b :: b
b) = ((b, b) -> (Either a b, Either a b))
-> Vect k (b, b) -> Vect k (Either a b, Either a b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\(b1 :: b
b1,b2 :: b
b2) -> (b -> Either a b
forall a b. b -> Either a b
Right b
b1, b -> Either a b
forall a b. b -> Either a b
Right b
b2)) (Vect k (b, b) -> Vect k (Either a b, Either a b))
-> Vect k (b, b) -> Vect k (Either a b, Either a b)
forall a b. (a -> b) -> a -> b
$ Vect k b -> Vect k (b, b)
forall k b. Coalgebra k b => Vect k b -> Vect k (Tensor b b)
comult (Vect k b -> Vect k (b, b)) -> Vect k b -> Vect k (b, b)
forall a b. (a -> b) -> a -> b
$ b -> Vect k b
forall (m :: * -> *) a. Monad m => a -> m a
return b
b
    -- comult = ( (i1 `tf` i1) . comult . p1 ) <<+>> ( (i2 `tf` i2) . comult . p2 )




-- Kassel p32
-- |The tensor product of k-algebras can itself be given the structure of a k-algebra
instance (Eq k, Num k, Ord a, Ord b, Algebra k a, Algebra k b) => Algebra k (Tensor a b) where
    -- unit 0 = V []
    unit :: k -> Vect k (Tensor a b)
unit x :: k
x = k
x k -> Vect k (Tensor a b) -> Vect k (Tensor a b)
forall k b. (Eq k, Num k) => k -> Vect k b -> Vect k b
*> (k -> Vect k a
forall k b. Algebra k b => k -> Vect k b
unit 1 Vect k a -> Vect k b -> Vect k (Tensor a b)
forall k a b. Num k => Vect k a -> Vect k b -> Vect k (Tensor a b)
`te` k -> Vect k b
forall k b. Algebra k b => k -> Vect k b
unit 1)
    mult :: Vect k (Tensor (Tensor a b) (Tensor a b)) -> Vect k (Tensor a b)
mult = (Vect k (Tensor a a) -> Vect k a
forall k b. Algebra k b => Vect k (Tensor b b) -> Vect k b
mult (Vect k (Tensor a a) -> Vect k a)
-> (Vect k (Tensor b b) -> Vect k b)
-> Vect k (Tensor (Tensor a a) (Tensor b b))
-> Vect k (Tensor a b)
forall k a' b' a b.
(Eq k, Num k, Ord a', Ord b') =>
(Vect k a -> Vect k a')
-> (Vect k b -> Vect k b')
-> Vect k (Tensor a b)
-> Vect k (Tensor a' b')
`tf` Vect k (Tensor b b) -> Vect k b
forall k b. Algebra k b => Vect k (Tensor b b) -> Vect k b
mult) (Vect k (Tensor (Tensor a a) (Tensor b b)) -> Vect k (Tensor a b))
-> (Vect k (Tensor (Tensor a b) (Tensor a b))
    -> Vect k (Tensor (Tensor a a) (Tensor b b)))
-> Vect k (Tensor (Tensor a b) (Tensor a b))
-> Vect k (Tensor a b)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Tensor (Tensor a b) (Tensor a b)
 -> Tensor (Tensor a a) (Tensor b b))
-> Vect k (Tensor (Tensor a b) (Tensor a b))
-> Vect k (Tensor (Tensor a a) (Tensor b b))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\((a :: a
a,b :: b
b),(a' :: a
a',b' :: b
b')) -> ((a
a,a
a'),(b
b,b
b')) )
    -- mult = linear m where
    --     m ((a,b),(a',b')) = (mult $ return (a,a')) `te` (mult $ return (b,b'))

-- Kassel p42
-- |The tensor product of k-coalgebras can itself be given the structure of a k-coalgebra
instance (Eq k, Num k, Ord a, Ord b, Coalgebra k a, Coalgebra k b) => Coalgebra k (Tensor a b) where
    counit :: Vect k (Tensor a b) -> k
counit = Vect k () -> k
forall k. Num k => Vect k () -> k
unwrap (Vect k () -> k)
-> (Vect k (Tensor a b) -> Vect k ()) -> Vect k (Tensor a b) -> k
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Tensor a b -> Vect k ()) -> Vect k (Tensor a b) -> Vect k ()
forall k b a.
(Eq k, Num k, Ord b) =>
(a -> Vect k b) -> Vect k a -> Vect k b
linear Tensor a b -> Vect k ()
forall k b b.
(Eq k, Num k, Coalgebra k b, Coalgebra k b) =>
(b, b) -> Vect k ()
counit'
        where counit' :: (b, b) -> Vect k ()
counit' (a :: b
a,b :: b
b) = (k -> Vect k ()
forall k. (Eq k, Num k) => k -> Vect k ()
wrap (k -> Vect k ()) -> (b -> k) -> b -> Vect k ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Vect k b -> k
forall k b. Coalgebra k b => Vect k b -> k
counit (Vect k b -> k) -> (b -> Vect k b) -> b -> k
forall b c a. (b -> c) -> (a -> b) -> a -> c
. b -> Vect k b
forall (m :: * -> *) a. Monad m => a -> m a
return) b
a Vect k () -> Vect k () -> Vect k ()
forall a. Num a => a -> a -> a
* (k -> Vect k ()
forall k. (Eq k, Num k) => k -> Vect k ()
wrap (k -> Vect k ()) -> (b -> k) -> b -> Vect k ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Vect k b -> k
forall k b. Coalgebra k b => Vect k b -> k
counit (Vect k b -> k) -> (b -> Vect k b) -> b -> k
forall b c a. (b -> c) -> (a -> b) -> a -> c
. b -> Vect k b
forall (m :: * -> *) a. Monad m => a -> m a
return) b
b -- (*) taking place in Vect k ()
    -- what this really says is that counit (a `tensor` b) = counit a * counit b
    -- counit = counit . linear (\(x,y) -> counit' (return x) * counit' (return y))
    comult :: Vect k (Tensor a b) -> Vect k (Tensor (Tensor a b) (Tensor a b))
comult = Vect k (Tensor (Tensor a b) (Tensor a b))
-> Vect k (Tensor (Tensor a b) (Tensor a b))
forall k b. (Eq k, Num k, Ord b) => Vect k b -> Vect k b
nf (Vect k (Tensor (Tensor a b) (Tensor a b))
 -> Vect k (Tensor (Tensor a b) (Tensor a b)))
-> (Vect k (Tensor a b)
    -> Vect k (Tensor (Tensor a b) (Tensor a b)))
-> Vect k (Tensor a b)
-> Vect k (Tensor (Tensor a b) (Tensor a b))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (((a, a), (b, b)) -> Tensor (Tensor a b) (Tensor a b))
-> Vect k ((a, a), (b, b))
-> Vect k (Tensor (Tensor a b) (Tensor a b))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\((a :: a
a,a' :: a
a'),(b :: b
b,b' :: b
b')) -> ((a
a,b
b),(a
a',b
b')) ) (Vect k ((a, a), (b, b))
 -> Vect k (Tensor (Tensor a b) (Tensor a b)))
-> (Vect k (Tensor a b) -> Vect k ((a, a), (b, b)))
-> Vect k (Tensor a b)
-> Vect k (Tensor (Tensor a b) (Tensor a b))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Vect k a -> Vect k (a, a)
forall k b. Coalgebra k b => Vect k b -> Vect k (Tensor b b)
comult (Vect k a -> Vect k (a, a))
-> (Vect k b -> Vect k (b, b))
-> Vect k (Tensor a b)
-> Vect k ((a, a), (b, b))
forall k a' b' a b.
(Eq k, Num k, Ord a', Ord b') =>
(Vect k a -> Vect k a')
-> (Vect k b -> Vect k b')
-> Vect k (Tensor a b)
-> Vect k (Tensor a' b')
`tf` Vect k b -> Vect k (b, b)
forall k b. Coalgebra k b => Vect k b -> Vect k (Tensor b b)
comult)
    -- comult = assocL . (id `tf` assocR) . (id `tf` (twist `tf` id))
    --        . (id `tf` assocL) . assocR . (comult `tf` comult)


newtype Op b = Op b deriving (Op b -> Op b -> Bool
(Op b -> Op b -> Bool) -> (Op b -> Op b -> Bool) -> Eq (Op b)
forall b. Eq b => Op b -> Op b -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Op b -> Op b -> Bool
$c/= :: forall b. Eq b => Op b -> Op b -> Bool
== :: Op b -> Op b -> Bool
$c== :: forall b. Eq b => Op b -> Op b -> Bool
Eq, Eq (Op b)
Eq (Op b) =>
(Op b -> Op b -> Ordering)
-> (Op b -> Op b -> Bool)
-> (Op b -> Op b -> Bool)
-> (Op b -> Op b -> Bool)
-> (Op b -> Op b -> Bool)
-> (Op b -> Op b -> Op b)
-> (Op b -> Op b -> Op b)
-> Ord (Op b)
Op b -> Op b -> Bool
Op b -> Op b -> Ordering
Op b -> Op b -> Op b
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 b. Ord b => Eq (Op b)
forall b. Ord b => Op b -> Op b -> Bool
forall b. Ord b => Op b -> Op b -> Ordering
forall b. Ord b => Op b -> Op b -> Op b
min :: Op b -> Op b -> Op b
$cmin :: forall b. Ord b => Op b -> Op b -> Op b
max :: Op b -> Op b -> Op b
$cmax :: forall b. Ord b => Op b -> Op b -> Op b
>= :: Op b -> Op b -> Bool
$c>= :: forall b. Ord b => Op b -> Op b -> Bool
> :: Op b -> Op b -> Bool
$c> :: forall b. Ord b => Op b -> Op b -> Bool
<= :: Op b -> Op b -> Bool
$c<= :: forall b. Ord b => Op b -> Op b -> Bool
< :: Op b -> Op b -> Bool
$c< :: forall b. Ord b => Op b -> Op b -> Bool
compare :: Op b -> Op b -> Ordering
$ccompare :: forall b. Ord b => Op b -> Op b -> Ordering
$cp1Ord :: forall b. Ord b => Eq (Op b)
Ord, Int -> Op b -> ShowS
[Op b] -> ShowS
Op b -> [Char]
(Int -> Op b -> ShowS)
-> (Op b -> [Char]) -> ([Op b] -> ShowS) -> Show (Op b)
forall b. Show b => Int -> Op b -> ShowS
forall b. Show b => [Op b] -> ShowS
forall b. Show b => Op b -> [Char]
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
showList :: [Op b] -> ShowS
$cshowList :: forall b. Show b => [Op b] -> ShowS
show :: Op b -> [Char]
$cshow :: forall b. Show b => Op b -> [Char]
showsPrec :: Int -> Op b -> ShowS
$cshowsPrec :: forall b. Show b => Int -> Op b -> ShowS
Show)

instance (Eq k, Num k, Ord b, Algebra k b) => Algebra k (Op b) where
    unit :: k -> Vect k (Op b)
unit = (b -> Op b) -> Vect k b -> Vect k (Op b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap b -> Op b
forall b. b -> Op b
Op (Vect k b -> Vect k (Op b))
-> (k -> Vect k b) -> k -> Vect k (Op b)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. k -> Vect k b
forall k b. Algebra k b => k -> Vect k b
unit
    mult :: Vect k (Tensor (Op b) (Op b)) -> Vect k (Op b)
mult = Vect k (Op b) -> Vect k (Op b)
forall k b. (Eq k, Num k, Ord b) => Vect k b -> Vect k b
nf (Vect k (Op b) -> Vect k (Op b))
-> (Vect k (Tensor (Op b) (Op b)) -> Vect k (Op b))
-> Vect k (Tensor (Op b) (Op b))
-> Vect k (Op b)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (b -> Op b) -> Vect k b -> Vect k (Op b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap b -> Op b
forall b. b -> Op b
Op (Vect k b -> Vect k (Op b))
-> (Vect k (Tensor (Op b) (Op b)) -> Vect k b)
-> Vect k (Tensor (Op b) (Op b))
-> Vect k (Op b)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Vect k (Tensor b b) -> Vect k b
forall k b. Algebra k b => Vect k (Tensor b b) -> Vect k b
mult (Vect k (Tensor b b) -> Vect k b)
-> (Vect k (Tensor (Op b) (Op b)) -> Vect k (Tensor b b))
-> Vect k (Tensor (Op b) (Op b))
-> Vect k b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Tensor (Op b) (Op b) -> Tensor b b)
-> Vect k (Tensor (Op b) (Op b)) -> Vect k (Tensor b b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\(Op a :: b
a, Op b :: b
b) -> (b
b, b
a)) -- ie mult . twist

instance (Eq k, Num k, Ord b, Coalgebra k b) => Coalgebra k (Op b) where
    counit :: Vect k (Op b) -> k
counit = Vect k b -> k
forall k b. Coalgebra k b => Vect k b -> k
counit (Vect k b -> k)
-> (Vect k (Op b) -> Vect k b) -> Vect k (Op b) -> k
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Op b -> b) -> Vect k (Op b) -> Vect k b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\(Op b :: b
b) -> b
b)
    comult :: Vect k (Op b) -> Vect k (Tensor (Op b) (Op b))
comult = Vect k (Tensor (Op b) (Op b)) -> Vect k (Tensor (Op b) (Op b))
forall k b. (Eq k, Num k, Ord b) => Vect k b -> Vect k b
nf (Vect k (Tensor (Op b) (Op b)) -> Vect k (Tensor (Op b) (Op b)))
-> (Vect k (Op b) -> Vect k (Tensor (Op b) (Op b)))
-> Vect k (Op b)
-> Vect k (Tensor (Op b) (Op b))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((b, b) -> Tensor (Op b) (Op b))
-> Vect k (b, b) -> Vect k (Tensor (Op b) (Op b))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\(a :: b
a, b :: b
b) -> (b -> Op b
forall b. b -> Op b
Op b
b, b -> Op b
forall b. b -> Op b
Op b
a)) (Vect k (b, b) -> Vect k (Tensor (Op b) (Op b)))
-> (Vect k (Op b) -> Vect k (b, b))
-> Vect k (Op b)
-> Vect k (Tensor (Op b) (Op b))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Vect k b -> Vect k (b, b)
forall k b. Coalgebra k b => Vect k b -> Vect k (Tensor b b)
comult (Vect k b -> Vect k (b, b))
-> (Vect k (Op b) -> Vect k b) -> Vect k (Op b) -> Vect k (b, b)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Op b -> b) -> Vect k (Op b) -> Vect k b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\(Op b :: b
b) -> b
b) -- ie twist . comult


-- The set coalgebra - can be defined on any set
instance (Eq k, Num k) => Coalgebra k EBasis where
    counit :: Vect k EBasis -> k
counit (V ts :: [(EBasis, k)]
ts) = [k] -> k
forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum [k
x | (ei :: EBasis
ei,x :: k
x) <- [(EBasis, k)]
ts]  -- trace
    comult :: Vect k EBasis -> Vect k (Tensor EBasis EBasis)
comult = (EBasis -> Tensor EBasis EBasis)
-> Vect k EBasis -> Vect k (Tensor EBasis EBasis)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ( \ei :: EBasis
ei -> (EBasis
ei,EBasis
ei) )        -- diagonal

newtype SetCoalgebra b = SC b deriving (SetCoalgebra b -> SetCoalgebra b -> Bool
(SetCoalgebra b -> SetCoalgebra b -> Bool)
-> (SetCoalgebra b -> SetCoalgebra b -> Bool)
-> Eq (SetCoalgebra b)
forall b. Eq b => SetCoalgebra b -> SetCoalgebra b -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: SetCoalgebra b -> SetCoalgebra b -> Bool
$c/= :: forall b. Eq b => SetCoalgebra b -> SetCoalgebra b -> Bool
== :: SetCoalgebra b -> SetCoalgebra b -> Bool
$c== :: forall b. Eq b => SetCoalgebra b -> SetCoalgebra b -> Bool
Eq,Eq (SetCoalgebra b)
Eq (SetCoalgebra b) =>
(SetCoalgebra b -> SetCoalgebra b -> Ordering)
-> (SetCoalgebra b -> SetCoalgebra b -> Bool)
-> (SetCoalgebra b -> SetCoalgebra b -> Bool)
-> (SetCoalgebra b -> SetCoalgebra b -> Bool)
-> (SetCoalgebra b -> SetCoalgebra b -> Bool)
-> (SetCoalgebra b -> SetCoalgebra b -> SetCoalgebra b)
-> (SetCoalgebra b -> SetCoalgebra b -> SetCoalgebra b)
-> Ord (SetCoalgebra b)
SetCoalgebra b -> SetCoalgebra b -> Bool
SetCoalgebra b -> SetCoalgebra b -> Ordering
SetCoalgebra b -> SetCoalgebra b -> SetCoalgebra b
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 b. Ord b => Eq (SetCoalgebra b)
forall b. Ord b => SetCoalgebra b -> SetCoalgebra b -> Bool
forall b. Ord b => SetCoalgebra b -> SetCoalgebra b -> Ordering
forall b.
Ord b =>
SetCoalgebra b -> SetCoalgebra b -> SetCoalgebra b
min :: SetCoalgebra b -> SetCoalgebra b -> SetCoalgebra b
$cmin :: forall b.
Ord b =>
SetCoalgebra b -> SetCoalgebra b -> SetCoalgebra b
max :: SetCoalgebra b -> SetCoalgebra b -> SetCoalgebra b
$cmax :: forall b.
Ord b =>
SetCoalgebra b -> SetCoalgebra b -> SetCoalgebra b
>= :: SetCoalgebra b -> SetCoalgebra b -> Bool
$c>= :: forall b. Ord b => SetCoalgebra b -> SetCoalgebra b -> Bool
> :: SetCoalgebra b -> SetCoalgebra b -> Bool
$c> :: forall b. Ord b => SetCoalgebra b -> SetCoalgebra b -> Bool
<= :: SetCoalgebra b -> SetCoalgebra b -> Bool
$c<= :: forall b. Ord b => SetCoalgebra b -> SetCoalgebra b -> Bool
< :: SetCoalgebra b -> SetCoalgebra b -> Bool
$c< :: forall b. Ord b => SetCoalgebra b -> SetCoalgebra b -> Bool
compare :: SetCoalgebra b -> SetCoalgebra b -> Ordering
$ccompare :: forall b. Ord b => SetCoalgebra b -> SetCoalgebra b -> Ordering
$cp1Ord :: forall b. Ord b => Eq (SetCoalgebra b)
Ord,Int -> SetCoalgebra b -> ShowS
[SetCoalgebra b] -> ShowS
SetCoalgebra b -> [Char]
(Int -> SetCoalgebra b -> ShowS)
-> (SetCoalgebra b -> [Char])
-> ([SetCoalgebra b] -> ShowS)
-> Show (SetCoalgebra b)
forall b. Show b => Int -> SetCoalgebra b -> ShowS
forall b. Show b => [SetCoalgebra b] -> ShowS
forall b. Show b => SetCoalgebra b -> [Char]
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
showList :: [SetCoalgebra b] -> ShowS
$cshowList :: forall b. Show b => [SetCoalgebra b] -> ShowS
show :: SetCoalgebra b -> [Char]
$cshow :: forall b. Show b => SetCoalgebra b -> [Char]
showsPrec :: Int -> SetCoalgebra b -> ShowS
$cshowsPrec :: forall b. Show b => Int -> SetCoalgebra b -> ShowS
Show)

instance (Eq k, Num k) => Coalgebra k (SetCoalgebra b) where
    counit :: Vect k (SetCoalgebra b) -> k
counit (V ts :: [(SetCoalgebra b, k)]
ts) = [k] -> k
forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum [k
x | (m :: SetCoalgebra b
m,x :: k
x) <- [(SetCoalgebra b, k)]
ts]  -- trace
    comult :: Vect k (SetCoalgebra b)
-> Vect k (Tensor (SetCoalgebra b) (SetCoalgebra b))
comult = (SetCoalgebra b -> Tensor (SetCoalgebra b) (SetCoalgebra b))
-> Vect k (SetCoalgebra b)
-> Vect k (Tensor (SetCoalgebra b) (SetCoalgebra b))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ( \m :: SetCoalgebra b
m -> (SetCoalgebra b
m,SetCoalgebra b
m) )          -- diagonal


newtype MonoidCoalgebra m = MC m deriving (MonoidCoalgebra m -> MonoidCoalgebra m -> Bool
(MonoidCoalgebra m -> MonoidCoalgebra m -> Bool)
-> (MonoidCoalgebra m -> MonoidCoalgebra m -> Bool)
-> Eq (MonoidCoalgebra m)
forall m. Eq m => MonoidCoalgebra m -> MonoidCoalgebra m -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: MonoidCoalgebra m -> MonoidCoalgebra m -> Bool
$c/= :: forall m. Eq m => MonoidCoalgebra m -> MonoidCoalgebra m -> Bool
== :: MonoidCoalgebra m -> MonoidCoalgebra m -> Bool
$c== :: forall m. Eq m => MonoidCoalgebra m -> MonoidCoalgebra m -> Bool
Eq,Eq (MonoidCoalgebra m)
Eq (MonoidCoalgebra m) =>
(MonoidCoalgebra m -> MonoidCoalgebra m -> Ordering)
-> (MonoidCoalgebra m -> MonoidCoalgebra m -> Bool)
-> (MonoidCoalgebra m -> MonoidCoalgebra m -> Bool)
-> (MonoidCoalgebra m -> MonoidCoalgebra m -> Bool)
-> (MonoidCoalgebra m -> MonoidCoalgebra m -> Bool)
-> (MonoidCoalgebra m -> MonoidCoalgebra m -> MonoidCoalgebra m)
-> (MonoidCoalgebra m -> MonoidCoalgebra m -> MonoidCoalgebra m)
-> Ord (MonoidCoalgebra m)
MonoidCoalgebra m -> MonoidCoalgebra m -> Bool
MonoidCoalgebra m -> MonoidCoalgebra m -> Ordering
MonoidCoalgebra m -> MonoidCoalgebra m -> MonoidCoalgebra m
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 m. Ord m => Eq (MonoidCoalgebra m)
forall m. Ord m => MonoidCoalgebra m -> MonoidCoalgebra m -> Bool
forall m.
Ord m =>
MonoidCoalgebra m -> MonoidCoalgebra m -> Ordering
forall m.
Ord m =>
MonoidCoalgebra m -> MonoidCoalgebra m -> MonoidCoalgebra m
min :: MonoidCoalgebra m -> MonoidCoalgebra m -> MonoidCoalgebra m
$cmin :: forall m.
Ord m =>
MonoidCoalgebra m -> MonoidCoalgebra m -> MonoidCoalgebra m
max :: MonoidCoalgebra m -> MonoidCoalgebra m -> MonoidCoalgebra m
$cmax :: forall m.
Ord m =>
MonoidCoalgebra m -> MonoidCoalgebra m -> MonoidCoalgebra m
>= :: MonoidCoalgebra m -> MonoidCoalgebra m -> Bool
$c>= :: forall m. Ord m => MonoidCoalgebra m -> MonoidCoalgebra m -> Bool
> :: MonoidCoalgebra m -> MonoidCoalgebra m -> Bool
$c> :: forall m. Ord m => MonoidCoalgebra m -> MonoidCoalgebra m -> Bool
<= :: MonoidCoalgebra m -> MonoidCoalgebra m -> Bool
$c<= :: forall m. Ord m => MonoidCoalgebra m -> MonoidCoalgebra m -> Bool
< :: MonoidCoalgebra m -> MonoidCoalgebra m -> Bool
$c< :: forall m. Ord m => MonoidCoalgebra m -> MonoidCoalgebra m -> Bool
compare :: MonoidCoalgebra m -> MonoidCoalgebra m -> Ordering
$ccompare :: forall m.
Ord m =>
MonoidCoalgebra m -> MonoidCoalgebra m -> Ordering
$cp1Ord :: forall m. Ord m => Eq (MonoidCoalgebra m)
Ord,Int -> MonoidCoalgebra m -> ShowS
[MonoidCoalgebra m] -> ShowS
MonoidCoalgebra m -> [Char]
(Int -> MonoidCoalgebra m -> ShowS)
-> (MonoidCoalgebra m -> [Char])
-> ([MonoidCoalgebra m] -> ShowS)
-> Show (MonoidCoalgebra m)
forall m. Show m => Int -> MonoidCoalgebra m -> ShowS
forall m. Show m => [MonoidCoalgebra m] -> ShowS
forall m. Show m => MonoidCoalgebra m -> [Char]
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
showList :: [MonoidCoalgebra m] -> ShowS
$cshowList :: forall m. Show m => [MonoidCoalgebra m] -> ShowS
show :: MonoidCoalgebra m -> [Char]
$cshow :: forall m. Show m => MonoidCoalgebra m -> [Char]
showsPrec :: Int -> MonoidCoalgebra m -> ShowS
$cshowsPrec :: forall m. Show m => Int -> MonoidCoalgebra m -> ShowS
Show)

instance (Eq k, Num k, Ord m, Mon m) => Coalgebra k (MonoidCoalgebra m) where
    counit :: Vect k (MonoidCoalgebra m) -> k
counit (V ts :: [(MonoidCoalgebra m, k)]
ts) = [k] -> k
forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum [if MonoidCoalgebra m
m MonoidCoalgebra m -> MonoidCoalgebra m -> Bool
forall a. Eq a => a -> a -> Bool
== m -> MonoidCoalgebra m
forall m. m -> MonoidCoalgebra m
MC m
forall m. Mon m => m
munit then k
x else 0 | (m :: MonoidCoalgebra m
m,x :: k
x) <- [(MonoidCoalgebra m, k)]
ts]
    comult :: Vect k (MonoidCoalgebra m)
-> Vect k (Tensor (MonoidCoalgebra m) (MonoidCoalgebra m))
comult = (MonoidCoalgebra m
 -> Vect k (Tensor (MonoidCoalgebra m) (MonoidCoalgebra m)))
-> Vect k (MonoidCoalgebra m)
-> Vect k (Tensor (MonoidCoalgebra m) (MonoidCoalgebra m))
forall k b a.
(Eq k, Num k, Ord b) =>
(a -> Vect k b) -> Vect k a -> Vect k b
linear MonoidCoalgebra m
-> Vect k (Tensor (MonoidCoalgebra m) (MonoidCoalgebra m))
forall m k.
(Mon m, Num k, Eq k, Ord m) =>
MonoidCoalgebra m -> Vect k (MonoidCoalgebra m, MonoidCoalgebra m)
cm
        where cm :: MonoidCoalgebra m -> Vect k (MonoidCoalgebra m, MonoidCoalgebra m)
cm m :: MonoidCoalgebra m
m = if MonoidCoalgebra m
m MonoidCoalgebra m -> MonoidCoalgebra m -> Bool
forall a. Eq a => a -> a -> Bool
== m -> MonoidCoalgebra m
forall m. m -> MonoidCoalgebra m
MC m
forall m. Mon m => m
munit then (MonoidCoalgebra m, MonoidCoalgebra m)
-> Vect k (MonoidCoalgebra m, MonoidCoalgebra m)
forall (m :: * -> *) a. Monad m => a -> m a
return (MonoidCoalgebra m
m,MonoidCoalgebra m
m) else (MonoidCoalgebra m, MonoidCoalgebra m)
-> Vect k (MonoidCoalgebra m, MonoidCoalgebra m)
forall (m :: * -> *) a. Monad m => a -> m a
return (MonoidCoalgebra m
m, m -> MonoidCoalgebra m
forall m. m -> MonoidCoalgebra m
MC m
forall m. Mon m => m
munit) Vect k (MonoidCoalgebra m, MonoidCoalgebra m)
-> Vect k (MonoidCoalgebra m, MonoidCoalgebra m)
-> Vect k (MonoidCoalgebra m, MonoidCoalgebra m)
forall k b.
(Eq k, Num k, Ord b) =>
Vect k b -> Vect k b -> Vect k b
<+> (MonoidCoalgebra m, MonoidCoalgebra m)
-> Vect k (MonoidCoalgebra m, MonoidCoalgebra m)
forall (m :: * -> *) a. Monad m => a -> m a
return (m -> MonoidCoalgebra m
forall m. m -> MonoidCoalgebra m
MC m
forall m. Mon m => m
munit, MonoidCoalgebra m
m)
-- Brzezinski and Wisbauer, Corings and Comodules, p5

-- Both of the above can be used to define coalgebra structure on polynomial algebras
-- by using the definitions above on the generators (ie the indeterminates) and then extending multiplicatively
-- They are then guaranteed to be algebra morphisms?


-- MODULES AND COMODULES

class Algebra k a => Module k a m where
    action :: Vect k (Tensor a m) -> Vect k m

r :: Vect k a
r *. :: Vect k a -> Vect k m -> Vect k m
*. m :: Vect k m
m = Vect k (Tensor a m) -> Vect k m
forall k a m. Module k a m => Vect k (Tensor a m) -> Vect k m
action (Vect k a
r Vect k a -> Vect k m -> Vect k (Tensor a m)
forall k a b. Num k => Vect k a -> Vect k b -> Vect k (Tensor a b)
`te` Vect k m
m)

class Coalgebra k c => Comodule k c n where
    coaction :: Vect k n -> Vect k (Tensor c n)


instance Algebra k a => Module k a a where
    action :: Vect k (Tensor a a) -> Vect k a
action = Vect k (Tensor a a) -> Vect k a
forall k b. Algebra k b => Vect k (Tensor b b) -> Vect k b
mult

instance Coalgebra k c => Comodule k c c where
    coaction :: Vect k c -> Vect k (Tensor c c)
coaction = Vect k c -> Vect k (Tensor c c)
forall k b. Coalgebra k b => Vect k b -> Vect k (Tensor b b)
comult

-- module and comodule instances for tensor products

-- Kassel p57-8

instance (Eq k, Num k, Ord a, Ord u, Ord v, Algebra k a, Module k a u, Module k a v)
         => Module k (Tensor a a) (Tensor u v) where
    -- action x = nf $ x >>= action'
    action :: Vect k (Tensor (Tensor a a) (Tensor u v)) -> Vect k (Tensor u v)
action = (Tensor (Tensor a a) (Tensor u v) -> Vect k (Tensor u v))
-> Vect k (Tensor (Tensor a a) (Tensor u v)) -> Vect k (Tensor u v)
forall k b a.
(Eq k, Num k, Ord b) =>
(a -> Vect k b) -> Vect k a -> Vect k b
linear Tensor (Tensor a a) (Tensor u v) -> Vect k (Tensor u v)
forall k a a a b.
(Num k, Module k a a, Module k a b) =>
((a, a), (a, b)) -> Vect k (a, b)
action'
        where action' :: ((a, a), (a, b)) -> Vect k (a, b)
action' ((a :: a
a,a' :: a
a'), (u :: a
u,v :: b
v)) = (Vect k (Tensor a a) -> Vect k a
forall k a m. Module k a m => Vect k (Tensor a m) -> Vect k m
action (Vect k (Tensor a a) -> Vect k a)
-> Vect k (Tensor a a) -> Vect k a
forall a b. (a -> b) -> a -> b
$ Tensor a a -> Vect k (Tensor a a)
forall (m :: * -> *) a. Monad m => a -> m a
return (a
a,a
u)) Vect k a -> Vect k b -> Vect k (a, b)
forall k a b. Num k => Vect k a -> Vect k b -> Vect k (Tensor a b)
`te` (Vect k (Tensor a b) -> Vect k b
forall k a m. Module k a m => Vect k (Tensor a m) -> Vect k m
action (Vect k (Tensor a b) -> Vect k b)
-> Vect k (Tensor a b) -> Vect k b
forall a b. (a -> b) -> a -> b
$ Tensor a b -> Vect k (Tensor a b)
forall (m :: * -> *) a. Monad m => a -> m a
return (a
a',b
v))

instance (Eq k, Num k, Ord a, Ord u, Ord v, Bialgebra k a, Module k a u, Module k a v)
         => Module k a (Tensor u v) where
    -- action x = nf $ x >>= action'
    action :: Vect k (Tensor a (Tensor u v)) -> Vect k (Tensor u v)
action = (Tensor a (Tensor u v) -> Vect k (Tensor u v))
-> Vect k (Tensor a (Tensor u v)) -> Vect k (Tensor u v)
forall k b a.
(Eq k, Num k, Ord b) =>
(a -> Vect k b) -> Vect k a -> Vect k b
linear Tensor a (Tensor u v) -> Vect k (Tensor u v)
forall k b a b.
(Num k, Ord b, Ord a, Ord b, Module k b a, Module k b b,
 Coalgebra k b, Eq k) =>
(b, (a, b)) -> Vect k (a, b)
action'
        where action' :: (b, (a, b)) -> Vect k (a, b)
action' (a :: b
a,(u :: a
u,v :: b
v)) = Vect k (Tensor (Tensor b b) (a, b)) -> Vect k (a, b)
forall k a m. Module k a m => Vect k (Tensor a m) -> Vect k m
action (Vect k (Tensor (Tensor b b) (a, b)) -> Vect k (a, b))
-> Vect k (Tensor (Tensor b b) (a, b)) -> Vect k (a, b)
forall a b. (a -> b) -> a -> b
$ (Vect k b -> Vect k (Tensor b b)
forall k b. Coalgebra k b => Vect k b -> Vect k (Tensor b b)
comult (Vect k b -> Vect k (Tensor b b))
-> Vect k b -> Vect k (Tensor b b)
forall a b. (a -> b) -> a -> b
$ b -> Vect k b
forall (m :: * -> *) a. Monad m => a -> m a
return b
a) Vect k (Tensor b b)
-> Vect k (a, b) -> Vect k (Tensor (Tensor b b) (a, b))
forall k a b. Num k => Vect k a -> Vect k b -> Vect k (Tensor a b)
`te` ((a, b) -> Vect k (a, b)
forall (m :: * -> *) a. Monad m => a -> m a
return (a
u,b
v))
-- !! Overlapping instances
-- If a == Tensor b b, then we have overlapping instance with the previous definition
-- On the other hand, if a == Tensor u v, then we have overlapping instance with the earlier instance

-- Kassel p63
instance (Eq k, Num k, Ord a, Ord m, Ord n, Bialgebra k a, Comodule k a m, Comodule k a n)
         => Comodule k a (Tensor m n) where
    coaction :: Vect k (Tensor m n) -> Vect k (Tensor a (Tensor m n))
coaction = (Vect k (Tensor a a) -> Vect k a
forall k b. Algebra k b => Vect k (Tensor b b) -> Vect k b
mult (Vect k (Tensor a a) -> Vect k a)
-> (Vect k (Tensor m n) -> Vect k (Tensor m n))
-> Vect k (Tensor (Tensor a a) (Tensor m n))
-> Vect k (Tensor a (Tensor m n))
forall k a' b' a b.
(Eq k, Num k, Ord a', Ord b') =>
(Vect k a -> Vect k a')
-> (Vect k b -> Vect k b')
-> Vect k (Tensor a b)
-> Vect k (Tensor a' b')
`tf` Vect k (Tensor m n) -> Vect k (Tensor m n)
forall a. a -> a
id) (Vect k (Tensor (Tensor a a) (Tensor m n))
 -> Vect k (Tensor a (Tensor m n)))
-> (Vect k (Tensor m n)
    -> Vect k (Tensor (Tensor a a) (Tensor m n)))
-> Vect k (Tensor m n)
-> Vect k (Tensor a (Tensor m n))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Vect k ((a, m), (a, n))
-> Vect k (Tensor (Tensor a a) (Tensor m n))
forall k a b a b.
(Num k, Ord a, Ord b, Ord a, Ord b, Eq k) =>
Vect k ((a, a), (b, b)) -> Vect k ((a, b), (a, b))
twistm (Vect k ((a, m), (a, n))
 -> Vect k (Tensor (Tensor a a) (Tensor m n)))
-> (Vect k (Tensor m n) -> Vect k ((a, m), (a, n)))
-> Vect k (Tensor m n)
-> Vect k (Tensor (Tensor a a) (Tensor m n))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Vect k m -> Vect k (a, m)
forall k c n. Comodule k c n => Vect k n -> Vect k (Tensor c n)
coaction (Vect k m -> Vect k (a, m))
-> (Vect k n -> Vect k (a, n))
-> Vect k (Tensor m n)
-> Vect k ((a, m), (a, n))
forall k a' b' a b.
(Eq k, Num k, Ord a', Ord b') =>
(Vect k a -> Vect k a')
-> (Vect k b -> Vect k b')
-> Vect k (Tensor a b)
-> Vect k (Tensor a' b')
`tf` Vect k n -> Vect k (a, n)
forall k c n. Comodule k c n => Vect k n -> Vect k (Tensor c n)
coaction)
        where twistm :: Vect k ((a, a), (b, b)) -> Vect k ((a, b), (a, b))
twistm x :: Vect k ((a, a), (b, b))
x = Vect k ((a, b), (a, b)) -> Vect k ((a, b), (a, b))
forall k b. (Eq k, Num k, Ord b) => Vect k b -> Vect k b
nf (Vect k ((a, b), (a, b)) -> Vect k ((a, b), (a, b)))
-> Vect k ((a, b), (a, b)) -> Vect k ((a, b), (a, b))
forall a b. (a -> b) -> a -> b
$ (((a, a), (b, b)) -> ((a, b), (a, b)))
-> Vect k ((a, a), (b, b)) -> Vect k ((a, b), (a, b))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ( \((h :: a
h,m :: a
m), (h' :: b
h',n :: b
n)) -> ((a
h,b
h'), (a
m,b
n)) ) Vect k ((a, a), (b, b))
x


-- PAIRINGS

-- |A pairing is a non-degenerate bilinear form U x V -> k.
-- We are typically interested in pairings having additional properties. For example:
--
-- * A bialgebra pairing is a pairing between bialgebras A and B such that the mult in A is adjoint to the comult in B, and vice versa, and the unit in A is adjoint to the counit in B, and vice versa.
--
-- * A Hopf pairing is a bialgebra pairing between Hopf algebras A and B such that the antipodes in A and B are adjoint.
class HasPairing k u v where
    pairing :: Vect k (Tensor u v) -> Vect k ()

-- |The pairing function with a more Haskellish type signature
pairing' :: (Num k, HasPairing k u v) => Vect k u -> Vect k v -> k
pairing' :: Vect k u -> Vect k v -> k
pairing' u :: Vect k u
u v :: Vect k v
v = Vect k () -> k
forall k. Num k => Vect k () -> k
unwrap (Vect k (Tensor u v) -> Vect k ()
forall k u v. HasPairing k u v => Vect k (Tensor u v) -> Vect k ()
pairing (Vect k u
u Vect k u -> Vect k v -> Vect k (Tensor u v)
forall k a b. Num k => Vect k a -> Vect k b -> Vect k (Tensor a b)
`te` Vect k v
v))

instance (Eq k, Num k) => HasPairing k () () where
    pairing :: Vect k (Tensor () ()) -> Vect k ()
pairing = Vect k (Tensor () ()) -> Vect k ()
forall k b. Algebra k b => Vect k (Tensor b b) -> Vect k b
mult

instance (Eq k, Num k, HasPairing k u v, HasPairing k u' v') => HasPairing k (Tensor u u') (Tensor v v') where
    pairing :: Vect k (Tensor (Tensor u u') (Tensor v v')) -> Vect k ()
pairing = Vect k (Tensor () ()) -> Vect k ()
forall k b. Algebra k b => Vect k (Tensor b b) -> Vect k b
mult (Vect k (Tensor () ()) -> Vect k ())
-> (Vect k (Tensor (Tensor u u') (Tensor v v'))
    -> Vect k (Tensor () ()))
-> Vect k (Tensor (Tensor u u') (Tensor v v'))
-> Vect k ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Vect k (Tensor u v) -> Vect k ()
forall k u v. HasPairing k u v => Vect k (Tensor u v) -> Vect k ()
pairing (Vect k (Tensor u v) -> Vect k ())
-> (Vect k (Tensor u' v') -> Vect k ())
-> Vect k (Tensor (Tensor u v) (Tensor u' v'))
-> Vect k (Tensor () ())
forall k a' b' a b.
(Eq k, Num k, Ord a', Ord b') =>
(Vect k a -> Vect k a')
-> (Vect k b -> Vect k b')
-> Vect k (Tensor a b)
-> Vect k (Tensor a' b')
`tf` Vect k (Tensor u' v') -> Vect k ()
forall k u v. HasPairing k u v => Vect k (Tensor u v) -> Vect k ()
pairing) (Vect k (Tensor (Tensor u v) (Tensor u' v'))
 -> Vect k (Tensor () ()))
-> (Vect k (Tensor (Tensor u u') (Tensor v v'))
    -> Vect k (Tensor (Tensor u v) (Tensor u' v')))
-> Vect k (Tensor (Tensor u u') (Tensor v v'))
-> Vect k (Tensor () ())
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Tensor (Tensor u u') (Tensor v v')
 -> Tensor (Tensor u v) (Tensor u' v'))
-> Vect k (Tensor (Tensor u u') (Tensor v v'))
-> Vect k (Tensor (Tensor u v) (Tensor u' v'))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\((u :: u
u,u' :: u'
u'),(v :: v
v,v' :: v'
v')) -> ((u
u,v
v),(u'
u',v'
v')))
    -- pairing = fmap (\((),()) -> ()) . (pairing `tf` pairing) . fmap (\((u,u'),(v,v')) -> ((u,v),(u',v')))