    -- 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 &#x2295; V &#x2295; V&#x2297;V &#x2295; V&#x2297;V&#x2297;V &#x2295; ...
    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'
    -}