nLab universal closure operator

Idea

If one considers a hyperdoctrine of subobject lattices, hence a collection of them parameterized over a category of contexts and equipped with pullback/substitution/context extension, then a universal closure operator or modality is a closure operator acting on each of the slices and being compatible with the pullback operation. A hyperdoctrine equipped with such an operator is sometimes called a modal hyperdoctrine.

If there is moreover a subobject classifier $\Omega$ (hence if that hyperdoctrine is the collection of slice categories of a topos) then a universal closure operator is represented by a single monad/comonad on that subobject classifier, $\Diamond \colon \Omega \to \Omega$, see the discussion below.

Instead of subobjects one may consider more generally closures acting on the full slice categories. This promotes the corresponding modal logic to modal type theory. Unlike in the posetal case, such a monad will not automatically be idempotent, but often one requires this explicitly.

Definition

For reflective subcategories

Let $Sh_j(\mathcal{C}) \stackrel{\overset{L}{\leftarrow}}{\hookrightarrow} \mathcal{E}$ be a reflective subcategory of a topos $\mathcal{E}$.

Here we discuss explicit translations between the structure given by the reflector $L$ and the corresponding closure operator $j \colon \Omega \to \Omega$ (the Lawvere-Tierney operator) in a way that makes the relation to modal type theory and monads (in computer science) most manifest.

Definition

Given a reflector $\sharp : \mathcal{E} \stackrel{L}{\to} Sh_j(\mathcal{E}) \hookrightarrow \mathcal{E}$, define for each object $X \in \mathcal{E}$ a closure operator, being a functor on the poset of subobjects of $X$

$$c_L : Sub(X) \to Sub(X) \,,$$

by sending any monomorphism $A \hookrightarrow X$ classified by a characteristic function $\chi_A : X \to \Omega$ to the pullback $c_L(A)$ in

$$\array{ c_L(A) &\to& \sharp A \\ \downarrow && \downarrow \\ X &\to& \sharp X } \,,$$

where $X \to \sharp X$ is the adjunction unit.

Proposition

This is well defined. Moreover, $c_L$ commutes with pullback (change of base).

This appears as (Johnstone, lemma A4.3.2).

Definition

A family of functors $Sub(X) \to Sub(X)$ for all objects $X$ that commutes with change of base is called a universal closure operation.

Proposition

Given a left exact reflector $\sharp$ as above with induced closure operation $c_L$, the corresponding Lawvere-Tierney operator $j : \Omega \to \Omega$ is given as the composite

$$j : \Omega \to \sharp \Omega \stackrel{\chi_{\sharp true}}{\to} \Omega \,,$$

where

• $\Omega \to \sharp \Omega$ is the adjunction unit;

• $\chi_{\sharp true} : \sharp \Omega \to \Omega$ is the characteristic function of the result of applying $\sharp$ to the universal subobject

  $$(* \stackrel{\sharp true}{\hookrightarrow} \sharp \Omega) := \sharp (* \stackrel{true}{\hookrightarrow} \Omega)$$

  (which is again a monomorphism since $\sharp$ preserves pullbacks).

Proof

For $A \hookrightarrow X$ any subobject with characteristic function $\chi_A : X \to \Omega$, we need to show that we have a pullback diagram

$$\array{ c_L(A) &\to& &\to& &\to& * \\ \downarrow && && && \downarrow \\ X &\stackrel{\chi_A}{\to}& \Omega &\stackrel{}{\to}& \sharp \Omega &\stackrel{}{\to}& \Omega } \,.$$

The pullback along the rightmost morphism is by definition $# * \to \sharp \Omega$

$$\array{ c_L(A) &\to& &\to& # * = * &\to& * \\ \downarrow && && \downarrow && \downarrow \\ X &\stackrel{\chi_A}{\to}& \Omega &\stackrel{}{\to}& \sharp \Omega &\stackrel{}{\to}& \Omega } \,.$$

Moreover, by the naturality of the adjunction unit we have a commuting diagram

$$\array{ X &\to& \sharp X \\ {}^{\mathllap{\chi_A}}\downarrow && \downarrow^{\mathrlap{\sharp \chi_A}} \\ \Omega &\to& \sharp \Omega } \,.$$

Using this in the remaining bottom morphism of our would-be pullback square we find that equivalently

$$\array{ c_L(A) &\to& &\to& # * = * &\to& * \\ \downarrow && && \downarrow && \downarrow \\ X &\stackrel{}{\to}& \sharp X &\stackrel{\sharp \chi_A}{\to}& \sharp \Omega &\stackrel{}{\to}& \Omega }$$

needs to be a pullback diagram. Since $\sharp$ preserves pullbacks we have that also the middle square in

$$\array{ c_L(A) &\to& \sharp A &\to& # * = * &\to& * \\ \downarrow && \downarrow && \downarrow && \downarrow \\ X &\stackrel{}{\to}& \sharp X &\stackrel{\sharp \chi_A}{\to}& \sharp \Omega &\stackrel{}{\to}& \Omega }$$

is a pullback. But then also the left square is a pullback, by def. . This finally means, by the pasting law, that also the total rectangle is a pullback.

Remark

Equivalently, by the pasting law, we have that $j : \Omega \to \Omega$ is the characteristic function of the $L$-closure, def. , of the universal subobject $* \to \Omega$, because we have a pasting diagram of pullback squares

$$\array{ c_L(*) &\to& \sharp * = * &\to & * \\ \downarrow && \downarrow && \downarrow \\ \Omega &\to& \sharp \Omega &\stackrel{\chi_{\sharp true}}{\to} & \Omega } \,.$$

In this form the statement appears in the proof of (Johnstone, Theorem A4.3.9).

Examples

• In a topos a universal closure operator as above is also called a Lawvere-Tierney topology.

• For a local topos there are the closure operators flat modality $\dashv$ sharp modality.

Related concepts

• modal type theory

References

Section A4.4 of

• Peter Johnstone, Sketches of an Elephant