Hi Steve, thank you for addressing the other part of my question.
There was also a second part to the question:
Btw, I frequently encounter monads in a categories of functors which are not endofunctors. An example are finite dimensional vectorspaces which can be constructed via a monoid in the category of functors FinSet -> Set, here I is the embedding and (x) can be constructed from the left kan extension and composition. The unit is given by the Kronecker delta and join can be constructed from Matrix multiplication. Should one call these beasts monads as well? Is there a good reference for this type of construction?
The category of functors from FinSet to Set is equivalent to the category of endofunctors of Set which preserve filtered colimits: such endofunctors are usually called finitary. Thus a monoid in [FinSet,Set] with respect to this tensor product is the same thing as a monad on Set whose endofunctor part is finitary: this is called a finitary monad.
These finitary monads on Set are equivalent to Lawvere theories and so in turn to (finitary, single-sorted) varieties.
Finitary monads can also be considered on other base categories than Set, especially on locally finitely presentable ones.
It is true that vector spaces are the algebras for a finitary monad on Set. There is no need to restrict to finite-dimensional vector spaces; in fact it is not true that there is a monad on Set whose algebras are the finite-dimensional vector spaces.
I am not sure I completely understand your comments. I guess it may be helpful to be more precise: F : FinSet -> Set F A = Real -> A together with:
eta_A : A -> F A eta a = \ b . if a=b then 1 else 0 (>>=) : F A -> (A -> F B) -> F B v >>= f = \ b. \Sigma a:A.(v a)*(f a b) My notation is inspired by functional programming and naturally as a Computer Scientist I am interested in the constructive content of theorems. This construction only works if the input is decidable (needed for eta) and if we can define Sigma (this certainly works if A is finite). I can see how to lift F to a functor on Sets by using a Kan extension (left ?). In my terminology it may be something like F' : Set -> Set F' X = Sigma A:FinSet. A -> X x F A I suspect my eta and >>= give then rise to a monad on Set? However, I don't see how to do this if the vector spaces are not finite. Btw, I only used this as an example. My question was rather wether people have studied monoids in categories of functors which are not endofunctors. I believe this notion is useful in functional programming and Type Theory as a natural generalisation of the notion of a monad. Cheers, Thorsten This message has been checked for viruses but the contents of an attachment may still contain software viruses, which could damage your computer system: you are advised to perform your own checks. Email communications with the University of Nottingham may be monitored as permitted by UK legislation.