generic families of finite sets in toposes with nno ?
I have the following question about finite objects in toposes with nno where with ``finite'' I mean K-finite and with decidable equality. It is well known that in every topos EE with nno N there exists a family k : K -> N of finite sets such that for every family a : A -> I of finite sets there exists an epi e : I ->> J and a map f : J -> N such that e^*a \cong f^*k. Such a map k one may call a ``weakly generic family of finite sets''. I would like to know whether there always exists a family \pi : E -> U of finite sets which is "generic" in the sense that for every family a : A -> I of finite sets there exists an f : I -> U with f^*k' \cong a. Already for Psh(G) with G a nontrivial finite group one cannot take the usual weakly generic map k = \succ \circ \add : N x N -> N because the representable object G = y(*) is finite but not isomorphic to n^*k for some n : 1 -> N. However, for arbitrary small cats C such a map \pi : E -> U exist: take for U(I) the set of presheaves on C/I valued in FinSet_iso and where u operates by precomposing with (C/u)^\op. E(I) consists of pairs (F,x) where F is in U(I) and x \in F(\id_I). (This is a variation of a construction in my paper "Universes in Toposes" pp.9-10 albeit with FinSet instead of a Groth.universe). However, it is not clear to me for the case of sheaf toposes. In realizability toposes I think the usual k = \succ \circ \add : N x N -> N does work. Anyway, I would like to know if anyone has considered the problem and whether there is a "logical" (i.e. in the internal language) construction of a generic family family \pi : E -> U for every topos with nno. Thomas Streicher
participants (1)
-
Thomas Streicher