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 $\text{Choq}$ is the 2-point space $\{t, f\}$ equipped with the codiscrete (or indiscrete) topology. If $X$ is a Choquet space, then the points of $P X = \Omega^X$ are given by subspaces of $X$ (i.e. subsets of $X$ with the subspace pseudotopology, or just the subspace topology if $X$ is a topological space). If $X$ is moreover an internal poset in $\text{Choq}$, given by a subspace $X_1 \subseteq X \times X$ satisfying standard properties, then sitting inside $P X$ is the poset-hom $[X^{op}, \Omega]$ whose points are the downward-closed subspaces of $X$. For example, for the special case $X = [0, 1]$, the poset $[X^{op}, \Omega]$ is identified with $[0, 1] \times \{f \leq t\}$ considered in lexicographic order, with topology given by the order topology. For internal posets $X$, there is a Yoneda embedding $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}, \Omega] \to X$. For example, in the case $X = [0, 1]$, this sup-map amounts to the surjection $[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 $\mathbf{P}$ takes a poset $X$ to $[X^{op}, \Omega]$, and takes a poset map $f: X \to Y$ to the left adjoint $\mathbf{P}f$ of $[f^{op}, \Omega]: [Y^{op}, \Omega] \to [X^{op}, \Omega]$. Concretely, for Choquet spaces, $\mathbf{P}f$ takes a down-set $S \subseteq X$ to the down-set generated by the image subspace $f(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 $\mathbf{P}$ is the Yoneda embedding $y: X \to \mathbf{P}X$, and the multiplication is left adjoint to the unit, given by the map

So here are some facts:

• Sup-lattices are the same thing as $\mathbf{P}$-algebras. Given that we know $I = [0, 1]$ is a sup-lattice, we conclude that any $n$-fold power $D = I^n$ is also a sup-lattice.

• Sup-lattice maps = $\mathbf{P}$-algebra maps are the same thing as left adjoints between $\mathbf{P}$-algebras. Explicitly, if $f: Y \to X$ is a $\mathbf{P}$-algebra map, then its right adjoint is given by a composite

  $$X \stackrel{y_X}{\to} [X^{op}, \Omega] \stackrel{[f^{op}, \Omega]}{\to} [Y^{op}, \Omega] \stackrel{\sup_Y}{\to} Y.$$

  (To get a sense of this, check that this formula for the right adjoint works for sup-lattices in $\text{Set}$.)

• There is a dual notion of inf-lattice, and an inf-lattice is the same as an algebra of the dual monad $\mathbf{R}$ defined by $(\mathbf{P}( -^{op}))^{op}$. Sup-lattices are in fact inf-lattices (and conversely), and the functor $\textbf{Sup} \to \textbf{Inf}$ taking $X$ to $X^{op}$ is an equivalence, as is the functor $\textbf{Sup}^{op} \to \textbf{Inf}$ that takes a left adjoint $f: X \to Y$ to its right adjoint $g: Y \to X$. Dual to the previous comment, $\mathbf{R}$-algebra maps coincide with right adjoints between $\mathbf{R}$-algebras.

• If $D$ is a sup-lattice in a quasitopos $Q$ and $X$ is an object of $Q$, then the $Q$-exponential $D^X$ is a sup-lattice, with sups computed “pointwise”. The last part means that $\sup_{D^X}: \mathbf{P}(D^X) \to D^X$ is explicitly given by a composite

  $$\mathbf{P}(D^X) \stackrel{\mathbf{P}(y^X)}{\to} \mathbf{P}(\mathbf{P}D^X) \cong \mathbf{PP}(D \times X) \stackrel{\text{mult}_X}{\to} \mathbf{P}(D \times X) \cong (\mathbf{P}D)^X \stackrel{\sup_D^X}{\to} D^X$$

  (in the isomorphism $\mathbf{P}(D \times X) \cong (\mathbf{P}D)^X$, we are implicitly treating the object $X$ as a “discrete” poset, so that there is an identification $X^{op} = X$). The last map $\sup_D^X$ explains the sense in which sups in $D^X$ are computed pointwise in $D$.

• If $f: X \to Y$ is a map between $Q$-objects and $D$ is a sup-lattice, then $D^f: D^Y \to D^X$ is both a sup-lattice map, and dually an inf-lattice map. By a dual of an earlier point, being an inf-lattice map, $D^f$ is a right adjoint, whose left adjoint is denoted $\text{Lan}_f$.

We haven’t yet checked that