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

- for P in {Post, Prior}, `P(f) subsumes P(g)' implies `P(T(f)) subsumes P(T(g))'
*ie*:- in U, `Post(f) subsumes Post(g)' implies, in V, `Post(T(f)) subsumes Post(T(g))'; and
- in U, `Prior(f) subsumes Prior(g)' implies, in V, `Prior(T(f)) subsumes Prior(T(g))'.

`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

- (U-Post(f)| T :V-Post(S(f))) or that
- (U-Prior(f)| S :V-Prior(T(f))).

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

- full
- iff, for every arrow f of U and every arrow v of V-Parallel(T(f)) there is an arrow g in U-Parallel(f) for which T(g) = v. [cf: (locally) surjective.]
- faithful
- iff, whenever arrows f, g of U are parallel, `T(f) = T(g)' implies `f = g' [cf: (locally) injective].

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;

- Post(f) subsumes Post(g) &implies; Prior(T(f)) subsumes Prior(T(g)); and
- Prior(f) subsumes Prior(g) &implies; Post(T(f)) subsumes Post(T(g)).

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:

- Post(f) subsumes Post(g) &implies;
- Prior(T(f)) subsumes Prior(T(g)) &implies;
- Post(S&on;T(f) subsumes Post(S&on;T(g)), and;
- Prior(f) subsumes Prior(g) &implies;
- Post(T(f)) subsumes Post(T(g)) &implies;
- Prior(S&on;T(f)) subsumes Prior(S&on;T(g)).

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

- a diagram C in V as a pre-Cone for some diagram D in V
iff it is pre-conjoinable between some point-transformation and D.

- a co-diagram C in V as a pre-coCone for some co-diagram D in V
iff it is pre-contrajoinable between some point-coTransformation and D.

$Id: transform.html,v 1.5 2004/02/29 21:14:19 eddy Exp $