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 (since about 1997), 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 JJ is the composite of taking the associated sheaf functor (which is left exact) followed by the forgetful functor from sheaves to presheaves; the JJ-algebras are the sheaves. The monad JJ is idempotent because the associated sheaf of a sheaf XX is canonically isomorphic to XX (alternatively, because the embedding of sheaves in presheaves is full and faithful). In fact, every such lex idempotent monad on a topos EE arises in this way, by sheafifying with respect to a Lawvere-Tierney topology in EE.

Thus the three theorems taken together effect the passage from a base category SetSet 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/XE/X is the category of coalgebras for the comonad ×X:EE- \times X: E \to E, where the comonad structure comes from the unique comonoid structure which exists on any object XX:

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

The comonad ×X- \times 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

If G:EEG: E \to E is a pullback-preserving comonad acting on a topos EE, then the category of coalgebras E GE_G is also a topos.

Proof

It suffices to produce finite limits and power objects in E GE_G. Pullbacks in E GE_G are created by the forgetful functor E GEE_G \to E because GG preserves pullbacks, and G1G 1 is terminal in E GE_G if 11 is terminal in EE, since the right adjoint G:EE GG-: E \to E_G preserves limits. So E GE_G is finitely complete.

Since G:EEG: E \to E preserves pullbacks, it also preserves monos. In particular, if YY×PY\in_Y \hookrightarrow Y \times P Y denotes the elementhood relation between YY and its power object PYP Y in EE, 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 EE. The composite of the monos in (1) names a subobject of GY×GPYG Y \times G P Y, which is classified by a map

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

in EE.

Let δ:GGG\delta: G \to G G denote the comultiplication and ε:G1 E\varepsilon: G \to 1_E the counit of GG, and suppose YY carries a GG-coalgebra η:YGY\eta: Y \to G Y. Define the object P GYP_G Y in E GE_G to be the equalizer in E GE_G of the following pair of coalgebra maps from the cofree coalgebra GPYG P Y 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 PP is the contravariant power object functor (whence the direction Pη:PGYPYP \eta: P G Y \to P Y). We will show that P GYP_G Y is the power object of YY in E GE_G.

So, let (X,θ:XGX)(X, \theta: X \to G X) be a coalgebra. We must show that coalgebra maps f:XP GYf: X \to P_G Y correspond precisely to subcoalgebras of the product X×YX \times Y in E GE_G (whose underlying object in EE is the pullback X× G1YX \times_{G 1} Y). The remainder of the proof will be proven with the help of three lemmas.

Lemma 0: If (S,γ:SGS)(S, \gamma: S \to G S) is a GG-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 γ\gamma), 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 ff, gg coincide because GγG \gamma and δS\delta S have a common left inverse GεS:GGSGSG\varepsilon S: G G S \to G S. Therefore the pullback of the arrows GγG\gamma, δS\delta S is the same as their equalizer, which is γ:SGS\gamma: S \to G S. 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

Suppose G:EEG: E \to E is a comonad which preserves pullbacks, and let (S,γ:SGS)(S, \gamma: S \to G S) be a GG-coalgebra. Then a pair (k:RS,β:RGR)(k: R \to S, \beta: R \to G R) defines a subcoalgebra of SS precisely when kk 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, GkG k is monic assuming kk is monic, since GG preserves pullbacks. Therefore β\beta is uniquely determined. We must show that β:RGR\beta: R \to G R 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 kk 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 ε\varepsilon, the square (3), and the fact that SS is a coalgebra.

Again, GG preserves pullbacks, so GGkG G k is monic assuming kk 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 δ\delta, the square (3), and the fact that SS is a coalgebra.

Lemma

In the notation of lemma 1, if k:RSk: R \to S 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 ff equalizes the pair δR,Gβ:GRGGR\delta R, G\beta: G R \to G G R. 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 GG), (6), the coassociativity on the coalgebra SS, (6) again, and naturality of δ\delta. Comparing the first and last terms of this series, and using the fact that GGkG G k is monic (because kk is monic and GG preserves pullbacks), we obtain δRf=Gβf\delta R \circ f = G\beta \circ f.

Thus ff factors through the equalizer β:RGR\beta: R \to G R of δR,Gβ:GRGGR\delta R, G \beta: G R \stackrel{\to}{\to} G G R. Write f=βpf = \beta \circ 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 γ\gamma is monic (cf. lemma 0), we infer that kp=gk \circ p = g. Moreover, this pp is unique since kk is monic. Thus, we have shown that any square (6) factors uniquely, via the map p:XRp: X \to R, 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)GPYj: P_G(Y) \to G P Y of the pair of maps in (2) is the power object of the coalgebra (Y,η:YGY)(Y, \eta: Y \to G Y). Let (X,θ:XGX)(X, \theta: X \to G X) be a coalgebra, and f:XP G(Y)f: X \to P_G(Y) a coalgebra map. Then g=jf:XGPYg = j f: X \to G P Y equalizes the maps in (2). Moreover, since GPYG P Y is cofree, we have that to each GG-coalgebra map g:XGPYg: X \to G P Y, there exists a unique h:XPYh: X \to P Y in the topos EE such that

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

Thus g:XGPYg: X \to G P Y in E GE_G or h:XPYh: X \to P Y in EE corresponds to a subobject i:RX×Yi: R \hookrightarrow X \times Y in EE. We need to check that the condition that gg equalizes the pair of maps in (2) corresponds precisely to the condition that RR is a subcoalgebra of X× G1YX \times_{G 1} Y (the product of XX and YY in E GE_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 γ\gamma is the coalgebra structure on X× G1YX \times_{G 1} Y, and kk is monic.

Proof of Theorem 1

That g:XGPYg: X \to G P Y equalizes the pair of maps in (2) translates to a condition on h:XPYh: X \to P Y, 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×Xi: R \hookrightarrow Y \times 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 ϕ\phi was defined, the subobject classified by ϕGh:GXPGY\phi \circ G h: G X \to P G Y 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\phi \circ G h by PηP\eta and precomposing with θ\theta, the subobject of Y×XY \times X classified by PηϕGhθP\eta \circ \phi \circ G h \circ \theta, which is obtained by further pulling back as below, should match the subobject i:RY×Xi: R \hookrightarrow Y \times 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×Xi: R \to Y \times X factors through the inclusion Y× G1XY×XY \times_{G 1} X \hookrightarrow Y \times X), since the other three squares are obviously pullbacks already if GG 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 EE to the topos of presheaves on an internal category can be accomplished in just one step, instead of two. Given an internal category in EE 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 * s^* denotes pulling back along ss, and Π t\Pi_t is right adjoint to t * t^* .

This comonad takes an object YY of EE (“a set”) to

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

where t 1(x)t^{-1}(x) denotes the set of all morphisms whose target is xC 0x \in C_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 yYy \in Y to some summand at an index xx (so we think of this yxy \mapsto x as giving a fibering p:YC 0p: Y \to C_0). More precisely, yy is mapped to a function y :t 1(x)Yy^{-}: t^{-1}(x) \to Y, so that given f:xx=p(y)f: x' \to x = p(y) in t 1(x)t^{-1}(x), hitting it with y y^{-} gives an element y fy^f in YY. The assignments (f,y)y f(f, y) \mapsto y^f should be thought of as producing a (contravariant) action of CC on the fibered set YC 0Y \to C_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 CC-action is simply another name for a presheaf FF on CC, where the fibering YC 0Y \to C_0 corresponds to the category of elements of FF.

In summary, coalgebras of this comonad G:EEG: E \to E are exactly internal presheaves on CC, 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 JE^J as in E GE_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 GG 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εG\varepsilon was a common left inverse to δ\delta, GγG\gamma. 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 JJ, there are two structure maps

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

where u:1Ju: 1 \to J 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:XJXu X: X \to J X. In particular, it is trivial that for a JJ-algebra XX, 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\delta: J \to J J to be uJu J, then this pullback square for JJ-algebras has the same formal shape as the pullback square for GG-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 EE be a finitely complete category.

The category of GG-structures will be denoted E GE_G. It is not hard to see that GG is strict if and only if G1G 1 is terminal in E GE_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 PXP X which maps a subset to its interior with respect to some given topology on XX; such interior operators are the same as left exact comonads on PXP X. (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 Ω\Omega, or (on a categorified level) a left exact idempotent monad on the ambient topos EE, should be construed as a modal operator jj where truth of jϕj\phi is read as saying ‘ϕ\phi 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. \Box

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

Theorem 2: Let (G,δ)(G, \delta) be a strict modal operator on a topos EE. Then the category of GG-structures E GE_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 GEE_G \to E, from GG-structures to EE, creates and preserves pullbacks if GG preserves pullbacks. Thus E GE_G admits pullbacks, and it admits a terminal object G1G 1 under the strictness assumption; therefore E GE_G admits all finite limits. In particular, the underlying object in EE of the product of two GG-structures XX, YY is X× G1YX \times_{G 1} Y.

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

ϕ: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 GG-structure (Y,η:YGY)(Y, \eta: Y \to G Y), a putative power object P G(Y)P_G(Y) in E GE_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 GE_G. One then has the task of proving that this works: that given a GG-structure (X,θ:XGX)(X, \theta: X \to G X), that GG-structure maps are in natural bijection with GG-structure subobjects of X× G1YX \times_{G 1} Y, the product of XX and YY in E GE_G. At the risk of some redundancy (by essentially repeating earlier arguments), let’s run through this now.

Lemma 3: Let G:EEG: E \to E be a modal operator, and (S,γ:SGS)(S, \gamma: S \to G S) a GG-structure. Then a mono in E GE_G targeted at (S,γ)(S, \gamma) is given precisely by a mono k:RSk: R \to S in EE 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 kk in E GE_G is monic if and only if its underlying morphism in monic in EE, because the underlying functor E GEE_G \to E creates and preserves pullbacks and therefore monos.

So let k:RSk: R \to S be a mono in EE, and suppose (9) is a pullback square. The map β:RGR\beta: R \to G R is uniquely determined since GkG k is monic, and we claim it defines a GG-structure on RR. 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 GG 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\beta: R \to G R indeed defines a GG-structure, and commutativity of (9) says kk is a GG-structure map. Thus one direction of the lemma is established.

For the other direction, suppose that (9) defines a monomorphism of GG-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 ff equalizes the pair δR,Gβ:GRGGR\delta R, G\beta: G R \to G G R. 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 GG), (10), the coassociativity on the GG-structure SS, (10) again, and naturality of δ\delta. Comparing the first and last terms of this series, and using the fact that GGkG G k is monic, we obtain δRf=Gβf\delta R \circ f = G\beta \circ f.

Thus ff factors through the equalizer β:RGR\beta: R \to G R of δR,Gβ:GRGGR\delta R, G \beta: G R \stackrel{\to}{\to} G G R. Write f=βpf = \beta \circ 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 γ\gamma is monic, we infer that kp=gk \circ p = g. Moreover, this pp is unique since kk is monic. Thus, we have shown that any square (10) factors uniquely, via the map p:XRp: X \to R, through the square (9); this completes the proof of lemma 3. \Box

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

Let h:XPYh: X \to P Y 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 gg, the second uses the fact that gg is a GG-structure map, and the third uses functoriality of GG. Hence gg is retrievable from hh. 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 gg satisfying the equalizing condition and maps h:XPYh: X \to P Y 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 hh classifies a subobject i:RX×Yi: R \hookrightarrow X \times Y in EE, and we need to check that condition (11) on hh corresponds precisely to the condition that RR is a sub-GG-structure of X× G1YX \times_{G 1} Y. 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 γ\gamma is the GG-structure on X× G1YX \times_{G 1} Y, and kk is monic.

Proof: The condition is that the subobject i:RY×Xi: R \hookrightarrow Y \times 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\phi \circ G h: G X \to P G Y 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\phi \circ G h by PηP\eta and precomposing with θ\theta, the subobject of Y×XY \times X classified by PηϕGhθP\eta \circ \phi \circ G h \circ \theta, which is obtained by further pulling back as below, should match the subobject i:RY×Xi: R \hookrightarrow Y \times 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×Xi: R \to Y \times X factors through the inclusion Y× G1XY×XY \times_{G 1} X \hookrightarrow Y \times X), since the other three squares are obviously pullbacks already if GG 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. \Box

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 GG-structures really are the same things as GG-coalgebras or GG-algebras, where GG is either a pullback-preserving comonad or a lex idempotent monad, seen as a modal operator.

First, suppose GG is a pullback-preserving comonad. We have already seen that a GG-coalgebra (X,η:XGX)(X, \eta: X \to G X) satisfies the GG-structure axiom. Converse, if (X,η:XGX)(X, \eta: X \to G X) is a GG-structure, then it is also a GG-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 η\eta is monic by lemma 0, so it suffices to show η=ηεXη\eta = \eta \circ \varepsilon X \circ \eta. 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 ε\varepsilon, the counit axiom for comonads, and commutativity of (13). Finally, since δ\delta is monic, we have η=ηεXη\eta = \eta \circ \varepsilon X \circ \eta, as was to be shown.

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

In the other direction, if (X,η:XGX)(X, \eta: X \to G X) is a GG-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:XXi: X \to X, and since η\eta is an isomorphism in this case, we must have i=1 Xi = 1_X, whence also η=uX\eta = u X. Thus uXu X is an isomorphism, so that XX is a GG-algebra. In other words, the category of GG-algebras for a lex idempotent monad GG is equivalent to the category of GG-structures where GG is viewed as a modal operator.

Finally, it is clear that 11 is a GG-algebra, hence the GG-algebra map G11G 1 \to 1 is an isomorphism. Hence G1G 1 is terminal in E GE_G, so that GG 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 EE to the topos of sheaves on an internal site in EE, 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)(C, j) in EE, a (strict) modal operator G:EEG: E \to E such that the category of sheaves Sh(C,j)Sh(C, j) is equivalent to the category of GG-structures. This GG 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 opEU: E^{C^{op}} \to E assigns to each presheaf its underlying “set” (object) of elements, and GG is right adjoint to UU; the comonad UG:EEU G: E \to E was the one used to describe E C opE^{C^{op}} as the category of coalgebras in the application of theorem 1. The functor a:E C opSh(C,j)a: E^{C^{op}} \to Sh(C, j) is the associated sheaf functor, and ii, its right adjoint, is the underlying functor from sheaves to presheaves. The composite J=iaJ = i a is a lex idempotent monad whose category of algebras is Sh(C,j)Sh(C, j), and naturally theorem 2 guarantees that Sh(C,j)Sh(C, j) is a topos, given that E C opE^{C^{op}} is.

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

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

This KK is a hybrid formed from the comonad UGU G and the monad J=iaJ = i a, but is neither a comonad nor a monad itself. It is, as we shall see, a (strict) modal operator on EE, such that Sh(C,j)Sh(C, j) is equivalent to the category of KK-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 EE be finitely complete, and let G:EEG: E \to E be a modal operator. For each GG-structure (Y,η):YGY(Y, \eta): Y \to G Y, the map η\eta is a map of GG-structures. Thus, if U:E GEU: E_G \to E denotes the underlying functor and G:EE GG: E \to E_G, by slight abuse of notation, denotes the evident functor XGXX \mapsto G X, 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 η\eta is cartesian with respect to monos. We take advantage of this fact repeatedly.

If furthermore (H,δ)(H, \delta) is a modal operator on E GE_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\lambda: K \to K K 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,λ)(K, \lambda) defines a modal operator on EE, and E K(E G) HE_K \simeq (E_G)_H. If the modal operators GG and HH are strict, then so is KK.

Proof: A completely detailed proof involves some largish diagrams, but we sketch the essential points. To prove KK 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 UHU H (at the argument HGH G) 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ηH\eta is monic, and the transformation η\eta is cartesian with respect to monos). This completes the sketch for why KK is a modal operator.

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

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

(where hXh X denotes the underlying object in EE of the value of HH applied to the GG-structure (X,η)(X,\eta)), subject to various pullback conditions. Observe that η\eta may be regarded as a map in E GE_G; by applying H:E GE GH: E_G \to E_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\zeta: X \to K X which defines a putative KK-structure. Indeed, in EE 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 θ\theta is the underlying map of an HH-structure, (2) is a pullback because hηh\eta is a monic HH-structure map (then use lemma 3), (3) is a pullback because HH preserves pullbacks and θ\theta is also a monic GG-structure map (lemma 3 again), and (4) is a pullback because HH preserves pullbacks and hηh\eta is a monic GG-structure map.

In the other direction, we now define a functor E K(E G) HE_K \to (E_G)_H. This is a bit trickier; the main hurdle to overcome is to produce a GG-structure η:XUGX\eta: X \to U G X from a KK-structure ζ:XUHGX\zeta: X \to U H G X. 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 XX (with both pullback projections being ζ:XhGX\zeta: X \to h G X), by taking advantage of the pullback axiom on the KK-structure ζ\zeta together with naturality of η\eta. 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 UGXU G X (with both pullback projections being UGζU G\zeta), by the pullback condition on ζ\zeta and the fact that UGU G preserves pullbacks. Thus the first pullback XX factors through the second pullback UGXU G X, by a map I shall again call η:XUGX\eta: X \to U G X. It may be checked that this makes XX a GG-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\zeta: X \to h G X is a GG-structure map, and it will be so regarded. Thus, we interpret this pullback square as lifted up to the category E GE_G, and we hit it with the pullback-preserving functor h=UHh = U H. 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 KK-structure axiom, XX with both pullback projections being ζ:XUHGX\zeta: X \to U H G X. 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ηθ\zeta = h\eta \circ \theta. It may be checked that θ\theta defines an HH-structure in E GE_G, and this concludes our sketch of the equivalence E K(E G) HE_K \simeq (E_G)_H.

Finally, if the modal operators GG and HH are strict, then G1G 1 is terminal in E GE_G, and then HG1H G 1 is terminal in (E G) HE K(E_G)_H \simeq E_K. Since K1=HG1K 1 = H G 1 is terminal in E KE_K, it follows that KK is strict. This concludes the proof of theorem 3. \Box

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 30, 2018 at 00:20:57 by Todd Trimble