7
$\begingroup$

Without power sets in meta-theory not every Grothendieck topos is an elementary topos, Set is still Grothendieck, but it lacks power objects.

Now I am looking for a definition of a logical functor that does not mention power objects, that is as follows, if C and D are elementary topoi, then the definition of a logical functor between them coincides with the standard definition. But if they lack power objects the definition is still sensible, i.e. for a Grothendieck topos in a predicative meta-theory.

Motivation here is defining an atomic geometric morphism without requiring power objects in metatheory.

Improve this question
$\endgroup$
6
  • 1
    $\begingroup$ Maybe being a lex and cartesian closed functor $F\colon E_1\to E_2$, hence preserving monomorphisms, and the induced map of preorders $Sub_{E_1}(X)\to Sub_{E_2}(F(X))$ is an equivalence, for every object $X$ of $E_1$? $\endgroup$
    – David Roberts ♦
    Commented Mar 6 at 11:33
  • 1
    $\begingroup$ @DavidRoberts I don't think that latter condition is strong enough: if subobject classifiers do exist, does it imply that $F$ preserves them? $\endgroup$
    – Mike Shulman
    Commented Mar 19 at 20:25
  • $\begingroup$ @MikeShulman hmm. I didn't check. But your answer is a nice compromise $\endgroup$
    – David Roberts ♦
    Commented Mar 19 at 23:29
  • $\begingroup$ @MikeShulman suppose the functor $F^{op}\colon E_1^{op} \to E_2^{op}$ forms a 2-commutative triangle with the subobject functors $Sub_{E_i}\colon E_i^{op} \to \mathbf{Preord}$ (so I should have said the equivalence is natural in my first comment). Or to be cleaner, look at the poset reflection, and then assume that both subobject functors are representable. Then $F$ preserves subobject classifiers, no? $\endgroup$
    – David Roberts ♦
    Commented Mar 20 at 7:21
  • $\begingroup$ @DavidRoberts I don't think so; I think all you can get from that argument is that a right adjoint of $F$, if it has one, preserves subobject classifiers, as in my answer. $\endgroup$
    – Mike Shulman
    Commented Mar 20 at 18:17

1 Answer 1

Reset to default
6
$\begingroup$

I don't know of a notion of "logical functor" between predicative topoi that specializes automatically to the standard notion if they happen to be elementary topoi. But I do know a definition of "logical functor with a left adjoint" that has this property, and this is sufficient for the purpose of defining atomic geometric morphisms, since a logical functor between elementary topoi has a left adjoint if and only if it has a right adjoint, so it is equivalent to say that $f^* \dashv f_*$ is atomic if $f^*$ is a "logical functor with a left adjoint".

The definition is: if $F:C\to D$ has a left adjoint $L:D\to C$, then $F$ is logical if and only if $L$ (not $F$!) induces isomorphisms of subobject lattices $\mathrm{Sub}_D(X) \cong \mathrm{Sub}_C(LX)$. The fact that this is equivalent to logicality of $F$ follows from the Yoneda lemma: we have

$$\mathrm{Sub}_D(X) \cong D(X,\Omega_D)$$

and

$$\mathrm{Sub}_C(LX) \cong C(LX, \Omega_C) \cong D(X,F\Omega_C)$$

both naturally. Thus, the left-hand sides are naturally isomorphic if and only if the right-hand sides are, and the latter is equivalent to $\Omega_D \cong F\Omega_C$ by the Yoneda lemma.

In this blog post I used this characterization to suggest a notion of "$\infty$-atomic geometric morphism" between $(\infty,1)$-topoi.

Improve this answer
$\endgroup$

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .