Boolean topos


Topos Theory

topos theory



Internal Logic

Topos morphisms

Extra stuff, structure, properties

Cohomology and homotopy

In higher category theory




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:


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

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.

Some characterisations


For \mathcal{E} a topos, then the following are equivalent:

  1. \mathcal{E} is a Boolean topos;

  2. Every subtopos of \mathcal{E} is Boolean.

  3. Every subtopos of \mathcal{E} is an open subtopos.

  4. Every subtopos of \mathcal{E} is a closed subtopos.

(Johnstone, prop. A 4.5.22)


Let jj be a Lawvere-Tierney topology on \mathcal{E}. Then j\mathcal{E}_j is Boolean iff there exists a subterminal object UU such that jj is the largest topology such that U1U\rightarrowtail 1 is jj-closed.

(Johnstone 2002, p.220)


\mathcal{E} is Boolean iff the only dense subtopos of \mathcal{E} is \mathcal{E} itself.

Proof. Suppose \mathcal{E} is Boolean. ¬¬=\mathcal{E}_{\neg\neg}=\mathcal{E} is the smallest dense subtopos (cf. double negation). Conservely, suppose \mathcal{E} is not Boolean then ¬¬\mathcal{E}_{\neg\neg} is a second dense subtopos.


In a lattice of subtoposes the 2-valued Boolean toposes are the atoms.

See this proposition.


Let \mathcal{E} be a topos. Then automorphisms of Ω\Omega correspond bijectively to closed Boolean subtoposes. The group operation on Aut(Ω)Aut(\Omega) corresponds to symmetric difference of subtoposes.

This result appears in Johnstone (1979). (See also Johnstone (2002), A1.6.11 pp.66-67.)


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 \mathcal{E} is any topos, the category of sheaves for the double-negation topology is a Boolean subtopos of \mathcal{E}.

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

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

Relation to measure theory

Boolean toposes are closely related to measurable spaces (e.g Jackson 06, Henry 14).


  • Andreas Blass, Andrej Scedrov, Boolean Classifying Topoi , JPAA 28 (1983) pp.15-30.

  • Radu Diaconescu, Axiom of Choice and Complementation , Trans. AMS 51 no.1 (1975) pp.176-178. (pdf)

  • Simon Henry, From toposes to non-commutative geometry through the study of internal Hilbert spaces, 2014. (pdf)

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

  • Peter Johnstone, Automorphisms of Ω\Omega , Algebra Universalis 9 (1979) pp.1-7.

  • Peter Johnstone, Sketches of an Elephant vols. I,II, Oxford UP 2002. (A4.5.22, D3.4, D4.5)

Revised on September 17, 2015 15:12:39 by Thomas Holder (