nLab locally decidable topos



Topos Theory

topos theory



Internal Logic

Topos morphisms

Extra stuff, structure, properties

Cohomology and homotopy

In higher category theory




Loosely speaking a locally decidable topos is a topos that is locally Boolean. Whereas in a Boolean topos every object is decidable, in a locally decidable topos every object is a quotient of a decidable object. This results in a reasonable approximation to the concept of ‘being almost Boolean’.

In Lawvere’s approach to cohesion locally decidable toposes are one of the principal classes of petit toposes (Lawvere 1991). In the 1991 paper Lawvere also hypothesizes the discrete base topos 𝒮\mathcal{S} that he contrasts with the cohesive topos of spaces, to be locally decidable.1


An object XX in a topos \mathcal{E} is called locally decidable (or, a quotient of a decidable object) iff there is an epimorphism YXY\twoheadrightarrow X such that YY is a decidable object. \mathcal{E} is called locally decidable iff every object XX is locally decidable.


  • The classifying topos Set[D]=[FinSet mono,Set]Set[\mathbf{D}]=[FinSet_{mono},Set] for the theory of decidable objects D\mathbf{D} is locally decidable. Here FinSet monoFinSet_{mono} is the category of finite sets and monomorphisms, whose opposite category is the carrier of the site for the so called (Myhill-) Schanuel topos.

  • Every localic topos is locally decidable.

  • For every Grothendieck topos \mathcal{E} the full subcategory QD\mathcal{E}_{QD} of locally decidable objects is a locally decidable topos.


  • Proposition. A topos \mathcal{E} is locally decidable iff there is a localic geometric morphism to a Boolean topos, or iff \mathcal{E} has a site (𝒞,J)(\mathcal{C}, J) with all morphisms in 𝒞\mathcal{C} epic.

  • Locally decidable (presheaf) toposes are ‘co-étendues’ in the sense that for a small 𝒞\mathcal{C} the functor category [𝒞,Set][\mathcal{C},Set] is locally decidable precisely if [𝒞 op,Set][\mathcal{C}^{op},Set] is an étendue. Also the all-epic-site property is dual to the all-monic-site property of étendues. Both concepts are subsumed under the notion of having a (sub canonical) site representation with no (non-trivial) idempotents (McLarty 2006, Lawvere 2007,2008).

  • A locally decidable topos has a localic geometric morphism to the Schanuel topos (cf. Johnstone 2002, p.794).


  • Peter Freyd, All topoi are localic - or, why permutation models prevail , JPAA 46 (1987) pp.49-58.

  • Simon Henry, On toposes generated by finite cardinal objects , arxiv:1505.04987 (2015). (pdf)

  • Peter Johnstone, Quotients of decidable objects in a topos , Math. Proc. Camb. Phil. Soc. 93 (1983) pp.409-419.

  • Peter Johnstone, How general is a generalized space? , London Math. Soc. LNS 93 (1985) pp.77-111.

  • Peter Johnstone, Sketches of an Elephant II, Oxford UP 2002. (sec. C5.4 pp.792-803)

  • F. William Lawvere, Qualitative Distinctions between some Toposes of Generalized Graphs , Cont. Math. 92 (1989) pp.261-299.

  • F. William Lawvere, Some Thoughts on the Future of Category Theory , pp.1-13 in Springer LNM vol. 1488 (1991).

  • F. William Lawvere, Axiomatic Cohesion , TAC 19 no. 3 (2007) pp.41-49. (pdf)

  • F. William Lawvere, Cohesive Toposes: Combinatorial and Infinitesimal Cases, Como Ms. 2008. (pdf)

  • Colin McLarty, Every Grothendieck Topos has a One-Way Site , TAC 16 no. 5 (2006) pp.123-126. (pdf)

  1. Lawvere uses the term ‘QD’-topos ( quotient of decidable) for ‘locally decidable topos’ in this paper. He also uses ‘SUD’-object (from separable-unramified-decidable to indicate equivalent concepts in algebra-topology-logic) for what we call a locally decidable object. In later papers Lawvere uses also the terms ‘locally separable’or ‘adequately separable’. The idea to take a locally decidable base topos is probably suggested by Galois theory where ‘locally decidable’ corresponds roughly to ‘product of separable field extensions’ for an algebra over a field kk. This also connects the notion ‘decidable’ via Grothendieck’s Galois theory to the topological notion ‘unramified’.

Last revised on May 20, 2015 at 09:46:00. See the history of this page for a list of all contributions to it.