Internal frame homomorphisms and sheafification

80 Views Asked by At

Let $\mathcal{E}$ be an elementary topos with subobject classifier $\Omega$, and let $j : \Omega \to \Omega$ be a Lawvere-Tierney topology. $\Omega$ is naturally seen as a frame object internal to $\mathcal{E}$, and the classified subobject $\Omega_j$ turns out to be (internally) a quotient frame of $\Omega$.

For any object $X \in \mathcal{E}$, one can define an object $\mathcal{Hom}_{\text{Frm}}(\Omega^X, \Omega) \in \mathcal{E}$ which (*waves hands*) internally parameterizes frame homomorphisms from $\Omega^X$ to $\Omega$. I think it should be possible to internalize the proof that discrete locales are spatial in order to prove that the evaluation map $X \to \mathcal{Hom}_{\text{Frm}}(\Omega^X, \Omega)$ is an isomorphism.

My question is, can we use this to cook up an alternative construction of the sheafification functor? Specifically, is the evaluation map $X \to \mathcal{Hom}_{\text{Frm}}({\Omega_j}^X, \Omega_j)$ naturally isomorphic to the unit $\eta : X \to a(X)$, where $a$ is the sheafification functor for $j$?