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 (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, , 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.
Let be a reflective subcategory of a topos .
Here we discuss explicit translations between the structure given by the reflector and the corresponding closure operator (the Lawvere-Tierney operator) in a way that makes the relation to modal type theory and monads (in computer science) most manifest.
Given a reflector , define for each object a closure operator, being a functor on the poset of subobjects of
by sending any monomorphism classified by a characteristic function to the pullback in
where is the adjunction unit.
This is well defined. Moreover, commutes with pullback (change of base).
This appears as (Johnstone, lemma A4.3.2).
A family of functors for all objects that commutes with change of base is called a universal closure operation.
Given a left exact reflector as above with induced closure operation , the corresponding Lawvere-Tierney operator is given as the composite
where
is the adjunction unit;
is the characteristic function of the result of applying to the universal subobject
(which is again a monomorphism since preserves pullbacks).
For any subobject with characteristic function , we need to show that we have a pullback diagram
The pullback along the rightmost morphism is by definition
Moreover, by the naturality of the adjunction unit we have a commuting diagram
Using this in the remaining bottom morphism of our would-be pullback square we find that equivalently
needs to be a pullback diagram. Since preserves pullbacks we have that also the middle square in
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.
Equivalently, by the pasting law, we have that is the characteristic function of the -closure, def. , of the universal subobject , because we have a pasting diagram of pullback squares
In this form the statement appears in the proof of (Johnstone, Theorem A4.3.9).
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 sharp modality.
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.