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

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

-- |A module defining the tensor algebra, symmetric algebra, exterior (or alternating) algebra, and tensor coalgebra
module Math.Algebras.TensorAlgebra where

import Prelude hiding ( (*>) )

import qualified Data.List as L

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

import Math.Algebra.Field.Base


-- TENSOR ALGEBRA

-- |A data type representing basis elements of the tensor algebra over a set\/type.
-- Elements of the tensor algebra are linear combinations of iterated tensor products of elements of the set\/type.
-- If V = Vect k a is the free vector space over a, then the tensor algebra T(V) = Vect k (TensorAlgebra a) is isomorphic
-- to the infinite direct sum:
--
-- T(V) = k ⊕ V ⊕ V⊗V ⊕ V⊗V⊗V ⊕ ...
data TensorAlgebra a = TA Int [a] deriving (TensorAlgebra a -> TensorAlgebra a -> Bool
(TensorAlgebra a -> TensorAlgebra a -> Bool)
-> (TensorAlgebra a -> TensorAlgebra a -> Bool)
-> Eq (TensorAlgebra a)
forall a. Eq a => TensorAlgebra a -> TensorAlgebra a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: TensorAlgebra a -> TensorAlgebra a -> Bool
$c/= :: forall a. Eq a => TensorAlgebra a -> TensorAlgebra a -> Bool
== :: TensorAlgebra a -> TensorAlgebra a -> Bool
$c== :: forall a. Eq a => TensorAlgebra a -> TensorAlgebra a -> Bool
Eq,Eq (TensorAlgebra a)
Eq (TensorAlgebra a) =>
(TensorAlgebra a -> TensorAlgebra a -> Ordering)
-> (TensorAlgebra a -> TensorAlgebra a -> Bool)
-> (TensorAlgebra a -> TensorAlgebra a -> Bool)
-> (TensorAlgebra a -> TensorAlgebra a -> Bool)
-> (TensorAlgebra a -> TensorAlgebra a -> Bool)
-> (TensorAlgebra a -> TensorAlgebra a -> TensorAlgebra a)
-> (TensorAlgebra a -> TensorAlgebra a -> TensorAlgebra a)
-> Ord (TensorAlgebra a)
TensorAlgebra a -> TensorAlgebra a -> Bool
TensorAlgebra a -> TensorAlgebra a -> Ordering
TensorAlgebra a -> TensorAlgebra a -> TensorAlgebra a
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 a. Ord a => Eq (TensorAlgebra a)
forall a. Ord a => TensorAlgebra a -> TensorAlgebra a -> Bool
forall a. Ord a => TensorAlgebra a -> TensorAlgebra a -> Ordering
forall a.
Ord a =>
TensorAlgebra a -> TensorAlgebra a -> TensorAlgebra a
min :: TensorAlgebra a -> TensorAlgebra a -> TensorAlgebra a
$cmin :: forall a.
Ord a =>
TensorAlgebra a -> TensorAlgebra a -> TensorAlgebra a
max :: TensorAlgebra a -> TensorAlgebra a -> TensorAlgebra a
$cmax :: forall a.
Ord a =>
TensorAlgebra a -> TensorAlgebra a -> TensorAlgebra a
>= :: TensorAlgebra a -> TensorAlgebra a -> Bool
$c>= :: forall a. Ord a => TensorAlgebra a -> TensorAlgebra a -> Bool
> :: TensorAlgebra a -> TensorAlgebra a -> Bool
$c> :: forall a. Ord a => TensorAlgebra a -> TensorAlgebra a -> Bool
<= :: TensorAlgebra a -> TensorAlgebra a -> Bool
$c<= :: forall a. Ord a => TensorAlgebra a -> TensorAlgebra a -> Bool
< :: TensorAlgebra a -> TensorAlgebra a -> Bool
$c< :: forall a. Ord a => TensorAlgebra a -> TensorAlgebra a -> Bool
compare :: TensorAlgebra a -> TensorAlgebra a -> Ordering
$ccompare :: forall a. Ord a => TensorAlgebra a -> TensorAlgebra a -> Ordering
$cp1Ord :: forall a. Ord a => Eq (TensorAlgebra a)
Ord)

instance Show a => Show (TensorAlgebra a) where
    show :: TensorAlgebra a -> String
show (TA _ []) = "1"
    show (TA _ xs :: [a]
xs) = (Char -> Bool) -> ShowS
forall a. (a -> Bool) -> [a] -> [a]
filter (Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
/= '"') ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ [String] -> String
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$ String -> [String] -> [String]
forall a. a -> [a] -> [a]
L.intersperse "*" ([String] -> [String]) -> [String] -> [String]
forall a b. (a -> b) -> a -> b
$ (a -> String) -> [a] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map a -> String
forall a. Show a => a -> String
show [a]
xs
    -- show (TA _ xs) = filter (/= '"') $ concat $ L.intersperse "\x2297" $ map show xs


instance Mon (TensorAlgebra a) where
    munit :: TensorAlgebra a
munit = Int -> [a] -> TensorAlgebra a
forall a. Int -> [a] -> TensorAlgebra a
TA 0 []
    mmult :: TensorAlgebra a -> TensorAlgebra a -> TensorAlgebra a
mmult (TA i :: Int
i xs :: [a]
xs) (TA j :: Int
j ys :: [a]
ys) = Int -> [a] -> TensorAlgebra a
forall a. Int -> [a] -> TensorAlgebra a
TA (Int
iInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
j) ([a]
xs[a] -> [a] -> [a]
forall a. [a] -> [a] -> [a]
++[a]
ys)

instance (Eq k, Num k, Ord a) => Algebra k (TensorAlgebra a) where
    unit :: k -> Vect k (TensorAlgebra a)
unit x :: k
x = k
x k -> Vect k (TensorAlgebra a) -> Vect k (TensorAlgebra a)
forall k b. (Eq k, Num k) => k -> Vect k b -> Vect k b
*> TensorAlgebra a -> Vect k (TensorAlgebra a)
forall (m :: * -> *) a. Monad m => a -> m a
return TensorAlgebra a
forall m. Mon m => m
munit
    mult :: Vect k (Tensor (TensorAlgebra a) (TensorAlgebra a))
-> Vect k (TensorAlgebra a)
mult = Vect k (TensorAlgebra a) -> Vect k (TensorAlgebra a)
forall k b. (Eq k, Num k, Ord b) => Vect k b -> Vect k b
nf (Vect k (TensorAlgebra a) -> Vect k (TensorAlgebra a))
-> (Vect k (Tensor (TensorAlgebra a) (TensorAlgebra a))
    -> Vect k (TensorAlgebra a))
-> Vect k (Tensor (TensorAlgebra a) (TensorAlgebra a))
-> Vect k (TensorAlgebra a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Tensor (TensorAlgebra a) (TensorAlgebra a) -> TensorAlgebra a)
-> Vect k (Tensor (TensorAlgebra a) (TensorAlgebra a))
-> Vect k (TensorAlgebra a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\(a :: TensorAlgebra a
a,b :: TensorAlgebra a
b) -> TensorAlgebra a
a TensorAlgebra a -> TensorAlgebra a -> TensorAlgebra a
forall m. Mon m => m -> m -> m
`mmult` TensorAlgebra a
b)

-- The tensor algebra is the free algebra. It has the following universal property:
-- Given f :: a -> Vect k b, where Vect k b is an algebra
-- (which induces a vector space morphism, linear f :: Vect k a -> Vect k b)
-- then we can lift to an algebra morphism, (liftTA f) :: Vect k (TensorAlgebra a) -> Vect k b
-- with (liftTA f) . linear injectTA = linear f

-- |Inject an element of the free vector space V = Vect k a into the tensor algebra T(V) = Vect k (TensorAlgebra a)
injectTA :: Num k => Vect k a -> Vect k (TensorAlgebra a)
injectTA :: Vect k a -> Vect k (TensorAlgebra a)
injectTA = (a -> TensorAlgebra a) -> Vect k a -> Vect k (TensorAlgebra a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\a :: a
a -> Int -> [a] -> TensorAlgebra a
forall a. Int -> [a] -> TensorAlgebra a
TA 1 [a
a])
-- The Num k context is not strictly necessary

-- |Inject an element of the set\/type A\/a into the tensor algebra T(A) = Vect k (TensorAlgebra a).
injectTA' :: (Eq k, Num k) => a -> Vect k (TensorAlgebra a)
injectTA' :: a -> Vect k (TensorAlgebra a)
injectTA' = Vect k a -> Vect k (TensorAlgebra a)
forall k a. Num k => Vect k a -> Vect k (TensorAlgebra a)
injectTA (Vect k a -> Vect k (TensorAlgebra a))
-> (a -> Vect k a) -> a -> Vect k (TensorAlgebra a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Vect k a
forall (m :: * -> *) a. Monad m => a -> m a
return
-- injectTA' a = return (TA 1 [a])

-- |Given vector spaces A = Vect k a, B = Vect k b, where B is also an algebra,
-- lift a linear map f: A -> B to an algebra morphism f': T(A) -> B,
-- where T(A) is the tensor algebra Vect k (TensorAlgebra a).
-- f' will agree with f on A itself (considered as a subspace of T(A)).
-- In other words, f = f' . injectTA
liftTA :: (Eq k, Num k, Ord b, Show b, Algebra k b) =>
     (Vect k a -> Vect k b) -> Vect k (TensorAlgebra a) -> Vect k b
liftTA :: (Vect k a -> Vect k b) -> Vect k (TensorAlgebra a) -> Vect k b
liftTA f :: Vect k a -> Vect k b
f = (TensorAlgebra a -> Vect k b)
-> Vect k (TensorAlgebra a) -> Vect k b
forall k b a.
(Eq k, Num k, Ord b) =>
(a -> Vect k b) -> Vect k a -> Vect k b
linear (\(TA _ xs :: [a]
xs) -> [Vect k b] -> Vect k b
forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
product [Vect k a -> Vect k b
f (a -> Vect k a
forall (m :: * -> *) a. Monad m => a -> m a
return a
x) | a
x <- [a]
xs])
-- The Show b constraint is required because we use product (and Num requires Show)!!

-- |Given a set\/type A\/a, and a vector space B = Vect k b, where B is also an algebra,
-- lift a function f: A -> B to an algebra morphism f': T(A) -> B.
-- f' will agree with f on A itself. In other words, f = f' . injectTA'
liftTA' :: (Eq k, Num k, Ord b, Show b, Algebra k b) =>
     (a -> Vect k b) -> Vect k (TensorAlgebra a) -> Vect k b
liftTA' :: (a -> Vect k b) -> Vect k (TensorAlgebra a) -> Vect k b
liftTA' = (Vect k a -> Vect k b) -> Vect k (TensorAlgebra a) -> Vect k b
forall k b a.
(Eq k, Num k, Ord b, Show b, Algebra k b) =>
(Vect k a -> Vect k b) -> Vect k (TensorAlgebra a) -> Vect k b
liftTA ((Vect k a -> Vect k b) -> Vect k (TensorAlgebra a) -> Vect k b)
-> ((a -> Vect k b) -> Vect k a -> Vect k b)
-> (a -> Vect k b)
-> Vect k (TensorAlgebra a)
-> Vect k b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> Vect k b) -> Vect k a -> Vect k b
forall k b a.
(Eq k, Num k, Ord b) =>
(a -> Vect k b) -> Vect k a -> Vect k b
linear
-- liftTA' f = linear (\(TA _ xs) -> product [f x | x <- xs])
-- The second version might be more efficient


-- |Tensor algebra is a functor from k-Vect to k-Alg.
-- The action on objects is Vect k a -> Vect k (TensorAlgebra a).
-- The action on arrows is f -> fmapTA f.
fmapTA :: (Eq k, Num k, Ord b, Show b) =>
    (Vect k a -> Vect k b) -> Vect k (TensorAlgebra a) -> Vect k (TensorAlgebra b)
fmapTA :: (Vect k a -> Vect k b)
-> Vect k (TensorAlgebra a) -> Vect k (TensorAlgebra b)
fmapTA f :: Vect k a -> Vect k b
f = (Vect k a -> Vect k (TensorAlgebra b))
-> Vect k (TensorAlgebra a) -> Vect k (TensorAlgebra b)
forall k b a.
(Eq k, Num k, Ord b, Show b, Algebra k b) =>
(Vect k a -> Vect k b) -> Vect k (TensorAlgebra a) -> Vect k b
liftTA (Vect k b -> Vect k (TensorAlgebra b)
forall k a. Num k => Vect k a -> Vect k (TensorAlgebra a)
injectTA (Vect k b -> Vect k (TensorAlgebra b))
-> (Vect k a -> Vect k b) -> Vect k a -> Vect k (TensorAlgebra b)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Vect k a -> Vect k b
f)
-- fmapTA f = linear (\(TA _ xs) -> product [injectTA (f (return x)) | x <- xs])

-- |If we compose the free vector space functor Set -> k-Vect with the tensor algebra functor k-Vect -> k-Alg,
-- we obtain a functor Set -> k-Alg, the free algebra functor.
-- The action on objects is a -> Vect k (TensorAlgebra a).
-- The action on arrows is f -> fmapTA' f.
fmapTA' :: (Eq k, Num k, Ord b, Show b) =>
    (a -> b) -> Vect k (TensorAlgebra a) -> Vect k (TensorAlgebra b)
fmapTA' :: (a -> b) -> Vect k (TensorAlgebra a) -> Vect k (TensorAlgebra b)
fmapTA' = (Vect k a -> Vect k b)
-> Vect k (TensorAlgebra a) -> Vect k (TensorAlgebra b)
forall k b a.
(Eq k, Num k, Ord b, Show b) =>
(Vect k a -> Vect k b)
-> Vect k (TensorAlgebra a) -> Vect k (TensorAlgebra b)
fmapTA ((Vect k a -> Vect k b)
 -> Vect k (TensorAlgebra a) -> Vect k (TensorAlgebra b))
-> ((a -> b) -> Vect k a -> Vect k b)
-> (a -> b)
-> Vect k (TensorAlgebra a)
-> Vect k (TensorAlgebra b)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> b) -> Vect k a -> Vect k b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap
-- fmapTA' f = liftTA' (injectTA' . f)
-- fmapTA' f = linear (\(TA _ xs) -> product [injectTA' (f x) | x <- xs])


bindTA :: (Eq k, Num k, Ord b, Show b) =>
    Vect k (TensorAlgebra a) -> (Vect k a -> Vect k (TensorAlgebra b)) -> Vect k (TensorAlgebra b)
bindTA :: Vect k (TensorAlgebra a)
-> (Vect k a -> Vect k (TensorAlgebra b))
-> Vect k (TensorAlgebra b)
bindTA = ((Vect k a -> Vect k (TensorAlgebra b))
 -> Vect k (TensorAlgebra a) -> Vect k (TensorAlgebra b))
-> Vect k (TensorAlgebra a)
-> (Vect k a -> Vect k (TensorAlgebra b))
-> Vect k (TensorAlgebra b)
forall a b c. (a -> b -> c) -> b -> a -> c
flip (Vect k a -> Vect k (TensorAlgebra b))
-> Vect k (TensorAlgebra a) -> Vect k (TensorAlgebra b)
forall k b a.
(Eq k, Num k, Ord b, Show b, Algebra k b) =>
(Vect k a -> Vect k b) -> Vect k (TensorAlgebra a) -> Vect k b
liftTA

bindTA' :: (Eq k, Num k, Ord b, Show b) =>
    Vect k (TensorAlgebra a) -> (a -> Vect k (TensorAlgebra b)) -> Vect k (TensorAlgebra b)
bindTA' :: Vect k (TensorAlgebra a)
-> (a -> Vect k (TensorAlgebra b)) -> Vect k (TensorAlgebra b)
bindTA' = ((a -> Vect k (TensorAlgebra b))
 -> Vect k (TensorAlgebra a) -> Vect k (TensorAlgebra b))
-> Vect k (TensorAlgebra a)
-> (a -> Vect k (TensorAlgebra b))
-> Vect k (TensorAlgebra b)
forall a b c. (a -> b -> c) -> b -> a -> c
flip (a -> Vect k (TensorAlgebra b))
-> Vect k (TensorAlgebra a) -> Vect k (TensorAlgebra b)
forall k b a.
(Eq k, Num k, Ord b, Show b, Algebra k b) =>
(a -> Vect k b) -> Vect k (TensorAlgebra a) -> Vect k b
liftTA'
-- Another way to think about this is variable substitution

-- "The algebra is free until we bind it"


-- SYMMETRIC ALGEBRA

-- |A data type representing basis elements of the symmetric algebra over a set\/type.
-- The symmetric algebra is the quotient of the tensor algebra by
-- the ideal generated by all
-- differences of products u&#x2297;v - v&#x2297;u.
data SymmetricAlgebra a = Sym Int [a] deriving (SymmetricAlgebra a -> SymmetricAlgebra a -> Bool
(SymmetricAlgebra a -> SymmetricAlgebra a -> Bool)
-> (SymmetricAlgebra a -> SymmetricAlgebra a -> Bool)
-> Eq (SymmetricAlgebra a)
forall a. Eq a => SymmetricAlgebra a -> SymmetricAlgebra a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: SymmetricAlgebra a -> SymmetricAlgebra a -> Bool
$c/= :: forall a. Eq a => SymmetricAlgebra a -> SymmetricAlgebra a -> Bool
== :: SymmetricAlgebra a -> SymmetricAlgebra a -> Bool
$c== :: forall a. Eq a => SymmetricAlgebra a -> SymmetricAlgebra a -> Bool
Eq,Eq (SymmetricAlgebra a)
Eq (SymmetricAlgebra a) =>
(SymmetricAlgebra a -> SymmetricAlgebra a -> Ordering)
-> (SymmetricAlgebra a -> SymmetricAlgebra a -> Bool)
-> (SymmetricAlgebra a -> SymmetricAlgebra a -> Bool)
-> (SymmetricAlgebra a -> SymmetricAlgebra a -> Bool)
-> (SymmetricAlgebra a -> SymmetricAlgebra a -> Bool)
-> (SymmetricAlgebra a -> SymmetricAlgebra a -> SymmetricAlgebra a)
-> (SymmetricAlgebra a -> SymmetricAlgebra a -> SymmetricAlgebra a)
-> Ord (SymmetricAlgebra a)
SymmetricAlgebra a -> SymmetricAlgebra a -> Bool
SymmetricAlgebra a -> SymmetricAlgebra a -> Ordering
SymmetricAlgebra a -> SymmetricAlgebra a -> SymmetricAlgebra a
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 a. Ord a => Eq (SymmetricAlgebra a)
forall a. Ord a => SymmetricAlgebra a -> SymmetricAlgebra a -> Bool
forall a.
Ord a =>
SymmetricAlgebra a -> SymmetricAlgebra a -> Ordering
forall a.
Ord a =>
SymmetricAlgebra a -> SymmetricAlgebra a -> SymmetricAlgebra a
min :: SymmetricAlgebra a -> SymmetricAlgebra a -> SymmetricAlgebra a
$cmin :: forall a.
Ord a =>
SymmetricAlgebra a -> SymmetricAlgebra a -> SymmetricAlgebra a
max :: SymmetricAlgebra a -> SymmetricAlgebra a -> SymmetricAlgebra a
$cmax :: forall a.
Ord a =>
SymmetricAlgebra a -> SymmetricAlgebra a -> SymmetricAlgebra a
>= :: SymmetricAlgebra a -> SymmetricAlgebra a -> Bool
$c>= :: forall a. Ord a => SymmetricAlgebra a -> SymmetricAlgebra a -> Bool
> :: SymmetricAlgebra a -> SymmetricAlgebra a -> Bool
$c> :: forall a. Ord a => SymmetricAlgebra a -> SymmetricAlgebra a -> Bool
<= :: SymmetricAlgebra a -> SymmetricAlgebra a -> Bool
$c<= :: forall a. Ord a => SymmetricAlgebra a -> SymmetricAlgebra a -> Bool
< :: SymmetricAlgebra a -> SymmetricAlgebra a -> Bool
$c< :: forall a. Ord a => SymmetricAlgebra a -> SymmetricAlgebra a -> Bool
compare :: SymmetricAlgebra a -> SymmetricAlgebra a -> Ordering
$ccompare :: forall a.
Ord a =>
SymmetricAlgebra a -> SymmetricAlgebra a -> Ordering
$cp1Ord :: forall a. Ord a => Eq (SymmetricAlgebra a)
Ord)

instance Show a => Show (SymmetricAlgebra a) where
    show :: SymmetricAlgebra a -> String
show (Sym _ []) = "1"
    show (Sym _ xs :: [a]
xs) = (Char -> Bool) -> ShowS
forall a. (a -> Bool) -> [a] -> [a]
filter (Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
/= '"') ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ [String] -> String
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$ String -> [String] -> [String]
forall a. a -> [a] -> [a]
L.intersperse "." ([String] -> [String]) -> [String] -> [String]
forall a b. (a -> b) -> a -> b
$ (a -> String) -> [a] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map a -> String
forall a. Show a => a -> String
show [a]
xs

instance Ord a => Mon (SymmetricAlgebra a) where
    munit :: SymmetricAlgebra a
munit = Int -> [a] -> SymmetricAlgebra a
forall a. Int -> [a] -> SymmetricAlgebra a
Sym 0 []
    mmult :: SymmetricAlgebra a -> SymmetricAlgebra a -> SymmetricAlgebra a
mmult (Sym i :: Int
i xs :: [a]
xs) (Sym j :: Int
j ys :: [a]
ys) = Int -> [a] -> SymmetricAlgebra a
forall a. Int -> [a] -> SymmetricAlgebra a
Sym (Int
iInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
j) ([a] -> SymmetricAlgebra a) -> [a] -> SymmetricAlgebra a
forall a b. (a -> b) -> a -> b
$ [a] -> [a]
forall a. Ord a => [a] -> [a]
L.sort ([a]
xs[a] -> [a] -> [a]
forall a. [a] -> [a] -> [a]
++[a]
ys)

instance (Eq k, Num k, Ord a) => Algebra k (SymmetricAlgebra a) where
    unit :: k -> Vect k (SymmetricAlgebra a)
unit x :: k
x = k
x k -> Vect k (SymmetricAlgebra a) -> Vect k (SymmetricAlgebra a)
forall k b. (Eq k, Num k) => k -> Vect k b -> Vect k b
*> SymmetricAlgebra a -> Vect k (SymmetricAlgebra a)
forall (m :: * -> *) a. Monad m => a -> m a
return SymmetricAlgebra a
forall m. Mon m => m
munit
    mult :: Vect k (Tensor (SymmetricAlgebra a) (SymmetricAlgebra a))
-> Vect k (SymmetricAlgebra a)
mult = Vect k (SymmetricAlgebra a) -> Vect k (SymmetricAlgebra a)
forall k b. (Eq k, Num k, Ord b) => Vect k b -> Vect k b
nf (Vect k (SymmetricAlgebra a) -> Vect k (SymmetricAlgebra a))
-> (Vect k (Tensor (SymmetricAlgebra a) (SymmetricAlgebra a))
    -> Vect k (SymmetricAlgebra a))
-> Vect k (Tensor (SymmetricAlgebra a) (SymmetricAlgebra a))
-> Vect k (SymmetricAlgebra a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Tensor (SymmetricAlgebra a) (SymmetricAlgebra a)
 -> SymmetricAlgebra a)
-> Vect k (Tensor (SymmetricAlgebra a) (SymmetricAlgebra a))
-> Vect k (SymmetricAlgebra a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\(a :: SymmetricAlgebra a
a,b :: SymmetricAlgebra a
b) -> SymmetricAlgebra a
a SymmetricAlgebra a -> SymmetricAlgebra a -> SymmetricAlgebra a
forall m. Mon m => m -> m -> m
`mmult` SymmetricAlgebra a
b)

-- |Algebra morphism from tensor algebra to symmetric algebra.
-- The kernel of the morphism is the ideal generated by all
-- differences of products u&#x2297;v - v&#x2297;u.
toSym :: (Eq k, Num k, Ord a) =>
     Vect k (TensorAlgebra a) -> Vect k (SymmetricAlgebra a)
toSym :: Vect k (TensorAlgebra a) -> Vect k (SymmetricAlgebra a)
toSym = (TensorAlgebra a -> Vect k (SymmetricAlgebra a))
-> Vect k (TensorAlgebra a) -> Vect k (SymmetricAlgebra a)
forall k b a.
(Eq k, Num k, Ord b) =>
(a -> Vect k b) -> Vect k a -> Vect k b
linear TensorAlgebra a -> Vect k (SymmetricAlgebra a)
forall (m :: * -> *) a.
(Monad m, Ord a) =>
TensorAlgebra a -> m (SymmetricAlgebra a)
toSym'
    where toSym' :: TensorAlgebra a -> m (SymmetricAlgebra a)
toSym' (TA i :: Int
i xs :: [a]
xs) = SymmetricAlgebra a -> m (SymmetricAlgebra a)
forall (m :: * -> *) a. Monad m => a -> m a
return (SymmetricAlgebra a -> m (SymmetricAlgebra a))
-> SymmetricAlgebra a -> m (SymmetricAlgebra a)
forall a b. (a -> b) -> a -> b
$ Int -> [a] -> SymmetricAlgebra a
forall a. Int -> [a] -> SymmetricAlgebra a
Sym Int
i ([a] -> [a]
forall a. Ord a => [a] -> [a]
L.sort [a]
xs) 


-- The symmetric algebra is the free commutative algebra. It has the following universal property:
-- Given f :: a -> Vect k b, where Vect k b is a commutative algebra
-- (which induces a vector space morphism, linear f :: Vect k a -> Vect k b)
-- then we can lift to a commutative algebra morphism, (liftSym f) :: Vect k (SymmetricAlgebra a) -> Vect k b
-- with (liftSym f) . injectSym = f

injectSym :: Num k => Vect k a -> Vect k (SymmetricAlgebra a)
injectSym :: Vect k a -> Vect k (SymmetricAlgebra a)
injectSym = (a -> SymmetricAlgebra a)
-> Vect k a -> Vect k (SymmetricAlgebra a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\a :: a
a -> Int -> [a] -> SymmetricAlgebra a
forall a. Int -> [a] -> SymmetricAlgebra a
Sym 1 [a
a])

injectSym' :: Num k => a -> Vect k (SymmetricAlgebra a)
injectSym' :: a -> Vect k (SymmetricAlgebra a)
injectSym' = Vect k a -> Vect k (SymmetricAlgebra a)
forall k a. Num k => Vect k a -> Vect k (SymmetricAlgebra a)
injectSym (Vect k a -> Vect k (SymmetricAlgebra a))
-> (a -> Vect k a) -> a -> Vect k (SymmetricAlgebra a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Vect k a
forall (m :: * -> *) a. Monad m => a -> m a
return
-- injectSym' a = return (Sym 1 [a])

liftSym :: (Eq k, Num k, Ord b, Show b, Algebra k b) =>
     (Vect k a -> Vect k b) -> Vect k (SymmetricAlgebra a) -> Vect k b
liftSym :: (Vect k a -> Vect k b) -> Vect k (SymmetricAlgebra a) -> Vect k b
liftSym f :: Vect k a -> Vect k b
f = (SymmetricAlgebra a -> Vect k b)
-> Vect k (SymmetricAlgebra a) -> Vect k b
forall k b a.
(Eq k, Num k, Ord b) =>
(a -> Vect k b) -> Vect k a -> Vect k b
linear (\(Sym _ xs :: [a]
xs) -> [Vect k b] -> Vect k b
forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
product [Vect k a -> Vect k b
f (a -> Vect k a
forall (m :: * -> *) a. Monad m => a -> m a
return a
x) | a
x <- [a]
xs])

liftSym' :: (Eq k, Num k, Ord b, Show b, Algebra k b) =>
     (a -> Vect k b) -> Vect k (SymmetricAlgebra a) -> Vect k b
liftSym' :: (a -> Vect k b) -> Vect k (SymmetricAlgebra a) -> Vect k b
liftSym' = (Vect k a -> Vect k b) -> Vect k (SymmetricAlgebra a) -> Vect k b
forall k b a.
(Eq k, Num k, Ord b, Show b, Algebra k b) =>
(Vect k a -> Vect k b) -> Vect k (SymmetricAlgebra a) -> Vect k b
liftSym ((Vect k a -> Vect k b) -> Vect k (SymmetricAlgebra a) -> Vect k b)
-> ((a -> Vect k b) -> Vect k a -> Vect k b)
-> (a -> Vect k b)
-> Vect k (SymmetricAlgebra a)
-> Vect k b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> Vect k b) -> Vect k a -> Vect k b
forall k b a.
(Eq k, Num k, Ord b) =>
(a -> Vect k b) -> Vect k a -> Vect k b
linear
-- liftSym' f = linear (\(Sym _ xs) -> product [f x | x <- xs])

fmapSym :: (Eq k, Num k, Ord b, Show b) =>
    (Vect k a -> Vect k b) -> Vect k (SymmetricAlgebra a) -> Vect k (SymmetricAlgebra b)
fmapSym :: (Vect k a -> Vect k b)
-> Vect k (SymmetricAlgebra a) -> Vect k (SymmetricAlgebra b)
fmapSym f :: Vect k a -> Vect k b
f = (Vect k a -> Vect k (SymmetricAlgebra b))
-> Vect k (SymmetricAlgebra a) -> Vect k (SymmetricAlgebra b)
forall k b a.
(Eq k, Num k, Ord b, Show b, Algebra k b) =>
(Vect k a -> Vect k b) -> Vect k (SymmetricAlgebra a) -> Vect k b
liftSym (Vect k b -> Vect k (SymmetricAlgebra b)
forall k a. Num k => Vect k a -> Vect k (SymmetricAlgebra a)
injectSym (Vect k b -> Vect k (SymmetricAlgebra b))
-> (Vect k a -> Vect k b)
-> Vect k a
-> Vect k (SymmetricAlgebra b)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Vect k a -> Vect k b
f)
-- fmapSym f = linear (\(Sym _ xs) -> product [injectSym (f (return x)) | x <- xs])

fmapSym' :: (Eq k, Num k, Ord b, Show b) =>
    (a -> b) -> Vect k (SymmetricAlgebra a) -> Vect k (SymmetricAlgebra b)
fmapSym' :: (a -> b)
-> Vect k (SymmetricAlgebra a) -> Vect k (SymmetricAlgebra b)
fmapSym' = (Vect k a -> Vect k b)
-> Vect k (SymmetricAlgebra a) -> Vect k (SymmetricAlgebra b)
forall k b a.
(Eq k, Num k, Ord b, Show b) =>
(Vect k a -> Vect k b)
-> Vect k (SymmetricAlgebra a) -> Vect k (SymmetricAlgebra b)
fmapSym ((Vect k a -> Vect k b)
 -> Vect k (SymmetricAlgebra a) -> Vect k (SymmetricAlgebra b))
-> ((a -> b) -> Vect k a -> Vect k b)
-> (a -> b)
-> Vect k (SymmetricAlgebra a)
-> Vect k (SymmetricAlgebra b)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> b) -> Vect k a -> Vect k b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap
-- fmapSym' f = liftSym' (injectSym' . f)
-- fmapSym' f = linear (\(Sym _ xs) -> product [injectSym' (f x) | x <- xs])

bindSym :: (Eq k, Num k, Ord b, Show b) =>
    Vect k (SymmetricAlgebra a) -> (Vect k a -> Vect k (SymmetricAlgebra b)) -> Vect k (SymmetricAlgebra b)
bindSym :: Vect k (SymmetricAlgebra a)
-> (Vect k a -> Vect k (SymmetricAlgebra b))
-> Vect k (SymmetricAlgebra b)
bindSym = ((Vect k a -> Vect k (SymmetricAlgebra b))
 -> Vect k (SymmetricAlgebra a) -> Vect k (SymmetricAlgebra b))
-> Vect k (SymmetricAlgebra a)
-> (Vect k a -> Vect k (SymmetricAlgebra b))
-> Vect k (SymmetricAlgebra b)
forall a b c. (a -> b -> c) -> b -> a -> c
flip (Vect k a -> Vect k (SymmetricAlgebra b))
-> Vect k (SymmetricAlgebra a) -> Vect k (SymmetricAlgebra b)
forall k b a.
(Eq k, Num k, Ord b, Show b, Algebra k b) =>
(Vect k a -> Vect k b) -> Vect k (SymmetricAlgebra a) -> Vect k b
liftSym

bindSym' :: (Eq k, Num k, Ord b, Show b) =>
    Vect k (SymmetricAlgebra a) -> (a -> Vect k (SymmetricAlgebra b)) -> Vect k (SymmetricAlgebra b)
bindSym' :: Vect k (SymmetricAlgebra a)
-> (a -> Vect k (SymmetricAlgebra b))
-> Vect k (SymmetricAlgebra b)
bindSym' = ((a -> Vect k (SymmetricAlgebra b))
 -> Vect k (SymmetricAlgebra a) -> Vect k (SymmetricAlgebra b))
-> Vect k (SymmetricAlgebra a)
-> (a -> Vect k (SymmetricAlgebra b))
-> Vect k (SymmetricAlgebra b)
forall a b c. (a -> b -> c) -> b -> a -> c
flip (a -> Vect k (SymmetricAlgebra b))
-> Vect k (SymmetricAlgebra a) -> Vect k (SymmetricAlgebra b)
forall k b a.
(Eq k, Num k, Ord b, Show b, Algebra k b) =>
(a -> Vect k b) -> Vect k (SymmetricAlgebra a) -> Vect k b
liftSym'
-- Another way to think about this is variable substitution


-- EXTERIOR ALGEBRA

-- |A data type representing basis elements of the exterior algebra over a set\/type.
-- The exterior algebra is the quotient of the tensor algebra by
-- the ideal generated by all
-- self-products u&#x2297;u and sums of products u&#x2297;v + v&#x2297;u
data ExteriorAlgebra a = Ext Int [a] deriving (ExteriorAlgebra a -> ExteriorAlgebra a -> Bool
(ExteriorAlgebra a -> ExteriorAlgebra a -> Bool)
-> (ExteriorAlgebra a -> ExteriorAlgebra a -> Bool)
-> Eq (ExteriorAlgebra a)
forall a. Eq a => ExteriorAlgebra a -> ExteriorAlgebra a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: ExteriorAlgebra a -> ExteriorAlgebra a -> Bool
$c/= :: forall a. Eq a => ExteriorAlgebra a -> ExteriorAlgebra a -> Bool
== :: ExteriorAlgebra a -> ExteriorAlgebra a -> Bool
$c== :: forall a. Eq a => ExteriorAlgebra a -> ExteriorAlgebra a -> Bool
Eq,Eq (ExteriorAlgebra a)
Eq (ExteriorAlgebra a) =>
(ExteriorAlgebra a -> ExteriorAlgebra a -> Ordering)
-> (ExteriorAlgebra a -> ExteriorAlgebra a -> Bool)
-> (ExteriorAlgebra a -> ExteriorAlgebra a -> Bool)
-> (ExteriorAlgebra a -> ExteriorAlgebra a -> Bool)
-> (ExteriorAlgebra a -> ExteriorAlgebra a -> Bool)
-> (ExteriorAlgebra a -> ExteriorAlgebra a -> ExteriorAlgebra a)
-> (ExteriorAlgebra a -> ExteriorAlgebra a -> ExteriorAlgebra a)
-> Ord (ExteriorAlgebra a)
ExteriorAlgebra a -> ExteriorAlgebra a -> Bool
ExteriorAlgebra a -> ExteriorAlgebra a -> Ordering
ExteriorAlgebra a -> ExteriorAlgebra a -> ExteriorAlgebra a
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 a. Ord a => Eq (ExteriorAlgebra a)
forall a. Ord a => ExteriorAlgebra a -> ExteriorAlgebra a -> Bool
forall a.
Ord a =>
ExteriorAlgebra a -> ExteriorAlgebra a -> Ordering
forall a.
Ord a =>
ExteriorAlgebra a -> ExteriorAlgebra a -> ExteriorAlgebra a
min :: ExteriorAlgebra a -> ExteriorAlgebra a -> ExteriorAlgebra a
$cmin :: forall a.
Ord a =>
ExteriorAlgebra a -> ExteriorAlgebra a -> ExteriorAlgebra a
max :: ExteriorAlgebra a -> ExteriorAlgebra a -> ExteriorAlgebra a
$cmax :: forall a.
Ord a =>
ExteriorAlgebra a -> ExteriorAlgebra a -> ExteriorAlgebra a
>= :: ExteriorAlgebra a -> ExteriorAlgebra a -> Bool
$c>= :: forall a. Ord a => ExteriorAlgebra a -> ExteriorAlgebra a -> Bool
> :: ExteriorAlgebra a -> ExteriorAlgebra a -> Bool
$c> :: forall a. Ord a => ExteriorAlgebra a -> ExteriorAlgebra a -> Bool
<= :: ExteriorAlgebra a -> ExteriorAlgebra a -> Bool
$c<= :: forall a. Ord a => ExteriorAlgebra a -> ExteriorAlgebra a -> Bool
< :: ExteriorAlgebra a -> ExteriorAlgebra a -> Bool
$c< :: forall a. Ord a => ExteriorAlgebra a -> ExteriorAlgebra a -> Bool
compare :: ExteriorAlgebra a -> ExteriorAlgebra a -> Ordering
$ccompare :: forall a.
Ord a =>
ExteriorAlgebra a -> ExteriorAlgebra a -> Ordering
$cp1Ord :: forall a. Ord a => Eq (ExteriorAlgebra a)
Ord)

instance Show a => Show (ExteriorAlgebra a) where
    show :: ExteriorAlgebra a -> String
show (Ext _ []) = "1"
    show (Ext _ xs :: [a]
xs) = (Char -> Bool) -> ShowS
forall a. (a -> Bool) -> [a] -> [a]
filter (Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
/= '"') ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ [String] -> String
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$ String -> [String] -> [String]
forall a. a -> [a] -> [a]
L.intersperse "^" ([String] -> [String]) -> [String] -> [String]
forall a b. (a -> b) -> a -> b
$ (a -> String) -> [a] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map a -> String
forall a. Show a => a -> String
show [a]
xs


instance (Eq k, Num k, Ord a) => Algebra k (ExteriorAlgebra a) where
    unit :: k -> Vect k (ExteriorAlgebra a)
unit x :: k
x = k
x k -> Vect k (ExteriorAlgebra a) -> Vect k (ExteriorAlgebra a)
forall k b. (Eq k, Num k) => k -> Vect k b -> Vect k b
*> ExteriorAlgebra a -> Vect k (ExteriorAlgebra a)
forall (m :: * -> *) a. Monad m => a -> m a
return (Int -> [a] -> ExteriorAlgebra a
forall a. Int -> [a] -> ExteriorAlgebra a
Ext 0 [])
    mult :: Vect k (Tensor (ExteriorAlgebra a) (ExteriorAlgebra a))
-> Vect k (ExteriorAlgebra a)
mult xy :: Vect k (Tensor (ExteriorAlgebra a) (ExteriorAlgebra a))
xy = Vect k (ExteriorAlgebra a) -> Vect k (ExteriorAlgebra a)
forall k b. (Eq k, Num k, Ord b) => Vect k b -> Vect k b
nf (Vect k (ExteriorAlgebra a) -> Vect k (ExteriorAlgebra a))
-> Vect k (ExteriorAlgebra a) -> Vect k (ExteriorAlgebra a)
forall a b. (a -> b) -> a -> b
$ Vect k (Tensor (ExteriorAlgebra a) (ExteriorAlgebra a))
xy Vect k (Tensor (ExteriorAlgebra a) (ExteriorAlgebra a))
-> (Tensor (ExteriorAlgebra a) (ExteriorAlgebra a)
    -> Vect k (ExteriorAlgebra a))
-> Vect k (ExteriorAlgebra a)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= (\(Ext i :: Int
i xs :: [a]
xs, Ext j :: Int
j ys :: [a]
ys) -> k
-> (Int, [a])
-> (Int, [a])
-> (Int, [a])
-> Vect k (ExteriorAlgebra a)
forall a k.
(Ord a, Eq k, Num k) =>
k
-> (Int, [a])
-> (Int, [a])
-> (Int, [a])
-> Vect k (ExteriorAlgebra a)
signedMerge 1 (0,[]) (Int
i,[a]
xs) (Int
j,[a]
ys))
        where signedMerge :: k
-> (Int, [a])
-> (Int, [a])
-> (Int, [a])
-> Vect k (ExteriorAlgebra a)
signedMerge s :: k
s (k :: Int
k,zs :: [a]
zs) (i :: Int
i,x :: a
x:xs :: [a]
xs) (j :: Int
j,y :: a
y:ys :: [a]
ys) =
                  case a -> a -> Ordering
forall a. Ord a => a -> a -> Ordering
compare a
x a
y of
                  EQ -> Vect k (ExteriorAlgebra a)
forall k b. Vect k b
zerov
                  LT -> k
-> (Int, [a])
-> (Int, [a])
-> (Int, [a])
-> Vect k (ExteriorAlgebra a)
signedMerge k
s (Int
kInt -> Int -> Int
forall a. Num a => a -> a -> a
+1,a
xa -> [a] -> [a]
forall a. a -> [a] -> [a]
:[a]
zs) (Int
iInt -> Int -> Int
forall a. Num a => a -> a -> a
-1,[a]
xs) (Int
j,a
ya -> [a] -> [a]
forall a. a -> [a] -> [a]
:[a]
ys)
                  GT -> let s' :: k
s' = if Int -> Bool
forall a. Integral a => a -> Bool
even Int
i then k
s else -k
s -- we had to commute y past x:xs, with i sign changes
                        in k
-> (Int, [a])
-> (Int, [a])
-> (Int, [a])
-> Vect k (ExteriorAlgebra a)
signedMerge k
s' (Int
kInt -> Int -> Int
forall a. Num a => a -> a -> a
+1,a
ya -> [a] -> [a]
forall a. a -> [a] -> [a]
:[a]
zs) (Int
i,a
xa -> [a] -> [a]
forall a. a -> [a] -> [a]
:[a]
xs) (Int
jInt -> Int -> Int
forall a. Num a => a -> a -> a
-1,[a]
ys)
              signedMerge s :: k
s (k :: Int
k,zs :: [a]
zs) (i :: Int
i,xs :: [a]
xs) (0,[]) = k
s k -> Vect k (ExteriorAlgebra a) -> Vect k (ExteriorAlgebra a)
forall k b. (Eq k, Num k) => k -> Vect k b -> Vect k b
*> (ExteriorAlgebra a -> Vect k (ExteriorAlgebra a)
forall (m :: * -> *) a. Monad m => a -> m a
return (ExteriorAlgebra a -> Vect k (ExteriorAlgebra a))
-> ExteriorAlgebra a -> Vect k (ExteriorAlgebra a)
forall a b. (a -> b) -> a -> b
$ Int -> [a] -> ExteriorAlgebra a
forall a. Int -> [a] -> ExteriorAlgebra a
Ext (Int
kInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
i) ([a] -> ExteriorAlgebra a) -> [a] -> ExteriorAlgebra a
forall a b. (a -> b) -> a -> b
$ [a] -> [a]
forall a. [a] -> [a]
reverse [a]
zs [a] -> [a] -> [a]
forall a. [a] -> [a] -> [a]
++ [a]
xs)
              signedMerge s :: k
s (k :: Int
k,zs :: [a]
zs) (0,[]) (j :: Int
j,ys :: [a]
ys) = k
s k -> Vect k (ExteriorAlgebra a) -> Vect k (ExteriorAlgebra a)
forall k b. (Eq k, Num k) => k -> Vect k b -> Vect k b
*> (ExteriorAlgebra a -> Vect k (ExteriorAlgebra a)
forall (m :: * -> *) a. Monad m => a -> m a
return (ExteriorAlgebra a -> Vect k (ExteriorAlgebra a))
-> ExteriorAlgebra a -> Vect k (ExteriorAlgebra a)
forall a b. (a -> b) -> a -> b
$ Int -> [a] -> ExteriorAlgebra a
forall a. Int -> [a] -> ExteriorAlgebra a
Ext (Int
kInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
j) ([a] -> ExteriorAlgebra a) -> [a] -> ExteriorAlgebra a
forall a b. (a -> b) -> a -> b
$ [a] -> [a]
forall a. [a] -> [a]
reverse [a]
zs [a] -> [a] -> [a]
forall a. [a] -> [a] -> [a]
++ [a]
ys)


-- |Algebra morphism from tensor algebra to exterior algebra.
-- The kernel of the morphism is the ideal generated by all
-- self-products u&#x2297;u and sums of products u&#x2297;v + v&#x2297;u
toExt :: (Eq k, Num k, Ord a) =>
     Vect k (TensorAlgebra a) -> Vect k (ExteriorAlgebra a)
toExt :: Vect k (TensorAlgebra a) -> Vect k (ExteriorAlgebra a)
toExt = (TensorAlgebra a -> Vect k (ExteriorAlgebra a))
-> Vect k (TensorAlgebra a) -> Vect k (ExteriorAlgebra a)
forall k b a.
(Eq k, Num k, Ord b) =>
(a -> Vect k b) -> Vect k a -> Vect k b
linear TensorAlgebra a -> Vect k (ExteriorAlgebra a)
forall k a.
(Eq k, Num k, Ord a) =>
TensorAlgebra a -> Vect k (ExteriorAlgebra a)
toExt'
    where toExt' :: TensorAlgebra a -> Vect k (ExteriorAlgebra a)
toExt' (TA i :: Int
i xs :: [a]
xs) = let (sign :: a
sign,xs' :: [a]
xs') = a -> Bool -> [a] -> [a] -> (a, [a])
forall a a. (Ord a, Num a) => a -> Bool -> [a] -> [a] -> (a, [a])
signedSort 1 Bool
True [] [a]
xs
                             in Integer -> k
forall a. Num a => Integer -> a
fromInteger Integer
forall a. Num a => a
sign k -> Vect k (ExteriorAlgebra a) -> Vect k (ExteriorAlgebra a)
forall k b. (Eq k, Num k) => k -> Vect k b -> Vect k b
*> ExteriorAlgebra a -> Vect k (ExteriorAlgebra a)
forall (m :: * -> *) a. Monad m => a -> m a
return (Int -> [a] -> ExteriorAlgebra a
forall a. Int -> [a] -> ExteriorAlgebra a
Ext Int
i [a]
xs')

signedSort :: a -> Bool -> [a] -> [a] -> (a, [a])
signedSort sign :: a
sign done :: Bool
done ls :: [a]
ls (r1 :: a
r1:r2 :: a
r2:rs :: [a]
rs) =
    case a -> a -> Ordering
forall a. Ord a => a -> a -> Ordering
compare a
r1 a
r2 of
    EQ -> (0,[])
    LT -> a -> Bool -> [a] -> [a] -> (a, [a])
signedSort a
sign Bool
done (a
r1a -> [a] -> [a]
forall a. a -> [a] -> [a]
:[a]
ls) (a
r2a -> [a] -> [a]
forall a. a -> [a] -> [a]
:[a]
rs)
    GT -> a -> Bool -> [a] -> [a] -> (a, [a])
signedSort (-a
sign) Bool
False (a
r2a -> [a] -> [a]
forall a. a -> [a] -> [a]
:[a]
ls) (a
r1a -> [a] -> [a]
forall a. a -> [a] -> [a]
:[a]
rs)
signedSort sign :: a
sign done :: Bool
done ls :: [a]
ls rs :: [a]
rs =
    if Bool
done then (a
sign,[a] -> [a]
forall a. [a] -> [a]
reverse [a]
ls [a] -> [a] -> [a]
forall a. [a] -> [a] -> [a]
++ [a]
rs) else a -> Bool -> [a] -> [a] -> (a, [a])
signedSort a
sign Bool
True [] ([a] -> [a]
forall a. [a] -> [a]
reverse [a]
ls [a] -> [a] -> [a]
forall a. [a] -> [a] -> [a]
++ [a]
rs)

-- !! The above code seems a bit clumsy - can we do better


injectExt :: Num k => Vect k a -> Vect k (ExteriorAlgebra a)
injectExt :: Vect k a -> Vect k (ExteriorAlgebra a)
injectExt = (a -> ExteriorAlgebra a) -> Vect k a -> Vect k (ExteriorAlgebra a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\a :: a
a -> Int -> [a] -> ExteriorAlgebra a
forall a. Int -> [a] -> ExteriorAlgebra a
Ext 1 [a
a])

injectExt' :: Num k => a -> Vect k (ExteriorAlgebra a)
injectExt' :: a -> Vect k (ExteriorAlgebra a)
injectExt' = Vect k a -> Vect k (ExteriorAlgebra a)
forall k a. Num k => Vect k a -> Vect k (ExteriorAlgebra a)
injectExt (Vect k a -> Vect k (ExteriorAlgebra a))
-> (a -> Vect k a) -> a -> Vect k (ExteriorAlgebra a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Vect k a
forall (m :: * -> *) a. Monad m => a -> m a
return
-- injectExt' a = return (Ext 1 [a])

liftExt :: (Eq k, Num k, Ord b, Show b, Algebra k b) =>
     (Vect k a -> Vect k b) -> Vect k (ExteriorAlgebra a) -> Vect k b
liftExt :: (Vect k a -> Vect k b) -> Vect k (ExteriorAlgebra a) -> Vect k b
liftExt f :: Vect k a -> Vect k b
f = (ExteriorAlgebra a -> Vect k b)
-> Vect k (ExteriorAlgebra a) -> Vect k b
forall k b a.
(Eq k, Num k, Ord b) =>
(a -> Vect k b) -> Vect k a -> Vect k b
linear (\(Ext _ xs :: [a]
xs) -> [Vect k b] -> Vect k b
forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
product [Vect k a -> Vect k b
f (a -> Vect k a
forall (m :: * -> *) a. Monad m => a -> m a
return a
x) | a
x <- [a]
xs])

liftExt' :: (Eq k, Num k, Ord b, Show b, Algebra k b) =>
     (a -> Vect k b) -> Vect k (ExteriorAlgebra a) -> Vect k b
liftExt' :: (a -> Vect k b) -> Vect k (ExteriorAlgebra a) -> Vect k b
liftExt' = (Vect k a -> Vect k b) -> Vect k (ExteriorAlgebra a) -> Vect k b
forall k b a.
(Eq k, Num k, Ord b, Show b, Algebra k b) =>
(Vect k a -> Vect k b) -> Vect k (ExteriorAlgebra a) -> Vect k b
liftExt ((Vect k a -> Vect k b) -> Vect k (ExteriorAlgebra a) -> Vect k b)
-> ((a -> Vect k b) -> Vect k a -> Vect k b)
-> (a -> Vect k b)
-> Vect k (ExteriorAlgebra a)
-> Vect k b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> Vect k b) -> Vect k a -> Vect k b
forall k b a.
(Eq k, Num k, Ord b) =>
(a -> Vect k b) -> Vect k a -> Vect k b
linear
-- liftExt' f = linear (\(Ext _ xs) -> product [f x | x <- xs])

fmapExt :: (Eq k, Num k, Ord b, Show b) =>
    (Vect k a -> Vect k b) -> Vect k (ExteriorAlgebra a) -> Vect k (ExteriorAlgebra b)
fmapExt :: (Vect k a -> Vect k b)
-> Vect k (ExteriorAlgebra a) -> Vect k (ExteriorAlgebra b)
fmapExt f :: Vect k a -> Vect k b
f = (Vect k a -> Vect k (ExteriorAlgebra b))
-> Vect k (ExteriorAlgebra a) -> Vect k (ExteriorAlgebra b)
forall k b a.
(Eq k, Num k, Ord b, Show b, Algebra k b) =>
(Vect k a -> Vect k b) -> Vect k (ExteriorAlgebra a) -> Vect k b
liftExt (Vect k b -> Vect k (ExteriorAlgebra b)
forall k a. Num k => Vect k a -> Vect k (ExteriorAlgebra a)
injectExt (Vect k b -> Vect k (ExteriorAlgebra b))
-> (Vect k a -> Vect k b) -> Vect k a -> Vect k (ExteriorAlgebra b)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Vect k a -> Vect k b
f)
-- fmapExt f = linear (\(Ext _ xs) -> product [injectExt (f (return x)) | x <- xs])

fmapExt' :: (Eq k, Num k, Ord b, Show b) =>
    (a -> b) -> Vect k (ExteriorAlgebra a) -> Vect k (ExteriorAlgebra b)
fmapExt' :: (a -> b)
-> Vect k (ExteriorAlgebra a) -> Vect k (ExteriorAlgebra b)
fmapExt' = (Vect k a -> Vect k b)
-> Vect k (ExteriorAlgebra a) -> Vect k (ExteriorAlgebra b)
forall k b a.
(Eq k, Num k, Ord b, Show b) =>
(Vect k a -> Vect k b)
-> Vect k (ExteriorAlgebra a) -> Vect k (ExteriorAlgebra b)
fmapExt ((Vect k a -> Vect k b)
 -> Vect k (ExteriorAlgebra a) -> Vect k (ExteriorAlgebra b))
-> ((a -> b) -> Vect k a -> Vect k b)
-> (a -> b)
-> Vect k (ExteriorAlgebra a)
-> Vect k (ExteriorAlgebra b)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> b) -> Vect k a -> Vect k b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap
-- fmapExt' f = liftExt' (injectExt' . f)
-- fmapExt' f = linear (\(Ext _ xs) -> product [injectExt' (f x) | x <- xs])

bindExt :: (Eq k, Num k, Ord b, Show b) =>
    Vect k (ExteriorAlgebra a) -> (Vect k a -> Vect k (ExteriorAlgebra b)) -> Vect k (ExteriorAlgebra b)
bindExt :: Vect k (ExteriorAlgebra a)
-> (Vect k a -> Vect k (ExteriorAlgebra b))
-> Vect k (ExteriorAlgebra b)
bindExt = ((Vect k a -> Vect k (ExteriorAlgebra b))
 -> Vect k (ExteriorAlgebra a) -> Vect k (ExteriorAlgebra b))
-> Vect k (ExteriorAlgebra a)
-> (Vect k a -> Vect k (ExteriorAlgebra b))
-> Vect k (ExteriorAlgebra b)
forall a b c. (a -> b -> c) -> b -> a -> c
flip (Vect k a -> Vect k (ExteriorAlgebra b))
-> Vect k (ExteriorAlgebra a) -> Vect k (ExteriorAlgebra b)
forall k b a.
(Eq k, Num k, Ord b, Show b, Algebra k b) =>
(Vect k a -> Vect k b) -> Vect k (ExteriorAlgebra a) -> Vect k b
liftExt

bindExt' :: (Eq k, Num k, Ord b, Show b) =>
    Vect k (ExteriorAlgebra a) -> (a -> Vect k (ExteriorAlgebra b)) -> Vect k (ExteriorAlgebra b)
bindExt' :: Vect k (ExteriorAlgebra a)
-> (a -> Vect k (ExteriorAlgebra b)) -> Vect k (ExteriorAlgebra b)
bindExt' = ((a -> Vect k (ExteriorAlgebra b))
 -> Vect k (ExteriorAlgebra a) -> Vect k (ExteriorAlgebra b))
-> Vect k (ExteriorAlgebra a)
-> (a -> Vect k (ExteriorAlgebra b))
-> Vect k (ExteriorAlgebra b)
forall a b c. (a -> b -> c) -> b -> a -> c
flip (a -> Vect k (ExteriorAlgebra b))
-> Vect k (ExteriorAlgebra a) -> Vect k (ExteriorAlgebra b)
forall k b a.
(Eq k, Num k, Ord b, Show b, Algebra k b) =>
(a -> Vect k b) -> Vect k (ExteriorAlgebra a) -> Vect k b
liftExt'
-- Another way to think about this is variable substitution


-- TENSOR COALGEBRA

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

instance (Eq k, Num k, Ord c) => Coalgebra k (TensorCoalgebra c) where
    counit :: Vect k (TensorCoalgebra c) -> k
counit = Vect k () -> k
forall k. Num k => Vect k () -> k
unwrap (Vect k () -> k)
-> (Vect k (TensorCoalgebra c) -> Vect k ())
-> Vect k (TensorCoalgebra c)
-> k
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (TensorCoalgebra c -> Vect k ())
-> Vect k (TensorCoalgebra c) -> Vect k ()
forall k b a.
(Eq k, Num k, Ord b) =>
(a -> Vect k b) -> Vect k a -> Vect k b
linear TensorCoalgebra c -> Vect k ()
forall k c. Num k => TensorCoalgebra c -> Vect k ()
counit'
        where counit' :: TensorCoalgebra c -> Vect k ()
counit' (TC 0 []) = () -> Vect k ()
forall (m :: * -> *) a. Monad m => a -> m a
return () -- 1
              counit' _ = Vect k ()
forall k b. Vect k b
zerov
    comult :: Vect k (TensorCoalgebra c)
-> Vect k (Tensor (TensorCoalgebra c) (TensorCoalgebra c))
comult = (TensorCoalgebra c
 -> Vect k (Tensor (TensorCoalgebra c) (TensorCoalgebra c)))
-> Vect k (TensorCoalgebra c)
-> Vect k (Tensor (TensorCoalgebra c) (TensorCoalgebra c))
forall k b a.
(Eq k, Num k, Ord b) =>
(a -> Vect k b) -> Vect k a -> Vect k b
linear TensorCoalgebra c
-> Vect k (Tensor (TensorCoalgebra c) (TensorCoalgebra c))
forall k c.
(Num k, Ord c, Eq k) =>
TensorCoalgebra c -> Vect k (TensorCoalgebra c, TensorCoalgebra c)
comult'
        where comult' :: TensorCoalgebra c -> Vect k (TensorCoalgebra c, TensorCoalgebra c)
comult' (TC d :: Int
d xs :: [c]
xs) = [Vect k (TensorCoalgebra c, TensorCoalgebra c)]
-> Vect k (TensorCoalgebra c, TensorCoalgebra c)
forall k b. (Eq k, Num k, Ord b) => [Vect k b] -> Vect k b
sumv [(TensorCoalgebra c, TensorCoalgebra c)
-> Vect k (TensorCoalgebra c, TensorCoalgebra c)
forall (m :: * -> *) a. Monad m => a -> m a
return (Int -> [c] -> TensorCoalgebra c
forall c. Int -> [c] -> TensorCoalgebra c
TC Int
i [c]
ls, Int -> [c] -> TensorCoalgebra c
forall c. Int -> [c] -> TensorCoalgebra c
TC (Int
dInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
i) [c]
rs) | (i :: Int
i,ls :: [c]
ls,rs :: [c]
rs) <- [Int] -> [[c]] -> [[c]] -> [(Int, [c], [c])]
forall a b c. [a] -> [b] -> [c] -> [(a, b, c)]
L.zip3 [0..] ([c] -> [[c]]
forall a. [a] -> [[a]]
L.inits [c]
xs) ([c] -> [[c]]
forall a. [a] -> [[a]]
L.tails [c]
xs)]


-- Now show that the tensor coalgebra is the cofree coalgebra
-- ie that it has the required universal property:
-- coliftTC f is a coalgebra morphism, and f == projectTC . coliftTC f

-- projection onto the underlying vector space
projectTC :: (Eq k, Num k, Ord b) => Vect k (TensorCoalgebra b) -> Vect k b
projectTC :: Vect k (TensorCoalgebra b) -> Vect k b
projectTC = (TensorCoalgebra b -> Vect k b)
-> Vect k (TensorCoalgebra b) -> Vect k b
forall k b a.
(Eq k, Num k, Ord b) =>
(a -> Vect k b) -> Vect k a -> Vect k b
linear TensorCoalgebra b -> Vect k b
forall k a. Num k => TensorCoalgebra a -> Vect k a
projectTC' where projectTC' :: TensorCoalgebra a -> Vect k a
projectTC' (TC 1 [b :: a
b]) = a -> Vect k a
forall (m :: * -> *) a. Monad m => a -> m a
return a
b; projectTC' _ = Vect k a
forall k b. Vect k b
zerov 
-- projectTC t = V [(b,c) | (TC 1 [b], c) <- terms t]


-- lift a vector space morphism C -> D to a coalgebra morphism C -> T'(D)
-- this function returns an approximation, valid only up to second order terms
coliftTC :: (Eq k, Num k, Coalgebra k c, Ord d) =>
     (Vect k c -> Vect k d) -> Vect k c -> Vect k (TensorCoalgebra d)
coliftTC :: (Vect k c -> Vect k d) -> Vect k c -> Vect k (TensorCoalgebra d)
coliftTC f :: Vect k c -> Vect k d
f = [Vect k c -> Vect k (TensorCoalgebra d)]
-> Vect k c -> Vect k (TensorCoalgebra d)
forall (t1 :: * -> *) k b t2.
(Foldable t1, Num k, Ord b, Eq k) =>
t1 (t2 -> Vect k b) -> t2 -> Vect k b
sumf [Int
-> (Vect k c -> Vect k d) -> Vect k c -> Vect k (TensorCoalgebra d)
forall k c b (m :: * -> *).
(Monad m, Num k, Ord c, Coalgebra k b, Eq k) =>
Int -> (m b -> Vect k c) -> Vect k b -> Vect k (TensorCoalgebra c)
coliftTC' Int
i Vect k c -> Vect k d
f | Int
i <- [0..2] ]

coliftTC' :: Int -> (m b -> Vect k c) -> Vect k b -> Vect k (TensorCoalgebra c)
coliftTC' 0 f :: m b -> Vect k c
f = (b -> Vect k (TensorCoalgebra c))
-> Vect k b -> Vect k (TensorCoalgebra c)
forall k b a.
(Eq k, Num k, Ord b) =>
(a -> Vect k b) -> Vect k a -> Vect k b
linear b -> Vect k (TensorCoalgebra c)
forall k b c.
(Eq k, Num k, Coalgebra k b) =>
b -> Vect k (TensorCoalgebra c)
f0'
    where f0' :: b -> Vect k (TensorCoalgebra c)
f0' c :: b
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
c) k -> Vect k (TensorCoalgebra c) -> Vect k (TensorCoalgebra c)
forall k b. (Eq k, Num k) => k -> Vect k b -> Vect k b
*> TensorCoalgebra c -> Vect k (TensorCoalgebra c)
forall (m :: * -> *) a. Monad m => a -> m a
return (Int -> [c] -> TensorCoalgebra c
forall c. Int -> [c] -> TensorCoalgebra c
TC 0 [])
coliftTC' 1 f :: m b -> Vect k c
f = (b -> Vect k (TensorCoalgebra c))
-> Vect k b -> Vect k (TensorCoalgebra c)
forall k b a.
(Eq k, Num k, Ord b) =>
(a -> Vect k b) -> Vect k a -> Vect k b
linear b -> Vect k (TensorCoalgebra c)
f1'
    where f1' :: b -> Vect k (TensorCoalgebra c)
f1' c :: b
c = (c -> TensorCoalgebra c) -> Vect k c -> Vect k (TensorCoalgebra c)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\d :: c
d -> Int -> [c] -> TensorCoalgebra c
forall c. Int -> [c] -> TensorCoalgebra c
TC 1 [c
d]) (m b -> Vect k c
f (m b -> Vect k c) -> m b -> Vect k c
forall a b. (a -> b) -> a -> b
$ b -> m b
forall (m :: * -> *) a. Monad m => a -> m a
return b
c)
coliftTC' n :: Int
n f :: m b -> Vect k c
f = (b -> Vect k (TensorCoalgebra c))
-> Vect k b -> Vect k (TensorCoalgebra c)
forall k b a.
(Eq k, Num k, Ord b) =>
(a -> Vect k b) -> Vect k a -> Vect k b
linear b -> Vect k (TensorCoalgebra c)
fn'
    where f1' :: Vect k b -> Vect k (TensorCoalgebra c)
f1' = Int -> (m b -> Vect k c) -> Vect k b -> Vect k (TensorCoalgebra c)
coliftTC' 1 m b -> Vect k c
f
          fn1' :: Vect k b -> Vect k (TensorCoalgebra c)
fn1' = Int -> (m b -> Vect k c) -> Vect k b -> Vect k (TensorCoalgebra c)
coliftTC' (Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
-1) m b -> Vect k c
f
          fn' :: b -> Vect k (TensorCoalgebra c)
fn' c :: b
c = ((TensorCoalgebra c, TensorCoalgebra c) -> TensorCoalgebra c)
-> Vect k (TensorCoalgebra c, TensorCoalgebra c)
-> Vect k (TensorCoalgebra c)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\(TC 1 [x :: c
x], TC _ xs :: [c]
xs) -> Int -> [c] -> TensorCoalgebra c
forall c. Int -> [c] -> TensorCoalgebra c
TC Int
n (c
xc -> [c] -> [c]
forall a. a -> [a] -> [a]
:[c]
xs)) (Vect k (TensorCoalgebra c, TensorCoalgebra c)
 -> Vect k (TensorCoalgebra c))
-> Vect k (TensorCoalgebra c, TensorCoalgebra c)
-> Vect k (TensorCoalgebra c)
forall a b. (a -> b) -> a -> b
$ ( (Vect k b -> Vect k (TensorCoalgebra c)
f1' (Vect k b -> Vect k (TensorCoalgebra c))
-> (Vect k b -> Vect k (TensorCoalgebra c))
-> Vect k (Tensor b b)
-> Vect k (TensorCoalgebra c, TensorCoalgebra c)
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 (TensorCoalgebra c)
fn1') (Vect k (Tensor b b)
 -> Vect k (TensorCoalgebra c, TensorCoalgebra c))
-> (Vect k b -> Vect k (Tensor b b))
-> Vect k b
-> Vect k (TensorCoalgebra c, TensorCoalgebra c)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Vect k b -> Vect k (Tensor b b)
forall k b. Coalgebra k b => Vect k b -> Vect k (Tensor b b)
comult) (b -> Vect k b
forall (m :: * -> *) a. Monad m => a -> m a
return b
c)


cobindTC :: (Eq k, Num k, Ord c, Ord d) =>
     (Vect k (TensorCoalgebra c) -> Vect k d) -> Vect k (TensorCoalgebra c) -> Vect k (TensorCoalgebra d)
cobindTC :: (Vect k (TensorCoalgebra c) -> Vect k d)
-> Vect k (TensorCoalgebra c) -> Vect k (TensorCoalgebra d)
cobindTC = (Vect k (TensorCoalgebra c) -> Vect k d)
-> Vect k (TensorCoalgebra c) -> Vect k (TensorCoalgebra d)
forall k c d.
(Eq k, Num k, Coalgebra k c, Ord d) =>
(Vect k c -> Vect k d) -> Vect k c -> Vect k (TensorCoalgebra d)
coliftTC

-- So we have a comonad:
-- projectTC is extract :: w a -> a
-- cobindTC is extend :: (w a -> b) -> w a -> w b

{-
Derivation of coliftTC:
Write f' = f0' + f1' + f2' + ...,
where fn' is the part of f' whose range is the nth iterated tensor product in TC.
Then we can deduce f0' from counit . f' == counit
If f': c -> sum ai*di + terms of other order
then counit c = sum ai*counit di
We can deduce f1' from f == projectTC . f'
We can deduce the rest recursively from comult
Write comult (on TC) = comult00 + (comult01+comult10) + (comult02+comult11+comult20) + ...,
where comultij is that part that operates on the i+j'th tensor product to produce i'th `te` jth
Then comult . f' = (f' `tf` f') . comult
can be expanded as
(comult00 + comult01+comult10 + ...) . (f0' + f1' + ...) = (f0' `tf` f0' + f0' `tf` f1' + f1' `tf` f0' + ...) . comult
Looking at the 1,n-1 term, we see that
comult1,n-1 . fn' = (f1' `tf` fn-1') . comult
-}

-- For example
{-
> let f = linear (\x -> case x of Dual One -> e1; Dual I -> e2; Dual J -> e3; Dual K -> e 4)
> let f' = sumf [coliftTC' i f | i <- [0..3] ]

-- then the following agree up to level three (inclusive)
> (comult . f') one'
> ((f' `tf` f') . comult) one'
-}