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.
It is asserted at internally projective object that a projective object in a topos is internally projective. I’m having a hard time seeing this. Can anyone help?
Isn’t the statement that the object is internally projective equivalent to the statement that is projective in the stack semantics? If so then the assertion follows quite quickly, I think.
If it’s easy to see, would you be able to write down a proof, written at a level understandable to a reader of Mac Lane-Moerdijk? I confess that I’m not following your suggestion.
Wait: I knew this topic seemed familiar! See this discussion. Why wasn’t the page internally projective object ever corrected?
Maybe I was just jumping to the assumption that the page was in fact correct :-) I’m glad you found the old discussion so quickly.
This comment also relates to the ongoing COSHEP/PAx thread.
I think I might have an example that shows that not even presheaf toposes need satisfy the internal PAx. This example would serve two purposes: to show the need for care in the examples under the topos section, and to give an example of an externally projective object which is not internally projective, which is the topic of this thread.
Let be the poset whose objects belong to the set , and whose non-identity morphisms consist of those of under its usual linear order, and a morphism from each in to , and a morphism from each to . I’m going to try to argue that is not internally projective in the presheaf topos . (Same for of course.)
Let be the presheaf defined by and , with transition map the obvious inclusion. Let be the presheaf defined by and for all . The unique morphism is clearly epic. I am going to try to argue that the induced map is not epic, more particularly that the function is not surjective.
By the usual formula for the exponential (internal hom) , we have
Let be a natural transformation. The components at and are fairly uninteresting: they just amount to identity maps . The component at amounts to a map . The naturality condition means that we have a matching family where the element maps to under the inclusion . In other words, a natural transformation amounts to an element of the inverse limit , in other words the intersection of the , which is empty.
Thus we calculate to be empty. On the other hand, it’s pretty easy to calculate that . Obviously is not surjective.
I have a new question about the notion of “internally projective”. For a notion to be sensibly regarded as “internal” (and in particular, for it to correspond to some statement in the stack semantics), it ought to be stable under pullback. Is it true that if is internally projective in , then is internally projective in for any ? If so, then right now I’m having a hard time seeing why.
The answer to my question in #6 is yes, see this answer. I’ve added this and a more explicit stack-semantics characterization to the page internally projective object.
1 to 7 of 7