When a mapping, C, has mappings as its outputs, it induces a relation W= `y in (|C(x)), x->y', which we can view as an arrow land. I'll refer to such a C as a composition for W precisely if:
It is usual to write a composition using an `infix operator', that is C(h,g) is written g&on;h with &on; possibly replaced by, for example, + or × (and note the order reversal). I'll describe a composition as factorising if, for every arrow f of W, there is some composable pair [g,h] of W with composite g&on;h = f. I will, in fact, usually work with factorising compositions.
The two conditions on Post and Prior are just what it takes to make it possible to compose any composable list. For any sub-list of length 3, [f, g, h], of a composable list, we obtain h in Prior(f&on;g) and f in Post(g&on;h): thus, for any sub-list of length 2, its composite is composable with the rest of the list if it replaces the pair. Thus we can shorten a composable list of length greater than one by replacing some adjacent pair of its members with their composite: applying this, repeatedly, to progressively shorter lists, we can compose any finite composable list. Indeed, composing any finite sub-list of a composable list and replacing the sub-list with the composite always yields a composable list. A list of length n gives us (n-1)! ways to compose it (corresponding to the possible bracketings of the list as a hierarchy of composable pairs): for now, we know nothing about relationships between the values of the composites thus implied.
I'll describe a composition as robust precisely if the subset relations in the definition above are equality: that is, the prior of a composite is the prior of its first (right-most) arrow and its post is that of its last. I may describe a composition as fragile if it is not robust.
Composition enables us to define, below, various important properties. These enrich transformations to the point where we can conjoin them. When composition is associative, it becomes possible to prove a few things and the door is at last open to the definition of the category.
Any composition, &on;, on an arrow world, W, implies one, transpose(&on;), on its dual, reverse(W): f transpose(&on;) g = g&on;f. (Composable(W)| (f,g)-> (g,f): Composable(W*)); for any composable (g, f) in W*, g &on;* f = f &on; g. This is the dual of the composition.
Similarly, given two [or more] arrow worlds, U and V, with compositions, &on;U and &on;V, we may form the product arrow world and obtain a composition on this, the product composition, given by: for any ((u, v), (f, g)) in Composable(U × V), (u, v) &on;U × V (f, g) = (u &on;U f, v &on;V g).
In an arrow world, W, with composition, &on;, I'll say that an arrow, f, of W is
I'll describe a composable pair (f,g) as an inverse pair if its composite, in the given order, is an identity and it is composable in the reverse order: in such a case, I'll call f a left-inverse for g and g a right-inverse for f. I'll call f and g (or the pair (f,g)) `mutually inverse' if (f,g) and (g,f) are both inverse pairs.
Monic and epic are dual to one another: iso, zero and identity are self-dual and the transpose of any inverse pair is an inverse pair in the dual arrow world. It is worthy of note that:
One arrow, f, factorises (or `may be factorised') via another, g, ⇔ g appears as a member of some composable list of which f is a composite. I'll describe an initial sub-list immediately followed by an appearance of g as a `head' of the factorisation; I'll describe a final sub-list immediately preceded by an appearance of g as a `tail' of the factorisation.
Arrows f and g are isomorphic (to one another) ⇔ each factorises via the other. I'll refer to the arrows forming the factorisations as the `isomorphism diagram' between f and g: I'll say that this diagram `begins with' the heads (if any) of each and `ends with' their tails. If each factorisation yields a non-empty head, these are mutually composable (ie antiparallel); the same applies to tails.
Factorisation is self-dual (with `tail' dual to `head' and `begin' dual to `end'). Note that:
I now have three concepts competing for very similar territory:
Even with robustness and associativity, the isomorphism diagram between isomorphic arrows merely begins with an antiparallel monic pair and ends with an antiparallel epic pair. I have no proof that iso or invertible arrows are implied - if you find, or know of, one please tell me.
In Set, at least two of the competitors can be proven equivalent; I would not be surprised if all three could be shown equivalent, though I'm not sure it could be done constructively - I suspect at least one of the proofs would need the axiom of choice or the law of the excluded middle (a pair of monstrous devices). It remains that the three concepts are distinct, at least in principle, except in so far as their own defining properties imply their equivalence - a proof in Set assumes far more than their definitions.
In the absence of confidence in the equivalence of these three properties, I'll rely on making it clear which I'm assuming. I shall be focussing on mutual factorisability (isomorphism) much of the time: where I need invertibility or iso, I'll make the distinction (well, subject to an error rate that you can help me keep low by warning me if you notice it).
For an associative composition, let a factorisation diagram be a factorisation of one arrow, f, via another, g, in which one particular instance of g (lest it be repeated) indicated in the list. This thus consists of f as the composite of: possibly a head; the indicated instance of g; and possibly a tail. I'll describe the factorisation of I'll describe a factorisation diagram of one arrow, f, via another, g, if, for any other factorisation, typically aogob=f, there is some instance of g in this second factorisation, and some instance of g in the putatively unique factorisation for which: if the portions of the With associativity, we can discuss a notion of uniqueness for a factorisation of one arrow via another
Notice that a null identity is self-composable and equal to its self-composite, so a composite of initial with terminal (since it is both), thus zero. As it is composable before some initial (itself), its Post has precisely one member composable before each arrow in its world: being composable after some terminal, it's Prior has precisely one member composable after each arrow in the world. Its posts are all initial and its priors are all terminal: its composite before any of its (initial) posts is the given post, which is therefore composable after any of its (terminal) priors. This yields a zero arrow, via any null identity, in each homset of the arrow world.
In the presence of two null identities, a and b, we obtain (from each being initial and the other terminal) unique morphisms c in Hom(a,b) and d in Hom(b,a): these are, in turn, both initial and terminal, therefore null. Being equal to their products with the null identities they are thus also zero. Their products are c &on; d, which is in Hom(b,b) = {b}, and d &on; c, which is in Hom(a,a) = {a}. Thus c and d are mutually inverse, while a and b are isomorphic.
A relation, f, is called a function precisely if, for each s in (|f), the set ({s}:f|) has exactly one member. It is usual to write this member as f(s), with the result that f= {(s,f(s)): s in (|f)}. When (|f) and (f|) are subsets of A and B, respectively, f is described as a partial function from A to B, which I'll write (A:f:B) [`partial' should, in practice, be understood as qualifying the use of `from', rather than `function' - f is a function from part of A to B]. I shall include the assertion (|f)=A, when it holds, by writing (A|f:B) instead: in such a case, f is described as a function from A to B. Please understand any of A, f and B introduced by such forms as joining the discourse in the relevant rôle.
We can define a composition on relations which implies one for functions: composing (f,g) yields a function f &on; g = ((|g:(|f))| a-> f(g(a)) |((g|):f|)), which `goes' via the intersection of (g|) and (|f). When (g|) and (|f) are disjoint, this is the empty function: which inevitably happens for a great variety of pairs of functions. The arrow world Partial is formed by taking any pair of functions to be composable, with the composite given above. This composition is associative and robust but has no identities, nor has it any monic, epic or iso arrows. Plenty of its arrows are, however, factorisable via one another.
We could define a variant on this which deals with triples: a function along with two sets - its nominal source and destination. We then distinguish between (A:f:B) and (C:f:D) even when the intersections of A and C with (|f) are equal, as are those of B and D with (f|). This is workable, but introduces a distinction which I find ugly. I suspect it will have interesting parallels, though: consider the representation of functions as functors between subset embedding categories.
We could try restricting composition to pairs (f,g) for which (g|) and (|f) have non-empty intersection: this cuts out all the uninteresting cases which yield empty composites, and it would probably make sense therefore to exclude the empty set and its functions entirely from the discourse. However, a list (f,g,h) is then composable precisely if (|f) meets (g|) and (|g) meets (h|): but f &on; g need not be in Post(h), nor need g &on; h be in Prior(f). [Proof: On a set, g = (:i->i:), is composable before and after its restriction to any non-empty subset: its composite with its restriction, in either order, is the restriction. Let f and h be g's restrictions to disjoint subsets: then (f,g) and (g,h) are composable, with composites f, h respectively, but (f,h) is not composable.] Thus, on this restricted arrow world, we can't use the usual composition: it doesn't satisfy the definition. To remedy this, we need a better constraint on (g|) and (|f).
The arrow world Set is formed by taking a pair, (f,g), of functions to be composable, with composite f &on; g again, only when (g|) is a subset of (|f). This restriction suffices to make Set a category. Furthermore, if you can stomach the law of the excluded middle and the (not merely finite) axiom of choice, the factorisations of isomorphic functions via one another can be done using functions which are iso and invertible. I'm not sure whether those heavy tools were needed: they were certainly used when, as an undergraduate, I was taught, with proof, that `epic and monic' implies `invertible' - but I know this can be proved without them, for Set.
A named function f may equally be denoted (:s->f(s):), and, for any expression, I'll write (A: s->expression(s) :) for the function {(s,expression(s)): s in A}, which implicitly restricts s in A to those for which expression(s) is defined. If this restriction, in context, makes mention of A redundant, I may well take the liberty of omitting it.
Notice that, for any functions f, g: f &on; g = {(s,f(g(s))): s in (|g)} = ((g|): r->f(r) :(f|)) &on; ((|g): s->g(s) :(g|)). Thus two partial functions (A::B) and (B::C) composed in the order (B::C) &on; (A::B) yield a result (A::C). Adding a third, (C::D), we see (C::D) &on; (B::C) &on; (A::B) = (A::D), and so on - the source-side (left) of the first-applied (rightmost, so written last) function is the source-side of the composite; and the destination-side (right) of the last-applied (leftmost, written first) is the destination-side of the composite. You have my sympathy if this ever trips you up - it is, none the less, a natural conflict between `reading from left to right' and the way many scientists (myself included) are used to writing function application.
Written by Eddy.