nLab toposes are extensive

Toposes are extensive

Toposes are extensive


Every elementary topos is a finitary extensive category. In fact, more is true: if an elementary topos has coproducts indexed by any arity class κ\kappa, then it is κ\kappa-extensive. In particular, a cocomplete elementary topos is infinitary extensive.


There are several possible proofs. In all cases, stability of coproducts under pullback is automatic since a topos is locally cartesian closed, so it suffices to consider disjointness.

From finitary to infinitary

As shown at extensive category, if we assume classical logic then jJA jA 1A 2 j1,2A j\coprod_{j\in J} A_j \cong A_1 \sqcup A_2 \sqcup \coprod_{j\neq 1,2} A_j, so that in a finitary-extensive category, any existing coproducts are stable and disjoint. Thus, in this case it suffices to deal with finite coproducts. However, in topos theory we are often interested in toposes “over an arbitrary base”, in which case the ambient logic is constructive logic and so this argument does not apply.

Nevertheless, we mention a couple of proofs that apparently apply only to the finitary case in addition to the fully general version.

Via pushouts of monos

A proof applying to finite coproducts is given in Johnstone, A2.4.4: since 0X0\to X and 0Y0\to Y are monic, it suffices to show that the pushout of a mono is a mono and also a pullback.

To see this, let f:ABf:A\rightarrowtail B be monic and g:ACg:A\to C any morphism, and let h:BPCh:B\to P C be the name of (f,g):AB×C(f,g):A\to B\times C, i.e. (f,g)(f,g) is the pullback CPC×C\in_C \rightarrowtail P C \times C along (h,1)(h,1). In other words, (k,l):XB×C(k,l):X\to B\times C factors through (f,g)(f,g) iff (hk,l)(h k,l) factors through C\in_C (i.e. l(x)hk(x)l(x) \in h k(x) for all x:Xx:X in the internal logic). This is in particular the case if hk={}lh k = \{\} \circ l (i.e. hk(x)={l(x)}h k(x) = \{l(x)\} for all x:Xx:X in the internal logic), which implies that the square

A g C f {} B h PC\array{A & \xrightarrow{g} & C \\ ^f\downarrow && \downarrow^{\{\}} \\ B & \xrightarrow{h} & P C }

is a pullback.

Now given a pushout

A g C f d B c D\array{A & \xrightarrow{g} & C \\ ^f\downarrow && \downarrow^{d} \\ B & \xrightarrow{c} & D }

with ff monic, with hh as above we have an induced m:DPCm:D \to P C by the universal property of the pushout, with md={}m d = \{\} and mc=hm c = h. Since {}\{\} is monic, dd must also be monic, and since the previous square is a pullback, so must this one be.

Via quasi-disjointness

A different proof applying to finite coproducts can be obtained by combining A1.5.14 and A1.6.2 of Johnstone. Define RR and SS to make the following squares pullbacks:

R r A s S r i A i A+B j B\array{ R & \xrightarrow{r} & A & \xleftarrow{s} & S\\ ^{r'}\downarrow && \downarrow^i && \downarrow\\ A & \xrightarrow{i} & A+B & \xleftarrow{j} & B}

Specifically, (r,r)(r,r') is the kernel pair of ii. In particular, there is an induced diagonal :AR\triangle : A \to R such that r=1 Ar \triangle = 1_A. On the other hand, since pullback preserves colimits, (r,s)(r,s) is a coproduct diagram. Thus, the pair of morphisms 1 R:RR1_R:R\to R and s:SR\triangle \circ s : S\to R factor (uniquely) through some h:ARh:A\to R, so that in particular hr=1 Rh r = 1_R. Thus, r:RAr:R\to A has both a left and a right inverse, so it is an isomorphism, and hence ii is monic. Dually, jj is monic.

Now we claim that any two morphisms f,g:SXf,g:S\to X with domain SS are equal. For the pair of morphisms RrAA+XR \xrightarrow{r} A \to A+X and SfXA+XS \xrightarrow{f} X \to A+X factor uniquely through AA (which, recall, is the coproduct R+SR+S). But since rr is an isomorphism, this factorization must be the left coprojection AA+XA\to A+X. Therefore, the composite SfXA+XS \xrightarrow{f} X \to A+X is equal to the composite SsAA+XS \xrightarrow{s} A \to A+X, and similarly so is the composite SgXA+XS \xrightarrow{g} X \to A+X. Since XA+XX\to A+X is monic by the previous paragraph, f=gf= g.

Finally, since 00 is a strict initial object, 0S0\to S is monic. And of course 1 S:SS1_S : S\to S is also monic, and these two monomorphisms are classified by two maps f,g:SΩf,g:S\to \Omega into the subobject classifier. By the previous paragraph, f=gf= g, hence S0S\cong 0 and is initial.

Via logical functors

Finally, we give a proof that applies constructively to arbitrary coproducts. This proof is due to Jibladze and can be found (in fibered-topos language) in Streicher, Appendix A. (Moens himself always just assumed that internal sums are stable and disjoint whereas Jibladze proved that for every fibered topos with internal sums these are actually stable and disjoint.)

Suppose \mathcal{E} a topos with JJ-indexed coproducts for all JJ belonging to some arity class κ\kappa. Then Δ: J\Delta : \mathcal{E} \to \mathcal{E}^J is a logical functor with a left adjoint J\coprod_J, so (by A2.3.8 of Johnstone, see also logical functor) to show that J\coprod_J induces equivalences J/{A j}/ jA j\mathcal{E}^J/\{A_j\} \to \mathcal{E}/\coprod_j A_j (which is one characterization of κ\kappa-extensivity) it suffices for J\coprod_J to be faithful. As with any adjunction, to show the left adjoint to be faithful it suffices to show that the unit η:IdΔ J\eta : Id \to \Delta \coprod_J is monic, which means in this case that the injections A j jA jA_j \to \coprod_j A_j are all monic.

Now since κ\kappa is an arity class, J×JJ\times J also belongs to it, and hence so do the fibers of the diagonal JJ×JJ\to J\times J. Thus, \mathcal{E} has coproducts indexed by the subsingletons determined by the equalities (j=k)(j=k) for any j,kJj,k\in J. Moreover, for any jj we can write A j= kJ (j=k)A kA_j = \coprod_{k\in J} \coprod_{(j=k)} A_{k}, and under this identification the injection A j kJA kA_j \to \coprod_{k\in J} A_{k} is obtained by applying the functor J\coprod_J to the evident family of maps (j=k)A kA k\coprod_{(j=k)} A_{k}\to A_k. But since J\coprod_J is the left adjoint of a logical functor, it preserves monomorphisms (see A2.4.8 of Johnstone, also logical functor). Thus, it suffices to prove that each (j=k)A kA k\coprod_{(j=k)} A_{k}\to A_k is monic.

Now, the functor (j=k): (j=k)\coprod_{(j=k)} : \mathcal{E}^{(j=k)} \to \mathcal{E} has a logical right adjoint sending BB\in\mathcal{E} to the subsingleton-indexed family {B} (j=k)\{B\}_{(j=k)}, and the units of its adjunction {A} (j=k){ (j=k)A} (j=k)\{A\}_{(j=k)} \to \{ \coprod_{(j=k)} A \}_{(j=k)} are isomorphisms (to define an inverse, it suffices to consider the object (j=k)A\coprod_{(j=k)} A under the assumption j=kj=k, in which case this object is isomorphic to AA). Thus, (j=k)\coprod_{(j=k)} is fully faithful, and in particular faithful, and since its right adjoint is also logical, it induces an equivalence (j=k)/ (j=k)1\mathcal{E}^{(j=k)} \simeq \mathcal{E}/\coprod_{(j=k)} 1.

However, the unit of a pullback adjunction /I\mathcal{E}/I \rightleftarrows \mathcal{E} is AA×IA\to A\times I, and if this is an isomorphism then in particular II×II\cong I\times I and thus II is subterminal. Moreover, in this case the counits of the adjunction are the projections A×IAA\times I \to A, which are pullbacks of the mono I1I\to 1 and therefore also monic. Finally, in our case where I= (j=k)1I = \coprod_{(j=k)} 1, the counit associated to A kA_k is precisely the map (j=k)A kA k\coprod_{(j=k)} A_{k} \to A_k that we wanted to prove to be monic.


Last revised on January 27, 2018 at 12:21:35. See the history of this page for a list of all contributions to it.