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.
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).
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:
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.
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).
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
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.
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.
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.