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.
Here is something dead elementary which I want to bounce off you to hear you say either “Sure, because this is a special case of the general statement …” or “Urs, you are making the following silly mistake …”.
[edit: of course what follows is nonsense]
Let be a small category and three functors/presheaves with colimits , respectively. Write for the presheaf constant on the singleton set and assume that
is a pullback diagram in .
I seem to be claiming that then also
is a pullback diagram, in , hence that colimits of fibers are fibers of colimits.
Proof:
I do an elementary analysis. Write for the component of over .
Express the elements of as equivalence classes of under the equivalence relation generated by .
Then the key observation is that if maps under to the equivalence class of the point , then there is a representative of this class such that is the point itself.
This is because if then either already or else it must be true that there is such that . In other words, it does not happen that the other way round for some we have , since by the naturality of we have .
But then by naturality of it follows that if then either already or else we have that is mapped to by , using the commutativity of
In summary this says that if an equivalence class maps to the equivalence class of the point, then at least some of its representatives do themselves map to the point. These identify a class , observing that is the set of equivalence classes in among elements that sit over the point.
But the equivalence classes that map to constitute the pullback , and so we have established that this pullback is .
Right?
Urs, I’m pretty sure there’s a mistake here, because I think it would imply that the colimit functor preserves monomorphisms . The key is that any monomorphism embeds in a pullback square of your form.
Specifically, there is a lemma that in a topos, if is any monomorphism, then the pushout square for any diagram of the form
is also a pullback. This is easy to verify directly for a presheaf topos because the lemma is obviously true for and since both limits and colimits in a presheaf topos are computed objectwise. Now take (so that we arrive at your pullback diagram). If the colimit functor preserved this pullback, then would have to be a monomorphism (since of course is a monomorphism, and the pullback of a monomorphism along any arrow such as is also a monomorphism).
But the colimit functor does not preserve monomorphisms generally. You know this already, but for the sake of completeness (or for anyone who didn’t know this), here is an example. Take to be the “walking span” , and consider the functor where and are both the same inclusion of a 1-element set into the same 2-element set, and consider the functor where and are both identity functions on that 2-element set. There is an obvious monomorphism . However, has 3 elements, and has 2 elements.
I didn’t look super-closely at your argument, but my rough impression is that you checked an existence condition but not a uniqueness condition. It may be true (I don’t know off-hand) that the colimit functor preserves weak pullbacks (where ’weak’ here involves existence but not uniqueness), and that’s what your argument is proving.
Thanks, Todd. I should have been actively aware of that simple pushout-along-mono-is-pullback-argument, but to my shame I wasn’t.
And I see the (necessarily stupid) error in my above argument now (for what it’s worth, what I ignored was, in the above words, that when restricting to elements over the point single equivalence classes may break up into several, if the zig-zag connecting elements runs via elements not over the point).
I was in the middle of struggling with an attempt to generalize the proof of the statement that for nice enough simplicial topological groups the geometric realization of morphisms out of simplicial manifolds preserves homotopy fibers, when suddenly I thought that if the above were true, I could make progress. But shortly after posting that nonsense here I realized that my whole strategy was collapsing anyway. :-/
Okay, sometimes I just need to indulge in errors a bit.
I don’t think there should be any shame in not being actively aware of that argument, but I would like to say that my own awareness was enhanced by working through the material recorded at AT category, or more precisely through the discussion between Freyd and Pratt at the categories list which forms the background of that entry. Freyd makes it clear that he finds that lemma utterly remarkable!
Freyd makes it clear that he finds that lemma utterly remarkable!
I used to wonder about good criteria for when an -pullback in an -topos is also an -pushout. Now that you mention this statement in the context of ordinary toposes, I suspect that it should have evident generalizations to the higher categorical context, with suitable notions of higher monomorphisms.
Will try to think about this, but not right this moment.
Incidentally, the fact that:
is of course trivial, by the definition of elementary topos (take and : any monomorphism is obtained by pulling back this universal monomorphism). This gives another way of seeing the statement I described as “key” in the first paragraph of #2.
1 to 6 of 6