The Disjoint Sum

Needing heavy re-work via stuff currently in the basement. I'd like to have the disjoint sum of two mappings from ordered sets to some given domain, (: f+g :D), be a mapping from (|f)+(|g) to D. The disjoint sum I defined while founding relations turns r into disjoin(r) which relates x to s precisely if s is a singleton sub-relation of some member of ({x}:r|). And I understood that when I defined it. disjoining a list, h, of relations, I find that this relates i to s precisely if s is some singleton sub-relation of h(i).

The Disjoint Sum is a construction which takes two sets and combines them to obtain a set in which the two originals may be embedded with no overlap: equally, it is a set via which any pair of functions, one from each of the given sets, can be factorised. If the sets are ordered, the construction can be extended to respect the ordering. The construction for two sets may be extended as a construction on an arbitrary list of sets, subject to suitable natural isomorphisms. The construction may equally be regarded as a construction combining a pair of functions. It is usual to denote disjoint sums using a + inscribed in a circle: however, I shall make do with plain + for now.

Given two sets, A and B, we define their disjoint sum, A+B, to be the collection of symbols of form (a,) with a in A or of form (,b) with b in B. If A and B are ordered, we can extend their orders to A+B by deeming every (a,) to come before every (,b). Given two functions (A|f:C) and (B|g:D), we define their disjoint sum, f+g, to be (A+B|f+g:C+D) mapping any (a,) to (f(a),) and any (,b) to (,g(b)).

Consider direct sums with the empty set: for any set A, A+{}= {(a,): a in A} is isomorphic to A, as is {}+A. Furthermore, {}+{}={}. We consequently make no distinction between a set and its direct sums with empty.

We can flatten any disjoint sum A+B of sets onto the union of A and B via (A+B| (a,)->a, (,b)->b: A&union;B). This flattening is an isomorphism when A and B are disjoint (ie their intersection is empty), which is where the disjoint sum (or disjoint union) gets its name. Flattening is particularly simple when applied to a disjoint self-sum: any set's self-union is the set itself. In particular, when we have two functions with common destination, (A|f:C) and (B|g:C), we can flatten f+g to (A+B|f+g:C), known as the disjoint union of f and g. It should be noted that the standard embeddings of A and B in A+B compose with this to yield f and g as appropriate: in this sense, A+B is a minimal set via embeddings of A and B in which one may factorise any pair of functions, as above.

If we have three sets, A, B and C, we can combine them (in that order) in either of two ways: as A+(B+C) or as (A+B)+C. That these two are naturally isomorphic follows from (A+(B+C)| (a,)->((a,),), (,(b,))->((,b),), (,(,c))-> (,c): (A+B)+C) and its inverse. We can, therefore, define A+B+C as either of these interpreted modulo natural isomorphisms. Using the same associative step repeatedly allows us to define the disjoint sum of any list of sets, up to natural isomorphisms. Note that the sets must come as a list (and, thus, be ordered), even if we are not interested in any ordering of the individual sets - this is just to keep the isomorphisms natural even when there are repeated entries in the list (or when the entries aren't all disjoint).

We can equally define the disjoint sum of a list of sets to be the collection of symbols having the form of a list with all but one entry blank, as (a,,), (,b,), or (,,c), and that one entry being a member of the set whose position in the list of sets corresponds to the position of that entry in the symbol in which it appears. Thus A+B+C contains symbols of form (a,,) with a in A, (,b,) with b in B and (,,c) with c in c. The associative step above can be used to prove that replacing any contiguous sub-list of the list of sets with the disjoint sum of that sub-list yields a naturally isomorphic result.

Maintained by Eddy.