How can I prove $\mathbf{1}_{Pa}=P\{\cdot\}_a\circ\{\cdot\}_{Pa}$

We have an elementary topos $$\mathbf{C}$$ with subobject classifier $$\Omega$$ and powerset functor $$P:\mathbf{C}^{op}\to\mathbf{C}$$, i.e, for all $$\mathbf{C}$$-objects $$x,y$$ we have $$\mathbf{C}(x\times y,\Omega)\cong\mathbf{C}(y,Px)$$ and the bijection is natural in both variables. There are "canonical" morphisms $$\{\cdot\}_a:a\longrightarrow Pa$$ for every object $$a$$. In $$\mathbf{Set}$$, given a set $$X$$, the map $$\{\cdot\}_X$$ maps the element $$x\in X$$ to the subset $$\{x\}\subseteq X$$ i.e the element $$\{x\}\in PX$$.

Every map $$f:x\to x'$$ transforms to a map $$Pf:Px'\to Px$$ by contravariance, so we have

$$a\xrightarrow{\quad\{\cdot\}_a\quad}Pa\xrightarrow{\quad\{\cdot\}_{Pa}\quad}PPa$$ $$Pa\xleftarrow{\quad P\{\cdot\}_a\quad}PPa$$

and this begs the question: is $$P\{\cdot\}_a\circ\{\cdot\}_{Pa}$$ the identity on $$Pa$$? And is $$\{\cdot\}_{Pa}\circ P\{\cdot\}_a$$ the identity on $$PPa$$?

I would like an "elementary" proof (that doesn't use adjoints or dinatural transformations or weird existence theorems). I've tried almost everything that comes to mind (writing down the diagrams takes too much time). If a dinatural transformation is unavoidable, then I don't mind it, but not adjoints by any means.

The ultimate goal of this is to prove that $$\in_a(f\times \mathbf{1}_{Pa})=\in_{x}(\mathbf{1}_x\times Pf)$$ for any objects $$a,x$$ and map $$f:x\to a$$. The arow $$\in_x:x\times Px\to\Omega$$ is given by the ismorphism above. All of this is outlined in Sheaves in Geometry and Logic: A First Introduction to Topos Theory by Mac Lane and Moerdijk.

Thanks!

• There is no hope for both $P\{.\}\circ \{.\}_{Pa}$ and $\{.\}_{Pa}\circ P\{.\}_a$ to be identities, or $Pa\cong PPa$, which is not true in the category of sets, or for that matter in any nontrivial topos (the magic name is "Cantor"). This said, there's something you can say without "weird existence theorems" (lol?) for example, $\{.\}_a$ is a monomorphism. Any chance that $P\{.\}_a$ is one of its left inverses? Jan 18, 2021 at 21:50
• @Fosco I only expect $P\{.\}_a\circ\{.}_{Pa}$ to be the identity, but who knows. In Set everything works. Any idea how to prove it in any topos? Jan 18, 2021 at 21:59
• In the category of sets, the functor $P\{.\}$ sends a subset $\cal U$ of $PA$ to its union $\bigcup \cal U$, so yes, it is true; in a generic topos one has to argue with a universal property, unfortunately :) Jan 19, 2021 at 10:58
• By "elementary", would you be excluding a Yoneda lemma style argument (which is what I would go for, after an argument based on the internal language of a topos which I would suppose would be even more excluded)? i.e. that argument would be to trace through the equivalences to see what both sides do to a subobject of $U \times a$ given a test object $U$. Jan 19, 2021 at 20:57

No, even in $$\mathbf{Set}$$, neither composition is the identity in general. First, if $$a$$ is a set, then for $$S \in Pa$$, $$\{\cdot\}_{Pa}$$ would send $$S \mapsto \{ S \}$$. Then, $$P\{\cdot\}_a ( \{ S \} ) = \{ b \in a \mid \{ b \} \in \{ S \} \} = \{ b \in a \mid \{ b \} = S \}.$$ Therefore, if $$S$$ has two or more elements, then $$P\{\cdot\}_a \circ \{\cdot\}_{Pa}$$ sends $$S \mapsto \emptyset$$. Thus $$P\{\cdot\}_a \circ \{\cdot\}_{Pa} \ne \mathbf{1}_{Pa}$$.
(I think in fact, it should be possible to prove in a general topos that $$P\{\cdot\}_a \circ \{\cdot\}_{Pa} = \mathbf{1}_{Pa}$$ if and only if $$a$$ is a subobject of 1, i.e. if and only if the unique morphism $$a \to 1$$ is a monomorphism. Any proof I can think of, however, would probably not qualify as being "elementary". For a nontrivial example where this condition can be satisfied: in the category of sheaves on a topological space $$X$$, the subobjects of 1 are exactly $$h_U$$ for open $$U \subseteq X$$ -- where by definition $$h_U(V) = \begin{cases}1, & V \subseteq U; \\ 0, & V \not\subseteq U.\end{cases}$$ Or, if you don't believe that the base universe satisfies excluded middle, then in general $$h_U(V) = (\mathcal{T}_X)(V, U) = \{ x \in 1 \mid V \subseteq U \}$$ where in the middle term we're using the partial order category on the collection of open subsets of $$X$$.)
As for the other composition, $$\{\cdot\}_{Pa}$$ is certainly never surjective (for instance $$\emptyset$$ is never in the image), so it is impossible to have $$\{\cdot\}_{Pa} \circ P\{\cdot\}_a = \mathbf{1}_{PPa}$$.
As for the ultimate question of how to show $${\in}_a(f \times \mathbf{1}_{Pa}) = {\in}_x(\mathbf{1}_x \times Pf)$$ for $$f \in \mathbf{C}(x, a)$$: as much as you don't want to use bifunctors, I don't see any way around using the naturality of the isomorphism of bifunctors $$\mathbf{C}(x \times y, \Omega) \simeq \mathbf{C}(y, Px)$$. If we let $$\Phi$$ be this isomorphism, then expanding the definitions, this naturality says exactly that for $$f \in \mathbf{C}(x, x')$$ and $$g \in \mathbf{C}(y, y')$$, and $$h \in \mathbf{C}(x' \times y', \Omega)$$, we have: $$\Phi_{x,y}(h \circ (f \times g)) = Pf \circ \Phi_{x',y'}(h) \circ g.$$ Now, by definition of $${\in}_a$$, we have that $$\Phi_{a,Pa}({\in}_a) = \mathbf{1}_{Pa}$$ and similarly for $${\in}_x$$. Therefore, $$\Phi({\in}_a \circ (f \times \mathbf{1}_{Pa})) = Pf \circ \mathbf{1}_{Pa} \circ \mathbf{1}_{Pa} = Pf.$$ Similarly, $$\Phi({\in}_x \circ (\mathbf{1}_x \times Pf)) = P\mathbf{1}_x \circ \mathbf{1}_{Px} \circ Pf = Pf.$$ Since $$\Phi$$ is an isomorphism, and $$\Phi$$ of both sides of the desired identity evaluates to the same thing, we conclude that the desired identity is true.