In intrinsic terms, a topos is localic if it is generated under colimits by the subobjects of its terminal object .
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 (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 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 as exhibiting E as a “localic S-topos”.
Moreover, just as localic topoi can be identified with locales, for any base topos the 2-category of localic -topoi is equivalent to the 2-category Loc of internal locales in .
Here is the 2-category whose
objects are localic toposes over ;
morphisms are geometric morphisms, i.e. adjunctions in which the left adjoint preserves finite limits, considered as pointing in the direction of their right adjoint; and
2-morphisms are mate-pairs of natural transformations.
Then the 2-category is equivalent to the 2-category of locales (see C1.4.5 in the Elephant).
The 2-category is actually a (1,2)-category; its 2-morphism are the pointwise ordering of frame homomorphisms. Thus this equivalence implies that 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 of all toposes is not locally essentially small.) Assuming sufficient separation axioms, the hom-posets of , and hence , become discrete.
Obviously, every Grothendieck topos that is a category of sheaves on (the category of open subsets of) a topological space is localic.
Every sheaf topos over a posite is localic. (See there for details.)
Many familiar toposes , even when they are not localic, can be covered by a localic slice (“covered” means the unique map is an epi). For example, if is a group, then is not itself localic, but it has a localic slice 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 , there exists an open surjection where 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 .
Then, using methods of descent theory, Joyal and Tierney deduce that every Grothendieck topos is equivalent to the category of continuous discrete representations of a localic groupoid . (Their result is relativized so as to hold internally over any Grothendieck topos 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 is equivalent to the category of continuous discrete representations of the fundamental pro-group , where denotes the separable closure of . It was a watershed event for the penetration of localic methods in topos theory.
Recall that a geometric theory 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, 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 , the theory of completely prime filters has a 0-ary relation symbol for each , thought to express the proposition that is contained in the filter , and the following sequents:
,
for all pairs ,
.
In models of correspond precisely to completely prime filters i.e. the multiplicatively closed subsets of containing that are inaccessible by infinite joins ( implies for some ). Note in particular, that the properness of a completely prime filter is implicit in the third axiom schema with .
The relation between and is that .
Conversely, given a propositional theory , the Lindenbaum-Tarski algebra of classes of provably equivalent formulas over together with the entailment order yields a locale such that classifies .
For illustration let us consider the empty theory over the empty signature i.e has no axioms. This is certainly propositional, its deductive closure consists of all tautologies using . The Lindenbaum-Tarski algebra is simply which corresponds to the frame of open sets of the one-point space whence . Similarly, , the theory of completely prime filters of the one-point locale , is classified by i.e. sheaves on the empty space.
Whereas has up to isomorphism exactly one model in every topos namely the one interpreting as and as , 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 is the terminal Grothendieck topos, the empty theory over the empty signature is Morita equivalent to any other geometric theory over any signature whatsoever provided has up to isomorphism exactly one model in every Grothendieck topos . E.g. a slight modification of the inconsistent theory over the empty signature, namely adding a sort symbol and “contextualising” has models exactly the initial objects but these are unique (and every topos has one) whence .
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 has entirely different categories of models from the empty theory over the signature containing a sort symbol since the latter is the theory of objects ; but is a quotient of whence we can think of as an axiomatisation of as subtopos of (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.
Saunders Mac Lane, Ieke Moerdijk, Sheaves in Geometry and Logic , Springer Heidelberg 1994. (chapter IX, p.472ff)
Peter Johnstone, Sketches of an Elephant 2 vols. , Oxford UP 2002. (In general around C.1.4.5 p.515f, cp filters at D1.1.7 p.816f, as classifying topos B4.2.12. p.431f, D1.1.14 p.897f.)
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.