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).

nLab > Latest Changes: dependent choice

Bottom of Page

1 to 26 of 26

  1.  
    • CommentRowNumber1.
    • CommentAuthorTodd_Trimble
    • CommentTimeMay 30th 2010

    Started the article dependent choice, and did some editing at COSHEP to make clearer to myself the argument that COSHEP + (1 is projective) implies dependent choice. It’s not clear to me that the projectivity of 1 is removable in that argument; maybe it is.

    • CommentRowNumber2.
    • CommentAuthorTobyBartels
    • CommentTimeMay 30th 2010
    • (edited May 30th 2010)

    Thanks!

    I don’t know anybody who doubts that the terminal object in the category of sets is projective, but it’s just as well to spell it out, especially if one wants to use the argument in some non-well-pointed topos.

    In particular, the terminal object of any topos is internally projective. That is what matters for COSHEP in topos theory.

    • CommentRowNumber3.
    • CommentAuthorMike Shulman
    • CommentTimeMay 30th 2010

    Yeah, I think it’s important to remember that for purposes of doing math in a topos, it’s the internal notions that matter: internal projectivity, internal COSHEP, internal choice. (I occasionally get bitten by messing up the internal/external distinction for notions of finiteness.) I guess sometimes the “external” notions are useful to have around too, but in non-well-pointed topoi they don’t seem to me to be very important.

    I’m glad to have that argument there in any case, thanks.

    • CommentRowNumber4.
    • CommentAuthorTodd_Trimble
    • CommentTimeMay 30th 2010

    Thanks for that reminder, guys!

    • CommentRowNumber5.
    • CommentAuthorTobyBartels
    • CommentTimeMay 30th 2010

    Sometimes I think that, while it’s neat (and handy, for us who are used to category theory) to express set-theoretic axioms as properties of the category of sets (choice = epis split, infinity = NNO, presentation/COSHEP = enough projectives of course), sometimes it gives the wrong impression. It is vital in interpreting all of these that Set is well-pointed (including the projectivity of 1) so that the internal versions are equivalent. Otherwise you would have to state the internal version instead.

    • CommentRowNumber6.
    • CommentAuthorTobyBartels
    • CommentTimeMay 30th 2010

    By the way, do we know a particular (necessarily non-well-pointed) topos with enough projectives and a natural numbers object but in which countable choice fails?

    • CommentRowNumber7.
    • CommentAuthorMike Shulman
    • CommentTimeMay 31st 2010

    I think that external COSHEP is stronger than internal COSHEP, just like external AC is stronger than internal AC. If that’s right, then the question to ask is rather whether there is a topos satisfying internal COSHEP but not external CC, hence in which the NNO is internally, but not externally, projective. I don’t know the answer to that, though.

    Could you be more explicit about the “wrong impression” that you think expressing set-theoretic axioms categorially may give? I’m not necessarily disagreeing, I just don’t quite understand. To me, being well-pointed is a vital characteristic for any category to deserve the name “Set”.

    • CommentRowNumber8.
    • CommentAuthorTobyBartels
    • CommentTimeMay 31st 2010

    If Todd is right that the projectivity of 11 is needed in the proof that COSHEP implies CC, then we need a topos which satisfies COSHEP externally (that is, it has enough projectives) but does not satisfy CC externally (that is, the NNO is not projective). If there is no such counterexample, then we ought to be able to simplify the proof, by removing reference to the projectivity of 11. (Not that every theorem has either a proof or a counterexample, of course, but one can hope so in particular cases).

    I certainly agree that any candidate for the category of sets and functions must be well pointed; if it’s not well pointed, then its morphisms probably aren’t really functions. (At first, I had written here that its object aren’t really sets, but I think that the morphisms are more likely to be at fault, if it’s a category that somebody earnestly suggests as the category of sets.)

    I think that what I meant about ‘the wrong impression’ is best illustrated by an example. I define COSHEP, as a foundational axiom, to mean that the category of sets has enough projectives (obviously). Then someone (person XX) comes along and, not so much interested in foundations (at least not in an absolute sense), still wants to know whether some particular category CC (considered, perhaps, as a model for some nonstandard foundation) satisfies COSHEP. Since I described COSHEP as a property of the category of sets, it’s quite natural for XX to think that CC satisfies COSHEP iff CC has enough projectives. But that is not true, or at least that is not what is really relevant. What matters is whether CC satisfies COSHEP internally. (For example, I don’t care so much whether the effective topos has enough projectives as whether it satisfies COSHEP, if you see what I mean.)

    On the other hand, if I define COSHEP without using category-theoretic language, but in purely set-theoretic terms (for every set AA, there exists a set BB and …), then anyone trying to interpret it in an arbitrary category will have to think harder (especially if I use words like ‘surjection’ and concepts like entire relations in my phrasing). Then they’re more likely to come up with the internal notion, or at least to realise that they’re not sure and had maybe better ask a categorial logician for help.

    All of this means, of course, that it is my fault for calling it ‘COSHEP’. If I’d known that Aczel called it ‘presentation’, then I’d probably have called it that all along.

    • CommentRowNumber9.
    • CommentAuthorTodd_Trimble
    • CommentTimeMay 31st 2010

    I’m a little confused why you (Toby) repeatedly mention CC as opposed to DC, since the argument I rewrote is specifically directed at DC. Maybe COSHEP (speaking externally) implies CC without projectivity of 11 – I don’t know – but does it imply DC?

    • CommentRowNumber10.
    • CommentAuthorMike Shulman
    • CommentTimeMay 31st 2010
    • (edited May 31st 2010)

    I see, I didn’t realize you were looking for a counterexample specifically to decide whether projectivity of 1 is essential. Here’s why I think there is no such counterexample. An object P is internally projective if for any epimorphism e:Q↠Pe\colon Q\twoheadrightarrow P, there exists a cover U↠1U\twoheadrightarrow 1 such that U *(e)U^*(e) is split, and externally projective if any such ee is already split. Clearly the latter implies the former, and “internal epimorphisms” are the same as external ones; thus if every object admits an epi from a projective, then a fortiori it admits an internal epi from an internal projective. Moreover, this is also automatically true in all slices, since projectives in slices are created in the underlying category. So COSHEP implies internal COSHEP, and thus also (internal) CC and DC.

    I think I see what you mean about the category of sets. Perhaps that is another nice thing about SEAR.

    All of this means, of course, that it is my fault for calling it ‘COSHEP’. If I’d known that Aczel called it ‘presentation’, then I’d probably have called it that all along.

    We could of course change it. “Presentation” seems like as good a name as any, and there’s no reason to needlessly proliferate terminology for the same thing.

    • CommentRowNumber11.
    • CommentAuthorTobyBartels
    • CommentTimeMay 31st 2010

    @ Todd: Re CC vs DC

    I’m suspecting that external COSHEP doesn’t even imply external CC and so looking for the strongest counterexample. And then forgetting that DC was the original topic, which may help explain Mike’s confusion over my motivation.

    @ Mike

    So COSHEP implies internal COSHEP, and thus also (internal) CC and DC.

    I buy your argument, but did I miss something showing that internal CC implies external CC? If there’s a category with enough projectives and an NNO which is not projective, then I will be confident that Todd’s proof that (internally) COSHEP implies DC cannot be simplified to remove any mention of the projectivity of 11. If on the contrary, there’s a proof that any category with enough projectives and an NNO has a projective NNO, then I’ll be looking for a way to remove any mention of the projectivity of 11 from our proof that (internally) COSHEP implies DC.

    • CommentRowNumber12.
    • CommentAuthorTodd_Trimble
    • CommentTimeMay 31st 2010

    I have a feeling that sheaves on a suitable space with nontrivial cohomology, say S 1S^1, would do the trick. Here’s the rough argument:

    (1) Any etale space SS over S 1S^1 ought to have a projective cover: it suffices to give a good cover U αU_\alpha (where every open in the covering is contractible). The idea would be that if U=U αU = U_\alpha is contractible, then every inhabited object in Sh(U)Sh(U) has a global section. Hence ∑ αU α\sum_\alpha U_\alpha is projective. (This part needs to be checked carefully).

    (2) However, globally speaking, 11 is not projective, since for example the nontrivial double cover as etale space S→S 1S \to S^1 has no section. By the same token, when we pull back this cover along the projection ℕ→1\mathbb{N} \to 1 in Sh(S 1)Sh(S^1), we get a nontrivial double cover of ℕ\mathbb{N} which has no section. So ℕ\mathbb{N} is not projective.

    • CommentRowNumber13.
    • CommentAuthorTobyBartels
    • CommentTimeMay 31st 2010

    Actually, this is something that I’ve been trying to get straight for a while; perhaps I’d better put the whole thing out here.

    It starts with intensional type theory with identity types and propositions as types. In this context, there are well-known proofs of DC and CC which go as follows:

    • Definition: Assume that we have constructed a type (pre-set) NN of natural numbers and wish to define equality to make the set ℕ\mathbb{N}. We do so by recursion on two elements simultaneously:

      • 0=00 = 0 is defined to be true.
      • 0=n +0 = n^+ is defined to be false.
      • m +=0m^+ = 0 is defined to be false.
      • m +=n +m^+ = n^+ is defined to be m=nm = n.

      (This definition makes sense even in the absence of identity types or propositions as types; we would use it even in SEAR without equality. Really this is just background information; you have to do this even before proving that ℕ\mathbb{N} is a Peano system, that is an internal natural-numbers object.)

    • Lemma: If any two elements of the set ℕ\mathbb{N} are equal, then they are identical as elements of NN.

      Proof: By induction on both elements simultaneously. 00 is identical to itself, by reflexivity of identity. There is nothing to prove if 0=n +0 = n^+ or m +=0m^+ = 0, since these are false. If m +=n +m^+ = n^+, then m=nm = n, so m≡nm \equiv n by the induction hypothesis, so m +=n +m^+ = n^+ since the successor operation (like every operation) preserves identity.

      (This lemma does not even make sense without identity types, or at least identity predicates, although it does not need propositions as types.)

    • Corollary: Any operation (type-function, or pre-function) ff from NN to the underlying type |X|{|{X}|} of any set XX is in fact a function from ℕ\mathbb{N} to XX (meaning that it preserves equality).

      Proof: Every operation preserves identity, and equality in NN is identity. So ff takes equal elements of ℕ\mathbb{N} to identical elements of XX, and identitity always implies equality (just not conversely).

      (The statement of this corollary makes perfect sense in the same contexts in which the definition of equality in ℕ\mathbb{N} made sense. But the proof does not go through without identity predicates.)

    • Theorem (DC): Given a set XX, an element aa of XX, a binary relation RR on XX, and a proof pp that RR is entire, then there is a function ff from ℕ\mathbb{N} to XX such that RR relates f(n)f(n) and f(n +)f(n^+) for every natural number nn.

      Proof: Define an operation ff from NN to |X|{|{X}|} recursively as follows:

      • let f(0)f(0) be aa;
      • given f(n)f(n), let f(n +)f(n^+) be the element of XX given by applying pp to f(n)f(n), so that RR holds when it should.

      To prove that ff is a function from ℕ\mathbb{N} to XX, we apply the corollary.

      (Here we need both propositions as types and identity types. The former is needed to construct ff, while the latter is needed to prove that ff is a function.)

    • Theorem (CC): Given a set XX, a binary relation RR from ℕ\mathbb{N} to XX, and a proof pp that RR is entire, then there is a function ff from ℕ\mathbb{N} to XX such that RR relates nn and f(n)f(n) for every natural number nn.

      Proof: Of course, we could use DC, but there’s a simpler proof. We define an operation ff from NN to |X|{|{X}|} by applying pp to any natural number nn to get an element of XX, so that RR holds when it should. To prove that ff is a function from ℕ\mathbb{N} to XX, we apply the corollary.

      (Again, this relies on both propositions as types and identity types.)

    All this is in a context where COSHEP also can be proved, and I have the idea that COSHEP is the set-theoretic (meaning using sets and functions, not types = pre-sets and operations = pre-functions) content of being in that context. Basically, given a set XX, COSHEP supplies a new set which I identify with the type |X|{|{X}|}. That we have identity predicates allows us to interpret any type as a set (by defining equality to be identity); that we have propositions as types means that any such set would have to be projective (by reasoning similar to the proof of CC above). The gap in this reasoning is that there is nothing to show that every projective set arises from a type in this way.

    Despite this gap, the proof of DC above seems to match very well the purely set-theoretic proof that COSHEP implies DC. Yet I have searched in vain for a simpler set-theoretic proof that COSHEP implies CC to stand as the analogue of the proof above! You will notice that 11 plays a role in DC (implicitly, through the element aa) that it does not play in CC. So I hoped that perhaps this discussion would lead to my sought set-theoretic proof of CC from COSHEP, out of a desire to avoid using the projectivity of 11.

    And all this would help me better understand whether COSHEP really is the full set-theoretic content of founding set theory on an intensional type theory with identity types and propositions as types.

    • CommentRowNumber14.
    • CommentAuthorMike Shulman
    • CommentTimeMay 31st 2010

    but did I miss something showing that internal CC implies external CC?

    No, I didn’t mean to claim that. When you said “countable choice fails” in a topos I assumed that meant the internal version. Sorry for the confusion.

    if U=U αU = U_\alpha is contractible, then every inhabited object in Sh(U)Sh(U) has a global section.

    I don’t think that’s true. The etale space (−∞,1)⊔(−1,∞)(-\infty, 1) \sqcup (-1,\infty) over ℝ\mathbb{R} is inhabited and ℝ\mathbb{R} is contractible, but it has no global section.

    • CommentRowNumber15.
    • CommentAuthorTodd_Trimble
    • CommentTimeMay 31st 2010

    Whoops.

    • CommentRowNumber16.
    • CommentAuthorTobyBartels
    • CommentTimeMay 31st 2010
    • (edited May 31st 2010)

    When you said “countable choice fails” in a topos I assumed that meant the internal version.

    That was reasonable of you. It was my fault for not being clear.

    • CommentRowNumber17.
    • CommentAuthorTodd_Trimble
    • CommentTimeJun 1st 2010
    • (edited Jun 1st 2010)

    After my former example was embarrassingly demolished, I’d like to try again. This time my example is a presheaf topos Set CSet^C (so COSHEP is satisfied), but one in which the terminal is not projective (unless I’ve made another dumb mistake). Otherwise the idea will be sort of similar.

    Here CC is the category with four objects a,b,c,da, b, c, d whose non-identity arrows are a←b→da \leftarrow b \to d, a←c→da \leftarrow c \to d. The idea is that CC has the shape of a circle. Now we’re going to mimic the nontrivial double cover.

    Define a presheaf UU with eight elements a 0,a 1,b 0,b 1,c 0,c 1,d 0,d 1a_0, a_1, b_0, b_1, c_0, c_1, d_0, d_1 sitting over their counterparts a,b,c,da, b, c, d as appropriate, where the CC-action looks like this:

    a 1←b 0→d 1 a 0←b 1→d 0 a 1←c 0→d 0 a 0←c 1→d 1\array{ a_1 \leftarrow b_0 \to d_1 & a_0 \leftarrow b_1 \to d_0 & a_1 \leftarrow c_0 \to d_0 &a_0 \leftarrow c_1 \to d_1 }

    (Draw a picture!) Now hopefully I have it right: this is clearly inhabited, but has no global section, so 11 is not projective.

    The NNO NN in Set CSet^C is just an ℕ\mathbb{N}-indexed coproduct of copies of the terminal object (I believe this is true in any Grothendieck topos), and the product projection π:N×U→N\pi: N \times U \to N cannot have a section (for by extensivity, π\pi splits up into an ℕ\mathbb{N}-indexed coproduct of epis all of the form U→1U \to 1, none of which has a section, so π\pi can’t either). Hence NN is not projective.

    Let me know if you think this holds water.

    • CommentRowNumber18.
    • CommentAuthorTodd_Trimble
    • CommentTimeJun 1st 2010

    Well obviously I could have made this a lot simpler, by taking UU to have just five elements a,b,c,d 0,d 1a, b, c, d_0, d_1 and mapping

    a←b→d 0a←c→d 1a \leftarrow b \to d_0 \qquad a \leftarrow c \to d_1

    and I don’t see how this could go wrong :-)

    • CommentRowNumber19.
    • CommentAuthorMike Shulman
    • CommentTimeJun 1st 2010

    That looks right to me. So this is a topos that satisfies external COSHEP, hence internal COSHEP, and thus internal CC, but not external CC?

    • CommentRowNumber20.
    • CommentAuthorTodd_Trimble
    • CommentTimeJun 1st 2010

    Yes, that interpretation sounds right to me.

    An even simpler example is a presheaf category where the category CC has only a→b←ca \to b \leftarrow c as its nonidentity arrows, and the functor U:C→SetU: C \to Set takes the form a→b 0a \to b_0, b 1←cb_1 \leftarrow c (only four objects in El(U)El(U)), where again U→1U \to 1 has no section. That may be the simplest example in some sense.

    • CommentRowNumber21.
    • CommentAuthorTobyBartels
    • CommentTimeJun 1st 2010

    So in the last example, ℕ×U\mathbb{N} \times U takes the form ℕ→ιℕ+ℕ←κℕ\mathbb{N} \overset{\iota}\rightarrow \mathbb{N} + \mathbb{N} \overset{\kappa}\leftarrow \mathbb{N} (where ι\iota and κ\kappa are left and right coproduct coprojections), and the projection ℕ×U→ℕ\mathbb{N} \times U \to \mathbb{N} is epic but has no section.

    Thanks! Somewhere along the way I tricked myself into thinking that 11 was projective in all presheaf topoi, so I wasn’t looking there.

    So there is no proof that COSHEP implies CC (hence no proof that COSHEP implies DC) that doesn’t implicitly use that SetSet is well-pointed; that is no proof that generalises to an arbitrary pretopos when the axioms are interpreted externally.

    • CommentRowNumber22.
    • CommentAuthorTobyBartels
    • CommentTimeJun 1st 2010

    Incidentally, I ran across some nice exercises about projective objects in topoi on pages 216&217 of Mac Lane and Moerdijk. They talk about internal projectivity and the projectivity of 11, among other things (but not the projectivity of ℕ\mathbb{N}).

    • CommentRowNumber23.
    • CommentAuthorTodd_Trimble
    • CommentTimeJun 1st 2010

    Thanks, Toby. That helped suggest a way to streamline some of the above discussion into the article COSHEP (look under Consequences).

    • CommentRowNumber24.
    • CommentAuthorTobyBartels
    • CommentTimeJun 1st 2010

    Now I think that there may be overemphasis on the projectivity of 11, but how does it look now?

    • CommentRowNumber25.
    • CommentAuthorTodd_Trimble
    • CommentTimeJun 1st 2010

    I’m not quite sure there’s overemphasis, but the point you’re making deserves to be made. I personally would prefer having that separated out as a remark, rather than have the remark in the statement of the proposition. Do we have a page where we go into greater length about internal vs. external? I think I tried looking recently and didn’t find much from a rapid search.

    • CommentRowNumber26.
    • CommentAuthorTobyBartels
    • CommentTimeJun 1st 2010

    I pulled it out.

    There’s internalization and internal language, but they may not really address what you’re looking for here.

1 to 26 of 26

  1.