Topos Theory

topos theory



Internal Logic

Topos morphisms

Extra stuff, structure, properties

Cohomology and homotopy

In higher category theory




The notion of posite (or (0,1)(0,1)-site , less properly 00-site ) is a decategorification of the notion of site (which may also be called a 11-site or (1,1)(1,1)-site). For categorifications thereof, see (∞,1)-site and 2-site.

Just as a site is a category with a coverage, whose (set-valued) sheaves form a Grothendieck topos, so a posite is a poset with a coverage, whose (0,1)(0,1)-sheaves (truth value-valued sheaves) form a locale. On the other hand, we can also consider a posite as a site in its own right, in which case the 11-sheaves on it form a localic topos.

As locale theory serves as an approach to topology in which locales take the role traditionally held by topological spaces, so posites take the role traditionally held by topological bases.

A formal topology may be generated by a posite equipped with a positivity predicate.


Definition (posite)

A posite is a site whose underlying category is thin.

In other words, a posite is a poset (or more generally a preordered set) equipped with a Grothendieck topology or a coverage. (The name is a portmanteau/pun on ‘poset’ and ‘site’.)

The definition of coverage may be simplified a little in this case.

Definition (coverage on a poset)

Let SS be a poset (or proset). A coverage on SS is a binary relation \lhd between SS and its power set that satisfies these conditions:

  • If uVu \lhd V and vVv \in V, then vuv \leq u;
  • If uVu \lhd V and uuu' \leq u, then uVu' \lhd V' for some VV' such that, for every vVv' \in V', there is a vVv \in V such that vvv' \leq v.

Then a posite is precisely a poset (or proset) equipped with a coverage.

If SS is a meet-semilattice, then there is another alternative defintion. (Actually, it is not necessary that the poset SS have all finitary meets but only bounded? ones. That is, if v,wuv, w \leq u for some fixed uu, then vwv \wedge w must exist, but not otherwise. Such a poset SS is a semilattice if and only if it has a top element. Compare the notion of locally cartesian category.)

Definition (cartesian coverage on a locally cartesian posite)

Let SS be a poset (or proset) with all bounded binary meets. A cartesian coverage on SS is a binary relation \lhd between SS and its power set that satisfies these conditions:

  • If uVu \lhd V and vVv \in V, then vuv \leq u;
  • If uVu \lhd V and uuu' \leq u, then u{vuvV}u' \lhd \{ v \wedge u' \;|\; v \in V \}.

Then a locally cartesian posite is such a poset (or proset) equipped with such a coverage.

It is a theorem that every posite whose underlying poset has all bounded binary meets is equivalent (in the sense that there is an isomorphism of sites as defined below) to a locally cartesian posite.

In any case, given an element uu of SS and a subset VV of SS, if

uV, u \lhd V ,

then we say that VV is a basic cover of uu.

Definition (morphism of posites)

Given two posites SS and TT, a morphism of posites from SS to TT is a function f:STf\colon S \to T such that:

  • If uvu \leq v in SS, then f(u)f(v)f(u) \leq f(v) in TT;
  • Given any uu in TT, for some vv in SS, we have uf(v)u \leq f(v);
  • If wf(u),f(v)w \leq f(u), f(v) in TT, then for some xu,vx \leq u, v in SS, we have wf(x)w \leq f(x); and
  • If uVu \lhd V, then f(u){f(v)vV}f(u) \lhd \{ f(v) \;|\; v \in V \}.

Clauses (1–3) simply state that ff is a flat functor; when SS and TT are semilattices, we can replace this with the requirement that ff preserves meets (including the top element). Clause (4) requires ff to respect covers.

Ideals and sheaves

One often looks at sheaves on sites. On posites, one can either look at sheaves or at ideals.

Definition (ideal)

Given a posite SS, an ideal on SS (also called a (0,1)(0,1)-sheaf; compare (,1)(\infty,1)-sheaf) is a subset II of SS satisfying these conditions:

  1. If uvu \leq v and vIv \in I, then uIu \in I; and
  2. If uVu \lhd V and VIV \subseteq I, then uIu \in I.

In other words, it is a sheaf valued in truth values (rather than in sets as is the default).

A subset II that satisfies condition (1) alone states that II is a lower subset (a (0,1)(0,1)-presheaf).

The ideals on a posite form a frame Id(S)Id(S) (or Sh 0,1(S)Sh_{0,1}(S)) under inclusion, which may alternately be interpreted as a locale.

Every element of SS may be interpreted as an ideal on SS; given two elements u,vu,v of SS, uu belongs to the ideal represented by vv if and only if uvu \leq v; that is, vv represents its down set.

The frame of ideals is given by a universal property. If LL is a frame, we make LL into a posite using its canonical coverage (see the examples below). Then the operation from elements of SS to ideals on SS is a morphism of posites; furthermore, given any morphism of posites from SS to a frame LL (with its canonical coverage), there exists a unique frame homomorphism from Id(S)Id(S) to LL that makes the obvious triangle commute.

If instead we treat a posite as a special kind of site and look at its 11-sheaves, we have this result:


The topos of sheaves on any posite PP is a localic topos.


This is obvious if we use the definition of “localic topos” which says that it is generated by subterminal objects, since the (sheafifications of) representable functors always generate a topos of sheaves, and for a posite these are subterminal.

The relevant locale is precisely the locale of ideals.


Given a posite SS, we may think of the elements of SS as basic opens of a space which is generated from SS using its coverage, to produce a locale. Thus a posite is precisely a base for a locale. See the example coming from a topological space below to see how this can work precisely for a topological locale.

A coverage can be seen as a sequent calculus; the interpretation of

uV u \lhd V

in topology is analogous to the interpretation of

pQ p \lhd Q

in logic. Note that we have a single proposition on the left but a set of propositions (interpreted disjunctively) on the right, the reverse of an intuitionistic sequent.


Using ideals

Any poset (or proset) SS has a canonical coverage, in which

  • uVu \lhd V if and only if, for any uuu' \leq u, uu' is a join of some VV' such that, for every vVv' \in V', there is a vVv \in V such that vvv' \leq v.

If SS is a frame, then we can simplify this condition:

  • uVu \lhd V if and only if uu is a join of VV;

and then the canonical coverage is cartesian. In this case, Id(S)Id(S) is naturally isomorphic to SS itself. (Analogously, if EE is a Grothendieck topos with its canonical coverage, then Sh(E)Sh(E), the topos of sheaves on EE, is naturally equivalent to EE.)

Let XX be a topological space, and let SS be a topological base of XX. Then SS is a semilattice under intersection; we make SS into a posite by defining

  • uVu \lhd V if and only if uu is the union of VV in XX (which is not necessarily the same as a join in SS).

The frame generated by this posite is naturally isomorphic to the frame of opens of XX. If XX is a sober space, then this frame, interpreted as a locale, may be identified with XX.

The locale of real numbers is generated from the locally cartesian poset S op×S \coloneqq \mathbb{Q}^op \times \mathbb{Q}, where \mathbb{Q} is the usual poset of rational numbers, equipped with the cartesian coverage given by

  • (x,y)(x,y) \lhd \empty whenever xyx \geq y;
  • (w,z){(w,x),(y,z)}(w,z) \lhd \{(w,x),(y,z)\} whenever wy<xzw \leq y \lt x \leq z; and
  • (w,z){(x,y)w<x<y<z}(w,z) \lhd \{ (x,y) \;|\; w \lt x \lt y \lt z \}.

Often you will see ±\pm\infty added to \mathbb{Q} in a description of this locale, which adds a top element to SS and so makes it into a semilattice, but that makes no difference to the generated locale in this case.

Using sheaves

The double negation topology used in the sheaf-theoretic approach to forcing is a posite. More generally, Classical set-theoretic forcing is done exclusively on posites. One “reason” for this (in the sense of a reason why set-theorists have not been forced to look beyond such models) is explained in the paper by Freyd below.

The semilattice of commutative subalgebras of a C *C^*-algebra AA is a posite (with trivial topology) internal to whose sheaf topos we have a constructive Gelfand duality theorem for AA, even if AA was externally non-commutative.

The classifying topos of any propositional geometric theory is localic, and can be presented as sheaves on a posite of propositions.

Use in predicative mathematics

We call a frame (or locale) LL accessible if it is isomorphic to Id(S)Id(S) for some small posite SS. (Compare the concept of accessible category, in the case of a cocomplete pretopos.)

In classical mathematics, an accessible frame must be small, but this fails in predicative mathematics. (Conversely, any small frame is trivially accessible; take SS to be LL with its canonical coverage.) Since many predicativists have philosophical objections to working with large objects at all, they may prefer to work with small posites directly. Whatever the philosophy, we may use small posites in place of accessible locales, or at any rate use this to prove that the category of the latter is essentially moderate.

Formal topology is a programme for topology which is based on using small posites. However, formal topologists also require a positivity predicate on their posites; the intended interpretation is that uu is positive iff its corresponding open subspace is inhabited. This seems to be needed for a good theory of compact spaces (and related notions) in a predicative constructive framework.


  • Most of this article is based on Stone Spaces, but with a different presentation.

On forcing, see:

  • Peter Freyd, All topoi are localic or why permutation models prevail, Journal of Pure and Applied Algebra 46 (1987) pp 49–58.

Revised on January 12, 2011 22:33:21 by Toby Bartels (