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.
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.
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.
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.
Thanks for that reminder, guys!
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.
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?
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”.
If Todd is right that the projectivity of $1$ 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 $1$. (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 $X$) comes along and, not so much interested in foundations (at least not in an absolute sense), still wants to know whether some particular category $C$ (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 $X$ to think that $C$ satisfies COSHEP iff $C$ has enough projectives. But that is not true, or at least that is not what is really relevant. What matters is whether $C$ 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 $A$, there exists a set $B$ 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.
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 $1$ – I don’t know – but does it imply DC?
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\colon Q\twoheadrightarrow P$, there exists a cover $U\twoheadrightarrow 1$ such that $U^*(e)$ is split, and externally projective if any such $e$ 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.
@ 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 $1$. 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 $1$ from our proof that (internally) COSHEP implies DC.
I have a feeling that sheaves on a suitable space with nontrivial cohomology, say $S^1$, would do the trick. Here’s the rough argument:
(1) Any etale space $S$ over $S^1$ ought to have a projective cover: it suffices to give a good cover $U_\alpha$ (where every open in the covering is contractible). The idea would be that if $U = U_\alpha$ is contractible, then every inhabited object in $Sh(U)$ has a global section. Hence $\sum_\alpha U_\alpha$ is projective. (This part needs to be checked carefully).
(2) However, globally speaking, $1$ is not projective, since for example the nontrivial double cover as etale space $S \to S^1$ has no section. By the same token, when we pull back this cover along the projection $\mathbb{N} \to 1$ in $Sh(S^1)$, we get a nontrivial double cover of $\mathbb{N}$ which has no section. So $\mathbb{N}$ is not projective.
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) $N$ of natural numbers and wish to define equality to make the set $\mathbb{N}$. We do so by recursion on two elements simultaneously:
(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 $N$.
Proof: By induction on both elements simultaneously. $0$ is identical to itself, by reflexivity of identity. There is nothing to prove if $0 = n^+$ or $m^+ = 0$, since these are false. If $m^+ = n^+$, then $m = n$, so $m \equiv n$ by the induction hypothesis, so $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) $f$ from $N$ to the underlying type ${|{X}|}$ of any set $X$ is in fact a function from $\mathbb{N}$ to $X$ (meaning that it preserves equality).
Proof: Every operation preserves identity, and equality in $N$ is identity. So $f$ takes equal elements of $\mathbb{N}$ to identical elements of $X$, 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 $X$, an element $a$ of $X$, a binary relation $R$ on $X$, and a proof $p$ that $R$ is entire, then there is a function $f$ from $\mathbb{N}$ to $X$ such that $R$ relates $f(n)$ and $f(n^+)$ for every natural number $n$.
Proof: Define an operation $f$ from $N$ to ${|{X}|}$ recursively as follows:
To prove that $f$ is a function from $\mathbb{N}$ to $X$, we apply the corollary.
(Here we need both propositions as types and identity types. The former is needed to construct $f$, while the latter is needed to prove that $f$ is a function.)
Theorem (CC): Given a set $X$, a binary relation $R$ from $\mathbb{N}$ to $X$, and a proof $p$ that $R$ is entire, then there is a function $f$ from $\mathbb{N}$ to $X$ such that $R$ relates $n$ and $f(n)$ for every natural number $n$.
Proof: Of course, we could use DC, but there’s a simpler proof. We define an operation $f$ from $N$ to ${|{X}|}$ by applying $p$ to any natural number $n$ to get an element of $X$, so that $R$ holds when it should. To prove that $f$ is a function from $\mathbb{N}$ to $X$, 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 $X$, COSHEP supplies a new set which I identify with the type ${|{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 $1$ plays a role in DC (implicitly, through the element $a$) 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 $1$.
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.
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_\alpha$ is contractible, then every inhabited object in $Sh(U)$ has a global section.
I don’t think that’s true. The etale space $(-\infty, 1) \sqcup (-1,\infty)$ over $\mathbb{R}$ is inhabited and $\mathbb{R}$ is contractible, but it has no global section.
Whoops.
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.
After my former example was embarrassingly demolished, I’d like to try again. This time my example is a presheaf topos $Set^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 $C$ is the category with four objects $a, b, c, d$ whose non-identity arrows are $a \leftarrow b \to d$, $a \leftarrow c \to d$. The idea is that $C$ has the shape of a circle. Now we’re going to mimic the nontrivial double cover.
Define a presheaf $U$ with eight elements $a_0, a_1, b_0, b_1, c_0, c_1, d_0, d_1$ sitting over their counterparts $a, b, c, d$ as appropriate, where the $C$-action looks like this:
$\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 $1$ is not projective.
The NNO $N$ in $Set^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 $\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 \to 1$, none of which has a section, so $\pi$ can’t either). Hence $N$ is not projective.
Let me know if you think this holds water.
Well obviously I could have made this a lot simpler, by taking $U$ to have just five elements $a, b, c, d_0, d_1$ and mapping
$a \leftarrow b \to d_0 \qquad a \leftarrow c \to d_1$and I don’t see how this could go wrong :-)
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?
Yes, that interpretation sounds right to me.
An even simpler example is a presheaf category where the category $C$ has only $a \to b \leftarrow c$ as its nonidentity arrows, and the functor $U: C \to Set$ takes the form $a \to b_0$, $b_1 \leftarrow c$ (only four objects in $El(U)$), where again $U \to 1$ has no section. That may be the simplest example in some sense.
So in the last example, $\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 $\mathbb{N} \times U \to \mathbb{N}$ is epic but has no section.
Thanks! Somewhere along the way I tricked myself into thinking that $1$ 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 $Set$ is well-pointed; that is no proof that generalises to an arbitrary pretopos when the axioms are interpreted externally.
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 $1$, among other things (but not the projectivity of $\mathbb{N}$).
Thanks, Toby. That helped suggest a way to streamline some of the above discussion into the article COSHEP (look under Consequences).
Now I think that there may be overemphasis on the projectivity of $1$, but how does it look now?
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.
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