Todd Trimble
Three topos theorems in one

I want to discuss a neat theorem (theorem 2 below) which manages to roll several fundamental theorems of topos theory into one.

I’ve known this theorem for some time now (about twelve years), but for a long time it struck me as just a kind of curiosity – I didn’t know any exciting new applications, and I didn’t even know what I should name the new concept that the theorem depends on. But, after thinking about some recent discussion on the blog on modal logic, it occurred to me there might be some justification for christening this new concept “modal operator”.

Just giving the baby a jazzy new name (even if it doesn’t really suit her in the end) somehow rekindled the motivation to want to show her to people: write down the proofs, see if I could make it grow, and so on. And in the process, I found a way to construct modal operators that for some reason hadn’t occurred to me before (theorem 3). If anyone knows about this concept from somewhere else, I’d really like to know about it!

Although this article is more or less self-contained, it’s really addressed to those who know some topos theory at an introductory level, say through the first five chapters of the book by Mac Lane and Moerdijk. I’ve included a little appendix on a way to think about sheafification, which I’m sure is known to experts but which I’ve never seen written down.

Three theorems

There are three basic theorems for building new toposes from old ones:

If the slice theorem is the one which passes to toposes of presheaves on internal discrete categories, then the lex comonad theorem is the one which, among other things, extends that further to toposes of presheaves on general internal categories.

This is the theorem which takes us from presheaves to sheaves. Here the monad J is the composite of taking the associated sheaf functor (which is left exact) followed by the forgetful functor from sheaves to presheaves; the J-algebras are the sheaves. The monad J is idempotent because the associated sheaf of a sheaf X is canonically isomorphic to X (alternatively, because the embedding of sheaves in presheaves is full and faithful). In fact, every such lex idempotent monad on a topos E arises in this way, by sheafifying with respect to a Lawvere-Tierney topology in E.

Thus the three theorems taken together effect the passage from a base category Set as a topos, to Grothendieck toposes. We will show how to effect this passage in just one step, instead of three separate ones. In fact, we will see that all three theorems can be combined into one master theorem (theorem 2 below).

Two theorems in one

The first reduction combines the slice theorem and the lex comonad theorem into one. The idea is rather simple. Indeed, notice that the slice E/X is the category of coalgebras for the comonad ×X:EE, where the comonad structure comes from the unique comonoid structure which exists on any object X:

δ:XX×Xε:X1\delta: X \to X \times X \qquad \varepsilon: X \to 1

The comonad ×X isn’t left exact (it doesn’t preserve the terminal object), but it does preserve pullbacks.

Thus, we will reproduce the following theorem. It has long been known as folklore to experts, and appears in Johnstone’s Sketches of an Elephant, section A, Remark 4.2.3.

Theorem 1: If G:EE is a pullback-preserving comonad acting on a topos E, then the category of coalgebras E G is also a topos.

Proof: It suffices to produce finite limits and power objects in E G. Pullbacks in E G are created by the forgetful functor E GE because G preserves pullbacks, and G1 is terminal in E G if 1 is terminal in E, since the right adjoint G:EE G preserves limits. So E G is finitely complete.

Since G:EE preserves pullbacks, it also preserves monos. In particular, if YY×PY denotes the elementhood relation between Y and its power object PY in E, we have a chain of monos

(1)G( Y)G(Y×PY)GY× G1GPYGY×GPYG(\in_Y) \hookrightarrow G(Y \times P Y) \cong G Y \times_{G 1} G P Y \hookrightarrow G Y \times G P Y

where the middle two objects are pullbacks of the diagram

GY G! GPY G! G1\array{ & & G Y \\ & & \downarrow G ! \\ G P Y & \stackrel{G !}{\to} & G 1 }

in E. The composite of the monos in (1) names a subobject of GY×GPY, which is classified by a map

ϕ:GPYPGY\phi: G P Y \to P G Y

in E.

Let δ:GGG denote the comultiplication and ε:G1 E the counit of G, and suppose Y carries a G-coalgebra η:YGY. Define the object P GY in E G to be the equalizer in E G of the following pair of coalgebra maps from the cofree coalgebra GPY to itself:

(2)GPY id GPY δPY GPη GGPY Gϕ GPGY\array{ G P Y & \stackrel{id}{\to} & G P Y \\ \delta P Y \downarrow & & \uparrow G P\eta \\ G G P Y & \stackrel{G\phi}{\to} & G P G Y }

where P is the contravariant power object functor (whence the direction Pη:PGYPY). We will show that P GY is the power object of Y in E G.

So, let (X,θ:XGX) be a coalgebra. We must show that coalgebra maps f:XP GY correspond precisely to subcoalgebras of the product X×Y in E G (whose underlying object in E is the pullback X× G1Y). The remainder of the proof will be proven with the help of three lemmas.

Lemma 0: If (S,γ:SGS) is a G-coalgebra, then the coassociativity square

S γ GS γ Gγ GS δS GGS\array{ S & \stackrel{\gamma}{\to} & G S \\ \gamma \downarrow & & \downarrow G\gamma \\ G S & \stackrel{\delta S}{\to} & G G S }

is a pullback. In any pullback, if the two pullback projections coincide (as here, where they are both γ), then the pullback projection is monic.

Proof: In any commutative square

X f GS g Gγ GS δS GGS\array{ X & \stackrel{f}{\to} & G S \\ g \downarrow & & \downarrow G\gamma \\ GS & \stackrel{\delta S}{\to} & G G S }

the arrows f, g coincide because Gγ and δS have a common left inverse GεS:GGSGS. Therefore the pullback of the arrows Gγ, δS is the same as their equalizer, which is γ:SGS. For the second sentence, the condition that the two pullback projections coincide is equivalent to the condition that the projection is the equalizer, and equalizers are monic.

Lemma 1: Suppose G:EE is a comonad which preserves pullbacks, and let (S,γ:SGS) be a G-coalgebra. Then a pair (k:RS,β:RGR) defines a subcoalgebra of S precisely when k is monic and the compatibility square

(3)R β GR k Gk S γ GS\array{ R & \stackrel{\beta}{\to} & G R \\ k \downarrow & & \downarrow G k \\ S & \stackrel{\gamma}{\to} & G S }

commutes.

Proof: First, Gk is monic assuming k is monic, since G preserves pullbacks. Therefore β is uniquely determined. We must show that β:RGR satisfies the axioms for a coalgebra structure, i.e., that

(4)Gββ=δRβεRβ=1 R.G\beta \circ \beta = \delta R \circ \beta \qquad \varepsilon R \circ \beta = 1_R.

Since k is monic, the second equation follows from the equation

kεRβ=kk \circ \varepsilon R \circ \beta = k

but this equation holds since

kεRβ=εSGkβ=εSγk=1 Skk \circ \varepsilon R \circ \beta = \varepsilon S \circ G k \circ \beta = \varepsilon S \circ \gamma \circ k = 1_S \circ k

using in turn naturality of ε, the square (3), and the fact that S is a coalgebra.

Again, G preserves pullbacks, so GGk is monic assuming k is. So the first equation of (4) follows from

GGkGββ=GGkδRβG G k \circ G\beta \circ \beta = G G k \circ \delta R \circ \beta

and this last equation is left to the reader; it follows from naturality of δ, the square (3), and the fact that S is a coalgebra.

Lemma 2: In the notation of lemma 1, if k:RS is a monic coalgebra map, then the square

(5)R β GR k Gk S γ GS\array{ R & \stackrel{\beta}{\to} & G R \\ k \downarrow & & \downarrow G k \\ S & \stackrel{\gamma}{\to} & G S }

is a pullback.

Proof: Suppose we have a commutative square

(6)X f GR g Gk S γ GS\array{ X & \stackrel{f}{\to} & G R \\ g \downarrow & & \downarrow G k \\ S & \stackrel{\gamma}{\to} & G S }

First, we prove that f equalizes the pair δR,Gβ:GRGGR. We have a series of equations

GGkGβf=GγGkf=Gγγg=δSγg=δSGkf=GGkδRfG G k \circ G\beta \circ f = G\gamma \circ G k \circ f = G\gamma \circ \gamma \circ g = \delta S \circ \gamma \circ g = \delta S \circ G k \circ f = G G k \circ \delta R \circ f

using, in turn, (5) (and functoriality of G), (6), the coassociativity on the coalgebra S, (6) again, and naturality of δ. Comparing the first and last terms of this series, and using the fact that GGk is monic (because k is monic and G preserves pullbacks), we obtain δRf=Gβf.

Thus f factors through the equalizer β:RGR of δR,Gβ:GRGGR. Write f=βp. We then have

γkp=(5)Gkβp=Gkf=(6)γg\gamma \circ k \circ p \stackrel{(5)}{=} G k \circ \beta \circ p = G k \circ f \stackrel{(6)}{=} \gamma \circ g

and since γ is monic (cf. lemma 0), we infer that kp=g. Moreover, this p is unique since k is monic. Thus, we have shown that any square (6) factors uniquely, via the map p:XR, through the square (5); this completes the proof.

Now we return to the proof of Theorem 1; it remains to show that the equalizer j:P G(Y)GPY of the pair of maps in (2) is the power object of the coalgebra (Y,η:YGY). Let (X,θ:XGX) be a coalgebra, and f:XP G(Y) a coalgebra map. Then g=jf:XGPY equalizes the maps in (2). Moreover, since GPY is cofree, we have that to each G-coalgebra map g:XGPY, there exists a unique h:XPY in the topos E such that

g=(XθGXGhGPY)g = (X \stackrel{\theta}{\to} G X \stackrel{G h}{\to} G P Y)

Thus g:XGPY in E G or h:XPY in E corresponds to a subobject i:RX×Y in E. We need to check that the condition that g equalizes the pair of maps in (2) corresponds precisely to the condition that R is a subcoalgebra of X× G1Y (the product of X and Y in E G). Or, taking into account lemmas 0, 1, 2: precisely to the condition that there is a pullback diagram of the form

(7)R β GR k Gk X× G1Y γ G(X× G1Y)\array{ R & \stackrel{\beta}{\to} & G R \\ k \downarrow & & \downarrow G k \\ X \times_{G 1} Y & \stackrel{\gamma}{\to} & G(X \times_{G 1} Y) }

where γ is the coalgebra structure on X× G1Y, and k is monic.

Proof: That g:XGPY equalizes the pair of maps in (2) translates to a condition on h:XPY, that the following diagram commutes:

X h PY θ g Pη GX Gh GPY ϕ PGY\array{ & & X & \stackrel{h}{\to} & P Y \\ & \theta \swarrow & \downarrow g & & \uparrow P\eta \\ G X & \stackrel{G h}{\to} & G P Y & \stackrel{\phi}{\to} & P G Y }

Or, that the subobject i:RY×X equals the subobject classified by

XθGXGhGPYϕPGYPηPY.X \stackrel{\theta}{\to} G X \stackrel{G h}{\to} G P Y \stackrel{\phi}{\to} P G Y \stackrel{P\eta}{\to} P Y.

First, remembering how ϕ was defined, the subobject classified by ϕGh:GXPGY appears as the left-hand column in

GR G( Y) Gi G(Y×X) G(1×h) G(Y×PY) G(π 1),G(π 2) G(π 1),G(π 2) GY×GX 1×Gh GY×GPY \array{ & G R & \to & G(\in_Y) & \\ & G i \downarrow & & \downarrow & \\ & G(Y \times X) & \stackrel{G(1 \times h)}{\to} & G(Y \times P Y) & \\ \langle G(\pi_1), G(\pi_2) \rangle & \downarrow & & \downarrow & \langle G(\pi_1), G(\pi_2) \rangle \\ & G Y \times G X & \stackrel{1 \times G h}{\to} & G Y \times G P Y & }

Then, the condition is that postcomposing ϕGh by Pη and precomposing with θ, the subobject of Y×X classified by PηϕGhθ, which is obtained by further pulling back as below, should match the subobject i:RY×X, as in the left-hand column below:

R GR G( Y) k Gi Y× G1X η× G1θ GY× G1GX G(Y×PY) Y×X η×θ GY×GX 1×Gh GY×GPY\array{ R & \to & G R & \to & G(\in_Y) \\ k \downarrow & & G i \downarrow & & \downarrow \\ Y \times_{G 1} X & \stackrel{\eta \times_{G 1} \theta}{\to} & G Y \times_{G 1} G X & \to & G(Y \times P Y) \\ \downarrow & & \downarrow & & \downarrow \\ Y \times X & \stackrel{\eta \times \theta}{\to} & G Y \times G X & \stackrel{1 \times G h}{\to} & G Y \times G P Y }

This condition amounts saying that the top left square is a pullback (and that i:RY×X factors through the inclusion Y× G1XY×X), since the other three squares are obviously pullbacks already if G preserves pullbacks. That the top left square is a pullback is tantamount to having a pullback (through which the top left square factors)

R GR k Gk Y× G1X γ G(Y× G1X)\array{ R & \to & G R \\ k \downarrow & & \downarrow G k \\ Y \times_{G 1} X & \stackrel{\gamma}{\to} & G(Y \times_{G 1} X) }

precisely as in (7). Thus the proof of theorem 1 is complete.

Application of theorem 1

Let us put this theorem to work, by showing how the passage from a topos E to the topos of presheaves on an internal category can be accomplished in just one step, instead of two. Given an internal category in E with underlying span

C 1 s t C 0 C 0\array{ & & C_1 & & \\ & s \swarrow & & \searrow t \\ C_0 & & & & C_0 }

there is a comonad formed as the composite

EC 0×E/C 0s *E/C 1Π tE/C 0 C 0EE \stackrel{C_0 \times -}{\to} E/C_0 \stackrel{s^*}{\to} E/C_1 \stackrel{\Pi_t}{\to} E/C_0 \stackrel{\sum_{C_0}}{\to} E

where s * denotes pulling back along s, and Π t is right adjoint to t *.

This comonad takes an object Y of E (“a set”) to

xC 0Y t 1(x)\sum_{x \in C_0} Y^{t^{-1}(x)}

where t 1(x) denotes the set of all morphisms whose target is xC 0. This comonad is manifestly pullback-preserving. A coalgebra structure

Y xC 0Y t 1(x)Y \to \sum_{x \in C_0} Y^{t^{-1}(x)}

sends yY to some summand at an index x (so we think of this yx as giving a fibering p:YC 0). More precisely, y is mapped to a function y :t 1(x)Y, so that given f:xx=p(y) in t 1(x), hitting it with y gives an element y f in Y. The assignments (f,y)y f should be thought of as producing a (contravariant) action of C on the fibered set YC 0, inasmuch as the coalgebra axioms guarantee equational axioms of the form

(y f) g=y fgy 1=1(y^f)^g = y^{f \circ g} \qquad y^1 = 1

wherever they make sense. But such a C-action is simply another name for a presheaf F on C, where the fibering YC 0 corresponds to the category of elements of F.

In summary, coalgebras of this comonad G:EE are exactly internal presheaves on C, and theorem 1 shows that the category of presheaves is a topos, in a single shot.

Two theorems in one, again

We’ve now given a reduction of three fundamental theorems of topos theory to two:

What is interesting in these cases is that the relevant constructions, in particular the construction of power objects, can be made to look exactly the same in E J as in E G. It is therefore very tempting to seek a further reduction, i.e., a generalization which combines these two theorems into one. But finding a common generalization of monads and comonads would seem to be an ill-advised task, to say the least.

In particular, there is no analogue of the counit

ε:G1 E:EE\varepsilon: G \to 1_E: E \to E

in the monad case, even when the monad is idempotent. However, looking over our earlier proofs, particularly of lemmas 0, 1, and 2, we found that the presence of a counit for our comonad G played a very restricted role. In fact, it played no essential role whatsoever, except in one place in the proof of lemma 0, where it was used to prove that coalgebra structures fit into pullback squares

S γ GS γ Gγ GS δS GGS;\array{ S & \stackrel{\gamma}{\to} & G S \\ \gamma \downarrow & & \downarrow G \gamma \\ G S & \stackrel{\delta S}{\to} & G G S; }

here we used only the fact that Gε was a common left inverse to δ, Gγ. In other words, if we take this pullback property for granted, then the rest of the proof of theorem 1 goes through without invoking the counit again.

Let’s look now at the monad side of things. For general monads J, there are two structure maps

Ju,uJ:JJJJ u, u J: J \stackrel{\to}{\to} J J

where u:1J denotes the unit, but for idempotent monads these maps coincide: each is the inverse of the monad multiplication

m:JJJm: J J \to J

which for an idempotent monad is an isomorphism, by definition. Moreover, an algebra structure for an idempotent monad,

ξ:JXX,\xi: J X \to X,

is itself an isomorphism with inverse given by the unit uX:XJX. In particular, it is trivial that for a J-algebra X, the following square is a pullback:

X uX JX uX JuX JX uJX JJX\array{ X & \stackrel{u X}{\to} & J X \\ u X \downarrow & & \downarrow J u X \\ J X & \stackrel{u J X}{\to} & J J X }

since all arrows in sight are isomorphisms. If we then define δ:JJJ to be uJ, then this pullback square for J-algebras has the same formal shape as the pullback square for G-coalgebras above.

With these preliminaries in place, we now propose the following definition as a generalization of pullback-preserving comonad and lex idempotent monad:

Definition 1: Let E be a finitely complete category.

The category of G-structures will be denoted E G. It is not hard to see that G is strict if and only if G1 is terminal in E G.

Remark: I invite discussion about the appropriateness of the term ‘modal operator’ to describe such structures. On the one hand, Tarski has given a topological interpretation of a modal operator ‘necessity’, by considering the operator on the Boolean algebra PX which maps a subset to its interior with respect to some given topology on X; such interior operators are the same as left exact comonads on PX. (See for instance the paper by Awodey-Kinisha.) On the other hand, Lawvere claims that a Lawvere-Tierney topology, that is a left exact internal monad on Ω, or (on a categorified level) a left exact idempotent monad on the ambient topos E, should be construed as a modal operator j where truth of jϕ is read as saying ’ϕ is true locally’ (where the meaning of ‘local’ depends on the Lawvere-Tierney topology chosen). It’s clear that I’m trying to consider an abstract common (categorified) generalization that covers these cases, but at present I haven’t assembled more convincing arguments for why ‘modal operator’ is a good term. Maybe it is, maybe it isn’t…

I’m happy to hear other suggestions, of course. I seem to recall that modal operators as defined here bear some broad resemblance to the notion of “interpolad” due to Koslowski, but I have not studied this work.

Here then is our fundamental three-in-one theorem:

Theorem 2: Let (G,δ) be a strict modal operator on a topos E. Then the category of G-structures E G is also a topos.

Proof: This proceeds pretty much the same way as the proof given above for theorem 1. It is straightforward to check that the underlying functor E GE, from G-structures to E, creates and preserves pullbacks if G preserves pullbacks. Thus E G admits pullbacks, and it admits a terminal object G1 under the strictness assumption; therefore E G admits all finite limits. In particular, the underlying object in E of the product of two G-structures X, Y is X× G1Y.

Power objects in E G are constructed just as they were in theorem 1. First one constructs an auxiliary map in E,

ϕ:GPYPGY,\phi: G P Y \to P G Y,

namely the map which classifies the subobject defined by the composite mono

G( Y)G(Y×PY)GY× G1GPYGY×GPYG(\in_Y) \hookrightarrow G(Y \times P Y) \cong G Y \times_{G 1} G P Y \hookrightarrow G Y \times G P Y

and then as before one defines, for a G-structure (Y,η:YGY), a putative power object P G(Y) in E G, namely the equalizer of the diagram

(8)GPY id GPY δPY GPη GGPY Gϕ GPGY\array{ G P Y & \stackrel{id}{\to} & G P Y \\ \delta P Y \downarrow & & \uparrow G P\eta \\ G G P Y & \stackrel{G\phi}{\to} & G P G Y }

in E G. One then has the task of proving that this works: that given a G-structure (X,θ:XGX), that G-structure maps are in natural bijection with G-structure subobjects of X× G1Y, the product of X and Y in E G. At the risk of some redundancy (by essentially repeating earlier arguments), let’s run through this now.

Lemma 3: Let G:EE be a modal operator, and (S,γ:SGS) a G-structure. Then a mono in E G targeted at (S,γ) is given precisely by a mono k:RS in E which fits into a pullback square of the form

(9)R β GR k Gk S γ GS\array{ R & \stackrel{\beta}{\to} & G R \\ k \downarrow & & \downarrow G k \\ S & \stackrel{\gamma}{\to} & G S }

Proof: A morphism k in E G is monic if and only if its underlying morphism in monic in E, because the underlying functor E GE creates and preserves pullbacks and therefore monos.

So let k:RS be a mono in E, and suppose (9) is a pullback square. The map β:RGR is uniquely determined since Gk is monic, and we claim it defines a G-structure on R. Indeed, we have a diagram

R β GR Gk GS β ? Gβ Gγ GR δR GGR GGk GGS\array{ R & \stackrel{\beta}{\to} & G R & \stackrel{G k}{\to} & G S \\ \beta \downarrow & ? & \downarrow G\beta & & \downarrow G\gamma \\ G R & \stackrel{\delta R}{\to} & G G R & \stackrel{G G k}{\to} & G G S }

where the right-hand square is a pullback by assumption and the fact that G preserves pullbacks. Therefore, to show the left-hand square is a pullback, it suffices to show the composite square is a pullback. But this composite is the same as the composite square for the diagram

R k S γ GS β γ Gγ GR Gk GS δS GGS\array{ R & \stackrel{k}{\to} & S & \stackrel{\gamma}{\to} & G S \\ \beta \downarrow & & \downarrow \gamma & & \downarrow G\gamma \\ G R & \stackrel{G k}{\to} & G S & \stackrel{\delta S}{\to} & G G S }

in which both squares are pullbacks. Thus β:RGR indeed defines a G-structure, and commutativity of (9) says k is a G-structure map. Thus one direction of the lemma is established.

For the other direction, suppose that (9) defines a monomorphism of G-structures. We must show (9) is a pullback. For this, suppose we have a commutative square

(10)X f GR g Gk S γ GS\array{ X & \stackrel{f}{\to} & G R \\ g \downarrow & & \downarrow G k \\ S & \stackrel{\gamma}{\to} & G S }

First, we prove that f equalizes the pair δR,Gβ:GRGGR. We have a series of equations

GGkGβf=GγGkf=Gγγg=δSγg=δSGkf=GGkδRfG G k \circ G\beta \circ f = G\gamma \circ G k \circ f = G\gamma \circ \gamma \circ g = \delta S \circ \gamma \circ g = \delta S \circ G k \circ f = G G k \circ \delta R \circ f

using, in turn, (9) (and functoriality of G), (10), the coassociativity on the G-structure S, (10) again, and naturality of δ. Comparing the first and last terms of this series, and using the fact that GGk is monic, we obtain δRf=Gβf.

Thus f factors through the equalizer β:RGR of δR,Gβ:GRGGR. Write f=βp. We then have

γkp=(9)Gkβp=Gkf=(10)γg\gamma \circ k \circ p \stackrel{(9)}{=} G k \circ \beta \circ p = G k \circ f \stackrel{(10)}{=} \gamma \circ g

and since γ is monic, we infer that kp=g. Moreover, this p is unique since k is monic. Thus, we have shown that any square (10) factors uniquely, via the map p:XR, through the square (9); this completes the proof of lemma 3.

Now we resume the proof of theorem 2; it remains to show that the equalizer j:P G(Y)GPY of the pair of maps in (8) is the power object of the G-structure (Y,η:YGY). Let (X,θ:XGX) be a G-structure, and f:XP G(Y) a G-structure map. Then g=jf:XGPY equalizes the maps in (8).

Let h:XPY be the composite

XgGPYϕPGYPηPYX \stackrel{g}{\to} G P Y \stackrel{\phi}{\to} P G Y \stackrel{P\eta}{\to} P Y

Then we have

g=GPηGϕδPYg=GPηGϕGgθ=Ghθg = G P\eta \circ G\phi \circ \delta P Y \circ g = G P \eta \circ G\phi \circ G g \circ \theta = G h \circ \theta

where the first equation is the equalizing condition on g, the second uses the fact that g is a G-structure map, and the third uses functoriality of G. Hence g is retrievable from h. In fact, the mapping

(g:XGPY)h=(XgGPYϕPGYPηPY)(g: X \to G P Y) \mapsto h = (X \stackrel{g}{\to} G P Y \stackrel{\phi}{\to} P G Y \stackrel{P\eta}{\to} P Y)

defines a bijection between maps g satisfying the equalizing condition and maps h:XPY such that

(11)h=(XθGXGhGPYϕPGYPηPY)h = (X \stackrel{\theta}{\to} G X \stackrel{G h}{\to} G P Y \stackrel{\phi}{\to} P G Y \stackrel{P\eta}{\to} P Y)

The map h classifies a subobject i:RX×Y in E, and we need to check that condition (11) on h corresponds precisely to the condition that R is a sub-G-structure of X× G1Y. Or, taking into account lemma 3: precisely to the condition that there is a pullback diagram of the form

(12)R β GR k Gk X× G1Y γ G(X× G1Y)\array{ R & \stackrel{\beta}{\to} & G R \\ k \downarrow & & \downarrow G k \\ X \times_{G 1} Y & \stackrel{\gamma}{\to} & G(X \times_{G 1} Y) }

where γ is the G-structure on X× G1Y, and k is monic.

Proof: The condition is that the subobject i:RY×X equals the subobject classified by the composite given in (11):

XθGXGhGPYϕPGYPηPY.X \stackrel{\theta}{\to} G X \stackrel{G h}{\to} G P Y \stackrel{\phi}{\to} P G Y \stackrel{P\eta}{\to} P Y.

The subobject classified by ϕGh:GXPGY appears as the left-hand column in

GR G( Y) Gi G(Y×X) G(1×h) G(Y×PY) G(π 1),G(π 2) G(π 1),G(π 2) GY×GX 1×Gh GY×GPY \array{ & G R & \to & G(\in_Y) & \\ & G i \downarrow & & \downarrow & \\ & G(Y \times X) & \stackrel{G(1 \times h)}{\to} & G(Y \times P Y) & \\ \langle G(\pi_1), G(\pi_2) \rangle & \downarrow & & \downarrow & \langle G(\pi_1), G(\pi_2) \rangle \\ & G Y \times G X & \stackrel{1 \times G h}{\to} & G Y \times G P Y & }

Then, the condition is that postcomposing ϕGh by Pη and precomposing with θ, the subobject of Y×X classified by PηϕGhθ, which is obtained by further pulling back as below, should match the subobject i:RY×X, as in the left-hand column below:

R GR G( Y) k Gi Y× G1X η× G1θ GY× G1GX G(Y×PY) Y×X η×θ GY×GX 1×Gh GY×GPY\array{ R & \to & G R & \to & G(\in_Y) \\ k \downarrow & & G i \downarrow & & \downarrow \\ Y \times_{G 1} X & \stackrel{\eta \times_{G 1} \theta}{\to} & G Y \times_{G 1} G X & \to & G(Y \times P Y) \\ \downarrow & & \downarrow & & \downarrow \\ Y \times X & \stackrel{\eta \times \theta}{\to} & G Y \times G X & \stackrel{1 \times G h}{\to} & G Y \times G P Y }

This condition amounts saying that the top left square is a pullback (and that i:RY×X factors through the inclusion Y× G1XY×X), since the other three squares are obviously pullbacks already if G preserves pullbacks. That the top left square is a pullback is tantamount to having a pullback (through which the top left square factors)

R GR k Gk Y× G1X γ G(Y× G1X)\array{ R & \to & G R \\ k \downarrow & & \downarrow G k \\ Y \times_{G 1} X & \stackrel{\gamma}{\to} & G(Y \times_{G 1} X) }

precisely as in (12). Thus the proof of theorem 2 is complete.

To tie up some loose ends, we should check that theorem 2 really does specialize to the pullback-preserving comonad theorem and the lex idempotent monad theorem. In other words, we should check that G-structures really are the same things as G-coalgebras or G-algebras, where G is either a pullback-preserving comonad or a lex idempotent monad, seen as a modal operator.

First, suppose G is a pullback-preserving comonad. We have already seen that a G-coalgebra (X,η:XGX) satisfies the G-structure axiom. Converse, if (X,η:XGX) is a G-structure, then it is also a G-coalgebra: all we have to do is verify the equation

1 X=(XηGXεXX)1_X = (X \stackrel{\eta}{\to} G X \stackrel{\varepsilon X}{\to} X)

Since we have a pullback

(13)X η GX η Gη GX δX GGX\array{ X & \stackrel{\eta}{\to} & G X \\ \eta \downarrow & & \downarrow G\eta \\ G X & \stackrel{\delta X}{\to} & G G X }

we know η is monic by lemma 0, so it suffices to show η=ηεXη. But we have

δXηεXη=δXεGXGηη=Gηη=δXη\delta X \circ \eta \circ \varepsilon X \eta = \delta X \circ \varepsilon G X \circ G\eta \circ \eta = G\eta \circ \eta = \delta X \circ \eta

using naturality of ε, the counit axiom for comonads, and commutativity of (13). Finally, since δ is monic, we have η=ηεXη, as was to be shown.

Next, let G be a lex idempotent monad, and define δ:GGG to be uG. Here we have a commuting coassociativity square for δ which consists of isomorphisms and is therefore a pullback, so (G,δ) is a modal operator. Also, for a G-algebra (X,α:GXX), the map α is an isomorphism, and so here algebra structure boils down to a condition that the unit uX:XGX is invertible (and then α=(uX) 1). It is then automatic that η=uX:XGX satisfies the G-structure pullback condition (again since all arrows in the coassociativity square (13) are isomorphisms).

In the other direction, if (X,η:XGX) is a G-structure, then the naturality square

X uX GX η Gη GX uGX GGX\array{ X & \stackrel{u X}{\to} & G X \\ \eta \downarrow & & \downarrow G\eta \\ G X & \stackrel{u G X}{\to} & G G X }

factors through the pullback (13) via a unique map i:XX, and since η is an isomorphism in this case, we must have i=1 X, whence also η=uX. Thus uX is an isomorphism, so that X is a G-algebra. In other words, the category of G-algebras for a lex idempotent monad G is equivalent to the category of G-structures where G is viewed as a modal operator.

Finally, it is clear that 1 is a G-algebra, hence the G-algebra map G11 is an isomorphism. Hence G1 is terminal in E G, so that G is strict.

Application of theorem 2, and further results

We have seen that pullback-preserving comonads and left exact idempotent monads (equivalently, pullback-preserving idempotent monads) are examples of modal operators. In order for the notion of modal operator to be a really viable concept, however, we should give some other interesting examples which fall outside these two classes. We should also make good on our promise to present the fundamental passage, from a topos E to the topos of sheaves on an internal site in E, in a single step (more precisely, a single application of theorem 2).

These goals are interconnected: we will construct, given an internal site (C,j) in E, a (strict) modal operator G:EE such that the category of sheaves Sh(C,j) is equivalent to the category of G-structures. This G is neither a pullback-preserving comonad nor a lex idempotent monad; it’s a hybrid which supports the viability of our notion of modal operator.

Indeed, it isn’t hard to imagine how this works. First, we have a two-step passage

Sh(C,j) ai E C op GU E\array{ Sh(C, j) \\ a \uparrow \downarrow i \\ E^{C^{op}} \\ G \uparrow \downarrow U \\ E }

where U:E C opE assigns to each presheaf its underlying “set” (object) of elements, and G is right adjoint to U; the comonad UG:EE was the one used to describe E C op as the category of coalgebras in the application of theorem 1. The functor a:E C opSh(C,j) is the associated sheaf functor, and i, its right adjoint, is the underlying functor from sheaves to presheaves. The composite J=ia is a lex idempotent monad whose category of algebras is Sh(C,j), and naturally theorem 2 guarantees that Sh(C,j) is a topos, given that E C op is.

Suppose we traverse the full circuit of arrows from E back to itself, giving rise to an operator

K=UiaG:EE.K = U i a G: E \to E.

This K is a hybrid formed from the comonad UG and the monad J=ia, but is neither a comonad nor a monad itself. It is, as we shall see, a (strict) modal operator on E, such that Sh(C,j) is equivalent to the category of K-structures! This is the denouement we were waiting for: it shows that the passage from sets to sheaves is really a one-step process, if we choose the modal operator on sets right.

The entire discussion is concentrated in theorem 3 below, after a few preliminaries. Let E be finitely complete, and let G:EE be a modal operator. For each G-structure (Y,η):YGY, the map η is a map of G-structures. Thus, if U:E GE denotes the underlying functor and G:EE G, by slight abuse of notation, denotes the evident functor XGX, then we have a natural transformation

η:1 E GGU:E GE G\eta: 1_{E_G} \to G U: E_G \to E_G

Of course, this isn’t generally a unit of an adjunction or anything like that, but much of the power of modal operators derives from a fact which is the essential point of lemma 3 above: that η is cartesian with respect to monos. We take advantage of this fact repeatedly.

If furthermore (H,δ) is a modal operator on E G, then we have a round trip operator

K=(EGE GHE GUE)K = (E \stackrel{G}{\to} E_G \stackrel{H}{\to} E_G \stackrel{U}{\to} E)

and we define a transformation λ:KKK in the only reasonable way possible: as the composite

UHGUδGUHHGUHηHGUHGUHGU H G \stackrel{U\delta G}{\to} U H H G \stackrel{U H \eta H G}{\to} U H G U H G

Theorem 3: (K,λ) defines a modal operator on E, and E K(E G) H. If the modal operators G and H are strict, then so is K.

Proof: A completely detailed proof involves some largish diagrams, but we sketch the essential points. To prove K is a modal operator, we need to contemplate a diagram of shape

UHG UδG UHHG UHηHG UHGUHG UδG UHδG UHGUδG UHHG UδHG UHHHG UHηHHG UHGUHHG UHηHG UHHηHG (4) UHGUHηG UHGUHG UδGUHG UHHGUHG UHηHGUHG UHGUHGUHG \array{ & U H G & \stackrel{U\delta G}{\to} & U H H G & \stackrel{U H\eta H G}{\to} & U H G U H G & \\ U\delta G & \downarrow & & U H \delta G \downarrow & & \downarrow & U H G U\delta G \\ & U H H G & \stackrel{U\delta H G}{\to} & U H H H G & \stackrel{U H\eta H H G}{\to} & U H G U H H G & \\ U H \eta H G & \downarrow & & U H H \eta H G \downarrow & (4) & \downarrow & U H G U H\eta G\\ & U H G U H G & \underset{U\delta G U H G}{\to} & U H H G U H G & \underset{U H\eta H G U H G}{\to} & U H G U H G U H G & }

where all four squares are pullbacks by more or less the same argument, which we give just for the square labeled (4): this square is obtained by applying the pullback-preserving functor UH (at the argument HG) to the square

H ηH GUH Hη GUHη HGU ηHGU GUHGU\array{ H & \stackrel{\eta H}{\to} & G U H \\ H\eta \downarrow & & \downarrow G U H\eta \\ H G U & \stackrel{\eta H G U}{\to} & G U H G U }

which is a pullback by lemma 3 (Hη is monic, and the transformation η is cartesian with respect to monos). This completes the sketch for why K is a modal operator.

Now we sketch the equivalence (E G) HE K. In one direction, it is relatively easy to define a functor (E G) HE K. For consider an object of (E G) H. This consists of an object X of E together with structures

η:XUGXθ:XhX\eta: X \to U G X \qquad \theta: X \to h X

(where hX denotes the underlying object in E of the value of H applied to the G-structure (X,η)), subject to various pullback conditions. Observe that η may be regarded as a map in E G; by applying H:E GE G to it, we obtain a map

hη:hXhGX=UHGXh\eta: h X \to h G X = U H G X

and hence a composite

XθhXhηUHGXX \stackrel{\theta}{\to} h X \stackrel{h\eta}{\to} U H G X

which is a map ζ:XKX which defines a putative K-structure. Indeed, in E we have a diagram of the form

X θ hX hη hGX θ (1) δX (2) δGX hX hθ hhX hhη hhGX hη (3) hη (4) hη hGX hGθ hGhX hGhη hGhGX\array{ X & \stackrel{\theta}{\to} & h X & \stackrel{h\eta}{\to} & h G X\\ \theta\downarrow & (1) & \downarrow \delta X & (2) & \downarrow \delta G X \\ h X & \stackrel{h\theta}{\to} & h h X & \stackrel{h h\eta}{\to} & h h G X\\ h\eta\downarrow & (3) & \downarrow h\eta & (4) & \downarrow h\eta\\ h G X & \stackrel{h G\theta}{\to} & h G h X & \stackrel{h G h\eta}{\to} & h G h G X }

where (1) is a pullback because θ is the underlying map of an H-structure, (2) is a pullback because hη is a monic H-structure map (then use lemma 3), (3) is a pullback because H preserves pullbacks and θ is also a monic G-structure map (lemma 3 again), and (4) is a pullback because H preserves pullbacks and hη is a monic G-structure map.

In the other direction, we now define a functor E K(E G) H. This is a bit trickier; the main hurdle to overcome is to produce a G-structure η:XUGX from a K-structure ζ:XUHGX. In summary, the pullback of a diagram having the form

hGX η UGhGX UGδGX UGhhGX UGhη hGX ηhGX UGhGX UGhGζ UGhGhGX \array{ & & & & h G X & \\ & & & & \downarrow & \eta \\ & & & & U G h G X & \\ & & & & \downarrow & U G\delta G X \\ & & & & U G h h G X & \\ & & & & \downarrow & U G h\eta \\ h G X & \stackrel{\eta h G X}{\to} & U G h G X & \stackrel{U G h G\zeta}{\to} & U G h G h G X & }

is X (with both pullback projections being ζ:XhGX), by taking advantage of the pullback axiom on the K-structure ζ together with naturality of η. If we leave off the leftmost and topmost map from this diagram, we get a diagram

UGhGX UGδGX UGhhGX UGhη UGhGX UGhGζ UGhGhGX \array{ & & U G h G X & \\ & & \downarrow & U G\delta G X \\ & & U G h h G X & \\ & & \downarrow & U G h\eta \\ U G h G X & \stackrel{U G h G\zeta}{\to} & U G h G h G X & }

whose pullback is UGX (with both pullback projections being UGζ), by the pullback condition on ζ and the fact that UG preserves pullbacks. Thus the first pullback X factors through the second pullback UGX, by a map I shall again call η:XUGX. It may be checked that this makes X a G-structure. From all this we get a pullback

X ζ hGX η η UGX UGζ UGhGX\array{ X & \stackrel{\zeta}{\to} & h G X \\ \eta \downarrow & & \downarrow \eta \\ U G X & \stackrel{U G\zeta}{\to} & U G h G X }

so that ζ:XhGX is a G-structure map, and it will be so regarded. Thus, we interpret this pullback square as lifted up to the category E G, and we hit it with the pullback-preserving functor h=UH. The result is the square appearing in the diagram

UHGX δGX hX hζ UHHGX hηX UHηHGX UHGX hGζ UHGUHGX \array{ & & U H G X & \\ & & \downarrow & \delta G X \\ h X & \stackrel{h\zeta}{\to} & U H H G X & \\ h\eta X \downarrow & & \downarrow & U H \eta H G X \\ U H G X & \stackrel{h G\zeta}{\to} & U H G U H G X & }

and the pullback of the right-hand column against the bottom map is, by the K-structure axiom, X with both pullback projections being ζ:XUHGX. Thus we arrive at a diagram

X ζ UHGX θ δGX hX hζ UHHGX hηX UHηHGX UHGX hGζ UHGUHGX \array{ X & \stackrel{\zeta}{\to} & U H G X \\ \theta \downarrow & & \downarrow & \delta G X \\ h X & \stackrel{h\zeta}{\to} & U H H G X & \\ h\eta X \downarrow & & \downarrow & U H \eta H G X \\ U H G X & \stackrel{h G\zeta}{\to} & U H G U H G X & }

in which ζ=hηθ. It may be checked that θ defines an H-structure in E G, and this concludes our sketch of the equivalence E K(E G) H.

Finally, if the modal operators G and H are strict, then G1 is terminal in E G, and then HG1 is terminal in (E G) HE K. Since K1=HG1 is terminal in E K, it follows that K is strict. This concludes the proof of theorem 3.

Theorem 3 gives one means of constructing new modal operators from old.

Acknowledgments

I thank Sridhar Ramesh and Mike Shulman for pointing out that Theorem 1 appears in print in Johnstone’s Elephant, and Mike for many thoughtful comments on a draft of this article, in particular for pointing out the closely related work by Toby Kenney on toposes constructed by means of diads reference to be inserted.

Revised on March 4, 2010 14:08:57 by Todd Trimble