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 definitions 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 k-theory lie-theory limits linear linear-algebra locale localization logic mathematics 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 object 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).

Atrium > Mathematics, Physics & Philosophy: attn: Toby - are singletons choice sets?

Bottom of Page

1 to 32 of 32

  1.  
    • CommentRowNumber1.
    • CommentAuthorDavidRoberts
    • CommentTimeNov 17th 2010

    Note that this might be called a ’soft question’, as they say on MO.

    This is to do with the answer [http://mathoverflow.net/questions/45927/a-conceptual-proof-that-local-fibrations-over-paracompact-spaces-are-global-fibra/46248#46248](here on MO) by Steven Gubkin. I quote

    Note that the axiom of choice is really a local to global principle for sets without any added structure: Given a surjection of sets it is easy to find local sections (i.e. you do not need to invoke choice to find an element of any particular fiber), but we need a new axiom to say that we can actually patch these local sections together to give a global section.

    I don’t know if this is constructively true as stated. Given a surjection, can we choose an element of a given fibre? I suppose if ’surjection’ is defined in a constructive manner it means ’every fibre is inhabited’ or similar, but I’d like to clarify this. How much can we patch together these ’local sections’ in a constructive setting?

    • CommentRowNumber2.
    • CommentAuthorMike Shulman
    • CommentTimeNov 17th 2010

    It is constructively true as stated, as you surmise: “surjection” means “every fiber is inhabited,” and so no choice is necessary to choose an element of any particular fiber. (BTW, I would prefer to phrase your question as “are singleton sets projective?” – see the comments at choice object.) The question of how much we can patch these local sections together is essentially the question of to what extent the axiom of choice holds.

    • CommentRowNumber3.
    • CommentAuthorSteven Gubkin
    • CommentTimeNov 18th 2010
    Hi there! Long time browser, first time poster.

    @Mike: It seems like you might be the kind of person who would know this: Andreas Blass has a paper "Cohomology detects failures in the axiom of choice", which seems relevant to this discussion. Do you know if this work has been taken anywhere? It seems like it would be fun to see what groups could be realized as cohomology groups of, say $\omega_n$ in a model of ZF. Also, I have an answer to your MO question about small complete categories in a grothendieck topos - my undergraduate advisor Colin McLarty worked it out, and I smoothed out some details. I should post it as an answer sometime this weekend.
    • CommentRowNumber4.
    • CommentAuthorHarry Gindi
    • CommentTimeNov 18th 2010

    Post more!

    • CommentRowNumber5.
    • CommentAuthorzskoda
    • CommentTimeNov 18th 2010

    Steven, nice to see you contributing to the discussions! Tip: When posting you can choose different formatting options including Markdown+iTeX. iTeX is needed to display the LaTeX if you want to display equations as equations.

    • CommentRowNumber6.
    • CommentAuthorDavidRoberts
    • CommentTimeNov 19th 2010

    @Mike - of course, ’projective’ is what I meant. As to the later question, I imagine that we can, for each finite set F↪XF \hookrightarrow X and surjection Z→XZ \to X (in the constructive sense), pick a local section F→ZF \to Z. With countable choice we should be able to extend this to countable FF and so on. So in this weak setting, we could work with ’covers’ by finite (or countable as appropriate) sets. This would have applications to Steven’s question, perhaps.

    • CommentRowNumber7.
    • CommentAuthorDavidRoberts
    • CommentTimeNov 19th 2010

    @Steven, Thanks for that Blass paper! I quite like it. Especially this bit:

    (Irrelevant exercise: Formulate the definition of Cech cohomology for general spaces so that it makes sense without the axiom of choice. The difficulty lies in passing from a cover to a refinement without being able to choose, for each set in the refinement, a superset in the original cover.)

    which with anafunctors (and WISC, perhaps) I think would be do-able. (Only need to show that WISC in Set implies it in Top. At present we know Choice in Set implies WISC in Top, but not the stronger statement)

    • CommentRowNumber8.
    • CommentAuthorUrs
    • CommentTimeNov 19th 2010

    Formulate the definition of Cech cohomology for general spaces so that it makes sense without the axiom of choice.

    I don’t see where the standard definition even uses choice: there is a poset of covers and we take a colimit over that. This does not need to choose any refinements (and make choices for that).

    Of course the question is if in a the given exotic setup, this algorithm still computes what it is supposed to compute. That’s always an issue with Cech cohomology, that it is just an algorithm meant to compute some cohomology and not a guaranteed construction of that cohomology.

    • CommentRowNumber9.
    • CommentAuthorMike Shulman
    • CommentTimeNov 19th 2010

    Hi Steven, welcome! I will take a look at that paper, I have not seen it before. I suspect that the presentation axiom might be relevant to the discussion as well.

    • CommentRowNumber10.
    • CommentAuthorTobyBartels
    • CommentTimeNov 19th 2010

    Hi David, Mike answered your question for me, but there is still a point of interest, which is discussed at well-pointed category. In a foundational setting such as ETCS, one can prove that the terminal object of SetSet is projective, using excluded middle and the axiom that SetSet is well-pointed (as usually stated). Without excluded middle, we need an extra axiom to explicitly state that 11 is projective. Mike and I decided that this really should be part of the definition of ‘well-pointed’ in a constructive theory.

    • CommentRowNumber11.
    • CommentAuthorMike Shulman
    • CommentTimeNov 19th 2010

    Like Urs, I don’t understand what Andreas Blass means by his “irrelevant exercise.” If a cover (U i)(U_i) refines a cover (V j)(V_j), then by definition, for every ii there exists a jj with U i⊆V jU_i\subseteq V_j. Given a Cech cocycle for the cover (V j)(V_j), consisting of elements x j∈F(V j)x_j \in F(V_j) which are pairwise compatible (x j| V j∩V j′=x j′| V j∩V j′x_j|_{V_j\cap V_{j'}} = x_{j'}|_{V_j\cap V_{j'}}), we want to define a Cech cocycle for the cover (U i)(U_i), and the obvious way to do it is to “choose” for each ii some j(i)j(i) with U i⊆V j(i)U_i \subseteq V_{j(i)} and define y i=x j(i)| U iy_i = x_{j(i)}|_{U_i}.

    However, pairwise compatibility of the family x jx_j implies that the resulting y iy_i is independent of whichever V jV_j we choose. So whether or not we can simultaneously choose a j(i)j(i) for each ii, we can still prove something like “for any ii, there exists a unique y i∈F(U i)y_i \in F(U_i) such that whenever U i⊆V jU_i \subseteq V_j then y i=x j| U iy_i = x_{j}|_{U_i}.” Then the “axiom of non-choice,” aka function comprehension, lets us define the family (y i)(y_i).

    • CommentRowNumber12.
    • CommentAuthorTim_Porter
    • CommentTimeNov 20th 2010

    @Mike That does not look quite right, but I see what you mean.

    There is a neat fact that if you use the nerves of covers to build the simplest form of Cech complex, (it is something like) choosing a refinement function at the level of the covers is enough to make the Cech complex a homotopy coherent diagram, i.e. all the higher homotopies can be derived just from that one family of choices. If this sounds interesting to someone then I can expand on it. The proof was hinted at by Andy Tonks but actually written down by a Bangor PhD student in his thesis some time later.

    • CommentRowNumber13.
    • CommentAuthorMike Shulman
    • CommentTimeNov 20th 2010

    @Tim: Can you explain further? What’s not right?

    • CommentRowNumber14.
    • CommentAuthorTim_Porter
    • CommentTimeNov 20th 2010

    @Mike. I reread what you wrote and withdraw the comment. I misunderstood something.

    • CommentRowNumber15.
    • CommentAuthorMike Shulman
    • CommentTimeNov 20th 2010

    okay. I don’t understand your comment about “making the Cech complex a homotopy coherent diagram” either – isn’t the Cech complex automatically a strictly commutative simplicial object? Or do I not understand what you mean by “Cech complex”?

    • CommentRowNumber16.
    • CommentAuthorTim_Porter
    • CommentTimeNov 20th 2010

    If you take the classical definition of the Cech complex, it gives a simplicial complex attached to each open cover. The maps corresponding to the refinements are only defined up to ’contiguity’. This means that the ’prosimplicial set’ that is the result lives in ProHo(sSet). What I was saying is that there is an explicit rectification of that diagram to a hocoh diagram and hence to an object in Ho(pro(sSet)).

    • CommentRowNumber17.
    • CommentAuthorMike Shulman
    • CommentTimeNov 21st 2010

    Ah. That sounds kind of like the Artin-Mazur sort of thing we were talking about in the other thread.

    • CommentRowNumber18.
    • CommentAuthorTodd_Trimble
    • CommentTimeDec 31st 2010

    Steven Gubkin has posted an answer on Math Overflow to Mike’s question about small complete categories in a Grothendieck topos. Also, he pointed out to me an error on the page geometric morphism that I’ve now corrected (it said every topos has a geometric morphism to SetSet; I inserted the qualifier “Grothendieck”).

    • CommentRowNumber19.
    • CommentAuthorTobyBartels
    • CommentTimeJan 2nd 2011

    That my name is in the subject header made me read this again, and there is potentially still something that David might wonder about from his beginning question.

    As Mike’s answer noted, the usual definition of “surjective” is precisely a function whose every fibre is inhabited, so there is no difficulty there. However, as category theorists, we might prefer to define “surjection” as an epimorphism in SetSet, and the question is how we prove that every fibre is inhabited.

    An easy method to prove this for f:X→Yf\colon X \to Y is to look at the two functions g,h:Y→TVg, h\colon Y \to TV, where TVTV is the set of truth values, where gg is constant to truth and hh is the characteristic function of the image of ff (details left to the reader). This proof is constructive in a weak sense, but it is not predicative constructive; that is, it only works in a situation (such as in any topos) where the set TVTV actually exists. However, you can instead use the functions in the pushout square

    X → Y ↓ ↓ Y → • \begin {matrix} X & \rightarrow & Y \\ \downarrow & & \downarrow \\ Y & \rightarrow & \bullet \end {matrix}

    (details again left to the reader). This proof generalises to any well-pointed pretopos. (Check that the pushout actually exists by writing down the relevant equivalence relation on Y⊎YY \uplus Y.)

    • CommentRowNumber20.
    • CommentAuthorMike Shulman
    • CommentTimeJan 2nd 2011

    Can’t we prove that just using the fact that Set is well-pointed, and that in particular 1 is projective?

    • CommentRowNumber21.
    • CommentAuthorTobyBartels
    • CommentTimeJan 3rd 2011

    Yes, but I think that this involves a subtle redefinition of David’s question.

    First, David asked whether 11 is a “choice set”. This is terminology used in foundations for a set AA such that any entire relation out of AA contains a function, or equivalently (by an elementary argument) such that any surjection to AA splits. You invited David to say “projective set” instead, since “choice object” is used in topos theory for the internal version of the converse notion: a set BB such that any entire relation into BB contains a function. OK, but literally “projective set” means a projective object in SetSet, which is (a priori) a stronger condition.

    David’s original question can be understood as asking whether any epimorphism to 11 in SetSet splits. If so interpreted, then your answer implicitly uses this argument:

    1. Every epimorphism is a surjection (defined as a function whose every fibre is inhabited).
    2. Every surjection to 11 obviously splits, since there is a unique fibre.

    But (1) was never proved. (Nor did it have to be, since David’s question can also be understood as asking whether any surjection to 11 splits, in which case (2) is sufficient.) So I decided to throw in a proof of (1).

    Now, if we assume that 11 is a projective object, then it’s easy to prove (1). But that’s begging the question; that 11 is projective is (a priori even stronger than) the question being asked. So really, we should prove (1) without using that 11 is projective.

    I muddied things by adding that my proof of (1) works in any well-pointed pretopos. Of course, 11 is projective in a well-pointed pretopos, but we really shouldn’t use that. It’s my fault for suggesting such a strong hypothesis.

    • CommentRowNumber22.
    • CommentAuthorMike Shulman
    • CommentTimeJan 3rd 2011

    Okay, I think I see… you were intending to start from some membership-based set theory. It was your comment about well-pointed pretopoi that confused me.

    • CommentRowNumber23.
    • CommentAuthorTobyBartels
    • CommentTimeJan 8th 2011
    • (edited Jan 8th 2011)

    Not necessarily a material set theory, but also not a structural set theory so explicitly categorial as ETCS (or CETCS). My comment (except for the bit about well-pointed pretoposes, which wasn’t really relevant and just confused things) would also be wanted in SEAR (or CSEAR). I expect that it would be wanted in most foundations of (possibly constructive) mathematics, material or structural (or even non-set-based); only a foundation in the style of (C)ETCS would explicitly state as an axiom that 11 is projective.

    • CommentRowNumber24.
    • CommentAuthorSridharRamesh
    • CommentTimeJan 10th 2011
    • (edited Jan 10th 2011)
    Just to reiterate something Toby essentially said before but which I think may not have been fully appreciated, another way to look at it is that this is the proof which _establishes_, in the internal logic of a (pre)topos, that 1 is projective. So, yes, you can use the fact that 1 is projective, so long as you establish that 1 is projective; and one interesting observation is that you can establish this in the internal logic of any pretopos using Toby's proof (that every epimorphism in a pretopos is regular).

    Talking about the "specific" topos SET is somewhat of a red herring; SET just happens to be, basically by definition, the context in which "internal" and "external" logic coincide, so that the "internal projectivity" of 1 coincides with the actual (external) projectivity of 1, and so on. In other words, every (pre)topos thinks, internally, that it is SET. But too much talk of SET and well-pointedness and so on makes it easy to lose track of the salient point in this case, that Toby's argument above is much more widely fruitfully applicable than just in the context of categories where 1 is externally projective.
    • CommentRowNumber25.
    • CommentAuthorMike Shulman
    • CommentTimeJan 10th 2011

    this is the proof which establishes, in the internal logic of a (pre)topos, that 1 is projective.

    I don’t think I agree with that. I think the internal logic is fundamentally a categorial set theory like ETCS. Toby’s argument makes sense when you are starting from a non-categorial notion of set and constructing a category of sets, but in the internal logic it is the category of sets that’s given to you.

    Here’s how I would prove that 1 is projective in the internal logic. The statement “1 is projective” is equivalent to “every epimorphism with target 1 splits” (whenever epimorphisms are stable under pullback), which in turn is an abbreviation of “for any epimorphism f:A→1f\colon A\to 1, there exists a morphism g:1→Ag\colon 1\to A such that fg=id 1f g = id_1.” If you interpret this in the internal logic using Kripke-Joyal / stack semantics, it becomes “for any object X and any epimorphism f:A→Xf\colon A\to X, there exists an epimorphism p:Y→Xp\colon Y\to X and a morphism g:Y→Y× XAg\colon Y \to Y\times_X A such that p *(f)∘g=1 Yp^*(f) \circ g = 1_Y.” But this is obviously true since we can take p=fp=f and let gg be the diagonal.

    If you prefer representing subobjects to Kripke-Joyal, then the argument is even easier: we have an object with an epimorphism A→1A\to 1 and we want to prove that “there exists an element of A.” But validity of “there exists an element of A” just means that the image of the projection A→1A\to 1 is all of 11, which is equivalent to saying that A→1A\to 1 is epic.

    • CommentRowNumber26.
    • CommentAuthorSridharRamesh
    • CommentTimeJan 10th 2011
    • (edited Jan 10th 2011)
    I also think the internal logic is fundamentally a categorial set theory. But I don't see why you feel Toby's argument starts from or has anything to do with a non-categorial notion of set.

    Here is why I would say Toby's argument establishes that 1 is projective in the internal logic of every pretopos:

    Take the definition of "1 is projective" to be "For any epimorphism f : X -> Y, and any global element y : 1 -> Y, there is some global element x : 1 -> X such that f x = y". In the internal logic, we identify the set Hom(1, A) with A^1, which is essentially A itself; thus, this amounts to establishing that for any epic morphism f : X -> Y in any pretopos, it is the case in the internal logic that for every y in Y, there is some x in X such that f x = y.

    If we take the internal logic to be the one in which propositions are interpreted as subobjects, as motivated in the definition of a pretopos, then the existential quantifier is interpreted by the left adjoint to pullback of subobjects; i.e., by image factorization. The predicate on y in Y that "there is some x in X such that f x = y" then becomes the subobject of Y corresponding to the image of f. To establish that this holds for every y in Y is thus to establish that the image of f is all of Y. This is what Toby's proof does; it shows that every epic has image equal to its codomain.

    As you yourself put it: "But validity of 'there exists an element of A' just means that the image of the projection A -> 1 is all of 1, which is equivalent to saying that A -> 1 is epic". But that equivalence is a nontrivial* fact about pretoposes, the very fact that Toby's proof establishes! (*: After all, it's certainly possible to have an epic in a regular category which is not regular epic)

    The only reason the Kripke-Joyal semantics can be presented in terms of using unrestricted epimorphisms to model the existential quantifier in the internal logic is by blessing of our already having established that every epimorphism is regular in suitable contexts; it's really the regular epimorphisms that directly relate to the existential quantifier, as given by the left adjoint to pullback of predicates. In contexts where epis and regular epis come apart, it would no longer be appropriate to use epimorphisms to model the internal logic in that way; one would want to restrict to using regular epis or such things instead, in those contexts.
    • CommentRowNumber27.
    • CommentAuthorMike Shulman
    • CommentTimeJan 10th 2011

    Okay, that’s all certainly true, but I would argue that if “epi ≠ regular epi” then the sensible definition of “projective” refers to regular epis, not to ordinary ones. Thus, I wouldn’t regard a proof that “all epis are regular” as a proof that 1 is projective, but rather as just a proof that all epis are regular. As a corollary, projectivity of 1 (with respect to regular epis, which is the sensible definition in general) implies the corresponding property for plain epis.

    • CommentRowNumber28.
    • CommentAuthorSridharRamesh
    • CommentTimeJan 11th 2011
    Yes, that's fair enough; I agree with that now as well. Projective generally ought to mean with respect to regular epis (or whatever best models the existential quantifier in the framework one is working in), in which case the internal projectivity of 1 is automatic.

    That having been said, for whatever reason (fun, presumably), Toby had chosen to look at the reanalysis of the original question as "Does every epimorphism to 1 split?" rather than "Does every surjection to 1 split?". I don't think this really captures what the original question was, but it does amount to "Is 1 projective with respect to arbitrary epimorphisms?", which is why he felt it wasn't sufficient to simply note the (internally automatic, or, if one insists, externally assumed) projectivity of 1 with respect to regular epis. It seemed there was some talking past each other on this point, though (and maybe some talking past me...), because I don't think Toby's post had anything to do with material/global membership vs. structural/local/categorial distinctions in set theories or any such things; it just had to do with rephrasing in terms of epis a question that was originally (trivially) interpreted in terms of regular epis.
    • CommentRowNumber29.
    • CommentAuthorTobyBartels
    • CommentTimeJan 11th 2011

    My intention behind the proof was Mike’s (current) interpretation, to establish that 11 is projective in an (unspecified but) non-categorial foundation of (possibly predicative constructive) mathematics. Whether that can be shown more quickly (say, in PSEARPSEAR, the predicative version with disjoint unions and quotient sets but not power sets) and whether the argument shows anything more general, I have no idea that’s not already in the discussion above.

    • CommentRowNumber30.
    • CommentAuthorSridharRamesh
    • CommentTimeJan 11th 2011
    • (edited Jan 11th 2011)
    Hm, I guess I'm the one who the talking is going past then. It doesn't really matter too much, so if you're tired of the discussion we can end it, but if you don't mind helping me understand: When you say your intention was to establish that 1 is projective, do you mean with respect to regular epis or arbitrary epis? And when you say a non-categorial foundation, what is it about your argument that was non-categorial?

    (In other words, it seemed to me that you were presenting an argument that arbitrary epis are surjections (i.e., their image is their codomain; equivalently, they are regular epis), in the predicative categorial framework of pretoposes. Apparently, this is a misunderstanding of what you were doing, but it's not clear to me where I went astray in my interpretation.)
    • CommentRowNumber31.
    • CommentAuthorTobyBartels
    • CommentTimeJan 11th 2011

    When you say your intention was to establish that 1 is projective, do you mean with respect to regular epis or arbitrary epis?

    For arbitrary ones (and thus also for regular ones).

    And when you say a non-categorial foundation, what is it about your argument that was non-categorial?

    Nothing, but that’s not the point.

    Any foundation worth its salt can prove that sets and functions form a category SetSet, and this is necessary before even asking whether singletons are projective in SetSet. However, the foundation need not start with the assumption that sets and functions form a category. This is important since such foundations may (like CETCSCETCS in fact does) take as an axiom that singletons are projective (as part of the axiom that SetSet is well-pointed).

    Of course, even in a categorial foundation, one might conceivably do things in such a way that there is no axiom that singletons are projective, and the quickest proof of that fact might still use my argument. (I once wrote out such a foundation as an exercise here, although it was a gross copyright violation and is no longer online.) So really, instead of a non-categorial foundation, I should have simply specified a foundation in which this is not an axiom (or a simple consequence of one, as it is in classical ETCSETCS), but really requires reasoning about sets and functions.

    it seemed to me that you were presenting an argument that arbitrary epis are surjections …

    It does prove this, since it’s obvious (and Mike said at the very beginning) that 11 is SS-projective (where SS is the class of surjections), so now we have a proof that 11 is EE-projective (where EE is the class of arbitrary epimorphisms).

    … in the predicative categorial framework of pretoposes

    That wasn’t part of my intention, although I said something in the epilogue that kind of sounded like that.

    • CommentRowNumber32.
    • CommentAuthorSridharRamesh
    • CommentTimeJan 11th 2011
    Alright, I think I understand what your intentions were now. Sorry for the confusion!

1 to 32 of 32

  1.