# Internal frame homomorphisms and sheafification

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$?

• Very interesting! Firstly, what you say in your second paragraph is definitely true. One needn't wave hands, waving the magic wand of the internal language is enough. :-) Secondly, I compared your construction with the one described at rawgit.com/iblech/internal-methods/master/notes.pdf#page=57 (Definition 6.8). I convinced myself that, at least assuming $X$ to be j-separated, there is a natural map from that construction to yours, and that this map admits a pre-inverse. I also sort-of convinced myself that your construction always yields a $j$-inverse. So the chances are good! May 30, 2018 at 19:56