A relation, f, for which f relates x to y and f relates x to z implies y=z is known as a mapping: in which case, whenever f relates x to y, f accepts x as input, yielding y as output; equally, f maps x to y. In the absence of any other notation for the output f produces on accepting x as input, I shall write this as f(x).

With the wording above, a mapping is anything to which values may be offered which will either reject the input or, accepting it, produce an output depending only on the input - not, for instance, on what values have previously been offered to the mapping. Evaluating an expression which depends on using the output of some mapping fails if that mapping rejects the input it is given. One may work from this as definition and, via collections as identities, define the successor mapping on collections - which suffices to deliver the natural numbers, hence lists and, in particular, pairs: whence, also, relations.

The definitive fact, f relates x to y and f relates x to z implies y=z, may equally be rearranged, via reverse(f) relates y to x and f relates x to z implies y=z, as f&on;reverse(f) is an identity. Indeed, f&on;reverse(f) is (f|), the collection of f's outputs, when f is a mapping. [Notice that reverse(f) need not be a mapping - &on; is defined on relations.]

Applying, to mappings, the natural composition of relations, we obtain: r&on;s maps x via y=s(x) to z=r(s(x)) precisely if s accepts x and r accepts s(x). I'll describe this composition as clean precisely when r accepts every output of s: that is, when the composite accepts every input s accepts, which many folk take as a precondition of composition.

Notice that equality is a mapping: when viewed as such, it is called the identity - it accepts any value and yields its input, and its (clean) composite before or after any mapping is that mapping. A collection is, equivalently, the identity on the values in it.

Definitions: some properties

A mapping f distinguishes values x and y if f(x) and f(y) are not equal. The definition of mappings means that x and y are, in that case, not equal. A mapping f distinguishes the inputs of a mapping g precisely if, whenever g accepts both a and b: f(a)=f(b) or f rejects both a and b implies a=b. A mapping which distinguishes its own inputs is described as one-to-one.

A mapping is perfectly at liberty to ignore the value of any input it accepts, producing some fixed output regardless: such a mapping is called constant. The simplest mapping is the empty mapping, which rejects all inputs (and so is trivially both constant and an identity, among many other things).

Untidy further thoughts

Composing a relation, a, with itself and uniting the result with a has an interesting effect. A fixed point of this action is any relation, w, whose self-composite is a sub-relation of w. The transitive completion of a relation a is the intersection of all fixed points of this compose and unite action which have a as a sub-relation. This trivially has a as a sub-relaton, and may readilly enough be shown to be a fixed point of the given action.

A mapping is said to accept n arguments if n is 1 or if n is the successor of some m, with every output of the mapping being a mapping which accepts m arguments. As an extreme case consider a constant mapping which accepts any input and produces itself as output (this may be a bogus concept, though). This then accepts arbitrarily many arguments. A close relative of this mapping is the polymorphic linear map 0, which accepts any member of any linear space which has an additive identity and returns the given additive identity: as such, it isn't actually constant, but the answer is always called 0 and, indeed, the restriction, to any one linear space, of our polymorphic linear map, 0, is just the constant mapping from that linear space to its additive identity (or empty if the linear space has no additive identity).

Consider a space, P, of polymorphic linear maps which accept the same inputs as one another, with all of these inputs being accepted, also, by our polymorphic 0 above. Suppose that, whenever g is a mapping whose outputs are all members of some single linear space whose members are all accepted by each of P's inputs, composing g before any polymorphic linear f in the space yields, as f&on;g, a mapping which accepts the same inputs as g and produces members of some linear space which may depend on g but not on f. If this supposition holds true, then P will be a linear space. If f in P accepts some x, so does 0: and 0(x) is in the same space as x, so the list [x, 0(x)] may be used in place of g. This tells us that f accepts 0(x): which is an additive identity and f is linear, so f(0(x)) is again an additive identity - and, by hypothesis, the linear space it's in doesn't depend on f, only on x, but additive identities are unique in linear spaces, so each f in P yields the same f(0(x)) for any given x accepted by any member of P. Thus every f in P has the same composite f&on;0, which accepts the same inputs as any member of P: and this composite serves as an additive identity for P. Thus P has an additive identity, so 0 accepts P's members, producing this as output: 0(f) = f&on;0 for each f in P, and this does not depend on f. On particular, when each f in P is auto, f&on;0 is just ((|f):0:) and 0's restriction to P is just the constant mapping whose single output is the restriction of 0 to the inputs accepted by P's members. Likewise, the universal identity mapping is, in particular, the identity linear map on any linear space, including the space of polymorphic linear maps. Indeed, the universal linear maps are all natural multiples of this polymorphic linear identity, or derived therefrom.

Consider these mappings, whose inputs are lists:

g-> [x]->g(x)

Which turns any mapping, g, into one which accepts a list (of length 1), provided g accepts that list's element, producing the consequent output.

h-> (1+n:L:)-> h(L(n))(in n, L)

To be accepted as an input, a mapping's outputs must be mappings which accept lists of length n: the resulting output accepts a list, L, of length 1+n, if its last element, L(n), is accepted by h, and its length n head, in n, L, is accepted by the resulting h(L(n)).

We can, equally, build up the list from the other end - for which it helps to know that [L(n), ..., L(1)] is i->L(1+i), aka L&on;successor, when L is a list of length 1+n = successor(n).

k-> (1+n:L:)-> k(i->L(1+i))(L(0))

This time, k must accept lists of length n and produce mappings: k is turned into a mapping which accepts a list, L, of length 1+n provided its length n tail is accepted by k and its initial element is accepted by k's output from this tail.

Now, when k(i->L(1+i))(L(0)) is again a mapping, we can apply the same again to get k(i->M(2+i))(M(1))(M(0)) out of any mapping (2+n:M:), with 2+n formally defined as successor&on;successor(n). We can keep adding further arguments onto the beginning (the right-handend) of our list as long as the resulting outputs are all mappings.

By applying the first mapping of the present description (for whose template I used the name g) and then repeatedly applying this third mapping, we can convert any mapping, f, which accepts n arguments, for any natural n, into a mapping which accepts lists of length n - it feeds the elements of the list to f one at a time, starting with the last element. The same effect may, of course, be achieved by suitable use of the second and first of these mappings. Notice that all three of these mappings are one-to-one, hence invertible

h-> (n:K:) -> (x -> h(0->x &else; 1+i-> K(i)))

This implicitly says that h, to be accepted, must itself accept lists, of length 1+n; it gets turned into a mapping which accepts any K which is the length n tail (the 1, ..., n part) of some input, L, accepted by h: the output produced from this K is again a mapping, which accepts L(0), for any such L, producing h(L) as output. This mapping is just the inverse of the second mapping in this description.

h-> (x-> ((n:K:)-> h(K &else; n->x)), in nonempty)

This, likewise, is the inverse of the second: it turns h, of the same form as before, into a mapping which accepts a value if it's the last element of some list, L, which h accepts; it produces a mapping which accepts the head of any such L, producing h(L) as its output.

f-> (1+n:L:)-> f(L(n))(...)(L(1))(L(0))

This turns a mapping which accepts 1+n arguments into a mapping which accepts lists of length 1+n. That this is well-defined is implied, inductively, by the mappings given before it, of which the first is just a specific case of this last.

We can define Cartesian product as: × accepts any relation, f, whose fixed points are all mappings; ×f accepts a mapping a precisely if a= ((|f): x-> a(x) :f(x)), ie a accepts the same inputs as f and each of its outputs is accepted by the corresponding output of f; ×f(a), meaning (×f)(a), is then ((|f): x-> f(x)(a(x)) :). This is like composition, in that we feed each x through a and then through f; but this time through f only in the sense of through what f produced given the same input. When f is a list and each of its elements is a collection (ie an identity, so f(x)(a(x)) is just a(x), provided a(x) is in f(x)), ×f is an identity on those lists of which each member is a member of the corresponding member of f. This is just the usual Cartesian product of the collections listed by f.

Notice that this generalisation of the Cartesian product expresses the tangent bundle of a smooth manifold, M, as ×(m-> M-tangents(m)) where M-tangents(m) is the collection of tangents to M at m. Each member of the tangent bundle, in these terms, is a mapping which accepts any member, m, of M (ie m is a point on the smooth manifold), producing as output a tangent at m. These mappings are exactly the vector fields or sections of the tangent bundle in the normal parlances of physics and differential geometry, respectively. Notice that, since each M-tangents(m) is a linear space, so is the tangent bundle; likewise, so is each of the other linear bundles derived from it by applying the standard tools of linear algebra (the tensor calculus) to each M-tangents(m) independently.

Looking at a Euclidean space, E, we have the same tangent space at each point and it is naturally isomorphic to the (additive completion of the) Euclidean space itself. Composing each E-tangents(m), the identity on the tangent bundle at a point m of E, with the relevant isomporphism and its inverse, one before and the other after, we convert it to the identity on E; this constitutes a natural isomorphism from ×(m-> E-tangents(m)) to ×(m->E), of which each member is just a mapping from E to itself (strictly, to its additive completion). In general, × of a constant mapping, f, is the identity on mappings from f's inputs to the inputs of f's one output, which are more easily understood in that form than in terms of ×f.

Written by Eddy.