On Wed, 13 Nov 2002, Michael Abbott wrote:
Am I being dim here? In an extensive category (coproducts are preserved by pullbacks and are disjoint), can I cancel thus: X+1 ~= Y+1 ?=>? X ~= Y ?
This is true in any topos -- and, as far as I can see, the argument works in arbitrary extensive categories. Unpacking the isomorphism and its inverse, one gets isomorphisms X \cong X_1 + X_2, 1 \cong U + V and Y \cong Y_1 + Y_2 where X_1\cong V \cong Y_1 and X_2\cong Y_2.
So far I have neither a proof nor a counterexample. If this cancellation principle exists it'll be slightly subtle, since 0+N ~= 1+N, and so we'd only be able to cancel adding a restricted class of (finite?) objects.
It works for a bit more than the class of (Kuratowski-)finite objects in a topos, since the argument above works if 1 is replaced by any subobject of 1. My guess is that, in a topos, it works for all \tilde{K}-finite objects in the sense of "Sketcehs of an Elephant", section D5.4. Whether it works for all R-finite objects in the sense of section D5.5, I'm not sure. Peter Johnstone 14-Nov-2002 22:43:21 -0400,1921;000000000000-00000000