Not signed in (Sign In)

Not signed in

Want to take part in these discussions? Sign in if you have an account, or apply for one below

  • Sign in using OpenID

Site Tag Cloud

2-category 2-category-theory abelian-categories adjoint algebra algebraic algebraic-geometry algebraic-topology analysis analytic-geometry arithmetic arithmetic-geometry book bundles calculus categorical categories category category-theory chern-weil-theory cohesion cohesive-homotopy-type-theory cohomology colimits combinatorics complex complex-geometry computable-mathematics computer-science constructive cosmology deformation-theory descent diagrams differential differential-cohomology differential-equations differential-geometry digraphs duality elliptic-cohomology enriched fibration foundation foundations functional-analysis functor gauge-theory gebra geometric-quantization geometry graph graphs gravity grothendieck group group-theory harmonic-analysis higher higher-algebra higher-category-theory higher-differential-geometry higher-geometry higher-lie-theory higher-topos-theory homological homological-algebra homotopy homotopy-theory homotopy-type-theory index-theory integration integration-theory internal-categories k-theory lie-theory limits linear linear-algebra locale localization logic mathematics measure measure-theory modal modal-logic model model-category-theory monad monads monoidal monoidal-category-theory morphism motives motivic-cohomology nlab noncommutative noncommutative-geometry number-theory of operads operator operator-algebra order-theory pages pasting philosophy physics pro-object probability probability-theory quantization quantum quantum-field quantum-field-theory quantum-mechanics quantum-physics quantum-theory question representation representation-theory riemannian-geometry scheme schemes set set-theory sheaf simplicial space spin-geometry stable-homotopy-theory stack string string-theory superalgebra supergeometry svg symplectic-geometry synthetic-differential-geometry terminology theory topology topos topos-theory tqft type type-theory universal variational-calculus

Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.

Welcome to nForum
If you want to take part in these discussions either sign in now (if you have an account), apply for one now (if you don't).
    • CommentRowNumber1.
    • CommentAuthorTodd_Trimble
    • CommentTimeNov 25th 2010
    • CommentRowNumber2.
    • CommentAuthorTobyBartels
    • CommentTimeNov 26th 2010

    Thanks!

    • CommentRowNumber3.
    • CommentAuthorTodd_Trimble
    • CommentTimeMar 3rd 2013

    Spurred by a MO question, I added a simple example to Cantor-Schroeder-Bernstein theorem that shows CSB fails in the arrow category Set Set^\to.

    • CommentRowNumber4.
    • CommentAuthorTobyBartels
    • CommentTimeMar 4th 2013

    I moved your example one section down where the counterexamples outside of SetSet live.

    • CommentRowNumber5.
    • CommentAuthorTodd_Trimble
    • CommentTimeMar 5th 2013
    • (edited Mar 5th 2013)

    I don’t know that I fully agree with your decision (and I also don’t know the intended scope of “SetSet”). 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 SetsSets, see for example WISC or COSHEP. But then the axiom is explored largely through examples which I guess you (Toby) would not call “SetSet”, 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 VectVect, as it should in spirit. Also, under “Naming”, I added the observation that Dedekind actually proved the theorem in 1887.

    • CommentRowNumber6.
    • CommentAuthorTobyBartels
    • CommentTimeMar 6th 2013

    Constructive set theory is different from topos theory. I had no idea that Set Set^\to 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; TopTop is not a topos. Perhaps the subject is failure in constructive mathematics? But then I'd still want TopTop, at least, listed in the ## Other categories ## section, since it's interesting in its own right too.

    • CommentRowNumber7.
    • CommentAuthorTodd_Trimble
    • CommentTimeMar 6th 2013

    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 TopTop is not a topos!!!!)

    • CommentRowNumber8.
    • CommentAuthorTodd_Trimble
    • CommentTimeMar 6th 2013

    I’ve now teased apart the TopTop example, so that it no longer gives an impression that someone around here thinks TopTop is a topos. :-)

    • CommentRowNumber9.
    • CommentAuthorTobyBartels
    • CommentTimeMar 6th 2013

    I like how the CSB page looks now.

    • CommentRowNumber10.
    • CommentAuthorTodd_Trimble
    • CommentTimeFeb 16th 2016
    • (edited Feb 16th 2016)

    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.

    • CommentRowNumber11.
    • CommentAuthorMike Shulman
    • CommentTimeFeb 16th 2016

    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. (-:

    • CommentRowNumber12.
    • CommentAuthorTodd_Trimble
    • CommentTimeFeb 16th 2016

    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!

    • CommentRowNumber13.
    • CommentAuthorTodd_Trimble
    • CommentTimeFeb 16th 2016

    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.

    • CommentRowNumber14.
    • CommentAuthorMike Shulman
    • CommentTimeFeb 16th 2016

    Do ++ and - in your alternating series mean \cup and \setminus respectively? I assumed that they did, but then you emphasized that we are in the Boolean ring PXP X, 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 ff or g 1g^{-1} on the doubly-infinite or cyclic elements?

    • CommentRowNumber15.
    • CommentAuthorTodd_Trimble
    • CommentTimeFeb 16th 2016
    • (edited Feb 16th 2016)

    My inner intuitive self was thinking of \cup and \setminus, 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 \cup and \setminus 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 ab=a+ba - b = a + b), so we could just write

    XgYgfXgfgYX \oplus g Y \oplus g f X \oplus g f g Y \oplus \ldots

    where an element gets “canceled out” if it occurs an even number of times in the series. So an element xx which sits in gfgYg f g Y but not in gfgfXg f g f X gets canceled out, since it occurs 4 times (in X,gY,gfXX, g Y, g f X, and gfgYg f g Y). The elements that don’t get canceled out belong to the maximal fixed point, those and the ones which are in the intersection n0(gf) nX\bigcap_{n \geq 0} (g f)^n X.

    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 ff for, to put it roughly.

    • CommentRowNumber16.
    • CommentAuthorMike Shulman
    • CommentTimeFeb 17th 2016

    Ohh, I see.

    • CommentRowNumber17.
    • CommentAuthorMike Shulman
    • CommentTimeFeb 17th 2016

    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?

    • CommentRowNumber18.
    • CommentAuthorTodd_Trimble
    • CommentTimeFeb 17th 2016

    Yes, that’s true. But for some reason the greatest fixed point proof came to me first.

    • CommentRowNumber19.
    • CommentAuthorTodd_Trimble
    • CommentTimeFeb 28th 2016

    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.

    • CommentRowNumber20.
    • CommentAuthorMike Shulman
    • CommentTimeFeb 29th 2016

    Awesome, thanks! I wasn’t actually intending a suggestion exactly, but it looks great.