Todd Trimble
sup-lattices in quasitoposes

Draft; it’s a fragment cut-and-paste of something I had begun writing up at MO.

First I should tell you what an internal sup-lattice is in a quasitopos; there is more than one possible notion, but the one that I think is appropriate is parallel to a standard notion in topos theory. In a quasitopos there is a regular subobject classifier Ω\Omega, which for Choq\text{Choq} is the 2-point space {t,f}\{t, f\} equipped with the codiscrete (or indiscrete) topology. If XX is a Choquet space, then the points of PX=Ω XP X = \Omega^X are given by subspaces of XX (i.e. subsets of XX with the subspace pseudotopology, or just the subspace topology if XX is a topological space). If XX is moreover an internal poset in Choq\text{Choq}, given by a subspace X 1X×XX_1 \subseteq X \times X satisfying standard properties, then sitting inside PXP X is the poset-hom [X op,Ω][X^{op}, \Omega] whose points are the downward-closed subspaces of XX. For example, for the special case X=[0,1]X = [0, 1], the poset [X op,Ω][X^{op}, \Omega] is identified with [0,1]×{ft}[0, 1] \times \{f \leq t\} considered in lexicographic order, with topology given by the order topology. For internal posets XX, there is a Yoneda embedding y:X[X op,Ω]y: X \to [X^{op}, \Omega] (as a function it takes a point to the down-set it generates). By a sup-lattice, I mean a poset whose Yoneda embedding has an (internal) left-adjoint sup:[X op,Ω]X\sup: [X^{op}, \Omega] \to X. For example, in the case X=[0,1]X = [0, 1], this sup-map amounts to the surjection [0,1]×{ft}[0,1][0, 1] \times \{f \leq t\} \to [0, 1], and you can check very easily that this is indeed a left adjoint (this is all very concrete; really you just check it at the underlying set level).

Now there are a whole bunch of facts about sup-lattices which I will claim without giving complete proofs (but all of which are standard in topos theory; for quasitoposes I unfortunately don’t have a reference). The big one is that sup-lattices are the algebras of a KZ or lax idempotent monad on the category of posets. The underlying functor P\mathbf{P} takes a poset XX to [X op,Ω][X^{op}, \Omega], and takes a poset map f:XYf: X \to Y to the left adjoint Pf\mathbf{P}f of [f op,Ω]:[Y op,Ω][X op,Ω][f^{op}, \Omega]: [Y^{op}, \Omega] \to [X^{op}, \Omega]. Concretely, for Choquet spaces, Pf\mathbf{P}f takes a down-set SXS \subseteq X to the down-set generated by the image subspace f(S)Yf(S) \subseteq Y, and you can check just at the underlying set level that we get an adjunction this way. The unit for the monad P\mathbf{P} is the Yoneda embedding y:XPXy: X \to \mathbf{P}X, and the multiplication is left adjoint to the unit, given by the map

[y op,Ω]:[(PX) op,Ω][X op,Ω].[y^{op}, \Omega]: [(\mathbf{P}X)^{op}, \Omega] \to [X^{op}, \Omega].

So here are some facts:

We haven’t yet checked that

Created on April 18, 2017 at 18:25:35 by Todd Trimble