CatDat

extensive

A category C\C is extensive when it has finite coproducts (denoted ++) and for all objects A,BCA,B \in \C the coproduct functor C/A×C/BC/(A+B),\C/A \times \C/B \to \C/(A+B), which maps (XA,YB)(X \to A, Y \to B) to (X+YA+B)(X+Y \to A+B), is an equivalence of categories. This is equivalent to the following three conditions:

  1. Pullbacks along binary coproduct inclusions exist, i.e. for every morphism TA+BT \to A + B, the pullback T×A+BAT \times_{A + B} A exists.
  2. Binary coproducts are disjoint: The coproduct inclusions AA+BBA \rightarrow A + B \leftarrow B are monomorphisms, and their pullback A×A+BBA \times_{A + B} B is the initial object 00.
  3. Binary coproducts are stable under pullbacks: For every morphism TA+BT \to A + B, if we define the pullbacks TAT×A+BAT_A \coloneqq T \times_{A + B} A and TBT×A+BBT_B \coloneqq T \times_{A + B} B, then the canonical morphism TA+TBTT_A + T_B \to T is an isomorphism.
For a proof of this equivalent characterization, see Section 2 in Introduction to extensive and distributive categories by Carboni-Lack-Walters.

Relevant implications

Examples

There are 28 categories with this property.

Counterexamples

There are 69 categories without this property.

Unknown

There are 0 categories for which the database has no information on whether they satisfy this property.