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


view this post on Zulip Morgan Rogers (he/him) (Jul 05 2021 at 16:00):

For any object XX in a topos, there is a canonical singleton map XΩXX \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 XX beforehand?
Another way of asking this is as follows: suppose I have an object YY; is there a way to reconstruct an XX such that Y=ΩXY = \Omega^X, if such an XX exists?

view this post on Zulip 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.

view this post on Zulip 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 YY here.

view this post on Zulip Fawzi Hreiki (Jul 05 2021 at 17:03):

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

view this post on Zulip Fawzi Hreiki (Jul 05 2021 at 17:03):

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

view this post on Zulip Fawzi Hreiki (Jul 05 2021 at 17:07):

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

view this post on Zulip 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.

view this post on Zulip Nathanael Arkor (Jul 05 2021 at 17:15):

Fawzi Hreiki said:

Given an object YY, the question of whether or not you can find an XX such that Y=PXY = \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?

view this post on Zulip 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).

view this post on Zulip Morgan Rogers (he/him) (Jul 05 2021 at 21:00):

Nathanael Arkor said:

Fawzi Hreiki said:

Given an object YY, the question of whether or not you can find an XX such that Y=PXY = \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 ΩX\Omega^X as a distributive lattice, we can identify XX 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 Hom(,ΩX)\mathrm{Hom}(-,\Omega^X) which sends ZZ to the union of the atoms in the lattice Hom(Z,ΩX)\mathrm{Hom}(Z,\Omega^X); is this functorial?

view this post on Zulip Morgan Rogers (he/him) (Jul 05 2021 at 21:07):

We would need to include the fact that ΩX\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.

view this post on Zulip 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?

view this post on Zulip Fawzi Hreiki (Jul 05 2021 at 22:30):

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

view this post on Zulip 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 Set\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.

view this post on Zulip Jens Hemelaer (Jul 06 2021 at 09:12):

The problem seems to be that, constructively, P(X)\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.

view this post on Zulip Jens Hemelaer (Jul 06 2021 at 09:14):

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

view this post on Zulip 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.

view this post on Zulip Matteo Capucci (he/him) (Jul 06 2021 at 09:28):

For any object XX in a topos, there is a canonical singleton map XΩXX \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 XX beforehand?
Another way of asking this is as follows: suppose I have an object YY; is there a way to reconstruct an XX such that Y=ΩXY = \Omega^X, if such an XX exists?

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

view this post on Zulip Matteo Capucci (he/him) (Jul 06 2021 at 09:28):

Mmh but I probably misunderstood your question

view this post on Zulip Matteo Capucci (he/him) (Jul 06 2021 at 09:29):

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

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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).

view this post on Zulip 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.

view this post on Zulip 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.