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.
I just feel like bringing up a trap I fell into recently. A model of ETCS is a well-pointed topos with natural numbers object and satisfying AC, right? Being well-pointed, the terminal object is (externally) projective and connected; I’m assuming here that the meta-logic is classical, as needed.
The trap I’d been falling into is thinking that projectivity and connectedness is the same as saying is right exact, i.e., preserves finite colimits. I don’t think that can be right, because it would imply that preserves the natural numbers object, since natural numbers objects in toposes can be characterized in terms of finite colimits (famous result due to Freyd). If that were the case, then there can be no “nonstandard” elements in (taking in as our “standard”).
So far I haven’t found a spot in the nLab where there is an outright error, but I do think there are spots that are at least misleading. Over at Freyd cover, Theorem 1, it says “The terminal object in the initial topos is connected and projective, i.e., preserves finite colimits.” Actually we do prove the stronger result that is right exact, but it’s that “i.e.” which seems a little misleading.
Lawvere does make a far-sighted remark on this in his ETCS paper (the TAC version), where he observes (Remark 8, page 31) that preserves coequalizers of kernel pairs = equivalence relations, but “it seems unlikely that it is necessary that be right exact, since as remarked above, the construction of the RST [reflective symmetric transitive] hull involves and by Gödel’s theorems the nature of the object may vary from one model of any theory to another model.” I call this far-sighted because I don’t think he was in possession of Freyd’s theorem (1972) or even of topos theory when that was first written.
That’s a good point and should be emphasized somewhere (everywhere)? I might have fallen into that trap myself on occasion. All finite colimits can be constructed from finite coproducts and coequalizers, and all coequalizers can be constructed from quotients of equivalence relations, but the latter requires some “infinitary” construction (either internal, by using an NNO, or external, by using countable unions/coproducts). Thus, a functor which preserves finite coproducts and epimorphisms, hence also quotients of equivalence relations, still may not preserve all coequalizers.
Thanks for the comment, Mike – I don’t think I was aware of the remark that preservation of finite coproducts and epis implies preservation of quotients of equivalence relations. I’m trying to think of a good place to put some of the information under discussion.
Hmm, possibly I meant to say that preservation of finite limits (as any representable does) and also epis is what implies preservation of quotients. Possibly that requires the domain and codomain to be regular categories. I don’t remember the exact statement, but I think something like that is true.
A functor that preserves pullbacks and regular epimorphisms will also preserve effective quotients of equivalence relations. So if the domain is an effective regular category, then such a functor preserves all quotients of equivalence relations.
That’s it, thanks. Here we’re in a topos, so no problem.
1 to 6 of 6