TL;DR
This paper characterizes toposes that can be generated by objects which are internally finite and decidable, linking these properties to topological conditions and providing a constructive classification.
Contribution
It provides a constructive characterization of toposes generated by cardinal finite objects using topological and localic conditions, extending previous results.
Findings
A hyperconnected separated locally decidable topos admits a generating family of cardinal finite objects.
A topos is generated by cardinal finite objects iff it is separated, locally decidable, and its localic reflection is zero dimensional.
The main theorem generalizes the characterization to arbitrary toposes via their localic reflection.
Abstract
We give a characterizations of toposes which admit a generating family of objects which are internally cardinal finite (i.e. Kuratowski finite and decidable) in terms of "topological" conditions. The central result is that, constructively, a hyperconnected separated locally decidable topos admit a generating family of cardinal finite objects. The main theorem is then a generalization obtained as an application of this result internally in the localic reflection of an arbitrary topos: a topos is generated by cardinal finite objects if and only if it is separated, locally decidable, and its localic reflection is zero dimensional.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.