RE: Why binary products are ordered

[S.J.Vickers@open.ac.uk]

 
> One might say that the ordering of binary products, with a first
projection
> and a second projection, is spurious but inevitable.  
> 
> The two components of a binary product must be distinguished, as Colin
> McLarty explained, but they must be allowed to be isomorphic.  The usual
> way we handle a situation like this in mathematics is to index them, in
> this case by a two-element set.  ...

Two points.

First, even in computer programming, one can lose the need for an ordering
by using what are often called "record types", so that

  <your age in years=99, your height in inches=70>

denotes the same record as

   <your height in inches=70, your age in years=99>

I don't think there's anything mysterious about this. A pair of sets can be
described as a function f: X -> 2, and we can quite happily replace 2 by any
isomorphic set (but we don't have to choose the isomorphism) such as

   M = {"your height in inches", "your age in years"}

The product of f: X -> M is then a universal solution to the problem of
finding

   g: YxM -> X  over M

and this is equivalent to the usual characterization once you have chosen
the isomorphism between M and 2.

A second, and deeper, point is that constructively there are unorderable
2-element sets, so there is a kind of binary product in which the ordering
first vs. second projection is impossible. It uses the same "record type"
construction.

An example in sheaves over the circle O is the twisted double cover M (edge
of a Mobius band). It is finite decidable set with cardinality 2. It is
isomorphic to 2 (i.e. 2xO) locally but not globally. It has no global
elements and no global total ordering. If you have a sheaf X with a map f: X
-> M, then locally it falls into two parts whose product you can take. It
can be expressed as

  Pi f = {(i,x,j,y) in MxXxX | f(x) = i and f(y) = j and j = s(i)} / ~

where s: M -> M swaps the two elements and ~ is the equivalence relation
generated by (i,x,j,y) ~ (j,y,i,x).

Globally, Pi f is the equalizer of two maps from X^M to M^M, namely f^M and
the constant identity map: so set theoretically it is the set of sections,

   {g: M -> X | g;f = Id_M}

The universal property is that for any YxM -> X over M you get a unique
corresponding Y -> Pi f.

The second description with X^M probably looks more natural to a topos
theorist, but the first one has the advantage of being geometric.
 

Steve.