nLab
Boolean topos
Contents
Definition
A Boolean topos is a topos that is also a Boolean category .

There are several conditions on a topos that are necessary and sufficient to be boolean: * Every subobject has a complement (the general definition of boolean category). * Every subobject lattice is a Boolean algebra . * The subobject classifier $\Omega$ is an internal Boolean algebra. * The maps $\top, \bot: 1 \to \Omega$ are a coproduct cone (so in particular, $\Omega \cong 1 + 1$ , but this alone is not sufficient).

Properties
As a context for foundations
The internal logic of a boolean topos with natural numbers object can serve as foundations for “ordinary” mathematics, except for that which relies on the axiom of choice . If you add the axiom of choice, then you get (an internal version of) ETCS ; conversely, if you use an arbitrary topos, then you get constructive mathematics . (For some high-powered work, you may also need to add a version of the axiom of replacement or an axiom of Grothendieck universe s.)

Every cartesian closed boolean pretopos is in fact a topos. This is why ‘generalised predicativism ’ (with function types but not power types) is necessarily a feature of constructive mathematics only.

Relation to measure theory
Boolean toposes are closed related to measurable spaces (e.g Jackson 06 ).

Examples
With excluded middle in the meta-logic, every well-pointed topos is a Boolean topos. This includes Set and models of ETCS .

The topos of canonical sheaves on a Boolean algebra is Boolean.

If $E$ is any topos, the category of sheaves for the double-negation topology is a Boolean subtopos of $E$ .

Any topos satisfying the axiom of choice is Boolean. This result is due to R. Diaconescu; see excluded middle for a brief discussion.

Barr's theorem implies that any topos $E$ can be covered by a Boolean topos $F$ , in the sense of there being a surjective geometric morphism $f \colon F \to E$ .

References
Matthew Jackson, A sheaf-theoretic approach to measure theory , 2006 (pdf )

Revised on April 3, 2014 05:47:02
by

Urs Schreiber
(145.116.129.110)