Power object ($PA={\Omega }^A$)

A power object $PA$ represents parameterized subobjects of $A$: $\mathcal{E}(X,PA)\cong \mathrm{Sub}(X\times A)$. In an elementary topos, it is ${\Omega }^A$, with the membership subobject supplied by evaluation at the subobject classifier.

An arrow $f:A\to B$ induces $Pf:PB\to PA$ by inverse image of predicates. Transposition of predicates on $A\times B$ gives $\mathcal{E}(A,PB)\cong \mathcal{E}(B,PA)$ and the adjunction $P^{\mathrm{op}}⊣P$. The induced monad on the topos is double power-object formation; it is distinct from the covariant powerset monad on sets.

The contravariant power-object functor of an elementary topos is monadic. Its double-power unit ${\eta }_A(a)(S)=(a\in S)$ is monic, which helps prove that $P$ reflects isomorphisms. Finite equalizers and the fact that power objects turn coreflexive equalizers into coequalizers give the remaining hypotheses of the crude monadicity theorem.

For a coreflexive pair $f,g:B\rightrightarrows A$ with equalizer $e:E\hookrightarrow B$, direct image along the mono $f$ satisfies $Pf{\exists }_f=1$ and $Pg{\exists }_f={\exists }_{e}Pe$. Thus any map $h:PB\to Z$ equalizing $Pf,Pg$ obeys $h=h{\exists }_{e}Pe$. Since $Pe{\exists }_e=1$, the map $Pe$ is their coequalizer. These identities hold for parameterized subobjects in any elementary topos.