Thanks! I did some editing; in particular I removed the piecewise proof that $B\le A$ implies $B \le^* A$, since the subquotient one works classically too and is IMHO more elegant. But if you really want it there we can put it back.
(By the way, note that $B=\emptyset$ is the same as “$B$ is not inhabited” even constructively.)
]]>Did so, but left the set-theorists one in, but clarified how they are related.
]]>Good. I think we should give that definition, then, not the piecemeal one.
]]>@Mike: sure, using subquotients, which give, in the presence of LEM, an equivalent preorder to $\leq^*$ as defined in the piecemeal fashion.
]]>Thanks! I put in a section heading, since it’s not part of the definition of surjection.
One also writes $\empty \leq^* |A|$ for all sets $A$, but this is a standalone definition, and doesn’t follow from a construction on $Surj$.
Ugh!! Do people really do that? Is there a way to define $\leq^*$ that doesn’t special-case $\emptyset$ (and hence in particular would make sense constructively)?
]]>I made some edits at surjection incorporating #25.
]]>Todd #27
I hear you. I plan to do something next week about this.
]]>whatever category one is calling $Set$, there is a well-defined notion of surjection, and $Surj$ is simply understood relative to that $Set$
Which is equally true with “surjection” replaced by any other object of mathematics: group, ring, field, topological space, etc.
]]>So here would be a sample theorem written according to the style I personally favor.
Theorem: Assuming the axiom of choice, every functor $F: Set \to Set$ maps surjections to surjections, i.e., restricts to a functor $Surj \to Surj$.
Proof: If $p: E \to B$ is a surjection, then it admits a section $s: B \to E$ according to the axiom of choice. From $p s = 1_B$ and functoriality, we have $F(p) F(s) = 1_{F B}$, so $F(p)$ is a retraction and therefore a surjection.
]]>That section 2 of Set is pretty circular actually (for instance, “locally small” depends on a background notion of $Set$), and relativizes to different models of set theory. (I don’t mean presentationally different such as the difference between ZFC and NBG; I mean what Lawvere would call “objectively” different in the sense of propositions that can be stated in terms of category theory, e.g., some categories $Set$ satisfy CH, some don’t.) So there is no one “$Set$”, although the section does explain how to characterize $Set$ among categories considered against the background theory.
Also, not everyone would even agree that $Set$ is a topos in the Lawvere-Tierney sense; for example I think those with predicativist commitments don’t think so. So I think section 1 comes closer to expressing the complicated truth of the matter (although it seems slightly weird to me to title it “Definition”), and it’s wise to keep such a foundational discussion on a descriptive level, to accommodate the various axes (“axises”) along which people consider the category “$Set$”.
$Surj_{ETCS}$, $Surj_{MK}$, $Surj_{NBG}$, $Surj_{SEAR}$, $Surj_{ZF}$, $Surj_{ZF+AC_\omega}$, $Surj_{ZF+DC}$, $Surj_{ZFC}$
Personally, I’d avoid writing all that. Since we agree that there is no one $Surj$ pretty much to the same extent as there is no one $Set$: whatever category one is calling $Set$, there is a well-defined notion of surjection, and $Surj$ is simply understood relative to that $Set$. For the most part the theorems will be the same regardless; if some use is made of AC or something, that can go into the hypotheses. To me it seems pointlessly heavy to draw especial attention to the fact that “$Surj_{ETCS}$” and “$Surj_{SEAR}$” are the same damn thing, insofar as the subject matter of ETCS and SEAR is the same, just presented differently.
]]>I disfavor writing nLab articles according to checklists and pre-set molds. Personally I would find it very unpleasant both to write and to read articles which follow mechanical routines
That seems sensible. What is gained in “guidance” and structure by such a routine can easily be outweighed by the burdensome rigidity of it.
Most of the time, it seems to me, nLab articles are written in a more organic fashion: if one has something useful or interesting to say to get a ball rolling,
A lighweight ball that is probably easy to return is this: Set in its Section 2 quickly tries to dispel worries that this might not be “the” category of sets by a passage which seems to be saying that—under resonable conditions—all categories obtained via ETCS, MK, NBG, SEAR, ZFC are equivalent, in the category-theoretic sense. (Incidentally, isn’t this so essential that it deserves to be said even in Section 1 of Set, which after all allows itself to say more than only a “Definition”?)
Surj should probably try to do something similar, and hasten to say something about (what one might be tempted to call)
$Surj_{ETCS}$, $Surj_{MK}$, $Surj_{NBG}$, $Surj_{SEAR}$, $Surj_{ZF}$, $Surj_{ZF+AC_\omega}$, $Surj_{ZF+DC}$, $Surj_{ZFC}$.
The latter notations of course bring to mind the usual reformulations of AC via “pre”-inverses of surjections.
That is another set-theoretic issue that the article-to-be on $Surj$ should maybe quickly address; actually writing such a sweeping passage seems a difficult task though.
]]>To some extent we do this already, but a general problem there are too many “qualities” around for it to be reasonable to set benchmarks in advance, to be applied to each article whose title names a particular category.
I disfavor writing nLab articles according to checklists and pre-set molds. Personally I would find it very unpleasant both to write and to read articles which follow such mechanical routines “agreed upon” in advance, and so I can’t see myself ever agreeing to agree upon a set $Q_{CAT}$ and a set $Q_{sub}$.
Most of the time, it seems to me, nLab articles are written in a more organic fashion: if one has something useful or interesting to say to get a ball rolling, then one says it. For example, David Roberts said something interesting in #25. That alone could be a good start. (David? (-: )
]]>I’m not sure quite what I’d put into $Surj$ if it were me.
To me it seems natural to proceed as follows (this is, overtly—and perhaps overly—mechanical, but nowadays one should be able to pull off such an approach routinely, and it seems a valuable routine to boot, like an exercise or “benchmark”):
to agree upon
a set $\mathcal{Q}_{CAT}$ of (codified, well-studied) definitions of qualities of categories. (Preferably, each quality is in some sense “decidable” from the “usual” presentation of the category under consideration, at least for “sufficiently decidable” categories.) Basic examples of qualities: having, respectively, an initial object, a terminal object, all finite products, all exponentials, all pullbacks, all small limits, being rigid, or even the ill-defined quality of having-an-opposite-category-with-a-“usual name”, etc. I know that there are interdependencies among some of these qualities.
a set $\mathcal{Q}_{sub}$ of (codified, well-studied) definitions of qualities of embeddings of categories.
(Obvious examples: dense, full, reflective, wide, etc.)
a set $\mathcal{I}$ of implications of the form
Then analyse
for which qualities $Q\in\mathcal{Q}_{CAT}$ it follows that Surj has $Q$ because of an implication in $\mathcal{I}$
for which qualities $Q\in\mathcal{Q}_{CAT}$ it follows that Surj has $Q$ as if by fluke, i.e., in general not every category with is a subcategory of a $Q_0$-category via a $Q_1$-embedding has property $P_2$, but this subcategory $Surj$ happens to have $P_2$ nevertheless.
Only then try to prove whatever quality of Surj one would like to be sure of.
Maybe Surj is not complex enough to harbour any surprises when proceeding along such a road, but for some qualities I personally feel at a loss to give general reasons, and would have to resort to working from the definitions.
I expect this kind of analysis to have been done in published form on several occasions, perhaps not for $Surj$, but cannot find an example.
The ordering of the preorder reflection of Surj is what set theorists call ≤*. The axiom WISC has an equivalent statement (that works in any Boolean topos) due to François Dorais phrased almost entirely in terms of surjections (or epimorphisms):
for every set X there is a set Y such that for every surjection q of Z on X there is a function s from Y to Z such that qs is a surjection of Y onto X.
Edit: I guess this is really a statement about the fibration over Set with fibre over X the full subcategory of Set/X on the surjections: every fibre has a weakly initial object.
]]>I like $Surj$ myself. BTW, I take back what I said about $Inj$ in the discussion Rod pointed to: sometimes when a category has a standard collection of objects but one is not looking at the “default” morphisms, we do name the category after the morphisms. For example, we name the category of sets and relations $Rel$, the bicategory of categories and profunctors $Prof$, and so on. So $Inj$ and $Surj$ now seem fine to me.
I’m not sure quite what I’d put into $Surj$ if it were me. Some of these things like $Inj$ and $Surj$ have a combinatorial significance which could provide interesting material. I might start something stubby sometime in the next few days if no one else does.
]]>back in 2013 I started a thread about $Inj$ (not $Sur$). Nothing ever came of it but you might find some of the discussion there useful.
From the perspective of finding uses of the categories $Sur$ and $Inj$ (or maybe $Set_Sur$) in the nLab this is difficult now because with out explicit names search phrases (say “category set surjection”) turn up way to many hits.
]]>I think I’ve seen it called $Surj$.
]]>Thanks for the comments. This seems a very nice part of the literature, I will look into it.
Some (nLab-)technical remarks, strictly speaking off-topic (if topic is defined by this thread’s name), but clearly a natural outcome of the above discussion:
(It seems not to have one let alone a page of its own, as far as I can tell from the pages on functions, partial functions, the category of sets, etc).
If it indeed does not have a name, $\mathsf{Sur}$ would suggest itself.
It could perhaps be useful to have $\mathsf{Sur}$ treated systematically somewhere on the nLab, perhaps within some of the above pages.
By the way, I do agree with Todd’s point that you (Peter) would probably be interested in reading some algebraic set theory, particularly Joyal-Moerdijk’s original paper, where they identify “successor” operations such as $S \mapsto \{S\}$ and $S\mapsto S\cup \{S\}$ algebraically as endomaps of certain “free ZF-algebras”.
]]>Very useful comment, Mike; thanks.
]]>Ordinals make perfect sense constructively, but the notion of “limit ordinal” is indeed harder to define constructively, and also less useful, because however you define it it will no longer be the case that every ordinal is either a successor or a limit. Instead, when working with ordinals constructively you generally have to phrase your definitions so that they work for all ordinals with a single definition rather than splitting into successor/limit cases as is often done classically. For instance, when iterating an endofunctor $f$ of a complete poset transfinitely, classically one writes $X_{\alpha+1} = f(X_\alpha)$ for a successor and $X_{\alpha} = sup_{\beta\lt\alpha} X_{\beta}$ for a limit, whereas constructively we write $X_{\alpha} = sup_{\beta\lt\alpha} f(X_\beta)$ covering all cases at once.
]]>Again, algebraic set theory studies the recursive structures of set theory from a categorical perspective.
being a purely negative definition, via not being a successor
Certainly there are category theorists who have studied constructive or intuitionistic ordinal analysis; I am not one of them. (Maybe Toby Bartels has, but we don’t see him here as often as we used to.) I don’t know what other definitions are standardly studied, but off the top of my head one could try a, well, limit definition that would say more positively that limit ordinals are precisely fixed points of a certain ordinal operation, namely the one taking a von Neumann ordinal $\kappa$ to $\kappa \cup \{\alpha + 1: \alpha \lt \kappa\}$. (Equivalently, $\kappa$ is limit if $\alpha \lt \kappa$ implies $\alpha + 1 \lt \kappa$.) Classically I imagine that should be the same; constructively, I haven’t thought about it.
]]>So are you saying that perhaps one reason that von Neumann’s natural numbers are preferred to Zermelo’s is that von Neumann’s are categorically sensible
Yes, or rather: certainly some of the advantages of von Neumann’s definition can be usefully described with the help of category theory. (E.g., without the concept of “isomorphism in $\mathsf{Set}$” one would have to take recourse to saying things like “Zermelo’s definition looks like a tally language” or the like; with it, one can say that it remains within the isomorphism class of $\{\{\}\}$, or rather, iterates an essentially constant functor.)
I think there are deeper things to work out and say here, especially if one allows oneself to characterize the approaches of Zermelo and von Neumann via a mixture of set-theory and category-theory.
You bring up an important new point, namely to reverse the direction of the exposition and start from category-theoretic considerations, and clearly describe how von Neumann’s definition emerges from them.
I was about to write much more on this, but realized on several occasions that the discussion would quickly veer into where I still feel out of my depth. So I write only little.
Maybe it could be discussed at natural numbers, which is currently lacking any mention of either von Neumann’s or Zermelo’s definition
I agree that it would be nice to have a discussion of it in natural numbers, but this is a touchy subject, and I will not touch it for the moment.
An expository issue is that it is easy to make a mess of it and contradict oneself, e.g. when discussing categorical advantages of von Neumann’s definition, then progressing to ordinals, the total ordering on the class of all ordinals, and so on, then arriving at the concept of limit ordinals—the latter being a concept which could be abhorrent to many readers (being a purely negative definition, via not being a successor; at least this is how I was taught it).
A deeper issue is what the natural category is for $S\mapsto S\cup\{S\}$ to be an endofunctor of.
vs is one of $\mathsf{Set}$. But there is something unsatisfactory about vs.
There is something to be said for focusing on the wide subcategory of $\mathsf{Set}$ having only surjections as the morphisms. One issue with this is its lack of initial object (robbing one of a canonical point where to start iterating). I have more to say on this, but, as I said, have to learn some things more carefully before doing so.
]]>Another connection could be drawn to algebraic set theory where the basic operations are a successor operation $\sigma$ (which in this discussion is $IP$) and a small power set operation $P_s$ on a poset $V$. One defines membership $\epsilon$ by $S \epsilon T$ iff $\sigma(S) \leq T$.
]]>