in defense of strictness

[selinger@mathstat.dal.ca (Peter Selinger)]

Here is a bit of hyperbole. Hopefully entertaining.

Suppose, hypothetically, that category theorist X had a close look at
the definition of "inverse": morphisms f : A -> B and g : B -> A are
inverses if fg = id_B and gf = id_A. Suppose that she makes the
following argument:

"The definition of inverse is really too strict. It requires an
equation between objects, namely, the domain of f must equal the
codomain of g, and vice versa. A natural thing to do would be to
weaken the definition to replace this equality by an isomorphism."

So what definition would she come up with?

Definition. Let f : A -> B be a morphism. A *weak inverse* of f is
given by the following data:

(1) Objects A', B', and a morphism g : B' -> A'
(2) an isomorphism a : A' -> A
(3) an isomorphism b : B' -> B
(4) such that the following diagram commutes:
          g
    A' <------- B'
  a |           | b
    v     f     v
    A --------> B

Everybody can see that this is nonsense. First, one must have a prior
definition of isomorphism before one can define inverse in this
way. But the definition of isomorphism depends on inverses, so this is
circular. Second, each "weak inverse" in the above sense already gives
rise to an ordinary inverse, namely a o g o (b^{-1}).  Perhaps
category theorist X would like to formulate this as a Coherence Lemma
("each weak inverse is canonically equivalent to a strict
inverse"). But it is clearly nonsense nevertheless.


Naive attempts to define a weak version of dagger structure fall into
the same category. Recall the definition of a dagger structure on a
category, namely a contravariant, involutive, identity-on-objects
functor. Or in elementary terms: to each f : A -> B, associate
some f+ : B -> A, such that f++ = f, (fg)+ = (g+)(f+), and id+ = id.

Each category theorist (including myself) who sees this definition
immediately dislikes the identity-on-objects part. The first instinct
is to try to weaken it. But what would one come up with? After one or
two failed attempts, it seems that the "correct" definition is the
following: a contravariant functor (-)+, and for each object A a
chosen unitary isomorphism a_A : A+ -> A, such that one has the
following diagram (but note that it doesn't have to commute):

          f+
    A+ <------- B+
a_A |           | a_B       [not assumed to commute]
    v     f     v
    A --------> B

Plus, there should be some further requirement to replace the
"involutive" condition (i.e., the obvious diagram involving f and f++
should commute), and perhaps a coherence condition or two.

Note that a_A and a_B must be assumed to be unitary. The analogous
definition where they are just isomorphisms does not work for a
variety of reasons. For example, this is supposed to be a weakening of
the strict situation, and identities are always unitary.

The problem with any such definition is the same as for the "weak
inverses" hyperbole above. First, to define dagger in this way, one
must have a prior definition of "unitary", but the definition of
"unitary" depends on "dagger", so this is circular. Second, given any
weak dagger structure in this sense, it already induces a strict
dagger structure, namely by using a_A o f+ o (a_B^{-1}) : B -> A as
the strict dagger. One could again regard this as a coherence lemma,
but it's clearly a pointless one.


Actually, my leading example of "weak inverses", while ludicrous, is
not entirely besides the point. One of the main reasons for
considering dagger structure is so that we can define a morphism
u : A -> B to be unitary if u+ is the inverse of u. Trying to say this
with the "weak" dagger structure inevitably leads to weak inverses.

In light of all this, I completely agree with Mark Weber that dagger
structure should be strict and that is what we should live with.

-- Peter



[For admin and other information see: http://www.mta.ca/~cat-dist/ ]