# Definition of $\in_c$ for power objects

On the nLab page for power objects, the object $$\in_c$$ is defined as the domain of a monomorphism $$\in_c\hookrightarrow c\times\Omega^c$$, and it is mentioned at the end of the article that in any topos we have that the power object of an arbitrary object is (isomorphic to) its exponential with the subobject classifier.

It is also mentioned that in the case $$c\cong{\bf 1}$$ the power object becomes a subobject classifier. This is easy to see considering the diagram

in the case $$c\cong{\bf 1}$$ since $${\bf1}\times\Omega^{\bf1}\cong\Omega$$ and $${\bf 1}\times d\cong d$$, which means that $$\in_{\bf 1}\cong{\bf 1}$$ with the mono in question being 'true' $$\top:{\bf 1}\to \Omega$$, $$\chi_m:d\to\Omega$$ the characteristic function of $$r$$, and the top of the square being $$!:r\to{\bf 1}$$.

I'm trying to understand the object $$\in_c$$ when $$c\ncong{\bf 1}$$, both in $${\bf Sets}$$ and more generally in any topos. I've tried 'fusing' the universal properties of an exponential and a subobject classifier to produce $$\in_c$$, but it is unclear how the domain of $$\top$$ changes to yield something besides $${\bf 1}$$ -- it seems like the monomorphism $$\in_c\hookrightarrow c\times\Omega^c$$ is perhaps a currying of some sort?

For a more precise version of the question:

Let $$\mathcal{C}$$ be a closed category with finite limits and a subobject classifier. How can we define $$\in_c$$ for an arbitrary $$c\in{\bf Ob}_\mathcal{C}$$ using just the above structure, and what set is $$\in_c$$ in the case $$\mathcal{C}={\bf Sets}$$?

For $$C=\mathbf{Set}$$, then $$\in_c \subset c \times \Omega^c$$ is literally the relation $$\in$$. That is, $$\in_c = \{ (x,U) \in x \times \Omega^c \mid x\in U \}$$

Other than that, you can take $$\in_c$$ to be defined by its universal property.

On the other hand, if you have cartesian closedness (which you didn't ask for in the precise question), then the monomorphism $$\in_c \to c\times \Omega^c$$ is classified by a map $$c \times \Omega^c \to \Omega$$ classifying $$\in_c$$, which corresponds to the identity map $$\mathrm{id}_{\Omega^c}\colon \Omega^c \to \Omega^c$$ using cartesian closedness. So to unwind, the following maps determine each other uniquely in a finitely complete cartesian closed category with subobject classifier:

• $$\mathrm{id}_{\Omega^c}$$,
• $$c \times \Omega^c \to \Omega$$
• $$\in_c := \left(c \times \Omega^c\right)\times_\Omega 1 \hookrightarrow c \times \Omega^c$$
• This is just what I was looking for, thank you. But for the cartesian closed bit, doesn’t closed with all finite limits imply cartesian closed? – Alec Rhea Dec 10 '18 at 6:49
• I'm not sure what you mean by 'closed': with respect to which monoidal product? If it's the cartesian product, this is just cartesian closed with all finite limits. – David Roberts Dec 10 '18 at 7:03
• (And by 'this' I mean "closed with all finite limits" as you say in your comment) – David Roberts Dec 10 '18 at 10:08
• @AlecRhea Being closed as at ncatlab.org/nlab/show/closed+category is extra structure on a category; it's sort of dual to imposing a monoidal structure. Just as a monoidal structure need not be cartesian, a closed structure need not correspond to the cartesian monoidal structure. For instance, take any closed monoidal category with finite limits, like the category of abelian groups with its tensor product, and forget about the monoidal structure: then you have a closed category with finite limits that's not cartesian closed. – Mike Shulman Dec 10 '18 at 18:23
• You could assert axioms on a closed structure ensuring that it corresponds to the cartesian monoidal structure, but it's easier just to say that the cartesian product has a right adjoint as in the usual definition of "cartesian closed category". – Mike Shulman Dec 10 '18 at 18:24