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: deprecated: topos theory

Topic: power objects up to internal equivalence

Tobias Fritz (Aug 08 2021 at 06:55):

Given a finitely complete category $\mathcal{C}$, a power object for $A \in \mathcal{C}$ is an object $PA$ which represents the presheaf $\mathsf{Sub}(A \times -)$. Unfolding this definition via the Yoneda lemma gives the equivalent definition of a power object: it comes equipped with a distinguished monomorphism $\in \, \subseteq A \times PA$ satisfying the usual property.

I've just come across the following slightly weaker notion of power object, and I wonder if this has been considered before. I'm also looking for examples that would not be power objects in the usual sense.

Note first that every $\mathsf{Sub}(X)$ is actually a partially ordered set; in fact, if we care about this poset only up to equivalence of preorders, then there is no need to define a subobject of $X$ as an isomorphism class of monomorphisms into $X$, and we may just as well do the simpler thing of defining $\mathsf{Sub}(X)$ as the collection of all monomorphisms into $X$, which makes it into a preordered (large) set with preorder given as usual with respect to factorization. My point is only to indicate that I care about $\mathsf{Sub}(X)$ only up to equivalence of preordered sets.

Now let's say that a poweroid object for $A$ is an internally preordered object $(PA,\le)$, by which I mean that $\le \hookrightarrow PA \times PA$ is reflexive and transitive, which represents the subobject functor in the sense that there is a (pseudo)natural equivalence
$\qquad \qquad \mathcal{C}(-,PA) \cong \mathsf{Sub}(A \times -),$
where the left-hand side is also a preordered set in the obvious way.

I can show that a power object is the same thing as a poweroid object for which $\le$ is internally antisymmetric (though I should double-check the proof). Now here are my questions:

• Is there an object $A$ in a finitely complete category which has a poweroid object but no power object? The obvious guess is that such a thing must exist, but finding an example seems to be quite tricky. I think that it will have to live in a finitely complete category that is not exact. Any ideas?

• What are poweroid objects really called, and where can I read about them?

Mike Shulman (Aug 08 2021 at 16:24):

I don't have a complete answer, but one thing to note is that the notion of poweroid object uniquely determines the relation $\le$, while if $\mathcal{C}$ is a Heyting category this relation can be constructed. Thus, in a Heyting category, a poweroid object is just a plain object $PA$ together with a natural transformation $\mathcal{C}(-,PA) \to \mathsf{Sub}(A\times -)$ that is pointwise essentially surjective; we can then use this to define $\le$ making $PA$ an internal preorder. Thus, a poweroid object in a Heyting category is equivalently a "generic subobject of $A$", where "generic" is used in the sense of "classifying up to existence but not uniqueness" — every subobject of $A\times B$ is classified, up to isomorphism, by some map $B\to PA$, but not necessarily a unique one.

Mike Shulman (Aug 08 2021 at 16:27):

Relatedly, a tripos is a first-order hyperdoctrine (i.e. a fibration of Heyting algebras with simple indexed products and coproducts) that has "generic predicates" in a sense that generalizes poweroid objects. Put differently, a Heyting category has all poweroid objects if and only if its subobject fibration is a tripos.

Mike Shulman (Aug 08 2021 at 16:31):

This emphasizes the connection to exactness: the category of PERs in a tripos is a topos, so the ex/reg completion of a category with poweroid objects will have power objects.

Mike Shulman (Aug 08 2021 at 16:54):

It also suggests one possible source of categories with poweroid objects: start with a tripos and do half of the tripos-to-topos construction. I haven't checked that this works, but my guess would be that if you start with a tripos and split only the coreflexive morphisms in its bicategory of relations, you would get a category with poweroid objects. For instance, you could investigate categories of assemblies.

Tobias Fritz (Aug 08 2021 at 17:46):

Excellent, thank you! I still need to understand why that is true, but the comment on $\le$ being automatic in a Heyting category if essential surjectivity holds looks like a crucial hint. Based on that, it seems plausible that I'll be able to make my original idea work, which was to consider the category of countable simple graphs (where simple means that adjacency is and irreflexive and symmetric relation). I had suspected that the single-vertex graph may have a poweroid object in this category, and with your hint the Rado graph starts to look like an excellent candidate for it. More generally, saturated structures may be good candidates for poweroid objects in categories of models where power objects do not exist.

Triposes and assemblies sound intriguing as well, but I'll start with structures more within my comfort zone. I'll report back here as soon as I have something definite.

Tobias Fritz (Aug 09 2021 at 07:08):

I think that the category of pairs of sets $(A,S)$ with $S \subseteq A$ will do it, with morphisms $(A,S) \to (B,T)$ given by the obvious $f : A \to B$ satisfying $f(S) \subseteq T$. I believe that this is a Heyting category that is not a topos, but still has poweroid objects: first, by Mike's criterion there is a poweroid object $P1$ that represents $\mathsf{Sub}(-)$ up to equivalence; the pair $(5,3)$ seems to do the trick by reasoning similar to the construction of the subobject classifier in the arrow category $\mathsf{Set}^\to$. Second, one can then use cartesian closure to construct general poweroid objects as $PA := (P1)^A$.

Does this all sound about right? I haven't been very careful with checking the details yet. (And can it be generalized to the analogously defined category of pairs in any topos?)

Tobias Fritz (Aug 09 2021 at 07:10):

Would anyone want to see the theory of poweroid objects and some example like this worked out and written up in some detail? I'm using it as an example in another project, but I wonder if it could be of some interest on its own. (Although I'd still be surprised if it was new.)

Morgan Rogers (he/him) (Aug 09 2021 at 08:15):

What motivated you to look at this concept in the first place? I would be curious to hear about that!

Tobias Fritz (Aug 09 2021 at 08:34):

I'm dabbling a bit with formal category theory, and in particular with Koudenburg's definition of presheaf objects for objects in proarrow equipments (Definition 5.2 in the link, which applies more generally in Koudenburg's augmented virtual double categories, of which proarrow equipments are a special case). My main motivation for this is that I have a characterization of presheaf objects which specializes in many different interesting ways: instiated in $\mathsf{Cat}$, it reproduces Bunge's theorem characterizing presheaf categories; in $\mathcal{V}-\mathsf{Cat}$ it should produce a similar enriched version of it; and hopefully it can also reproduce Gabriel-Ulmer duality when instantiated on a suitable virtual proarrow equipment involving finitely complete categories, but I haven't worked this out yet.

In order to have a relatively low-brow example, I was wondering what presheaf objects are when one instantiates Koudenburg's definition in the proarrow equipment of internal relations $\mathsf{Rel}(\mathsf{C})$ in a finitely complete category $\mathsf{C}$. It turns out to produce precisely the definition of poweroid object that I gave above (if I've done this right). This made me wonder if one could show that presheaf objects exist in $\mathsf{Rel}(\mathsf{C})$ if and only if $\mathsf{C}$ is a topos. But this seems to be wrong, since the class of finitely complete categories with poweroid objects is apparently strictly larger.

Morgan Rogers (he/him) (Aug 09 2021 at 08:51):

Seeing the necessary conditions on a category to produce a presheaf object would certainly be interesting! :grinning_face_with_smiling_eyes:

Mike Shulman (Aug 09 2021 at 17:09):

@Tobias Fritz Note that your category of pairs is the category of separated objects for a Lawvere-Tierney topology on the topos $\rm Set^{\to}$. In particular, it is a quasitopos, so it has a strong-subobject classifier (namely $(2,2)$). On the other hand there is also the actual subobject classifier of the ambient topos, "$(2,3)$", which is not separated. I think your observation is that there's a strong epimorphism $(5,3) \to (2,3)$ (actually wouldn't $(3,3)$ work as well?) and that your category satisfies an axiom of choice with respect to this strong epi. Does that seem right? If so, it seems unlikely to generalize to other toposes, since having this axiom of choice seems likely to depend on the ordinary axiom of choice, or at least the law of excluded middle, in Set.

Tobias Fritz (Aug 10 2021 at 06:32):

Those are good points about the category being a quasitopos and already $(3,3)$ (rather than $(5,3)$) being a model for $P1$. I'm not sure about choice, but I definitely use excluded middle in the proof (in the form of subobject complementation).

In any case, I think I have enough material to include it in my draft (a category with finite limits and poweroid objects is not necessarily a topos, and there's a concrete example), assuming that you don't mind me including some of your observations (with attribution).

Mike Shulman (Aug 10 2021 at 13:09):

Of course not.

Mike Shulman (Aug 10 2021 at 13:09):

By the way, what led you to think first of (5,3)? Why 5 rather than 3, 4, 6, ...?

Tobias Fritz (Aug 10 2021 at 13:59):

Not sure if it's interesting, but my "5" arose out of thinking that for an object $(A,S)$ and a specified subobject of it, there are 5 cases that can occur for every element of $A$ concerning whether and how it is contained in $S$ and in the subobject. In other words, I still had distinguished the elements of $S$ from the elements of $A \setminus S$ explicitly, which as you've pointed out is not neccessary.

fosco (Aug 10 2021 at 16:09):

hopefully it can also reproduce Gabriel-Ulmer duality when instantiated on a suitable virtual proarrow equipment involving finitely complete categories, but I haven't worked this out yet.

@Ivan Di Liberti and I have thought for quite some time, a long time ago, about this. At some point, @Nathanael Arkor joined us and we started again. I'll try to say something meaningful about this thread.

Tobias Fritz (Aug 10 2021 at 18:02):

Looking forward to hearing about it! I know about your paper Accessibility and presentability in 2-categories, which seems closely related, though I have to admit that I still need to give it a detailed read.