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 etendue (see 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 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.


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.


Localic toposes are discussed around proposition 1.4.5 of section C.1.4 of

  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 June 19, 2017 at 06:19:44. See the history of this page for a list of all contributions to it.