An elementary topos is well-pointed if
the terminal object 1 is a generator;
equivalently: the global section functor is a faithful functor;
equivalently: if are morphisms such that for all global elements , then ;
equivalently: every global element is an epimorphism.
and is nondegenerate, i.e., 1 is not an initial object.
The category Set. Here the global section functor is even (isomorphic to) the identity functor.
Any model of ETCS.
Assuming that one accepts excluded middle in one's metalogic, a well-pointed topos is also Boolean. Similarly, a well-pointed topos is two-valued; that is, the only global elements of the subobject classifier are and (and these are distinct, by nondegeneracy).
The main point of a well-pointed topos in logic is the equivalence of external and internal properties. In particular, a statement in the internal logic of the topos will be satisfied if and only if it holds for all global terms. (For the ‘only if’ part, it is necessary that the topos be nondegenerate.)
To maintain this logical result in constructive mathematics (that is, without excluded middle in the metalogic), one must add the following requirements:
These are analogues, for disjunction and existential quantification, of the nondegeneracy requirement (which is about falsehood). Classically, they follow from the two conditions given above.
Incidentally, a well-pointed topos in a constructive metalogic is still “two-valued” in the sense that a global element of the subobject classifier is false if and only if it is not true. However, it is not two-valued in the (classically equivalent) sense that every global element of the subobject classifier is either true or false.
If is only a pretopos, we have to strengthen the condition that 1 is a generator to the condition that 1 is a strong generator, i.e. for any monomorphism , if every global element factors through , then is an isomorphism. In a category with a subobject classifier (such as a topos), any generator is a strong generator.
This strengthening is important in predicative mathematics, where the category of sets (and in general, a category of sheaves) is a pretopos but need not be a topos. But of course, the same applies whenever one is studying an arbitrary pretopos, not just a predicative version of .
Do we know what these should be in any more general situations?
Mike Shulman: Well, the pretopos version makes sense in any coherent category, and I would bet that it’s the right notion in that generality. In a regular category one might just want to assert that is a (regular-)projective strong generator, which would probably be enough for regular logic. And in a category with mere finite limits, being a strong generator is all one could ask for, and that’d probably be enough for finite-limit logic.
Urs: an attempt
One might like to say that “∞Grpd is essentially the unique (∞,1)-topos with all small limits and colimits that is well-pointed .”
Possibly one should say: an -topos is well-pointed if the terminal object is not the initial one and the global section (∞,1)-functor is faithful…
…which should mean that on hom--groupoids it is a monomorphism in an (∞,1)-category…
…which should mean that for all the image of the morphism in the homotopy category identifies as a direct summand of .
Last revised on December 10, 2020 at 13:52:24. See the history of this page for a list of all contributions to it.