extensive category in nLab

Context

Regular and Exact categories

Category Theory

• Idea
• Definitions
• Extensive categories
• Superextensive sites
• Pre-lextensive categories
• Examples
• Properties
• Related concepts
• References

Definition

A finitely extensive category (or finitary extensive category) is a category EE with finite coproducts such that one, and hence all, of the following equivalent conditions holds:

1. For any pair of objects a,ba, b the coproduct functor on slice categories is an equivalence of categories:

   (1)E /a×E /b →≃ E /(a⊔b) (X ↓ a),(Y ↓ b) ↦ (X⊔Y ↓ a⊔b) \array{ E_{/a} \,\times\, E_{/b} &\xrightarrow{\;\;\;\simeq\;\;\;}& E_{/(a \sqcup b)} \\ \left( \array{ X \\ \downarrow \\ a } \right) ,\; \left( \array{ Y \\ \downarrow \\ b } \right) &\mapsto& \left( \array{ X \sqcup Y \\ \downarrow \\ a \sqcup b } \right) }

   (e.g. Carboni, Lack & Walters 1993, Def. 2.1).

2. Pullbacks of finite-coproduct injections along arbitrary morphisms exist and finite coproducts are disjoint and stable under pullback.

   (e.g CLW93, Prop. 2.6, Lem. 2.11)

3. Pullbacks of finite-coproduct injections (and thus all coproduct injections) along arbitrary morphisms exist, and in any commutative diagram

   (2)x → z ← y ↓ ↓ ↓ a → a+b ← b \array{ x & \to & z & \leftarrow & y \\ \downarrow & & \downarrow & & \downarrow \\ a & \to & a+b & \leftarrow & b }

   the two squares are pullbacks if and only if the top row is a coproduct diagram

   (e.g. CLW93, Prop. 2.2).

4. Finite coproducts are van Kampen colimits. By definition, this is just to say that one of the previous two conditions holds.

Definition

An infinitary extensive category is a category EE with all (small) coproducts such that the following analogous equivalent conditions hold:

1. Pullbacks of coproduct injections along arbitrary morphisms exist

   and small coproducts are disjoint and stable under pullback.

2. For any small-indexed set (a i)(a_i) of objects, the coproduct functor of slice categories, generalizing (1), is an equivalence of categories:

   ∏i∈I(E /a i)⟶∼E /(∐ ia i). \underset{i \in I}{\prod} (E_{/a_i}) \overset{\sim}{\longrightarrow} E_{/(\coprod_i a_i)} \,.

3. Pullbacks of finite-coproduct injections (and thus all coproduct injections) along arbitrary morphisms exist, and for any family of commutative squares

   x i → z ↓ ↓ f a i → ∐ ia i\array{ x_i & \to & z \\\downarrow &&\downarrow^f \\ a_i & \to & \coprod_i a_i }

   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 z=∐ ix iz = \coprod_i x_i) if and only if all the squares are pullbacks.

4. All small coproducts are van Kampen colimits.

Definition

If an extensive category also has finite limits, it is called lextensive or disjunctive.

Proposition

(in extensive categories connected objects are primitive under coproduct)
An object XX in an extensive category 𝒞\mathcal{C} is a connected object (in that the hom-functor 𝒞(X,−):𝒞→Set\mathcal{C}(X,-) \,\colon\, \mathcal{C} \to Set preserves coproducts) if and only if in any coproduct decomposition X≃U+VX \simeq U + V, exactly one of UU, VV is not the initial object.

Proof

In one direction, assume that XX is connected and consider an isomorphism X→∼X 1⊔X 2X \xrightarrow{\sim} X_1 \sqcup X_2 to a coproduct. By assumption of connectedness, this morphism factors through one of the summands, say through X 1X_1, as shown in the bottom row of the following diagram:

Consider then the pullback of the total bottom morphism along the inclusion i 2i_2 of the other summand. Since pullbacks of isomorphisms are isomorphisms, the resulting top left object must be (isomorphic to) X 2X_2, as shown. On the other hand, by the pasting law this pullback factors into two pullback squares, as shown above. But the pullback on the right gives the initial object, since coproducts are disjoint in an extensive category (see above). This exhibits a morphisms X 2→∅X_2 \to \varnothing. But since the initial objects in extensive categories are strict initial objects, this must be an isomorphism, X 2≃∅X_2 \simeq \varnothing. By the same argument, X 1X_1 cannot be an initial object, since otherwise XX would be too, which it is not by assumption of connectedness (Rem. ). Hence we have shown that exactly one of the two summands in X≃X 1⊔X 2X \simeq X_1 \sqcup X_2 is initial.

In the other direction, assume that XX has non non-trivial coproduct decomposition and consider any morphism f:X→Y+Zf \colon X \to Y + Z into a coproduct. By extensivity, this implies (2) a coproduct decomposition X=U+VX = U + V with U≔f *(i Y)U \coloneqq f^\ast(i_Y) and V≔f *(i Z)V \coloneqq f^\ast(i_Z). But, by assumption, either UU or VV is initial, meaning that XX is isomorphic to either VV or UU, respectively, so that ff factors through either YY or XX, respectively. In other words, ff belongs to exactly one of the two subsets hom(X,Y)↪hom(X,Y+Z)\hom(X, Y) \hookrightarrow \hom(X, Y + Z) or hom(X,Z)↪hom(X,Y+Z)\hom(X, Z) \hookrightarrow \hom(X, Y + Z).