From mboxrd@z Thu Jan 1 00:00:00 1970 X-Msuck: nntp://news.gmane.io/gmane.science.mathematics.categories/3836 Path: news.gmane.org!not-for-mail From: Thomas Streicher Newsgroups: gmane.science.mathematics.categories Subject: generic families of finite sets in toposes with nno ? Date: Tue, 24 Jul 2007 15:25:26 +0200 (CEST) Message-ID: NNTP-Posting-Host: main.gmane.org Mime-Version: 1.0 Content-Type: text/plain; charset=US-ASCII Content-Transfer-Encoding: 7bit X-Trace: ger.gmane.org 1241019553 10521 80.91.229.2 (29 Apr 2009 15:39:13 GMT) X-Complaints-To: usenet@ger.gmane.org NNTP-Posting-Date: Wed, 29 Apr 2009 15:39:13 +0000 (UTC) To: categories@mta.ca Original-X-From: rrosebru@mta.ca Tue Jul 24 12:14:27 2007 -0300 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Tue, 24 Jul 2007 12:14:27 -0300 Original-Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1IDLxG-0006Cv-VG for categories-list@mta.ca; Tue, 24 Jul 2007 12:05:43 -0300 Original-Sender: cat-dist@mta.ca Precedence: bulk X-Keywords: X-UID: 30 Original-Lines: 31 Xref: news.gmane.org gmane.science.mathematics.categories:3836 Archived-At: 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