The *disjoint union* is a coproduct in Set, the category of sets.

In a general category coproducts need not have the expected disjointness property of those in Set. If they do they are called *disjoint coproducts*.

Given any family $(A_i)_{i:I}$ of sets, the (external) **disjoint union** $\biguplus_i A_i$ (also written $\sum_i A_i$, $\coprod_i A_i$, etc) of the family is the set of all (ordered) pairs $(i,a)$ with $i$ in the index set $I$ and $a$ in $A_i$.

As stated, the type of the second element of such a pair depends on the first element, which is natural in dependent type theory (see at *dependent sum type*) and no problem for material set theory, but it may be ill formed in a structural set theory or in some forms of type theory, especially those based on the internal language of topos theory. Alternatively, one may define $\biguplus_i A_i$ to be the set of those elements $x$ of the cartesian product $\prod_i \mathcal{P}A_i$ of the power sets such that there is exactly one index $j$ such that $x_j$ is inhabited and that $x_j$ is a singleton. If you're trying to be predicative too, then you may need to simply adopt the existence of disjoint unions as an axiom (the **axiom of disjoint unions**) in your foundations, stating the following facts about it.

There is a natural injection $A_j \to \biguplus_i A_i$ (mapping $a$ to $(j,a)$, or mapping $a$ to $(i \mapsto \{a \;|\; i = j\})$) for each index $j$. Conversely, for each element $x$ of $\biguplus_i A_i$, there is a unique index $j$ and such that $x$ is in the image of the injection from $A_j$. It is common to treat $A_j$ as a subset of $\biguplus_i A_i$; so if no confusion can result (in particular, when the notation for an element of $A_j$ always makes the ambient set clear), one often suppresses the index in the notation for an element of the disjoint union.

Given sets $A$ and $B$, the disjoint union of the binary family $(A,B)$ is written $A \uplus B$ (also $A + B$, $A \amalg B$, etc); its elements may be written (if care is needed) as $(0,a)$ and $(1,b)$, $(1,a)$ and $(2,b)$, $\iota{a}$ and $\kappa{b}$, and in many other styles.

Given sets $A_1$ through $A_n$, the disjoint union of the $n$-ary family $(A_1,\ldots,A_n)$ is written $\biguplus_{i=1}^n A_i$ (or similarly); its elements may be written (if care is needed) as $(i,a)$ for $1 \leq i \leq n$ and $a \in A_i$.

Given sets $A_1$, $A_2$, etc, the disjoint union of the countably infinitary family $(A_1,A_2,\ldots)$ is written $\biguplus_{i=1}^\infty A_i$ (or similarly); its elements may be written (if care is needed) as $(i,a)$ for $i$ a natural number and $a \in A_i$.

Given a set $A$, the disjoint union of the unary family $(A)$ may be identified with $A$ itself; that is, we identify $(i,a)$ for the unique index $i$ with $a$.

The disjoint union of the empty family $()$ is empty; it has no elements.

(This is internal in the sense of ‘internal direct sum’, not internalization. For that, just see coproduct.)

If a family $(A_i)_{i: I}$ of subsets of a given set $X$ are all pairwise disjoint (that is, $A_i \cap A_j$ has an element only if $i = j$, for any indices $i$ and $j$), then the union $\bigcup_i A_i$ is naturally bijective with the (external) disjoint union defined above. Conversely, given an external disjoint union $\biguplus_i A_i$, each $A_j$ may be identified with a subset of $\biguplus_i A_i$ (as explained above); these subsets are all pairwise disjoint, and their union is the entire disjoint union.

Accordingly, a union of pairwise disjoint subsets may be called an **internal disjoint union**. (Compare the internal vs external notions of direct sum.)

category: foundational axiom

Last revised on May 18, 2017 at 18:13:27. See the history of this page for a list of all contributions to it.