An autonomous category

[Marco Grandis <grandis@dima.unige.it>]

The Lawvere category of extended positive real numbers has also an
autonomous structure, with a multiplicative tensor product (instead
of the original additive one). Has this been considered somewhere?

To be more explicit:

The well-known article of Lawvere on "Metric spaces..." (Rend. Milano
1974, republished in TAC Reprints n. 1) introduced the category of
extended positive real numbers, from  0 to oo (infinity included),
with arrows  x \geq y,  equipped with a strict symmetric monoidal
closed structure:  the tensor product is the sum, the internal hom is
truncated difference (with oo - oo = 0).

Now, the same category can be equipped with a multiplicative tensor
product,  x.y.
Provided we define  0.oo = oo  (so that tensoring by any element
preserves the initial object oo), this is again a strict symmetric
monoidal closed structure, with  hom(y, z) = z/y.  Now, the
'undetermined forms'  0/0  and  oo/oo  are defined to be 0.
The new multiplicative structure is even *-autonomous, with
involution  x* = 1/x  (and 'nearly' compact).

(Note that this choice of values of the undetermined forms comes from
privileging the direction  x \geq y,  which is necessary if we want
to view metric spaces, normed categories etc. as enriched categories).

Marco Grandis