Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
In response to a very old query at connected object, I gave a proof that in an infinitary extensive category , that an object is connected iff merely preserves binary coproducts.
The proof was written in classical logic. If Toby would like to rework the proof so that it is constructively valid, I would be delighted.
Offhand, that proof looks irremediably nonconstructive! Now I need to think about this theorem.
Toby: That was my reaction too. Now I’m curious whether the theorem is even true constructively.
I now tend to think it’s not true constructively.
Any objection if I port the query box over to the Forum (or just erase it entirely)?
I have small problem with the proof as it stands: the phrase “the canonical map is an isomorphism”. This is patently false. I’m not sure what the chain of statements is supposed to be, because later we have the claim at for exactly one .
Am I just being thick?
Why do you say it’s false? Isn’t that just part of what extensivity means? It doesn’t contradict for exactly one if the other are initial.
Duh, of course. I am being thick. [hangs head in shame]
Since no objections were raised, I am removing from connected object and recording here the old query box, which I hope the most recent edit has addressed:
Mike Shulman: It’s not obvious to me that preserving binary coproducts is enough to ensure preservation of infinitary coproducts. Unless you meant “preserves all finite coproducts”?
Toby: I just copied what was at connected space. It's true that homming out of a connected space preserves all coproducts, but it's not clear to me whether that is a theorem at this level either. Maybe we need to distinguish finitarily connected objects of finitarily extensive categories from infinitarily connected objects of infinitarily extensive categories?
Thanks!
1 to 9 of 9