The notion of posite (or -site, less properly -site) is a decategorification of the notion of site (which may also be called an -site or -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 -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 -sheaves on it form a localic topos.
The definition of coverage may be simplified a little in this case.
Then a posite is precisely a poset (or proset) equipped with a coverage.
If is a meet-semilattice, then there is another alternative defintion. (Actually, it is not necessary that the poset have all finitary meets but only bounded? ones. That is, if for some fixed , then must exist, but not otherwise. Such a poset is a semilattice if and only if it has a top element. Compare the notion of locally cartesian category.)
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 of and a subset of , if
then we say that is a basic cover of .
Given two posites and , a morphism of posites from to is a function such that:
Clauses (1–3) simply state that is a flat functor; when and are semilattices, we can replace this with the requirement that preserves meets (including the top element). Clause (4) requires to respect covers.
The frame of ideals is given by a universal property. If is a frame, we make into a posite using its canonical coverage (see the examples below). Then the operation from elements of to ideals on is a morphism of posites; furthermore, given any morphism of posites from to a frame (with its canonical coverage), there exists a unique frame homomorphism from to that makes the obvious triangle commute.
If instead we treat a posite as a special kind of site and look at its -sheaves, we have this result:
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 , we may think of the elements of as basic opens of a space which is generated from 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
in topology is analogous to the interpretation of
Any poset (or proset) has a canonical coverage, in which
If is a frame, then we can simplify this condition:
and then the canonical coverage is cartesian. In this case, is naturally isomorphic to itself. (Analogously, if is a Grothendieck topos with its canonical coverage, then , the topos of sheaves on , is naturally equivalent to .)
Often you will see added to in a description of this locale, which adds a top element to and so makes it into a semilattice, but that makes no difference to the generated locale in this case.
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 -algebra is a posite (with trivial topology) internal to whose sheaf topos we have a constructive Gelfand duality theorem for , even if was externally non-commutative.
In classical mathematics, an accessible frame must be small, but this fails in predicative mathematics. (Conversely, any small frame is trivially accessible; take to be 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 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.
On forcing, see: