A natural transformation is an indexed family of arrows such that a certain diagram commutes. One could require a stronger condition, namely that the said diagram is a pullback. What would such a transformation be called? I'm sure I've seen this in the literature before but I cant remember where. Pointers? This problem arose in the context of finitary monads where T(X) is the derived operations over a set X for some signature. The naturality square for the unit turns out to be a pullback. This then implies that the unit of the monad is a monic - presumably this is a result in the literature somewhere. Again, pointers? Neil Ghani
In response to the question of Neil Ghani, namely A natural transformation is an indexed family of arrows such that a certain diagram commutes. One could require a stronger condition, namely that the said diagram is a pullback. What would such a transformation be called? I'm sure I've seen this in the literature before but I cant remember where. Pointers? This problem arose in the context of finitary monads where T(X) is the derived operations over a set X for some signature. The naturality square for the unit turns out to be a pullback. This then implies that the unit of the monad is a monic - presumably this is a result in the literature somewhere. Again, pointers? Neil Ghani this phenomenon is now quite well recognised. some call such natural transformations "cartesian", while others use Robin Cockett's term "shapely". For my own contribution to the subject, see [G.M. Kelly, On clubs and data-type constructors, in applications of Categories to Computer Science (Proc. LMS Symposium, Durham 1991), Cambridge Univ. Press 1992, 163-190]. Max Kelly.
Natural transformations for which the naturality square is a pullback are commonly called cartesian: it's not an ideal name for them, but it's quite well established. For the question of when the unit and multiplication of a monad on Sets are cartesian, see section 3 of "Connected limits, familial representability and Artin glueing" by A. Carboni and P.T. Johnstone (Math. Struct. Comp. Sci. 5 (1995), 441--459). Peter Johnstone
A natural transformation is an indexed family of arrows such that a certain diagram commutes. One could require a stronger condition, namely that the said diagram is a pullback. What would such a transformation be called? I'm sure I've seen this in the literature before but I cant remember where. Pointers?
Cartesion natural transformations data:F=>L into the list functor have been used to represent the data-shape decomposition of many data types of the form FX. data_X FX --------> LX | | | F! = | | | L! = shape |-- | length | | F1 --------> L1 data_1 = arity Examples include tree types and array types. See, for example @Article{Jay95b, Author= cbj, Title={A semantics for shape}, Journal={Science of Computer Programming}, Volume=25, Year={1995}, Pages={251--283} } and other papers at http://linus.socs.uts.edu.au/~cbj.
This problem arose in the context of finitary monads where T(X) is the derived operations over a set X for some signature. The naturality square for the unit turns out to be a pullback. This then implies that the unit of the monad is a monic - presumably this is a result in the literature somewhere. Again, pointers?
Neil Ghani
If T(X) = mu_Y. X + P(X,Y) for some polynomial P then the cartesian-ness of the unit for the monad follows from one of the main theorems of the paper above, which shows that taking initial algebras preserves cartesian-ness. Here it is applied to the (cartesian) inclusion X -> X + P(X,Y). Barry Jay | Associate Professor C. Barry Jay www: linus.socs.uts.edu.au/~cbj | Reader in Computing Sciences ftp: ftp.socs.uts.edu.au/Users/cbj
participants (4)
-
Barry Jay -
Dr. P.T. Johnstone -
maxk＠maths.usyd.edu.au -
Neil Ghani