nLab well-pointed topos

Redirected from "well-pointed pretopos".
Contents

Context

Topos Theory

topos theory

Background

Toposes

Internal Logic

Topos morphisms

Extra stuff, structure, properties

Cohomology and homotopy

In higher category theory

Theorems

Contents

Definition

An elementary topos EE is well-pointed if

  1. the terminal object 1 is a generator;

    • equivalently: the global section functor Γ:ESet=E(1,)\Gamma : E \to Set = E(1, -) is a faithful functor;

    • equivalently: if f,g:abf, g: a \rightarrow b are morphisms such that fx=gxf x = g x for all global elements x:1ax: 1 \to a, then f=gf = g;

    • equivalently: the family of all global elements x:1ax: 1 \to a is a jointly epimorphic family.

  2. and EE is nondegenerate, i.e., 1 is not an initial object.

Examples

Properties

Strong generation

In a well-pointed topos, the terminal object is even an extremal generator,

  • equivalently: the global section functor E(1,)E(1,-) is a conservative functor.
  • equivalently: if f:ABf:A\to B induces a bijection E(1,A)E(1,B)E(1,A) \cong E(1,B), then ff is an isomorphism.
  • equivalently: if m:ABm:A\rightarrowtail B is a monomorphism such that every global element 1B1\to B factors through AA, then mm is an isomorphism.

To prove the last version, let χ A:BΩ\chi_A : B\to \Omega be the classifying map of AA, and let :BΩ\top : B\to \Omega be the classifying map of the maximal subobject. If every global element b:1Bb:1\to B factors through AA, then χ Ab=b\chi_A b = \top b for all such bb. Hence χ A=\chi_A = \top by well-pointedness, so AA is isomorphic to the maximal subobject.

Note that in any category with equalizers, an extremal generator is automatically a generator, since the equalizer of two parallel morphisms is the maximal subobject just when the two morphisms are equal. So the above statements are also equivalent to well-pointedness.

Boolean properties

Assuming that one accepts excluded middle in one's metalogic, a well-pointed topos is also Boolean. To see this, let UAU\rightarrowtail A be a subobject and ¬U\neg U its Heyting complement. Then by definition, the global elements of ¬U\neg U are precisely the global elements of AA that do not factor through UU. But then every global element of AA factors through U¬UU \cup \neg U, hence by strong generation U¬U=AU\cup \neg U = A.

Similarly, a well-pointed topos is two-valued. In other words, that is, the only global elements of the subobject classifier are \top and \bot (and these are distinct, by nondegeneracy) – or equivalently, the only subterminal objects are 00 and 11. To see this, note by strong generation a subobject of any object is uniquely determined by the global elements that factor through it. But 11 has only one global element, so it only has two possible global elements.

Finally, a well-pointed topos has split supports. For the support of any object AA must be either 00 or 11 by two-valuedness. If it is 00 then A0A\cong 0 also and its support is split. Otherwise, A0A\ncong 0; now consider the two coproduct inclusions inl,inr:AA+Ainl, inr : A \rightrightarrows A+A. Their pullback is 00 by disjointness. Since A0A\ncong 0, we have inlinrinl\neq inr, hence by well-pointedness there is a global element a:1Aa:1\to A such that inlainrainl a \neq inr a. Thus aa splits the support of AA.

Conversely, we have the following:

Theorem

If EE is nondegenerate (i.e. 101\ncong 0), Boolean, two-valued, and split supports, then it is well-pointed.

Proof

This is Proposition 9.33 on p. 314 of Johnstone, Topos Theory, attributed there to Freyd. Let ABA\rightarrowtail B be a monomorphism such that every global element of BB factors through it. Then BA\forall_B A is a subterminal object, hence either 11 or 00. If it is 00, then its complement ¬ BA= B¬A\neg\forall_B A = \exists_B \neg A is 11, which is to say that ¬A\neg A is well-supported. Hence, since supports split, ¬A\neg A has a global element, which is impossible since every global element of BB factors through AA. Hence it must be that BA=1\forall_B A = 1, which implies A=BA=B.

Thus, in external classical logic, a topos is well-pointed if and only if it is nondegenerate, Boolean, two-valued, and has split supports. In particular, a nondegenerate two-valued topos satisfying the external axiom of choice is well-pointed.

Logical properties

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.)

Well-pointedness and concrete categories

The category Set of sets and functions is both well-pointed and concrete. However, not every concrete category is a well-pointed category: the category FieldField of fields and field homomorphisms is concrete, but is not well-pointed because it doesn’t have a terminal object. Moreover, not every well-pointed category is a concrete category, as well-pointed categories are not required to be concrete categories: most models of ETCS aren’t defined to be concrete.

The distinction between well-pointed categories and concrete categories is the distinction between elements and global elements in a concrete category, as it is not true that elements and global elements (if they exist) coincide in general.

Generalizations

In constructive mathematics

To maintain this logical result in constructive mathematics (that is, without excluded middle in the metalogic), one must add the following requirements:

  1. the terminal object is indecomposable, and
  2. the terminal object is projective.

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.

In a pretopos or coherent category

If EE is only a pretopos or a coherent category, we have to strengthen the condition that 1 is a generator to the condition that 1 is an extremal generator, i.e. for any monomorphism m:ABm:A\to B, if every global element 1B1\to B factors through mm, then mm is an isomorphism. In a category with a subobject classifier (such as a topos), any generator is a extremal 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 SetSet.

In a lextensive category

If EE is only a lextensive category, such as in a category of sets without quotient sets (as commonly found in the syntactic category of an extensional type theory), then EE is well-pointed if 11 is only a noninitial indecomposable extremal generator.

In more general categories

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 11 is a (regular-)projective extremal generator, which would probably be enough for regular logic. And in a category with mere finite limits, being a extremal generator is all one could ask for, and that’d probably be enough for finite-limit logic.

Well-pointed (,1)(\infty,1)-toposes

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 (,1)(\infty,1)-topos H\mathbf{H} is well-pointed if the terminal object is not the initial one and the global section (∞,1)-functor Γ:HGrpd\Gamma : \mathbf{H} \to \infty Grpd is faithful…

…which should mean that on hom-\infty-groupoids it is a monomorphism in an (∞,1)-category

…which should mean that for all X,YHX,Y \in \mathbf{H} the image of the morphism Γ X,Y:H(X,Y)Func(Γ(X),Γ(Y))\Gamma_{X,Y} : \mathbf{H}(X,Y) \to Func(\Gamma(X),\Gamma(Y)) in the homotopy category identifies H(X,Y)\mathbf{H}(X,Y) as a direct summand of Func(Γ(X),Γ(Y))Func(\Gamma(X),\Gamma(Y)).

As an axiom schema of separation

Well-pointedness in a Boolean category (if using classical logic) or a Heyting category (if using intuitionistic logic) could also be represented, in addition to the terminal object being a strong generator, by a version of the axiom schema of bounded separation.

Let us define the following

  • A Δ 0\Delta_0-variable is a global element variable.
  • A Δ 0\Delta_0-context is a context only containing Δ 0\Delta_0-variables
  • An Δ 0\Delta_0-atomic formula is an equality of global elements
  • A Δ 0\Delta_0-quantifier is a quantifier over a Δ 0\Delta_0-variable.
  • A formula whose only atomic subformulas are Δ 0\Delta_0-atomic and whose only quantifiers are Δ 0\Delta_0-quantifiers is a Δ 0\Delta_0-formula.

A Boolean category or Heyting category \mathcal{E} is well-pointed if

  • the terminal object 1Ob()1 \in \mathrm{Ob}(\mathcal{E}) is a strong generator: given objects AOb()A \in \mathrm{Ob}(\mathcal{E}) and BOb()B \in \mathrm{Ob}(\mathcal{E}) and monomorphism m:ABm:A \hookrightarrow B, if for every global element x:1Bx:1 \to B there exists a global element y:1Ay:1 \to A such that my=xm \circ y = x, then mm is an isomorphism.

  • the axiom schemata of bounded separation holds for global elements: for any Δ 0\Delta_0-formula ϕ(x)\phi(x) with global element free variable x:1Bx:1 \to B, there exists an object AOb()A \in \mathrm{Ob}(\mathcal{E}) and a monomorphism m:ABm:A \hookrightarrow B such that for any global element x:1Bx:1 \to B, ϕ(x)\phi(x) holds if and only if there exists a global element y:1Ay:1 \to A such that my=xm \circ y = x.

In fact, given that \mathcal{E} is a finitely complete category, we could use this as the definition of a well-pointed Boolean category or well-pointed Heyting category, and thus in a foundational categorical set theory:

  • Improper subsets: given a subset ABA \subseteq B with chosen injection m:ABm:A \hookrightarrow B, if for every element xBx \in B there exists an element yAy \in A such that m(y)=xm(y) = x, then AA is the improper subset of BB and mm is a bijection.

  • Bounded separation: for any Δ 0\Delta_0-formula ϕ(x)\phi(x) with free variable xBx \in B, there exists a subset ABA \subseteq B with chosen injection m:ABm:A \hookrightarrow B such that for every element xBx \in B, ϕ(x)\phi(x) holds if and only if there exists an element yAy \in A such that m(y)=xm(y) = x.

References

  • Sheaves in Geometry and Logic, Sections VI.1 and 10. Thm. in this article is a strengthening of SGL’s Prop. VI.1.7. SGL’s Section VI.10 is a comparison of well-pointed toposes to RZC (Restricted Zermelo with Choice).

  • Peter Freyd, Aspects of Topoi, Bull. Austral. Soc. Math. no.7 pp.1-76,467-480 (1970).

  • Peter Johnstone, Topos Theory, Academic Press New York 1977. (also available as Dover reprint, Minneola 2014). See Section 9.3.

For constructive well-pointedness of Heyting categories as a structural axiom schemata of separation in addition to the terminal object being a strong generator, see:

Last revised on January 10, 2023 at 02:48:44. See the history of this page for a list of all contributions to it.