From: Thomas Streicher <streicher@mathematik.tu-darmstadt.de>
To: categories@mta.ca
Subject: generic families of finite sets in toposes with nno ?
Date: Tue, 24 Jul 2007 15:25:26 +0200 (CEST) [thread overview]
Message-ID: <E1IDLxG-0006Cv-VG@mailserv.mta.ca> (raw)
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
reply other threads:[~2007-07-24 13:25 UTC|newest]
Thread overview: [no followups] expand[flat|nested] mbox.gz Atom feed
Reply instructions:
You may reply publicly to this message via plain-text email
using any one of the following methods:
* Save the following mbox file, import it into your mail client,
and reply-to-all from there: mbox
Avoid top-posting and favor interleaved quoting:
https://en.wikipedia.org/wiki/Posting_style#Interleaved_style
* Reply using the --to, --cc, and --in-reply-to
switches of git-send-email(1):
git send-email \
--in-reply-to=E1IDLxG-0006Cv-VG@mailserv.mta.ca \
--to=streicher@mathematik.tu-darmstadt.de \
--cc=categories@mta.ca \
/path/to/YOUR_REPLY
https://kernel.org/pub/software/scm/git/docs/git-send-email.html
* If your mail client supports setting the In-Reply-To header
via mailto: links, try the mailto: link
Be sure your reply has a Subject: header at the top and a blank line
before the message body.
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for NNTP newsgroup(s).