Category Theory
Zulip Server
Archive

You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.

Stream: theory: category theory

Topic: Proof that locales gives a separating family in topoi

Fernando Yamauti (Oct 29 2025 at 10:28):

Hi. Does anyone know perhaps a proof of the following fact without using any specific construction of a covering of effective descent given by a localic topos?

Statement. The functor $\mathbf{Topos} \to \widehat{\mathbf{Loc}}$ given by $\mathcal{X} \mapsto {h_{\mathcal{X}}}_{| \mathbf{Loc}}$, i.e., Yoneda and then restriction, is fully faithful.

Perhaps there's a tricky way using some property about models of geometric theories in locales...?

Jens Hemelaer (Oct 29 2025 at 18:49):

Some ideas:

You can decompose a topos into locale slices: for each object $X$ in the topos $\mathcal{E}$ you can write $L_X$ for the localic reflection of $\mathcal{E}/X$ (its opens correspond to the subobjects of $X$). There is a geometric morphism
$i_X : L_X \to \mathcal{E}$
for each $X$. The pullback $i_X^*$ restricts a sheaf to the frame of subobjects of $X$.

The family of the $i_X$'s is jointly surjective: if there are two objects $F$ and $G$ in $\mathcal{E}$ and $i_X^*F \cong i_X^*G$ for each $X$ then $F \cong G$.

Now for two geometric morphisms $\phi,\psi: \mathcal{E} \to \mathcal{E'}$ you can similarly show that $\phi \cong \psi$ as soon as $\phi\circ i_X \cong \psi\circ i_X$ for all objects $X$.

Jens Hemelaer (Oct 29 2025 at 19:30):

Ok, this doesn't seem to work... there is no geometric morphism $i_X$ in general the way I described it.