(For most purposes, we may assume that these distance functions are pointwise-bounded: taking only finite values. On the other hand, for full generality in constructive mathematics, we must allow the distance functions to take nonnegative extended upper real values, although again we may assume them to be pointwise-bounded and pointwise-located for many purposes.)
Let be a collection of such distance functions.
Consider the following potential properties of :
Reflexivity: For every and , we have .
Transitivity (a version of the triangle identity): For any there exists an with
for all .
Symmetry: For every , there is an with for all . (In light of Isotony below, we may require .)
Nontriviality: There exists a . (In light of Isotony below, we may require for all .)
Filtration: For all , there is an with and for all . (In light of Isotony below, we may require for all .)
Isotony: If and is a distance function with for all , then .
With the aid of abstract algebra? (but nothing too fancy), we may view these same 6 axioms in another light, as follows.
The order is given pointwise:
The corresponding join operation is also pointwise:
The monoid operation is defined so:
The involution is defined so:
Then the same 6 axioms may be expressed as follows:
Reflexivity: For every , we have .
Transitivity: For every , there exists such that .
Symmetry: For every , there exists such that . (In light of Isotony, we may require ; in other words, .)
Nontriviality: There exists a . (In light of Isotony, we may require .)
Filtration: For all , there is an with and . (In light of Isotony, we may require .)
Isotony: If and is a distance function with , then .
Reflexivity and Transitivity are a binary–nullary pair whose unbiased combination is as follows:
for each list .
Similarly, Nontriviality and Filtration are a binary–nullary pair whose unbiased version states (in light of Isotony) closure under finitary joins; but this is properly discussed at ideal.
A collection of distance functions that satisfies all of (1–6) is a prometric; if we drop (3), then we still have a quasi-prometric. If we are working with quasi-prometrics generally, then one that happens to satisfy (3) is called symmetric; in other words, a prometric is precisely a symmetric quasi-prometric.
Finally, a prometric space is a set equipped with a prometric, and likewise a quasi-prometric space is a set equipped with a quasi-prometric.
We sometimes wish to consider collections of distance functions that generate (quasi)-prometrics. In the following table, a collection satisfying the conditions listed on the left has the name on the right:
|1,2, 4,5||quasi-prometric base|
Here we always use the original (either elementary or sophisticated) formulation of (3–5); one might consider what it means if these satisfy the stronger versions rewritten in light of Isotony, but it's getting a bit far along into centipede mathematics to actually give these things names.
A (quasi)-prometric base is precisely an ideal base whose generated ideal is a (quasi)-prometric. We may also speak of a (quasi)-prometric subbase as an ideal subbase (that is, an arbitrary collection) whose generated ideal base is a (quasi)-prometric base, or equivalently whose generated ideal is a (quasi)-prometric. A pre-(quasi)-prometric is always a (quasi)-prometric subbase, but not conversely; but thinking too hard about subbases risks more centipedes.
A pre-quasi-prometric is symmetric if its generated quasi-prometric is symmetric (hence a prometric); a quasi-prometric base is symmetric iff it is a prometric base (and the analogous result holds for subbases), but a symmetric pre-quasi-prometric need not be a pre-prometric. Some authors may require a strong version of Symmetry in which the distance functions are all individually required to be symmetric; that is, (or simply ). Every prometric has a base with this property; in particular, if is a prometric, then
is a prometric base that generates , and it is this base that some authors may refer to as the prometric itself. (I write ‘some authors may’, but there are few authors on this subject; still, it's the sort of thing that somebody might do.)
A pre-quasi-prometric is pointwise-bounded if every is pointwise-bounded; that is, for every (or simply ). If is a (quasi)-prometric, then
is a (quasi)-prometric that is very similar to (in particular, they are uniformly equivalent?), and some authors may prefer to work with . Indeed, when pointwise boundedness is not required, some authors may call the structure extended, as an instance of the red herring principle. However, requiring pointwise boundedness interferes with the more sophisticated approaches to (quasi)-prometrics; in particular, is not pointwise-bounded. (It is possible that prometric spaces would work better with a closure condition that would make generate .)
Most definitions are no more complicated when phrased in terms of (quasi)-prometric bases or even pre-(quasi)-prometrics, and some constructions give one of these more naturally than the generated (quasi)-prometric. When working in predicative mathematics, it is preferable to work exclusively with (quasi)-prometric bases, as the generated (quasi)-prometric will typically be a proper class. However, it is ultimately the generated (quasi)-prometric (even if referred to only obliquely) that matters.
Any (quasi)-gauge is a (quasi)-prometric base; similarly, given any (quasi)-pseudometric , the singleton is a (quasi)-prometric base (and its generated (quasi)-gauge in turn generates the same (quasi)-prometric). One might call a (quasi)-prometric (space) simple if it is generated in this way by a (quasi)-pseudometric; this term is used analogously in the theory of syntopogenous spaces, but the term (quasi)-pseudometrizable is more likely to be understood. (See Subcategories below.)
A short map between (quasi)-prometric spaces and is a function such that for every , we have . We write for the category of prometric spaces and short maps, and similarly for the category of quasi-prometric spaces and short maps.
If the (quasi)-prometrics of and are presented by bases, then this is equivalent to saying that for any basic distance function on , there is a basic on such that for all . Thus, for (quasi)-pseudometric spaces and (quasi)-gauge spaces considered as (quasi)-prometric spaces, this reduces to the usual notion of short map (i.e., distance-decreasing map). Hence the category of gauge spaces and short maps is included as a full subcategory of , and similarly with in .
Since includes the categories of metric spaces and uniform spaces (disjointly), so does . Likewise, since includes the category of topological spaces (disjointly from metric and uniform spaces), so does .
There is also another embedding of into , however, which is notably simpler than its embedding into (both easier to state and not using dependent choice). Given a uniform space , we define for each entourage a distance function
(Again, this may be defined constructively as an infimum.) The collection of such is a base for a prometric on . The short maps between such prometric spaces are precisely the uniformly continuous ones, so this defines another embedding of into . The full image of this embedding consists precisely of those prometric spaces generated by a base of -valued functions. Note that replacing by any positive real number also defines an embedding of into , but a yet different one.
Conversely, every prometric induces a uniformity, where the entourages are the sets
In this way every short map induces a uniformly continuous map as well. This operation is compatible with the above inclusions of , as well as with the inclusion via .
As observed by Lawvere, an extended quasi-pseudo-metric space is a category enriched over the monoidal category . In other words, it is a monoid (or monad) in the bicategory of matrices with values in this monoidal category. Analogously, an extended quasi-prometric space is a monad in the bicategory whose hom-categories are the categories of pro-objects in the hom-categories of .
Generalized uniform structures
|binary relation||preorder||quasiuniformity||symmetric relation||equivalence relation||uniformity|
|binary function to||quasipseudometric||quasiprometric||symmetric binary function||pseudometric||prometric|
|topogeny||quasiproximity||syntopogeny||symmetric topogeny||proximity||symmetric syntopogeny|