Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
I wrote Cantor-Schroeder-Bernstein theorem.
Thanks!
Spurred by a MO question, I added a simple example to Cantor-Schroeder-Bernstein theorem that shows CSB fails in the arrow category .
I moved your example one section down where the counterexamples outside of live.
I don’t know that I fully agree with your decision (and I also don’t know the intended scope of “”). The basic idea I had wanted to get across here is that the theorem fails in constructive set theory, and constructive set theory can be interpreted in Grothendieck toposes. “Other categories” starts off talking about non-toposes.
The same thing happens a lot throughout the nLab: an axiom is introduced as an axiom on sets or , see for example WISC or COSHEP. But then the axiom is explored largely through examples which I guess you (Toby) would not call “”, for example judiciously chosen Grothendieck toposes. (Very often I mentally substitute “any base topos” when I see an axiom introduced this way.) Anyway, I’ll bet this way of introducing an axiom is confusing to many readers; it mildly confuses me for example. Probably this needs to be discussed.
Edit: I wound up just inserting another subsection, “Failure in toposes”, followed by the two examples. “Other categories” now refers to decidedly non-set-like categories like , as it should in spirit. Also, under “Naming”, I added the observation that Dedekind actually proved the theorem in 1887.
Constructive set theory is different from topos theory. I had no idea that was supposed to say anything about constructive set theory, although it's clear enough now that you added the note that the isomorphism can't exist internally either.
The section ## Failure in toposes ## isn't even only about toposes; is not a topos. Perhaps the subject is failure in constructive mathematics? But then I'd still want , at least, listed in the ## Other categories ## section, since it's interesting in its own right too.
Did I say constructive set theory is the same as topos theory?
“Constructive” is a tricky and pliable and overloaded word, but there is a meaningful sense in which people say (usually informally) that theorems which are proved constructively are valid in toposes. That’s what I meant in the first paragraph of #5.
I’m not quite sure what you’re disagreeing with, but I’ve opened another thread on related matters.
(I am quite aware, dear Toby, that is not a topos!!!!)
I’ve now teased apart the example, so that it no longer gives an impression that someone around here thinks is a topos. :-)
I like how the CSB page looks now.
I’ve added an alternative proof of the CSB theorem, one which I haven’t seen spelled out before (but which might beta-reduce to one of the standard proofs). The application of the Knaster-Tarski lemma is replaced by an application of (a special case of) Adamek’s theorem on terminal coalgebras, but unlike Knaster-Tarski, this approach is predicatively valid.
The immediate application of all this was a slightly novel proof that any two uncountable Polish spaces are Borel-isomorphic, by adapting this other way of proving CSB to the Borel context.
Intriguing! What are “standard proofs” you have in mind to compare it to? In a sense this is the same as the Knaster-Tarski lemma proof since it just needs that there is a fixed point, but I guess here you are getting the greatest fixed point whereas the proof given on that page of the KT lemma yields the least fixed point, so the resulting bijection may be different. Does either of them produce the same bijection as the back-and-forth proof?
Amusingly, if we state CSB type-theoretically in a non-truncated way (constructing an isomorphism rather than merely proving that one exists), this question really is literally a question about “equality of proofs” in the formal sense. (-:
Yes, exactly: the proof that uses the maximal fixed point (that is produced either by dualizing KT or by applying Adamek’s construction for terminal coalgebras) beta reduces to the back-and-forth argument. I’ve put down some details on this, but let me know if it doesn’t read clearly.
I got the impression from a Café post that Emily Riehl had gone through these details as well, but I’ve never seen these connections written down anywhere. I think they are well worth knowing!
Something else I’m idly wondering about: what is a nice abstract niche for CSB?
I mean, it’s claimed that there is a nice model-theoretic context, and I can fully believe that, but it would be very nice to see details. I’m beginning to wonder whether back-and-forth arguments can be tied to matroid structure (such as occurs for vector spaces and algebraically closed fields) and Steinitz exchange lemmas.
Do and in your alternating series mean and respectively? I assumed that they did, but then you emphasized that we are in the Boolean ring , which confused me because when a Boolean algebra is regarded as a ring, its “addition” is actually symmetric difference.
Is there any chance that the choice of maximal/minimal fixed point just corresponds to whether you use or on the doubly-infinite or cyclic elements?
My inner intuitive self was thinking of and , to be honest, but I said to myself let’s use addition and subtraction in the Boolean ring (so symmetric difference), so that I or other readers wouldn’t have to worry much over the order of operations. The and interpretation should be fine, as long as one is careful to maintain the order in which they appear.
If we use the Boolean ring operations, then there is no particular reason to use minus (since ), so we could just write
where an element gets “canceled out” if it occurs an even number of times in the series. So an element which sits in but not in gets canceled out, since it occurs 4 times (in , and ). The elements that don’t get canceled out belong to the maximal fixed point, those and the ones which are in the intersection .
As to your second question: I think that’s exactly what’s going on. You can also envision what the fixed points between these two extremes look like, in terms of the partition described in the Wikipedia article: the bigger the fixed point, the more equivalence classes we use for, to put it roughly.
Ohh, I see.
In that case, it seems to me that the dual of Adamek’s theorem should also work to construct the least fixed point in this situation?
Yes, that’s true. But for some reason the greatest fixed point proof came to me first.
I have done some rewriting at Cantor-Schroeder-Bernstein theorem, following some hints that I think Mike was very gently suggesting (as for example in #17), which might make the general flow of the article easier to follow.
Awesome, thanks! I wasn’t actually intending a suggestion exactly, but it looks great.
1 to 20 of 20