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 C, that an object X is connected iff hom(X,−):C→Set 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 ∑αUα→X 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 X≃Uα 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 X≅Uα for exactly one α if the other Uβ 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