A Transformation, (U|T:V), between arrow worlds U and V, is a mapping, with (U|) = (|T) and (T|) a sub-collection of (|V), which preserves containment relationships between Prior and Post (and, therefore, preserves the property `parallel'). Formally, T must satisfy: for any arrows f and g of U
`Prior(f) subsumes Prior(g)' iff `[g,h] composable implies [f,h] composable'.
If we have two transformations (A|T:B) and (B|S:C), then we can compose them, obtaining (A|S&on;T:C). This is, in turn, a transformation, as may be verified with ease.
Note that a transformation (U|T:V) is equivalently a transformation (reverse(U)| T: reverse(V)) whose action on (|reverse(U))=(U|)=(|U) is identical to the action of T on (|U).
Two parallel transformations, (U|S:V) and (U|T:V), are preConjoinable (in that order) in {transformation (U|:V)} iff: `U relates f to g' &implies; `V relates S(f) to T(g)'. I also describe the pair [T, S] as preconjoinable: note that this implies that [T, S] is likewise preconjoinable in {(reverse(U)|:reverse(V))}. We could equally define preConjoinability of [T, S] as requiring, of each arrow f of U, either that
Note that a transformation, (U|T:V), which respects composability, ie `U relates f to g' implies `V relates T(f) to T(g)', is preconjoinable with itself. [Look out, there's a functor coming.]
Describe a transformation (U|T:V) as
Given a collection of arrow worlds, a collection of transformations on them may form an arrow world in two ways; given (M|T:N) and (U|S:V), one relates S to T when U is N, the other relates S to T when M is U, N is V and [S, T] is pre-conjoinable.
Consider a transformation, T, from the dual of some arrow land, A, to some arrow land W. The image, in this, of an arrow, a, in A is then an arrow, T(a), in W (but it `goes the other way', as we'll see). However, because T acted on the dual of A, we have: for any arrows f, g in A;
I shall also refer to this as a coTransformation from A to W: which just means a transformation from the dual of A to W. Just as a transformation U to V is equally one from the dual of U to that of V, so a coTransformation A to W is equally one from the dual of A to that of W.
Given two composable coTransformations, (U|T:V) and (V|S:W), we have a natural composite S&on;T= (U| u->S(T(u)) :W). Chasing the implications, we obtain, for f, g in U:
Consequently, the natural composition of coTransformations yields transformations. This may at first seem a matter of mere sophistry: however, when we come to describe transformations between an arrow world and its dual, their self-dual relationships may be better described by coTransformations. In physical theory, one might speculate on how the relationship between fermion (which combine pairwise to give bosons, or singly with arbitrarily many bosons to produce a fermion) and boson (which compose to produce bosons) relates to that between coTransformation and transformation. This last relationship has much in common with that between anti-linear maps and linear maps.
What relative of pre-conjoinability do we get between coTransformations ? The natural answer is the face presented, in the base arrow lands, by conjoinability among coTransformations. This says that `f composable before g in U', or `g composable before f in dual-U', implies `T(g) composable before S(f) in V'. In such a case, I may refer to T as `pre-contrajoinable before' S, though only as a way to emphasise the fact that S and T are coTransformations: aside from that, pre-contrajoin is merely a synonym for pre-conjoin. When we come to conjoin (or contrajoin) coTransformations, we'll get a coTransformation (not a transformation, this time).
When we escape from the foundations and begin building some real category theory, a lot of the interesting concepts are best described by diagrams. For instance, one can describe composition in terms of a composable pair of arrows and an arrow beginning where one begins and ending where the other ends. This simple triangle suffices to describe composition. More complex diagrams, and relationships between diagrams, are used to describe a wide variety of structures in categories. A crucial property of diagrams is that they are obliged to respect composability: this serves as the foundation on which to insist that alternate paths within the diagram have equal composite, in which case the diagram is said to `commute'.
I'll describe a transformation from one (typically simple) arrow world to another as a diagram precisely if it is self-preConjoinable. That is to say, it respects composability. The source arrow world is described as the `type' or `kind' of the diagram; and it is described as a diagram of this kind `in' the destination arrow world - so a transformation (U|T:V) is a diagram of kind U in V. (I'll describe a self-preContrajoinable coTransformation as a co-diagram of kind 'its source` in destination.)
Suppose I've factorised one diagram via another: consider the pattern of arrows this latter's image in the target arrow world forms and the pattern formed, therein, by the image of the original diagram. When we have a specific embedding of one arrow world in another (preferably both of them simple), we can take a lively interest in which diagrams of some simple kind, in some arrow world, can be factorised via some particular diagram of that kind in another arrow world. If our diagrams are not merely self-(pre)conjoinable but equal to their self-(pre)conjoint (so they're functors), the notion of factorisation here equates to that of factorising arrows, or their composites, via one another. However, while the notion of a diagram can be defined in an arrow world, it is pretty useless without a composition; and much of its value only emerges in the presence of associativity.
I'll describe a transformation as a point-transformation if it is constant: that is, P is a point-transformation iff (P|) is {p} for some arrow p: likewise for point-coTransformations. [Of course, for P to be a transformation from A to W, this will require p to be self-composable in W if A is non-empty.] I'll describe
iff it is pre-conjoinable between some point-transformation and D.
iff it is pre-contrajoinable between some point-coTransformation and D.