nLab universal closure operator

Contents

Contents

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(𝒞)LSh_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 LL and the corresponding closure operator j:ΩΩ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 :LSh j()\sharp : \mathcal{E} \stackrel{L}{\to} Sh_j(\mathcal{E}) \hookrightarrow \mathcal{E}, define for each object XX \in \mathcal{E} a closure operator, being a functor on the poset of subobjects of XX

c L:Sub(X)Sub(X), c_L : Sub(X) \to Sub(X) \,,

by sending any monomorphism AXA \hookrightarrow X classified by a characteristic function χ A:XΩ\chi_A : X \to \Omega to the pullback c L(A)c_L(A) in

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

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

Proposition

This is well defined. Moreover, c Lc_L commutes with pullback (change of base).

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

Definition

A family of functors Sub(X)Sub(X)Sub(X) \to Sub(X) for all objects XX 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 Lc_L, the corresponding Lawvere-Tierney operator j:ΩΩj : \Omega \to \Omega is given as the composite

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

where

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

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

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

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

Proof

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

c L(A) * X χ A Ω Ω Ω. \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

c L(A) #*=* * X χ A Ω Ω Ω. \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

X X χ A χ A Ω Ω. \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

c L(A) #*=* * X X χ A Ω Ω \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

c L(A) A #*=* * X X χ A Ω Ω \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:ΩΩj : \Omega \to \Omega is the characteristic function of the LL-closure, def. , of the universal subobject *Ω* \to \Omega, because we have a pasting diagram of pullback squares

c L(*) *=* * Ω Ω χ true Ω. \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

References

Section A4.4 of

Last revised on April 11, 2013 at 16:56:07. See the history of this page for a list of all contributions to it.