Given the naturals, {0, 1, 2, 3, …}, we can define repetition on relations:
One may as readily take repeat(0,r) = (|r:) with repeat(1+n,r) =
repeat(n,r)&on;r, but the choice above works well for mappings: repeating no
times a mapping which doesn't deliver all of its inputs as outputs has the
desired effect of accepting the same inputs as the mapping (and considering the
same ones equivalent), but doing nothing to them
(aside from declaring
that it considers some of them equivalent).
There's a natural addition on naturals, and a natural multiplication; these may, indeed, be defined by:
with both + and . being symmetric, i.e. n+m = m+n and n.m = m.n, obtained by inductive proofs. The structure of the naturals makes these interact well with repeat: repeat(n+m) = (: repeat(n,f)&on;repeat(m,f) ←f :) and repeat(n.m) = repeat(n)&on;repeat(m).
Now, for natural n, repeat(1+n) maps mappings to mappings and maps monics to monics; in contrast, repeat(0) doesn't - though it does maps each relation to an equivalence and both mappings and relations to identities, i.e. collections. As a result, I'm going to leave 0 out of the discussion hereafter.
Now, as each repeat(n) is a relation, we may take its reverse, (: r ← repeat(n,r) :), so define:
Which is pretty much reverse&on;repeat, save for restricting out n=0. (Note that this is a quite different thing from reverse(repeat) = ({naturals}: n ← repeat(n) :) - quite another matter). Note that share(n) is, in general, a relation - if repeat(n) maps two relations to the same value, share(n) relates that value to each of them.
When we compose repeat(n)&on;share(m), we get (: repeat(n,f) ← repeat(m,f) :), whose inputs are all outputs of repeat(m), i.e. in (| repeat(m) :), even if n and m have a common factor, i, and some f in (| repeat(i) :) aren't in (| repeat(m) :). Still, repeat(n)&on;share(m) relates x to y if x is repeat(n,f) and y is repeat(m,f) for some relation f; so repeat(m,x) is repeat(n.m,f), as is repeat(n,y).
Composing in the other order, share(m)&on;repeat(n) gives (: repeat(m,f) = repeat(n,g), f←g :), which patently subsumes repeat(n)&on;share(m) - read f for x, g for y in the foregoing. [So, given the choice, share(m)&on;repeat(n) is the more helpful representation of n/m, for which m\n seems an appropriate synonym.]
One may thus construe the positive rationals as {share(1+i)&on;repeat(1+j): i, j are naturals} or, at worst, the collection of composites of its members.
Now, to describe (m\n).(q\p), take share(m)&on;repeat(n)&on;share(q)&on;repeat(p) and observe that it's subsumed by share(m)&on;share(q)&on;repeat(n)&on;repeat(p) = share(m.q)&on;repeat(n.p), i.e. (m.q)\(n.p).
Now, consider addition: repeat(n+p) = (: repeat(n,f)&on;repeat(p,f) ←f :) and use share(m)&on;repeat(n) in place of repeat n, and likewise with q for p, noting that, were it but a mapping, the former would map f to share(m,repeat(n,f)), so our putative replacement for repeat(n,f)&on;repeat(p,f) is share(m,repeat(n,f))&on;share(q,repeat(p,f)). Fortunately, cheating is easy: we know (m\n)+(q\p) has to be (m.q)\(n.q+m.p), i.e. share(m.q)&on;repeat(n.q+m.p) which would map f to share(m.q, repeat(n.q, f)&on;repeat(m.p,f)), which we now merely need to relate to the above.
Not that it's pretty yet.
This construction yields a natural consequence for any commutative binary
operator; characterize the last by a mapping V, for which each f in (|V:) has
(:f|) = (:V|) and this subsumes (|f:), V combines a with b to yield V(a,b) also
written a+b, so that V = (: (: a+b ←a :) ←b :), with a+b = b+a for all
a, b in (:V|). (:V|) will be closed under
the addition
denoted by
+ only if (|V:) is closed under composition, i.e. f, g in (|V:) implies f&on;g
in (|V:). When V is monic, V embeds (:V|) in (|V:), which is a collection of
relations (V: :(:V|)). As relations these are amenable to repeat and share; if
(|V:) is closed under composition, repeating any of its members produces
another, so (|V:) will be closed under repeat(1+i) for each natural i; if V is
also monic, we'll be able to infer, for any given a in (:V|), a unique member of
(:V|) which V maps to repeat(n,V(a)); we can describe this member of (:V|) as
n.a, thereby establishing reverse(V)&on;repeat(n)&on;V as a scaling
of
(:V|) by each positive natural n.
Equally, reverse(V)&on;share(m)&on;repeat(n)&on;V enables us to express the rationals as scalings of (:V|); notably, reverse(V)&on;share(m) is simply reverse(repeat(m)&on;V), which gives the expression a clearer form.
The crucial properties of V were: it's monic; {relations} subsumes (|V:) so we can apply repeat's outputs to its members; every composite of members of (|V:) is a member of (|V:). We may be able to relax the last to require composites, or even just repeats, of members to be, each, subsumed by a unique member of (|V:), probably imposing, in such a case, that, given two members of (|V:), either one of them subsumes the other or their intersection is empty. These suffice, in any case, to express V as the binary operator
a.k.a. (: (: reverse(V, V(a)&on;V(b)) ←a :) ←b :), further
exposing the parallels with the action of the rationals - which naturally also
apply themselves as scalings
for the addition
inferred from V.
When all that works, we get a V for which {(V:|(:V|))} subsumes (|V:).
Write P for the collection of positive rationals, on which I'll suppose I've
built addition and multiplication, each of which is commutative and cuddly,
along with a strict order respected by both. From addition we obtain (P: sum
|{non-empty finite (P:f:)}), extending the bulk action of addition on lists by;
exploiting the natural one-to-one relation between any given finite (:f|) and
some natural (backed up, when f isn't a mapping, by the implied finite
enumeration of each (|f:{x}) with x in (:f|), required for f to be finite
as a relation, i.e. the union of some list of atomic relations), while; relying
on commutativity to ensure that sum(f) won't depend on which one-to-one
relation you use, between F and that natural (and, likewise, between each
(|f:{x}) and its associated natural).
For distinctness, while keeping the the names 0 and 1 for the naturals {}
and {{}}, I'll refer to the rational identity, share(1) = share(1)&on;repeat(1)
= repeat(1), as one
and, in so far as I chose to talk about it, I'll
refer to the rational additive identity, share(1)&on;repeat(0) = repeat(0),
as zero
; but note that zero isn't in P, whereas one is; and, since sum is
defined on non-empty mappings to P, which is closed under addition, sum's
outputs are all in P.
Among mappings (P::), I can define an addition by:
This means (f+g)(x) is f(x)+g(x) when both accept x as input, is f(x) when only f accepts x and is g(x) when only g accepts x; if neither f nor g accepts x as input, nor does f+g. [In the specification given, these cases are catered to by applying sum to (: k(x)←k :)&on;[f,g], for given x (note: [f,g] is a list; it maps 0 to f, 1 to g); the composite maps 0 to f(x) if f accepts x as input, otherwise it ignores f; likewise for 1 and g. If both ignore some value (offered as x), the composite is empty, so not in (:sum|), so sum(…)←x rejects the value - refuses to let us bind x to it. If either accepts a value, however, the composite is a non-empty mapping (P: :{0,1}), which sum duly accept; our value is mapped to the sum of the outputs of this, whether there be one or two of them.]
These suffice to define the universal simplex, Simplex = {mappings (P:f:n):
sum(f) = one, n is natural}. Note that (P:f:n) isn't constrained to accept all
members of n as inputs; only to draw its inputs only from n, delivering outputs
in P; it may ignore
some members of n. Since sum(f) is involved in the
constraint, f is implicitly obliged to be non-empty (i.e. accept at least one
input); but the constraint sum(f) = one equally obliges f to be non-empty, even
if sum's definition is extended to allow sum(empty) = zero. [Since sum respects
addition on mappings, sum(f)+sum(g) = sum(f+g), and f+empty = f for every
(P:f:), we're obliged to have sum(f)+sum(empty) = sum(f), making sum(empty) an
additive identity - i.e. zero.]
Now, Simplex spans an infinite-dimensional linear domain within {(P::)},
under the addition just given and the scalings natural to that domain (induced
by composing each (P:f:) before (: a.x ← x :P) for some a in P, to give (P:
a.f(y)←y :) as a.f; then (: a.f←f :{(P::)}) is scale by a
for
any a in P). When describing a finite-dimensional simplex, we can readily
restrict to {(::n) in Simplex} for any natural n. When n is 0, this is clearly
empty, as 0 is empty, i.e. {}, so the only (P:f:0) is f = empty, which sum
definitely doesn't map to one.
Next we have {(P::1) in Simplex}, with 1 = {0} having only one element, and
(P:f:1) in Simplex forbids f to be empty, so f is simply the list [f(0)], its
sum is f(0), so f(0) must be one, making f = [one], so {(::1) in Simplex} =
{[one]}, a.k.a. {[{{}}]}. This has exactly one member; I'll call this member,
[one], the canonical vertex
.
So far so dull. For collections M, N of naturals, describe {(::N) in
Simplex} as a face
of {(::M) in Simplex} precisely if M subsumes N; and
as a proper face
if N and M are distinct. Taking N = M = {naturals},
Simplex = {(::{naturals}) in Simplex} is a face of itself; likewise, any face of
Simplex is a face of itself. Describe a one-to-one correspondence between two
faces, (F|g|H), as simplicial
if (hmm, well … it's continuous and)
for each face E of F or I of H, (|g:I) is a face of F and (E:g|) is a face of H;
describe F and H as simplicially equivalent in such a case - that this is an
equivalence is easy to verify.
Whenever there is a one-to-one correspondence, (N|s|M), between two
collections of naturals, it induces ({(P::M) in Simplex}: f&on;s ← f
:{(P::N) in Simplex}) as a (very well-behaved, e.g. continuous) simplicial
equivalence between their respective faces. For every collection of naturals,
M, there is some such (N|s|M) with N either {naturals} or a natural, so
every face of Simplex is simplicially equivalent either to Simplex itself or to
some {(::n) in Simplex} with n natural; call these the natural
faces of
Simplex. For any two members of {{naturals}, n: n is natural}, one of them
subsumes the other; so, for any two natural faces, one of them is a face of the
other. Thus, for any two faces of Simplex, one of them is simplicially
equivalent to a face of the other.
Note that Simplex has plenty of proper faces (associated with infinite
collections of naturals) with which it is simplicially equivalent. Describe a
face of Simplex as finite-dimensional
iff it isn't simplicially
equivalent to Simplex, i.e. iff it is simplicially equivalent to {(::n)
in Simplex} for some natural n. Since every f in Simplex is (P:f:n) for some
finite n, hence in a finite-dimensional face, Simplex (though
infinite-dimensional) is the union of its finite-dimensional faces. Further,
every finite-dimensional face of Simplex is {(::N) in Simplex} for some finite
collection, N, of naturals; if we take successor(unite(N)) we get a natural
which subsumes N; so every finite-dimensional face of Simplex is a face of a
natural face of Simplex, so Simplex is the union of its natural faces, each of
which is finite-dimensional.
The mappings (P: f(n) ←f :Simplex), for natural n, are scalar
functions of position
on Simplex; their sum is ({one}::Simplex) but they are
otherwise as independent as this allows. On any finite-dimensional face, only
finitely-many of these functions accept any f in the face; if we partition these
scalar fields into those with n in N and those with n in M, for some disjoint
finite collections N, M of naturals, we can define scalar fields (P: sum(:f:N)
←f :Simplex) and (P: sum(:f:M) ←f :Simplex); the first is undefined on
{(::M) in Simplex} and one on {(::N) in Simplex}; likewise for the second but
with the two faces swapped; on the original face, {(::U) in Simplex} with U the
union of N and M, these two scalar fields sum to one everywhere. In this sense,
the faces associated with N and M are opposite
faces of the face
associated with U.
Earlier we visited the empty face, {(::0) in Simplex}, and the canonical vertex, {(::1) in Simplex}. We now have the means to continue with the faces associated with progressively larger naturals. First, note that any natural face {(::n) in Simplex} has, for each i in n, a face {(::{i}) in Simplex}; and a mapping (P:f:{i}) with sum(f) = one must be, as f accepts only one input, the unique mapping ({one}:|{i}), so each {(::{i}) in Simplex} face is simplicially equivalent to the canonical vertex, and {(::n) in Simplex} has n such faces. A face simplicially equivalent to the canonical vertex is described as a vertex; every vertex of Simplex is just {({one}:|{n})} for some natural n. (Note that all faces simplicially equivalent to the empty face are, in fact, empty, so identically the same thing as one another: there is only one empty face, whereas there are many distinct vertices.)
For the natural face S = {(::1+n) in Simplex}, for some natural n > 0, we have a vertex {(::{n}) in S} = {({one}:|{n})}; this is opposite the face {(::n) in S}, which I'll suppose we've already described. We have complementary scalar functions (P::S) defined by f(n)←f and sum(:f:n)←f; the former is one on the {n}-vertex, the latter is one on the face opposite it; the latter is defined everywhere except on the vertex, the former everywhere except on the opposite face. Whenever one = p+q in P, we have (S: ({q}::{n}) +p.f ←f |{(::n) in S}) as an embedding of the face, opposite our {n}-vertex, in S. This clearly varies continuously in p, q and f; its outputs are in S, every position in S appears as an output and, for every g in S, there's a unique choice of p, q and f (namely q = g(n), p = one-q, f = (:g:n)/p) which yields that g as output, unless g is in either the {n}-vertex or the face opposite this. At these two ends, the above function approaches the identity on {(::n) in S} and the constant mapping which maps this whole face to the opposite vertex. We may, thus, construe the function as a continuous deformation of the face down on to the point.
Thus the face {(::2) in Simplex} is just the trail left by moving its {0}-vertex to its {1}-vertex - i.e. it's a line. Likewise, {(::3) in Simplex} is obtained by scaling down this line, by the varying factor p < one, while moving it towards the {2}-vertex, forming a triangle.
Valid CSS ? Valid HTML ? Written by Eddy.