nLab localic topos



Topos Theory

topos theory



Internal Logic

Topos morphisms

Extra stuff, structure, properties

Cohomology and homotopy

In higher category theory




In intrinsic terms, a topos is localic if it is generated under colimits by the subobjects of its terminal object 11.

In equivalent but extrinsic terms, a category is a localic topos if it is equivalent to the category of sheaves on a locale with respect to the topology of jointly epimorphic families (accordingly, every localic topos is a Grothendieck topos).

The frame of opens specifying the locale may indeed be taken as the poset of subobjects of 11 (i.e., internal truth values). From the perspective of logic, localic toposes are those categories which are equivalent to the category of partial equivalence relations of the tripos given by a complete Heyting algebra (as before, the complete Heyting algebra may be taken as the poset of internal truth values).


  • A Grothendieck topos EE is a localic topos if and only if its unique global section geometric morphism to Set is a localic geometric morphism.

    Thus, in general we regard a localic geometric morphism ESE \to S as exhibiting E as a “localic S-topos”.

  • Moreover, just as localic topoi can be identified with locales, for any base topos SS the 2-category of localic SS-topoi is equivalent to the 2-category Loc(S)(S) of internal locales in SS.

    LocTopos(S)(Topos/S) locLoc(S). LocTopos(S) \simeq (Topos/S)_{loc} \simeq Loc(S) \,.

    Here LocTopos(S)LocTopos(S) is the 2-category whose

    Then the 2-category LocToposLocTopos is equivalent to the 2-category LocLoc of locales (see C1.4.5 in the Elephant).

    The 2-category LocLoc is actually a (1,2)-category; its 2-morphism are the pointwise ordering of frame homomorphisms. Thus this equivalence implies that LocToposLocTopos is also a (1,2)-category, and moreover that it is locally essentially small, in the sense that its hom-categories are essentially small. (The 2-category ToposTopos of all toposes is not locally essentially small.) Assuming sufficient separation axioms, the hom-posets of LocLoc, and hence LocToposLocTopos, become discrete.


Many familiar toposes EE, even when they are not localic, can be covered by a localic slice E/XE/X (“covered” means the unique map X1X \to 1 is an epi). For example, if GG is a group, then E=Set GE = Set^G is not itself localic, but it has a localic slice Set G/GSetSet^G/G \simeq Set that covers it. Such a topos is called an étendue (cf. Lawvere’s 1975 monograph Variable Sets Etendu and Variable Structure in Topoi).1

A significant result due to Joyal and Tierney is that for any Grothendieck topos EE, there exists an open surjection FEF \to E where FF is localic. This fact is reproduced in Mac Lane and Moerdijk’s text Sheaves in Geometry and Logic (section IX.9), where the localic cover taken is called the Diaconescu cover of EE.

Then, using methods of descent theory, Joyal and Tierney deduce that every Grothendieck topos is equivalent to the category BGB G of continuous discrete representations of a localic groupoid GG. (Their result is relativized so as to hold internally over any Grothendieck topos SS as base.) This should be regarded as a major extrapolation of Grothendieck’s Galois theory (as in SGA 1), where it is shown that the etale topos of a field kk is equivalent to the category of continuous discrete representations of the fundamental pro-group Gal(k¯/k)Gal(\bar{k}/k), where k¯\bar{k} denotes the separable closure of kk. It was a watershed event for the penetration of localic methods in topos theory.

The connection with propositional logic

Recall that a geometric theory \mathbb{P} over a signature with no sort symbols is called propositional. Such a signature can contain at most 0-ary relation symbols but lacks variables and, accordingly, \mathbb{P} admits only sequents over the empty context consisting of nested conjunctions or (infinitary) disjunctions of such relation symbols - in other words, logic boils down to propositional logic.

Propositional theories have the peculiarity that their classifying toposes always exist regardless of the availability of a natural numbers object in the base topos (cf. for details&references see at classifying topos).


Localic toposes correspond exactly to classifying toposes of propositional theories.

This appears in Johnstone (2002, D3.1.14, p.897f.).

Given a locale LL, the theory of completely prime filters L\mathbb{P}_L has a 0-ary relation symbol F xF_x for each xLx\in L, thought to express the proposition that xx is contained in the filter FF, and the following sequents:

  • F 1\top\vdash F_1 ,

  • F xF yF xyF_x\wedge F_y\vdash F_{x\wedge y} for all pairs x,yLx,y\in L,

  • F ( iIy i) iIF y iF_{\big (\bigvee_{i\in I} y_i\big )}\vdash \bigvee_{i\in I} F_{y_i} .

In SetSet models of L\mathbb{P}_L correspond precisely to completely prime filters i.e. the multiplicatively closed subsets of LL containing 11 that are inaccessible by infinite joins ((y i)F(\bigvee y_i)\in F implies y iFy_i\in F for some ii). Note in particular, that the properness 0F0\notin F of a completely prime filter FF is implicit in the third axiom schema with I=I=\emptyset.

The relation between LL and L\mathbb{P}_L is that Sh(L)Set[ L]Sh(L)\simeq Set[\mathbb{P}_L].

Conversely, given a propositional theory \mathbb{P}, the Lindenbaum-Tarski algebra of classes of provably equivalent formulas over \mathbb{P} together with the entailment order yields a locale L L_{\mathbb{P}} such that Sh(L )Sh(L_\mathbb{P}) classifies \mathbb{P}.

The initial and terminal toposes as classifying toposes

For illustration let us consider the empty theory 𝕋 1\mathbb{T}_1 over the empty signature i.e 𝕋 1\mathbb{T}_1 has no axioms. This is certainly propositional, its deductive closure consists of all tautologies using ,,,\bot,\top,\wedge,\bigvee. The Lindenbaum-Tarski algebra is simply 2{[][]}\mathbf{2}\simeq\{[\bot]\leq[\top]\} which corresponds to the frame of open sets of the one-point space whence Set[𝕋 1]=Sh(2)=SetSet[\mathbb{T}_1]=Sh(\mathbf{2})=Set. Similarly, 1\mathbb{P}_{\mathbf{1}}, the theory of completely prime filters of the one-point locale 1\mathbf{1}, is classified by Sh()Sh(\emptyset) i.e. sheaves on the empty space.

Whereas 2\mathbb{P}_{\mathbf{2}} has up to isomorphism exactly one model in every topos \mathcal{E} namely the one interpreting F 1F_1 as id 1 id_{1_\mathcal{E}} and F 0F_0 as 0 1 0_{\mathcal{E}}\hookrightarrow 1_{\mathcal{E}}, 1\mathbb{P}_{\mathbf{1}} has up to isomorphism exactly one model in up to isomorphism exactly one topos i.e. its model is the zero object of the (necessarily) degenerate topos.

Note that since SetSet is the terminal Grothendieck topos, the empty theory 𝕋 1\mathbb{T}_1 over the empty signature is Morita equivalent to any other geometric theory 𝕋\mathbb{T} over any signature whatsoever provided 𝕋\mathbb{T} has up to isomorphism exactly one model in every Grothendieck topos \mathcal{E}. E.g. a slight modification of the inconsistent theory {}\{\top\vdash\bot\} over the empty signature, namely adding a sort symbol OO and “contextualising” 𝕋 1={ x:O}\mathbb{T}_1'=\{\top\vdash_{x:O}\bot\} has models exactly the initial objects but these are unique (and every topos has one) whence Set[𝕋 1]SetSet[\mathbb{T}_1']\simeq Set.

Note also the difference in behavior between the inconsistent and the empty theory with respect to enlargening the signature: adding a sort symbol does not change the categories of models of the inconsistent theory up to isomorphism whereas 𝕋 1\mathbb{T}_1' has entirely different categories of models from the empty theory over the signature containing a sort symbol OO since the latter is the theory of objects 𝕆\mathbb{O}; but 𝕋 1\mathbb{T}_1' is a quotient of 𝕆\mathbb{O} whence we can think of 𝕋 1\mathbb{T}_1' as an axiomatisation of SetSet as subtopos of Set[𝕆]Set[\mathbb{O}] (see at level for further information on the duality between quotient theories and subtoposes of the classifying topos). To sum up “paraphrasing” Tolstoy: there is only one way to be inconsistent but an infinite number of ways of being empty!


In the context of (∞,1)-topos theory there is a notion of n-localic (∞,1)-topos.

Notice that a locale is itself a (Grothendieck) (0,1)-topos. Hence a localic topos is a 1-topos that behaves essentially like a (0,1)-topos. In the wider context this would be called a 1-localic (1,1)-topos.


  1. The ‘etendu’ in the title of Lawvere’s monograph might not be a misspelled noun, but an adjective as part of a back translation of a (hypothetical) French expression ‘ensembles étendus’. See this nForum thread for some discussion and speculation on this point.

Last revised on May 19, 2020 at 10:36:18. See the history of this page for a list of all contributions to it.