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.
For any object in a topos, there is a canonical singleton map 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 beforehand?
Another way of asking this is as follows: suppose I have an object ; is there a way to reconstruct an such that , if such an exists?
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.
If it helps, as a starting point, I'm happy to assume that we have some ordering structure on here.
I'm not sure about the general singleton map, but if is a poset, then the object of order preserving maps from to is the free cocompletion of .
But this is just the Yoneda lemma for posets (except internalised to the topos)
Given an object , the question of whether or not you can find an such that seems in general intractable.
I recall reading somewhere that there are models of ZFC where the power set operation is not injective.
Fawzi Hreiki said:
Given an object , the question of whether or not you can find an such that 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?
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).
Nathanael Arkor said:
Fawzi Hreiki said:
Given an object , the question of whether or not you can find an such that 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 as a distributive lattice, we can identify 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 which sends to the union of the atoms in the lattice ; is this functorial?
We would need to include the fact that 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.
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?
The characterisation question is much easier than the extraction one. For example, in , complete atomic Boolean algebras are precisely the power sets.
Fawzi Hreiki said:
The characterisation question is much easier than the extraction one. For example, in , 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.
The problem seems to be that, constructively, 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.
Sometimes is called the "object of points" of . This seems to suggest that is the subobject of consisting of the "internal frame morphisms". But I would have to think about what this means concretely.
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.
For any object in a topos, there is a canonical singleton map 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 beforehand?
Another way of asking this is as follows: suppose I have an object ; is there a way to reconstruct an such that , if such an exists?
That map is the transpose of the equality predicate on . Maybe equality is more readily characterized? I used to know this stuff :sweat_smile:
Mmh but I probably misunderstood your question
You want to characterize those maps which happen to be isomorphic to the singleton mono?
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?
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.
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.
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).
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.
It's okay, I'll try constructing the adjoint/joins and see how that goes.