nLab subset

Idea

A subset of a given set $A$ is a set $B$ that may be viewed as contained within $A$.

Definitions

In set theory

In material set theory, a subset of a set $A$ is a set $B$ with the property that

$$x \in B \;\Rightarrow\; x \in A$$

for any object $x$ whatsoever. One writes $B \subseteq A$ or $B \subset A$ (depending on the author) if $B$ has this property. Set theory's axiom of extensionality says that $A = B$ if (and only if) $A \subseteq B$ and $B \subseteq A$ (although this is only strong enough for well-founded set?s).

In structural foundations of mathematics, this definition doesn't make sense, because there is no global membership predicate $\in$ (and there may not be a global equality predicate either). Accordingly, we define a subset of $A$ to be a set $B$ with the structure of an injection

$$i\colon B \hookrightarrow A .$$

We can still define a local membership predicate $\in_A$ as follows: Given an element $x$ of $A$ and a subset $B$ (technically, $(B,i)$) of $A$,

(1)$$x \in_A B \;\Leftrightarrow\; \exists(y\colon B),\; x = i(y) .$$

Similarly, we can define a local containment predicate $\subseteq_A$ as follows: Given subsets $B$ and $C$ of $A$,

$$B \subseteq_A C \;\Leftrightarrow\; \forall(x\colon A),\; x \in B \;\Rightarrow\; x \in C .$$

We can also define a local equality predicate $=_A$ on subsets of $A$:

$$B =_A C \;\Leftrightarrow\; B \subseteq C \;\wedge\; C \subseteq B .$$

In foundations that already have a global equality predicate on sets (and functions between equal sets), this local equality predicate must be interpreted as an equivalence relation; then a subset of $A$ is technically an equivalence class of injections to $A$ rather than simply an injection to $A$.

In any case, if $A$ is a subset of $B$, then $B$ is a superset of $A$.

In type theory

In homotopy type theory, the inclusion relation between two types $A$ and $B$ is defined as

$$A \subseteq B \coloneqq \left[\sum_{f:A \to B} \prod_{b:B} \mathrm{isProp}\left(\sum_{a:A} f(a) = b\right)\right]$$

A subset of a set $B$ is a set $A$ with a term $p:A \subseteq B$.

Every subset $A$ of $B$ in a universe $\mathcal{U}$ comes with a choice of injection $i:A \hookrightarrow B$ if and only if the axiom of choice holds for sets in the universe:

$$\prod_{A:\mathrm{Set}_\mathcal{U}} \left[\sum_{f:A \to B} \prod_{b:B} \mathrm{isProp}\left(\sum_{a:A} f(a) = b\right)\right] \to \left[\sum_{g:\prod_{A:\mathrm{Set}_\mathcal{U}} A \to B} \prod_{A:\mathrm{Set}_\mathcal{U}} \prod_{b:B} \mathrm{isProp}\left(\sum_{a:A} g(A)(a) = b\right)\right]$$

As a result, subsets equipped with an injection are typically used when doing mathematics in homotopy type theory.

Remarks

As you can see from the right-hand sides of the above sequence of definitions, one usually suppresses the subscript $A$ from the notation. Even the right-hand side of (1) may use a local equality relation on elements of $A$. It may be necessary to distinguish $x\colon E$ (the typing declaration introducing a variable $x$ for an element of a given set $E$) from $x \in_A E$ (the proposition that a given element $x$ of a given set $A$ is a member of a given subset $E$ of $A$). Some authors may use $x \in A$ for either or both of these, trusting on context (particularly whether $x$ has been introduced before) to distinguish them. Another notational convenience is to suppress the injection $i$, writing $y$ instead of $i(y)$.

The concept of subset as it appears here generalises to subobject in category theory. To be precise, a subset of $A$ is exactly a subobject of $A$ when $A$ is thought of as an object of the category Set. The concept of superset then generalises to a notion of extension analogous to that of field extension.

When the abstract set $A$ is fixed, a subset $B$ of $A$ may be thought of as a concrete set.

Related concepts

• subtype

• cofinite subset

• saturated subset

• subspace

• causally closed subset

• space of finite subsets