Power sets

(0,1)-category

(0,1)-topos

# Power sets

## Definition

Given a set $S$, the power set of $S$ is the set $\mathcal{P}S$ of all subsets of $S$. Equivalently, it is

• the set $\TV^S$ of all functions from $S$ to the set $\TV$ of truth values. This is often written $2^S$, since there are (at least in classical logic) exactly $2$ truth values;

• the collection of subobjects of $X$ in the topos Set.

• the slice category $Inj/S$, where Inj is the wide subcategory of Set with morphisms restricted to injections. This is similar to the subobject definition but is more unpacked. $Inj/S$ has objects that are injections to $S$ and morphisms that are commuting triangles of injections.

## Foundational status

One generally needs a specific axiom in the foundations of mathematics to ensure the existence of power sets. In material set theory, this can be phrased as follows:

• If $S$ is a set, then there exists a set $\mathcal{P}$ such that $A \in \mathcal{P}$ if $A \subseteq S$.

One can then use the axiom of separation (bounded separation is enough) to prove that $\mathcal{P}$ may be chosen so that the subsets of $A$ are the only members of $\mathcal{P}$; the axiom of extensionality proves that this $\mathcal{P}$ is unique.

Alternatively, one could include a powerset structure, a primitive unary operator $\mathcal{P}(S)$ such that for all sets $S$, if for all sets $A$ and sets $B$, $B \in A$ implies that $B \in S$, then $A \in \mathcal{P}(S)$.

In structural set theory, we state rather that there exists a set $\mathcal{P}$ which indexes the subsets of $A$ and prove uniqueness up to unique isomorphism.

In predicative mathematics, the existence of power sets (along with other “impredicative” axioms) is not accepted. However we can still speak of a power set as a proper class, sometimes called a power class.

One can use power sets to construct function sets; the converse also works using excluded middle (or anything else that will guarantee the existence of the set of truth values). In particular, power sets exist in any theory containing excluded middle and function sets; thus predicative theories which include function sets must also be constructive.

### In dependent type theory

In dependent type theory, if one has a univalent type of all propositions $(\mathrm{Prop}, \mathrm{El})$, then given a type $S$, the power set of $S$ is the function type $\mathcal{P}S \coloneqq S \to \mathrm{Prop}$. The power set of a type is always a set, because $\mathrm{Prop}$ is always a set by univalence; and if the codomain of a function type is a set, then the function type itself is a set.

An element of a power set $P:\mathcal{P}S$ is a predicate. The type

$\sum_{x:S} \mathrm{El}(P(x))$

is the corresponding subtype of $S$, with canonical embedding given by the first projection function defined in the elimination rules of the negative dependent sum type.

$\pi_1:\left(\sum_{x:S} \mathrm{El}(P(x))\right) \to S$

There is also a local membership relation $(-)\in_S(-):\mathcal{P}(S \times \mathcal{P}S)$ defined by $a \in_S B \coloneqq B(a)$ for all $a:S$ and $B:\mathcal{P}S$, where $B(a)$ is defined in the elimination rules for function types.

## Properties

### Power set functor

The power set construction gives rise to two functors, the contravariant power set functor $Set^op \to Set$ and the covariant power set functor $Set \to Set$. The first sends a function $f\colon S\to T$ to the preimage function $f^*\colon P(T) \to P(S)$, whereas the second sends $f$ to the image function $f_*\colon P(S) \to P(T)$.

Last revised on May 3, 2023 at 15:19:35. See the history of this page for a list of all contributions to it.