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: singleton morphism

Morgan Rogers (he/him) (Jul 05 2021 at 16:00):

For any object $X$ in a topos, there is a canonical singleton map $X \to \Omega^X$ which is the analogue of the mapping of elements to their singleton subsets in the category of sets. Does this map have a universal property that doesn't rely on knowing $X$ beforehand?
Another way of asking this is as follows: suppose I have an object $Y$; is there a way to reconstruct an $X$ such that $Y = \Omega^X$, if such an $X$ exists?

Morgan Rogers (he/him) (Jul 05 2021 at 16:14):

The singleton mapping is a monomorphism (see Corollary A2.2.3 in the Elephant), so the above amounts to identifying what the properties of this "special subobject" should be.

Morgan Rogers (he/him) (Jul 05 2021 at 16:19):

If it helps, as a starting point, I'm happy to assume that we have some ordering structure on $Y$ here.

Fawzi Hreiki (Jul 05 2021 at 17:03):

I'm not sure about the general singleton map, but if $X$ is a poset, then the object of order preserving maps from $X^\text{op}$ to $\Omega$ is the free cocompletion of $X$.

Fawzi Hreiki (Jul 05 2021 at 17:03):

But this is just the Yoneda lemma for posets (except internalised to the topos)

Fawzi Hreiki (Jul 05 2021 at 17:07):

Given an object $Y$, the question of whether or not you can find an $X$ such that $Y = \mathcal{P}X$ seems in general intractable.

Fawzi Hreiki (Jul 05 2021 at 17:10):

I recall reading somewhere that there are models of ZFC where the power set operation is not injective.

Nathanael Arkor (Jul 05 2021 at 17:15):

Fawzi Hreiki said:

Given an object $Y$, the question of whether or not you can find an $X$ such that $Y = \mathcal{P}X$ seems in general intractable.

If this is the internal Yoneda lemma, might it be possible to use an (internal version of the) characterisation of presheaf categories as cocomplete atomic categories to answer this question?

Fawzi Hreiki (Jul 05 2021 at 17:58):

I think you need to consider structured objects and structure preserving maps for that to work (for some kind of structure, e.g. category objects).

Morgan Rogers (he/him) (Jul 05 2021 at 21:00):

Nathanael Arkor said:

Fawzi Hreiki said:

Given an object $Y$, the question of whether or not you can find an $X$ such that $Y = \mathcal{P}X$ seems in general intractable.

If this is the internal Yoneda lemma, might it be possible to use an (internal version of the) characterisation of presheaf categories as cocomplete atomic categories to answer this question?

This sounds like an outdated use of the term "atom" for "tiny object".
That concept seems promising, at least initially: in Set, if we take $\Omega^X$ as a distributive lattice, we can identify $X$ with the union of the atoms in that lattice. But I don't immediately see how to abstract this: I would need a notion of "generalized atom". One idea would be to make it representable: attempt to construct the subpresheaf of the representable $\mathrm{Hom}(-,\Omega^X)$ which sends $Z$ to the union of the atoms in the lattice $\mathrm{Hom}(Z,\Omega^X)$; is this functorial?

Morgan Rogers (he/him) (Jul 05 2021 at 21:07):

We would need to include the fact that $\Omega^X$ is a complete lattice for this to work, I suppose, which is not ideal for my intended application of this characterization.
Fawzi Hreiki said:

I think you need to consider structured objects and structure preserving maps for that to work (for some kind of structure, e.g. category objects).

A sufficiently flexible Stone-type duality would probably do, even a posetal one. I'll look into that.

Fawzi Hreiki (Jul 05 2021 at 22:29):

Do you only care about characterising when an object is a power object or also about extracting the (or some) object which it is a power object of?

Fawzi Hreiki (Jul 05 2021 at 22:30):

The characterisation question is much easier than the extraction one. For example, in $\text{Set}$, complete atomic Boolean algebras are precisely the power sets.

Morgan Rogers (he/him) (Jul 06 2021 at 05:59):

Fawzi Hreiki said:

The characterisation question is much easier than the extraction one. For example, in $\text{Set}$, complete atomic Boolean algebras are precisely the power sets.

Wait, are you claiming that isn't constructive? You can just take the set of atoms in a CABA to recover a set isomorphic to the one being exponentiated. My problem is working out what the equivalent process should be in a not-necessarily-Boolean setting.

Jens Hemelaer (Jul 06 2021 at 09:12):

The problem seems to be that, constructively, $\mathcal{P}(X)$ does not have to be a boolean algebra.

Some background is given on this nLab page. On this page, CABA is not used as an abbreviation of complete atomic boolean algebra, but is defined to be something else.

Jens Hemelaer (Jul 06 2021 at 09:14):

Sometimes $X$ is called the "object of points" of $\Omega^X$. This seems to suggest that $X$ is the subobject of $\Omega^{(\Omega^X)}$ consisting of the "internal frame morphisms". But I would have to think about what this means concretely.

Morgan Rogers (he/him) (Jul 06 2021 at 09:22):

Jens Hemelaer said:

Some background is given on this nLab page. On this page, CABA is not used as an abbreviation of complete atomic boolean algebra, but is defined to be something else.

Since I'm in the middle of arguing about naming conventions elsewhere, I want to put out there that this is a terrible naming convention, which fortunately does not seem to have become standard.

Matteo Capucci (he/him) (Jul 06 2021 at 09:28):

For any object $X$ in a topos, there is a canonical singleton map $X \to \Omega^X$ which is the analogue of the mapping of elements to their singleton subsets in the category of sets. Does this map have a universal property that doesn't rely on knowing $X$ beforehand?
Another way of asking this is as follows: suppose I have an object $Y$; is there a way to reconstruct an $X$ such that $Y = \Omega^X$, if such an $X$ exists?

That map is the transpose of the equality predicate on $X$. Maybe equality is more readily characterized? I used to know this stuff :sweat_smile:

Matteo Capucci (he/him) (Jul 06 2021 at 09:28):

Mmh but I probably misunderstood your question

Matteo Capucci (he/him) (Jul 06 2021 at 09:29):

You want to characterize those maps $A \to B$ which happen to be isomorphic to the singleton mono?

Fawzi Hreiki (Jul 06 2021 at 09:49):

No. The question is (as I understand it) given some (possibly structured) object in a topos, can we know when it’s a power object?

Fawzi Hreiki (Jul 06 2021 at 09:51):

The same way we can pick out power set posets as the complete atomic Boolean algebras and we can pick out presheaf categories as the cocomplete atomic categories.

Graham Manuell (Jul 06 2021 at 11:48):

If we are allowed to remember the order structure isn't this trivial? There also isn't any problem with doing it constructively. If Y is a poset, then it is isomorphic to the powerset of a set X if and only if Y is a frame corresponding to a discrete locale and X is isomorphic to its set of points. We just need an intrinsic definition of when a locale is discrete and one exists: a locale is discrete if the unique map to the terminal locale and the diagonal are both open.

Morgan Rogers (he/him) (Jul 06 2021 at 12:05):

Graham Manuell said:

If we are allowed to remember the order structure isn't this trivial? [proceeds to give non-trivial characterization]

Okay, good point! With all of the order structure, it's certainly possible. Here's my problem: I'm constructing an object which I know should be such a locale. However, the construction I'm working with is only guaranteed to produce a distributive lattice; it's constructed from the images of frames/locales under an inverse image functor, and such functors aren't guaranteed to preserve completeness/infinite joins.
If I have a distributive lattice, I can tell it's a frame because the depleted Yoneda embedding into its ideal completion will have a left adjoint. So I was wondering whether it might be possible to avoid constructing that adjoint (to show it's a locale and then a discrete locale) by instead constructing a subobject with a suitable universal property (going smaller rather than bigger).

Graham Manuell (Jul 06 2021 at 14:29):

Lol. Fair. I should have instead said that it follows easily from Stone duality.

I can't immediately think of a characterisation that avoids checking it has arbitrary joins.

Morgan Rogers (he/him) (Jul 06 2021 at 14:48):

It's okay, I'll try constructing the adjoint/joins and see how that goes.