regular category = unary regular
coherent category = finitary regular
geometric category = infinitary regular
A category is extensive if it has coproducts that interact well with pullbacks. Variations (some only terminological) include lextensive, disjunctive, and positive categories. All of these come in finitary and infinitary versions (and, more generally, -ary versions for any arity class ).
An finitely extensive category (or finitary extensive category) is a category with finite coproducts such that one, and hence all, of the following equivalent conditions holds:
the two squares are pullbacks if and only if the top row is a coproduct diagram.
An infinitary extensive category is a category with all (small) coproducts such that the following analogous equivalent conditions hold:
in which the bottom family of morphisms is the coproduct injections and the right-hand morphism is always the same, the top family are the injections of a coproduct diagram (hence ) if and only if all the squares are pullbacks.
In between, a -ary extensive category (for a cardinal number or an arity class) is one with disjoint and stable coproducts of fewer than objects. The unqualified term extensive category can refer to either the finitary or infinitary version, depending on the author; the more usual meaning is the finitary version.
Extensive categories are also called positive categories, especially if they are also coherent. Note that any disjoint coproduct in a coherent category is automatically pullback-stable. A positive coherent category which is also exact is called a pretopos. Infinitary pretoposes encapsulate all the exactness conditions of Giraud’s theorem characterizing Grothendieck toposes (the remaining condition is the existence of a small generating set).
If an extensive category also has finite limits, it is called lextensive or disjunctive. (Note that the more usual default meaning of ‘disjunctive’, unlike the other terms, is the infinitary case.)
The alternative definitions of finitary disjunctive refer only to binary coproducts, but they obviously imply analogous statements for -ary coproducts for all finite . Less obviously, they also imply the analogous statement for -ary coproducts (that is, initial objects). In this case, the statement is that the initial object 0 is strict (any map is an isomorphism).
Furthermore, if binary coproducts are disjoint, then (at least assuming classical logic) any infinitary coproducts that exist are also disjoint, since
for any . Therefore, if a finitary-extensive category has infinitary pullback-stable coproducts, it is necessarily infinitary-extensive. In particular, a cocomplete locally cartesian closed category is finitary extensive if and only if it is infinitary extensive. Thus, for instance, any cocomplete elementary topos is infinitary extensive.
A quasitopos with disjoint coproducts, or more generally a locally cartesian closed category with disjoint coproducts, is extensive. (Of course not all quasitoposes have disjoint coproducts, one example being a complete Heyting algebra.)
The category of schemes is infinitary lextensive. In more detail: the category of functors is infinitary lextensive (since finite limits and small coproducts are computed pointwise in ), then sheaves with respect to the Zariski topology on form an infinitary lextensive category (since finite limits and small coproducts are reflected back from by applying a left exact reflection to the inclusion of sheaves in presheaves). Finally, the category of schemes, as a full subcategory of the Zariski sheaves, are closed under finite limits and small coproducts. (Some discussion of these points can be found at the nForum, particularly in comment #18.)
The category of affine schemes (opposite to the category of commutative rings with identity) is lextensive, but (perhaps contrary to geometric intuition) not infinitary lextensive. Some details may be found here.
The category Cat is infinitary lextensive.
Any extensive category admits a Grothendieck topology whose covering families are (generated by) the families of inclusions into a coproduct (finite or small, as appropriate). We call this the extensive coverage or extensive topology. The codomain fibration of any extensive category is a stack for its extensive topology.
In general, we call a site superextensive if its underlying category is extensive, its covering families are generated by (finite or small) families, and its coverage includes the extensive one. See superextensive site for more details.
Extensivity is an “exactness” condition, analogous to being a exact category or a pretopos (a pretopos being precisely a category that is exact and finitary-extensive). The corresponding “regularity” condition analogous to being a regular category or a coherent category is not well-known, but is not hard to write down.
Let us say (without making any assertion that this is good or permanent terminology) that a category is pre-lextensive if
This is intended to complete the table of analogies:
|regular category||exact category|
|pre-lextensive category||lextensive category|
Regular/exact categories have quotients of (some) congruences. Exact categories have quotients of all congruences, while regular ones have quotients only of congruences that are kernel pairs. Another way to say that is that in a regular category, you can conclude that the quotient of some congruence exists if you can exhibit another object of which the quotient would be a subobject if it existed. Similarly, pre-/lextensive categories have disjoint unions. Lextensive categories have all disjoint unions (= coproducts), while in a pre-lextensive category you can conclude that a pair of objects have a disjoint union if you can exhibit another object in which and can be embedded disjointly. Finally, coherent categories/pretoposes have both quotients and disjoint unions, or equivalently quotients and not-necessarily-disjoint unions, with the same sort of relationship between the two.
Evidently a pre-lextensive category is lextensive as soon as any two objects can be embedded disjointly in a third. Pre-lextensive categories also suffice for the interpretation of disjunctive logic.
Being pre-lextensive is also sufficient to define the extensive topology and show that it is subcanonical, since it implies that whatever disjoint coproducts exist must be pullback-stable. The codomain fibration of a pre-lextensive category is not necessarily a stack for its extensive topology, but this condition is weaker than extensivity. It is true, however, that if is a pre-lextensive category whose codomain fibration is a stack for its extensive topology, and in which the disjoint coproduct exists, then is extensive, for arbitrary disjoint (binary) coproducts can then be obtained by descent along the covering family .
Carboni, Aurelio and Lack, Stephen and Walters, R. F. C., Introduction to extensive and distributive categories, JPAA 84 no. 2
While creating this page, we had the following discussion regarding “finitely” versus “infinitary.”
Can we say ‘small-extensive’? Or even redefine ‘extensive’ to have this meaning, using ‘finitely extensive’ for the first version? —Toby
I think “extensive” is pretty well established for the finite version, and I would be reluctant to try to change it. I wouldn’t object too much to “small-extensive” for the infinitary version in principle, but -positive is used in the Elephant and possibly elsewhere. I think the topos theorists think by analogy with -pretopos, which I don’t think we have much hope of changing, despite the unfortunate clash with “-topos.” But you can use “finitary disjunctive” and “disjunctive” in the lex case, which most examples are. -Mike
Mike: Okay, I just ran across one paper that uses “(infinitary) extensive” for the infinitary version the first time it was introduced, and then dropped the parenthetical for the rest of the paper. I also recall seeing “extensive fibration” used for a fibration having disjoint and stable indexed coproducts, which is certainly a (potentially) infinitary notion. So perhaps there is no real consensus on whether “extensive” definitely implies the finite version or the infinitary one.
Toby: It would be nice to not overload the prefix ‘-’ so much. It's like ‘continuous’; default to small.
Mike: I agree that it would be nice to avoid -. What if we do what we did for omega-category? That is, if you want to be unambiguous, say either “finitary extensive” or “infinitary extensive,” and in any particular context you are allowed to define “extensive” at the beginning to be one of the two and use it without prefix in what follows.
Toby: Sure. Of course, the general concept is -extensive, where is any cardinal (which we may assume to be regular).