nLab subset




A subset of a given set AA is a set BB that may be viewed as contained within AA.


In set theory

In material set theory, a subset of a set AA is a set BB with the property that

xBxA x \in B \;\Rightarrow\; x \in A

for any object xx whatsoever. One writes BAB \subseteq A or BAB \subset A (depending on the author) if BB has this property. Set theory's axiom of extensionality says that A=BA = B if (and only if) ABA \subseteq B and BAB \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 AA to be a set BB with the structure of an injection

i:BA. i\colon B \hookrightarrow A .

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

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

Similarly, we can define a local containment predicate A\subseteq_A as follows: Given subsets BB and CC of AA,

B AC(x:A),xBxC. 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=_A on subsets of AA:

B= ACBCCB. 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 AA is technically an equivalence class of injections to AA rather than simply an injection to AA.

In any case, if AA is a subset of BB, then BB is a superset of AA.

In type theory

In homotopy type theory, the inclusion relation between two types AA and BB is defined as

AB[ f:AB b:BisProp( a:Af(a)=b)]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 BB is a set AA with a term p:ABp:A \subseteq B.

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

A:Set 𝒰[ f:AB b:BisProp( a:Af(a)=b)][ g: A:Set 𝒰AB A:Set 𝒰 b:BisProp( a:Ag(A)(a)=b)]\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.


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

The concept of subset as it appears here generalises to subobject in category theory. To be precise, a subset of AA is exactly a subobject of AA when AA 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 AA is fixed, a subset BB of AA may be thought of as a concrete set.

Last revised on May 26, 2022 at 19:46:41. See the history of this page for a list of all contributions to it.