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.
dusko (May 01 2020 at 07:40):sarahzrf said:
(btw, im pretty sure the anthropic principle doesnt have anything to do with free will, it's more like "of course we're gonna observe a bunch of phenomena that allow human life to exist, because otherwise we wouldn't be here to observe the lack of those phenomena")
i hope you don't mind that i just entered your name into duckduck, and it took me to to the mathoverflow page where you ask "How much of the Cantor-Schröder-Bernstein theorem is constructively recoverable if the injections have retractions and decidable images?".
PROPOSITION. A topos is boolean if and only if it satisfies
(CSB*) if f:A->B and g:B->A are monics
then there is an iso h:A->B
such that for every x in A holds
h(x) = f(x) or h(x) = g^{-1}(x)
PROOF of the "if" part: Let X be a subobject of Y. We use (CSB*) to
construct its complement. Define
A = YxN
B = X+(YxN)
(where N is the object of natural numbers). Let f:A-->B be the
inclusion, and g:B-->A the unique arrow which maps X into the first
copy of Y in A, while it takes the copies of Y contained in B into the
second one, the third one and so on. (Formally, g is defined using the
universal property of coproducts, and the structure of N.) It is clear
that both f and g are monics.
By (CSB*), there is a bijection h:A-->B with h(x)=f(x) or
h(x)=g^{-1}(x). This means that the union of
C = {z | h(z)=f(z)} and
D = {z | h(z)=g^{-1}(z)}
covers A. On the other hand, the definitions of f and g imply that C
and D are disjoint. So they are complements in A. By pulling back C and D
along the inclusion of Y iso Yx{0} in A, we get two complementary
subobjects of Y. The claim is now that the intersection (pullback) X'
of D and Yx{0} is isomorphic to X -- so that the intersection of C and
Yx{0} yields the complement of X in Y.
First of all, each element <y,n> of D must surely be in the image of
g. Thus, if <y,0> is in D, then y must be in X. So X' is contained in
Xx{0}. The other way around, since h(C) is contained in f(C), the
intersection in B of X and h(C) must be empty. Therefore, X must be
contained in h(D): indeed, h is an iso, and the direct images h(C) and
h(D) must be complementary in B. But h(D) is contained in
g^{-1}(D). So X is in g^{-1}(D), i.e. g(X) is in D. Hence, Xx{0}=g(X)
is contained in X'.
[it is from here: https://www.mta.ca/~cat-dist/archive/1994/94-2]
dusko (May 01 2020 at 07:43):dusko said:
sarahzrf said:
(btw, im pretty sure the anthropic principle doesnt have anything to do with free will, it's more like "of course we're gonna observe a bunch of phenomena that allow human life to exist, because otherwise we wouldn't be here to observe the lack of those phenomena")
i hope you don't mind that i just entered your name into duckduck, and it took me to to the mathoverflow page where you ask "How much of the Cantor-Schröder-Bernstein theorem is constructively recoverable if the injections have retractions and decidable images?".
PROPOSITION. A topos is boolean if and only if it satisfies
(CSB*) if f:A->B and g:B->A are monics
then there is an iso h:A->B
such that for every x in A holds
h(x) = f(x) or h(x) = g^{-1}(x)PROOF of the "if" part: Let X be a subobject of Y. We use (CSB*) to
construct its complement. Define
A = YxN
B = X+(YxN)(where N is the object of natural numbers). Let f:A-->B be the
inclusion, and g:B-->A the unique arrow which maps X into the first
copy of Y in A, while it takes the copies of Y contained in B into the
second one, the third one and so on. (Formally, g is defined using the
universal property of coproducts, and the structure of N.) It is clear
that both f and g are monics.By (CSB*), there is a bijection h:A-->B with h(x)=f(x) or
h(x)=g^{-1}(x). This means that the union of
C = {z | h(z)=f(z)} and
D = {z | h(z)=g^{-1}(z)}
covers A. On the other hand, the definitions of f and g imply that C
and D are disjoint. So they are complements in A. By pulling back C and D
along the inclusion of Y iso Yx{0} in A, we get two complementary
subobjects of Y. The claim is now that the intersection (pullback) X'
of D and Yx{0} is isomorphic to X -- so that the intersection of C and
Yx{0} yields the complement of X in Y.First of all, each element <y,n> of D must surely be in the image of
g. Thus, if <y,0> is in D, then y must be in X. So X' is contained in
Xx{0}. The other way around, since h(C) is contained in f(C), the
intersection in B of X and h(C) must be empty. Therefore, X must be
contained in h(D): indeed, h is an iso, and the direct images h(C) and
h(D) must be complementary in B. But h(D) is contained in
g^{-1}(D). So X is in g^{-1}(D), i.e. g(X) is in D. Hence, Xx{0}=g(X)
is contained in X'.[it is from here: https://www.mta.ca/~cat-dist/archive/1994/94-2]
if you want to look at a constructive version of CSB, decidability does not seem to help, but if you assume that your the two sets, injected into one another, are totally ordered, like for instance programs of some programming languages, then the CSB becomes hartley rogers' theorem that every two acceptable enumerations are isomorphic.
sarahzrf (May 01 2020 at 07:43):you're going over stuff that's already covered in the MO thread in question :sweat_smile:
sarahzrf (May 01 2020 at 07:44):well, the "topos is boolean" stuff is not quite the same as what is covered there, but it's also not what i was asking about
dusko (May 01 2020 at 07:46):sarahzrf said:
you're going over stuff that's already covered in the MO thread in question :sweat_smile:
i thought that you might be interested that it was covered in 1994, at a mailing list, with a 30 line proof, which is still simpler than the corollary in your MO thread.
sarahzrf (May 01 2020 at 07:46):also if you're searching me you should know that there's apparently another sarahzrf (maybe more than one?) on the internet
sarahzrf (May 01 2020 at 07:46):which corollary?
sarahzrf (May 01 2020 at 07:47):oh
sarahzrf (May 01 2020 at 07:48):i mean i complained about that answer too :p
sarahzrf (May 01 2020 at 07:48):it's not really dealing with what i was asking
dusko (May 01 2020 at 07:48):the question was settled at MO by a corollary from a recent publication. i thought that you might be interested that there was a simpler proof, which no one though worth publishing.
sarahzrf (May 01 2020 at 07:48):no, the answer i accepted was a different one
sarahzrf (May 01 2020 at 07:49):in fact the accepted answer's citation is from 1968, if we're competing for older proofs for some reason :shrug:
dusko (May 01 2020 at 07:50):i addressed the original question that you asked in the post after the proof. did you read the proof through? did you click at the link at the bottom? some people when they ask a question tend to be interested in the answer. i am sorry about all this. take care.
sarahzrf (May 01 2020 at 07:51):i didn't read the proof, sorry—i looked at the theorem statement and recognized it as something i knew before posting the question
sarahzrf (May 01 2020 at 07:52):if you read the question you'll see that i'm specifically asking about the case where there are retractions and the images are decidable
sarahzrf (May 01 2020 at 07:53):My impression is that the inability to invert an arbitrary function is ordinarily the biggest obstacle in Cantor-Schröder-Bernstein, so I'm interested in knowing what difficulties are left if you skip over that issue by fiat.
sarahzrf (May 01 2020 at 08:00):yeah—i've now read the beginning of the proof & one of the two monics involved has a decidable image iff the subobject you start with is decidable
Todd Trimble (May 01 2020 at 15:11):"A topos is boolean if and only if it satisfies (CSB*)"
FWIW (and as indicated in your proof), you must mean a topos with NNO. Otherwise, is a non-Boolean topos in which CSB holds (since endomonos in are isos). Anyway, nice proof!
Todd Trimble (May 01 2020 at 15:19):For what interest it may have, this was published in 2019.
sarahzrf (May 01 2020 at 19:17):and we've come full circle :D
sarahzrf (May 01 2020 at 19:18):that's the thing cited in the MO thread which dusko was replying to
Todd Trimble (May 01 2020 at 19:54):Well, I do see now that Andrej Bauer points to that paper in his answer (I missed it before by not scrolling past your question and dusko's answer), but if that's what dusko was "replying to", then it was easy to miss. The only possible reference to Andrej's answer I see would have to be the indirect allusion "if we go back even further".
In other words: gimme a break!
sarahzrf (May 01 2020 at 21:03):okay yeah to be fair it also took me a minute to figure out what dusko was referring to (i ctrl+f'd "corollary" on the MO page, it was a reference to that paper)
dusko (May 02 2020 at 06:32):i posted the link above, but it seems that nobody noticed it. i copied and pasted from an email exchange from 1994:
https://www.mta.ca/~cat-dist/archive/1994/94-2
i did not state all conditions or the context, because i posted the link.
(=_=) (May 02 2020 at 07:48):dusko said:
i posted the link above, but it seems that nobody noticed it. i copied and pasted from an email exchange from 1994:
https://www.mta.ca/~cat-dist/archive/1994/94-2
i did not state all conditions or the context, because i posted the link.
At least on my desktop interface, Zulip makes it very difficult to read long comments. I had to "Quote and Reply" to see the full text and discover the link at the very end of your comment.
I don't use the mobile version, so I don't know about the experience on other devices. My workaround is to comment with shorter paragraphs.
David Michael Roberts (May 04 2020 at 01:48):@dusko I took the liberty of copying in the proof onto MathOverflow to save people a click, and in case the categories archive ever evaporates (like the more recent and more substantial archive not in this format).
sarahzrf (May 04 2020 at 01:48):the question it answers isn't the one i was asking, though >_<
David Michael Roberts (May 04 2020 at 01:49):@sarahzrf that may be, but it's additional context and history and content, that someone might find useful, regardless of the specific hypotheses.
David Michael Roberts (May 04 2020 at 01:49):Also, I like having the scholarly record better preserved :-)
dusko (May 04 2020 at 05:00):Rongmin Lu said:
dusko said:
i posted the link above, but it seems that nobody noticed it. i copied and pasted from an email exchange from 1994:
https://www.mta.ca/~cat-dist/archive/1994/94-2
i did not state all conditions or the context, because i posted the link.At least on my desktop interface, Zulip makes it very difficult to read long comments. I had to "Quote and Reply" to see the full text and discover the link at the very end of your comment.
I don't use the mobile version, so I don't know about the experience on other devices. My workaround is to comment with shorter paragraphs.
sorry. i had no idea. thanks for telling me.
dusko (May 05 2020 at 03:49):David Michael Roberts said:
dusko I took the liberty of copying in the proof onto MathOverflow to save people a click, and in case the categories archive ever evaporates (like the more recent and more substantial archive not in this format).
thanks. i first pasted it there, then i remembered "hyperlinks are like procedure calls"; then i got here and thought "people here prefer to stay within the conversation" and pasted it. "goto considered harmful" :)
Valeria de Paiva (May 24 2020 at 14:52):David Michael Roberts said:
dusko I took the liberty of copying in the proof onto MathOverflow to save people a click, and in case the categories archive ever evaporates (like the more recent and more substantial archive not in this format).
hi, which category theory archive are you talking about here? Hypatia? does anyone know if a copy was preserved?