Alternative definition of power object in a category

Question

The standard definition of a power object seems to be: objects $\mathcal{P}X, K \in \mathbf{C}$ and a monic $\in: K \hookrightarrow X \times \mathcal{P}X$ such that for every monic $r: A \hookrightarrow X \times B$, there is a unique morphism $\chi_r: B \to \mathcal{P}X$ such that $r$ is the pullback of $\in$ along $\mathrm{id}_X \times \chi_r$ (e.g. here).

I'm struggling to see how this faithfully captures the notion of a power set. Intuitively, this idea should be captured by a natural isomorphism between subobjects/monics $r: A \hookrightarrow X$ and elements $1 \to \mathcal{P}X$. Which would lead to a definition such as the following:

Alternative definition: a power object of $X \in \mathbf{C}$ is objects $\mathcal{P}X, K \in \mathbf{C}$ and a monic $\in: K \hookrightarrow X \times \mathcal{P}X$ such that for every monic $r: A \hookrightarrow X$, there is a map $\bar{r}: 1 \to \mathcal{P}X$ such that $r \times \bar{r}: A \to X \times \mathcal{P}X$ factors through $\in$, and is universal for this property.

Intuitively, if $r$ represents the inclusion of a subset $A \subseteq X$, then $\bar{r}$ is the inclusion of $\{ A \}$ into $\mathcal{P}X$. $r \times \bar{r}$ factors through $\in$ since all elements of $A$ are elements of $A$, and $A$ is the universal set with this property.

Is this an equivalent definition? Is it equivalent under some assumptions, such as existence of finite limits/colimits?

Answer 1

Let's first consider the analogous case of the exponential object $Y^X$. You might want to give an "alternative" definition that an exponential object should be an object $Y^X$ together with an evaluation map $\text{eval} : Y^X \times X \to Y$ such that for every morphism $f : X \to Y$ there is a point $r : 1 \to Y^X$ such that the composite

$$X \xrightarrow{r \times \text{id}_X} Y^X \times X \xrightarrow{\text{eval}} Y$$

is equal to $f$, and $Y^X$ is universal with this property.

The problem is that this is not actually a universal property! I've only talked about how morphisms from a point into $Y^X$ behave. To actually define an object universally we have to describe the entire functor $\text{Hom}(-, Y^X)$ it represents; among other things this guarantees uniqueness by the Yoneda lemma. As it stands I have no idea if an object defined as above is unique.

The way we do this, which gives the standard definition of the exponential object, is to say that we want morphisms $B \to Y^X$ to correspond to morphisms $B \times X \to Y$, which we think of as $B$-parameterized families of morphisms $X \to Y$. This is a genuine universal property in the sense of specifying a representable functor and so we have the usual Yoneda uniqueness up to unique isomorphism.

In particular we get the evaluation map for free from this universal property; it's not necessary to specify it in advance. Taking $B = Y^X$, the evaluation map is the map corresponding via the universal property to the identity map $Y^X \to Y^X$; in other words, it's the universal family of morphisms $X \to Y$, parameterized tautologically by the exponential object itself. So we see that already in the evaluation map we were naturally considering a parameterized family of morphisms and not just a single morphism.

The discussion for power objects can now be done completely analogously. We ask what we want morphisms $B \to PX$ to correspond to and the answer is $B$-parameterized families of subobjects of $X$, which means monomorphisms into $B \times X$, and this is a perfectly fine universal property. Again taking $B = PX$ itself we get a monomorphism $\in : K \hookrightarrow PX \times X$ which now reveals itself to be the universal family of subobjects of $X$, so we again see that already we were naturally considering a parameterized family.