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.
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.
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/blend of ‘poset’ and ‘site’.)
The definition of coverage may be simplified a little in this case.
Let be a poset (or proset). A coverage on is a binary relation between and its power set that satisfies these conditions:
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.)
Let be a poset (or proset) with all bounded binary meets. A cartesian coverage on is a binary relation between and its power set that satisfies these conditions:
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.
One often looks at sheaves on sites. On posites, one can either look at sheaves or at ideals.
Given a posite , an ideal on (also called a -sheaf; compare -sheaf) is a subset of satisfying these conditions:
In other words, it is a sheaf valued in truth values (rather than in sets as is the default).
A subset that satisfies condition (1) alone states that is a lower subset (a (0,1)-presheaf).
The ideals on a posite form a frame (or ) under inclusion, which may alternately be interpreted as a locale.
Every element of may be interpreted as an ideal on ; given two elements of , belongs to the ideal represented by if and only if ; that is, represents its down set.
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:
The topos of sheaves on any posite 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 , 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
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.
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 .)
Let be a topological space, and let be a topological base of . Then is a semilattice under intersection; we make into a posite by defining
The frame generated by this posite is naturally isomorphic to the frame of opens of . If is a sober space, then this frame, interpreted as a locale, may be identified with .
The locale of real numbers is generated from the locally cartesian poset , where is the usual poset of rational numbers, equipped with the cartesian coverage given by
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.
The classifying topos of any propositional geometric theory is localic, and can be presented as sheaves on a posite of propositions.
We call a frame (or locale) accessible if it is isomorphic to for some small posite . (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 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:
Last revised on May 5, 2021 at 04:48:17. See the history of this page for a list of all contributions to it.