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 nforum 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.
    • CommentAuthorEric
    • CommentTimeNov 3rd 2009

    Moved the definition of constant functor from cone to a new page constant functor.

    • CommentRowNumber2.
    • CommentAuthorEric
    • CommentTimeNov 3rd 2009

    Asked a question about notation at constant functor

    • CommentRowNumber3.
    • CommentAuthorPeter Heinig
    • CommentTimeJun 25th 2017

    Suggestion of an addition to constant functor, not important, and not to be carried out by myself: it might add a nice touch to constant functor to add a brief discussion why

    • constant functors are not an **** concept,
    • it is easy to accidentally define constant functors in an **** fashion, by requiring F(O 0)=F(O 1)F(O_0)=F(O_1) for all objects O 0O_0 and O 1O_1
    • even if defining constant functors in the usual non-**** way, the negation of the concept, i.e., the property of a functor to be non-constant seems (to me) an irredeemably **** concept,

    the latter giving an example that non-****-ness is not preserved under negation.

    This can be seen as a strawman-like argumentation, of course, first describing that someting can be done wrong (which is true for almost everything), and then pointing out that it has not been done wrongly.

    This is only to suggest a “sujet”, or to “select a target”, for another, more experienced, nLab author, not to say that this should be added to the constant functor.

    • CommentRowNumber4.
    • CommentAuthorMike Shulman
    • CommentTimeJun 26th 2017

    Actually those definitions are different in a subtle way that has nothing to do with evil: they give different answers to whether the identity functor of the empty category is constant. See constant function.

    • CommentRowNumber5.
    • CommentAuthorPeter Heinig
    • CommentTimeJun 26th 2017
    • (edited Jun 26th 2017)

    Thanks, did not know this aspect yet.

    So it seems that that constant function and constant function could instructively correspond with one another, but this would require experience, tact, time and possibly a type-theoretic touch.

    It seems to me that an illustrative elementary example is the endofunctor IPIP of Set\mathsf{Set} sending each set-map ff to the unique set map {dom(f)}IP(f){cod(f)}\{\mathrm{dom}(f)\}\overset{\mathrm{IP}(f)}{\rightarrow}\{\mathrm{cod}(f)\}.

    In particular it sends each set SS to the singleton {S}\{S\}. It is sometimes called indiscrete partition. I recently had occasion to discuss it, and was unsure what terms to use. IPIP is not a constant functor. But any two values of IPIP are isomorphic objects of Set\mathsf{Set}. So in that sense it is essentially constant. I was sort surprised how rarely the term essentially constant functor appears to be used. In particular, it is hardly ever used on the nLab.

    In a sense, IP\mathrm{IP} is a trivial but “pointed” example contrasting a set-theoretic with a category-theoretic point of view: from the former, it seems about as wrong as wrong can be to consider IP a “constant” “function” (in a sense it is set-theoretically essentially the identity function) while from the latter it is, to the contrary, category-theoretically essentially the constant function, essentially constant to the terminal object of the category, even though the members x 0x_0 and x 1x_1 of two values IP(x 0)IP(x 1)IP(x_0)\cong IP(x_1) can be arbitrarily complicated and different sets. One can see this as a reason to omit the topic, but I was recently more or less forced to consider this endofunctor by a larger machinery.

    Would you consider calling IP\mathrm{IP} an “essentially constant functor” (in analogy with e.g. “essentially surjective” functors) acceptable?

    • CommentRowNumber6.
    • CommentAuthorMike Shulman
    • CommentTimeJun 26th 2017

    Sure, “essentially constant functor” seems like a reasonable terminology. I am surprised if there is any reason to consider your IPIP as a functor, though, since as you say categorically it is uninteresting. Can you say anything brief about in what context it arose?

    • CommentRowNumber7.
    • CommentAuthorMike Shulman
    • CommentTimeJun 26th 2017

    I added some remarks to constant functor.

    • CommentRowNumber8.
    • CommentAuthorPeter Heinig
    • CommentTimeJun 27th 2017
    • (edited Jun 28th 2017)

    Can you say anything brief about in what context it arose?

    In the context of endofunctors of Set\mathsf{Set}.

    This is a rather tautological answer to your question though; in slightly more detail: in a systematic analysis of certain objects with neither left nor right adjoints of the functor category Set Set\mathsf{Set}^{\mathsf{Set}}. Incidentally, IP quite evidently does not have a right-adjoint, despite passing the terminal-object-preservation-test (as it takes singletons to singletons). Saying more would be a bit lengthy, and in particular would require more care on my part, so as to not make false statements, since I have not double checked some of my arguments yet

    EDIT: in the above, the “despite” is sort-of-wrong, of course.

    • CommentRowNumber9.
    • CommentAuthorTodd_Trimble
    • CommentTimeJun 27th 2017

    The necessary condition for a functor to have a right adjoint is that it preserves colimits, not that it preserves limits such as the terminal object.

    Of course this functor, being naturally isomorphic to the constant functor Set!1*SetSet \stackrel{!}{\to} 1 \stackrel{\ast}{\to} Set (*\ast being any terminal object), has a left adjoint which is Set!1SetSet \stackrel{!}{\to} 1 \stackrel{\emptyset}{\to} Set, the constant functor at the empty set which is the initial object.

    • CommentRowNumber10.
    • CommentAuthorMike Shulman
    • CommentTimeJun 27th 2017

    Let me say what I meant more explicitly: what led you to consider your functor IP as distinct from the constant functor at a one-element set? Having a left or right adjoint is a “categorical” property of a functor (invariant under natural isomorphism), so if that’s the only question you’re asking about functors, then there is no reason to consider any functor that’s essentially constant at a one-element set as different from any other such functor.

    • CommentRowNumber11.
    • CommentAuthorPeter Heinig
    • CommentTimeJun 28th 2017
    • (edited Jun 28th 2017)

    The necessary condition for a functor to have a right adjoint is that it preserves colimits, not that it preserves limits such as the terminal object.

    Thanks for correcting. I misspoke within the concessive clause in #8, mixing up the two criteria, despite knowing the principles behind these criteria. (Probably the reason was haste, exacerbated by the being-a-right-adjoint-versus-having-a-right-adjoint-issue.) Needless to say, the claim that IP does not have a right-adjoint is correct, for example since IP maps the terminal (CORRECTED: initial) object to an object not isomorphic to it.

    what led you to consider your functor IP as distinct from the constant functor at a one-element set?

    What led me to it, was, inter alia, having had to discuss and compare Zermelo’s and von Neumann’s models of the natural numbers.

    Zermelo modelled the natural numbers by iterates of the indiscrete-partition-endofunctor.

    (Or so I was often told; I never saw an original article of Zermelo where he does so.)

    If one would look at Zermelo’s construction purely categorically, it would never get off the ground (or, more precisely, only make it to height 11).

    • Zermelo modelled the natural numbers by iterating a non-constant essentially-constant endofunctor of Set\mathsf{Set}.

    • Von Neumann modelled the natural numbers by iterating a non-(essentially-constant), or rather, essentially non-constant, endofunctor of Set\mathsf{Set}. (The successor operation.)

      Some details, probably needlessly.

      Zermelo (is said to have) modelled the natural nubmers by the iterates o=IP 0(o),{o}=IP 1(o),{{o}}=IP 2(o),...\text{o} = IP^0(o), \{o\} = IP^1(o), \{\{o\}\} = IP^2(o),... of IPIP, for brevity called zermelos, while von Neumann in a letter to Zermelo from the 1920s, which I did see, modelled the natural numbers by the iterates o=vs 0(o),{o}=vs 1(o),{o,{o}}=vs 2(o)o = vs^0(o), \{o\} = vs^1(o), \{ o , \{o\} \} = vs^2(o) of the endofunctor vsvs defined below.

    (Here oo could be taken to be any set, but usually one takes oo to mean the empty set.)

    Nowadays, zermelos appear to be deemed worse than von Neumann’s naturals in various well-known ways (zermelos larger than 11 are not transitive sets, a zermelo larger than 11 does not have the cardinality of the number it is intended to model, zermelos larger than 00 are all isomorphic objects of Set\mathsf{Set}). Von Neumann’s naturals do not have any of these defects.

    We happend to have IP 0(o)=Vs 0(o)IP^0(o)=Vs^0(o) and IP 1(o)=Vs 1(o)IP^1(o)=Vs^1(o), the agreement of the first iterates being somewhat irritating, but IP k(o)IP^k(o) and Vs k(o)Vs^k(o) disagree ever after; and not only are they unequal, but even non-isomorphic ever after, which in Set\mathsf{Set} of course is equivalent to having unequal cardinalities.

    None of the Zermelo natural numbers larger than 11 is a transitive set. (For example, 2 Zermelo={{o}}2_{\mathrm{Zermelo}} = \{\{o\}\} has the element 1={o}1=\{o\}, but it does not have 11 as a subset, whereas 2 vonNeumann={o,{o}}2_{\mathrm{von Neumann}}=\{ o , \{o\} \} has 11 both as an element and as a subset.)

    Definition (the endofunctor vsvs). Let vsvs consist of the class-function Ob(Set)Ob(Set)\mathrm{Ob}(\mathsf{Set})\rightarrow\mathrm{Ob}(\mathsf{Set})

    which sends any set SS to the set (S)vs:=S{S}(S)vs := S\cup\{S\},

    together with the class-function Mor(Set)Mor(Set)\mathrm{Mor}(\mathsf{Set})\rightarrow\mathrm{Mor}(\mathsf{Set})

    which sends any set-map ff to the set-map

    with

    (f)vs(x):=f(x)\dom(f)\cup\{\dom(f)\} \xrightarrow[](f)vs (x) := f(x) for each xSx\in S, and (f)vs(S):=cod(f)(f)vs(S) := \cod(f).

    Remark. The argument of vsvs is purposefully written to the left of the functor’s name.

    Remark. The tempting definition of letting vs(f)(S)vs(f)(S) be f *(S)f_\ast(S), where f *f_\ast denotes the usual direct-image function 𝒫(dom(f))𝒫(cod(f))\mathcal{P}(\dom(f))\rightarrow\mathcal{P}(\cod(f)), would not result in a functor, since then for non-surjective maps ff one has (f)vs(S)cod(f)(f)vs(S)\neq\cod(f), so then (f)vs(S)(f)vs(S) is not an element of cod(f){cod(f)}\cod(f)\cup\{\cod(f)\}.

    Remark. With the alternative definition of letting (f)vs(S)(f)vs(S) be f *(S)f_\ast(S), we would get an endofunctor of the wide subcategory of Set\mathsf{Set} consisisting of surjections only. This subcategory does not have an initial object.

    Remark. With the above definition, vsvs is an endofunctor of Set\mathsf{Set}, since it is clear that for any set SS we have vs(1 S)=1 (S)vs=1 S{S}vs(1_S) = 1_{ (S)vs } = 1_{S\cup\{S\}}, and it can be calculated that for arbitrary set-maps we have an equality of set-maps (f 0f 1)vs=((f 0)vs)((f 1)vs)S_2\xrightarrow[](f_0\circ f_1)vs = ((f_0)vs)\circ((f_1)vs).

    Remark. vsvs does neither have a left nor a right adjoint, and this already follows from the trivial necessary conditions of having to preserve terminal resp. initial objects, because vsvs increments the cardinality of its argument. More precisely, no extension of the class-function vs:Ob(Set)Ob(Set)vs\colon\Ob(\mathsf{Set})\rightarrow\Ob(\mathsf{Set}) to an endofunctor of Set\mathsf{Set} can ever have a left or a right adjoint, already for the said reasons.

    • CommentRowNumber12.
    • CommentAuthorTodd_Trimble
    • CommentTimeJun 28th 2017
    • (edited Jun 28th 2017)

    Needless to say, the claim that IP does not have a right-adjoint is correct, for example since IP maps the terminal object to an object not isomorphic to it.

    Of course it doesn’t have a right adjoint (i.e., it isn’t a left adjoint), but (1) this can’t be the reason for it, since typically left adjoints don’t preserve the terminal object, and (2) what do you mean IPIP maps the terminal object to an object not isomorphic to it? Isn’t every value of IP a singleton and therefore terminal (you said so yourself in #8)?

    (Maybe you meant to say “initial” instead of “terminal”?)

    As for “vsvs”: a category-theorist wouldn’t particularly care how it’s coded up in ZFC, but as an endofunctor it takes a set SS to S+1S + 1, the coproduct of SS with a terminal object 11. A natural numbers object is by definition the initial algebra of that endofunctor.

    • CommentRowNumber13.
    • CommentAuthorPeter Heinig
    • CommentTimeJun 28th 2017

    what do you mean IPIP maps the terminal object to an object not isomorphic

    Simply chose the wrong word; I meant to write

    • IP maps the initial object to an object not isomorphic to it

    an intention which is somewhat visible from the somewhat-wrong definite article “the” in my “the terminal object”. (Needless to say, in Set\mathsf{Set} there is only generalized-the terminal object.

    • CommentRowNumber14.
    • CommentAuthorMike Shulman
    • CommentTimeJun 28th 2017

    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 (as Todd says, they arise from the endofunctor whose initial algebra is the categorical natural numbers object) whereas Zermelo’s are not? I think that’s an interesting observation. Maybe it could be discussed at natural numbers, which is currently lacking any mention of either von Neumann’s or Zermelo’s definition, with a short pointer from constant functor?

    • CommentRowNumber15.
    • CommentAuthorTodd_Trimble
    • CommentTimeJun 29th 2017

    Another connection could be drawn to algebraic set theory where the basic operations are a successor operation σ\sigma (which in this discussion is IPIP) and a small power set operation P sP_s on a poset VV. One defines membership ε\epsilon by SεTS \epsilon T iff σ(S)T\sigma(S) \leq T.

    • CommentRowNumber16.
    • CommentAuthorPeter Heinig
    • CommentTimeJun 29th 2017
    • (edited Jun 29th 2017)

    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 Set\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 SS{S}S\mapsto S\cup\{S\} to be an endofunctor of.

    vs is one of Set\mathsf{Set}. But there is something unsatisfactory about vs.

    There is something to be said for focusing on the wide subcategory of Set\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.

    • CommentRowNumber17.
    • CommentAuthorTodd_Trimble
    • CommentTimeJun 29th 2017
    • (edited Jun 29th 2017)

    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 κ{α+1:α<κ}\kappa \cup \{\alpha + 1: \alpha \lt \kappa\}. (Equivalently, κ\kappa is limit if α<κ\alpha \lt \kappa implies α+1<κ\alpha + 1 \lt \kappa.) Classically I imagine that should be the same; constructively, I haven’t thought about it.

    • CommentRowNumber18.
    • CommentAuthorMike Shulman
    • CommentTimeJun 30th 2017

    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 ff of a complete poset transfinitely, classically one writes X α+1=f(X α)X_{\alpha+1} = f(X_\alpha) for a successor and X α=sup β<αX βX_{\alpha} = sup_{\beta\lt\alpha} X_{\beta} for a limit, whereas constructively we write X α=sup β<αf(X β)X_{\alpha} = sup_{\beta\lt\alpha} f(X_\beta) covering all cases at once.

    • CommentRowNumber19.
    • CommentAuthorTodd_Trimble
    • CommentTimeJun 30th 2017

    Very useful comment, Mike; thanks.

    • CommentRowNumber20.
    • CommentAuthorMike Shulman
    • CommentTimeJun 30th 2017

    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{S}S \mapsto \{S\} and SS{S}S\mapsto S\cup \{S\} algebraically as endomaps of certain “free ZF-algebras”.

    • CommentRowNumber21.
    • CommentAuthorPeter Heinig
    • CommentTimeJun 30th 2017
    • (edited Jun 30th 2017)

    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:

    • Does the wide subcategory of Set\mathsf{Set} consisting precisely of the surjective set-maps have something like an official nLab name?

    (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, Sur\mathsf{Sur} would suggest itself.

    • It could perhaps be useful to have Sur\mathsf{Sur} treated systematically somewhere on the nLab, perhaps within some of the above pages.

      • If a list of basic properties of Sur\mathsf{Sur} indeed does not exist on the nLab (which still seems unlikely), I would perhaps like to do so in the near future,but it might be more efficient for someone else with more experience to do so, especially if he or she can give the “right” general reason for this or that property to hold or not to hold, mostly arguing from known categorical properties of Set\mathsf{Set}. I do not recall to have seen Sur\mathsf{Sur} been treated per se in textbooks, although it still seems likely that this is a standard exercise. Many basic properties of Sur\mathsf{Sur} are straightforward to work out, especially since elements are available, but it might be better to tap existing expertise and better methods to compile a list of properties of Sur\mathsf{Sur}. This is not to ask for a list of its properties to be given to me now. It is only to suggest some contribution to the nLab, and plan how to construct it before setting out to do so.
    • CommentRowNumber22.
    • CommentAuthorMike Shulman
    • CommentTimeJun 30th 2017

    I think I’ve seen it called SurjSurj.

    • CommentRowNumber23.
    • CommentAuthorRodMcGuire
    • CommentTimeJun 30th 2017

    back in 2013 I started a thread about InjInj (not SurSur). Nothing ever came of it but you might find some of the discussion there useful.

    nforum: power set & Inj

    From the perspective of finding uses of the categories SurSur and InjInj (or maybe Set SurSet_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.

    • CommentRowNumber24.
    • CommentAuthorTodd_Trimble
    • CommentTimeJun 30th 2017

    I like SurjSurj myself. BTW, I take back what I said about InjInj 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 RelRel, the bicategory of categories and profunctors ProfProf, and so on. So InjInj and SurjSurj now seem fine to me.

    I’m not sure quite what I’d put into SurjSurj if it were me. Some of these things like InjInj and SurjSurj 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.

    • CommentRowNumber25.
    • CommentAuthorDavidRoberts
    • CommentTimeJun 30th 2017
    • (edited Jun 30th 2017)

    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.

    • CommentRowNumber26.
    • CommentAuthorPeter Heinig
    • CommentTimeJul 1st 2017
    • (edited Jul 1st 2017)

    I’m not sure quite what I’d put into SurjSurj 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 𝒬 CAT\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 𝒬 sub\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

        • if η:CD\eta\colon\mathsf{C}\hookrightarrow\mathsf{D} is an embedding of categories, and if Q 0𝒬 CATQ_0\in\mathcal{Q}_{CAT}, and if D\mathsf{D} is a Q 0Q_0-category, and if Q 1𝒬 subQ_1\in\mathcal{Q}_{sub}, and if η\eta is a Q 1Q_1-embedding, and if Q 2𝒬 CATQ_2\in\mathcal{Q}_{CAT}, then C\mathsf{C} necessarily is a Q 2Q_2-category.

      Then analyse

    • for which qualities Q𝒬 CATQ\in\mathcal{Q}_{CAT} it follows that Surj has QQ because of an implication in \mathcal{I}

    • for which qualities Q𝒬 CATQ\in\mathcal{Q}_{CAT} it follows that Surj has QQ as if by fluke, i.e., in general not every category with is a subcategory of a Q 0Q_0-category via a Q 1Q_1-embedding has property P 2P_2, but this subcategory SurjSurj happens to have P 2P_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 SurjSurj, but cannot find an example.

    • CommentRowNumber27.
    • CommentAuthorTodd_Trimble
    • CommentTimeJul 1st 2017

    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 CATQ_{CAT} and a set Q subQ_{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? (-: )

    • CommentRowNumber28.
    • CommentAuthorPeter Heinig
    • CommentTimeJul 1st 2017
    • (edited Jul 1st 2017)

    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 ETCSSurj_{ETCS}, Surj MKSurj_{MK}, Surj NBGSurj_{NBG}, Surj SEARSurj_{SEAR}, Surj ZFSurj_{ZF}, Surj ZF+AC ωSurj_{ZF+AC_\omega}, Surj ZF+DCSurj_{ZF+DC}, Surj ZFCSurj_{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 SurjSurj should maybe quickly address; actually writing such a sweeping passage seems a difficult task though.

    • CommentRowNumber29.
    • CommentAuthorTodd_Trimble
    • CommentTimeJul 1st 2017

    That section 2 of Set is pretty circular actually (for instance, “locally small” depends on a background notion of SetSet), 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 SetSet satisfy CH, some don’t.) So there is no one “SetSet”, although the section does explain how to characterize SetSet among categories considered against the background theory.

    Also, not everyone would even agree that SetSet 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 “SetSet”.

    Surj ETCSSurj_{ETCS}, Surj MKSurj_{MK}, Surj NBGSurj_{NBG}, Surj SEARSurj_{SEAR}, Surj ZFSurj_{ZF}, Surj ZF+AC ωSurj_{ZF+AC_\omega}, Surj ZF+DCSurj_{ZF+DC}, Surj ZFCSurj_{ZFC}

    Personally, I’d avoid writing all that. Since we agree that there is no one SurjSurj pretty much to the same extent as there is no one SetSet: whatever category one is calling SetSet, there is a well-defined notion of surjection, and SurjSurj is simply understood relative to that SetSet. 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 ETCSSurj_{ETCS}” and “Surj SEARSurj_{SEAR}” are the same damn thing, insofar as the subject matter of ETCS and SEAR is the same, just presented differently.

    • CommentRowNumber30.
    • CommentAuthorTodd_Trimble
    • CommentTimeJul 1st 2017

    So here would be a sample theorem written according to the style I personally favor.

    Theorem: Assuming the axiom of choice, every functor F:SetSetF: Set \to Set maps surjections to surjections, i.e., restricts to a functor SurjSurjSurj \to Surj.

    Proof: If p:EBp: E \to B is a surjection, then it admits a section s:BEs: B \to E according to the axiom of choice. From ps=1 Bp s = 1_B and functoriality, we have F(p)F(s)=1 FBF(p) F(s) = 1_{F B}, so F(p)F(p) is a retraction and therefore a surjection.

    • CommentRowNumber31.
    • CommentAuthorMike Shulman
    • CommentTimeJul 1st 2017

    whatever category one is calling SetSet, there is a well-defined notion of surjection, and SurjSurj is simply understood relative to that SetSet

    Which is equally true with “surjection” replaced by any other object of mathematics: group, ring, field, topological space, etc.

    • CommentRowNumber32.
    • CommentAuthorDavidRoberts
    • CommentTimeJul 5th 2017

    Todd #27

    I hear you. I plan to do something next week about this.

    • CommentRowNumber33.
    • CommentAuthorDavidRoberts
    • CommentTimeJul 11th 2017

    I made some edits at surjection incorporating #25.

    • CommentRowNumber34.
    • CommentAuthorMike Shulman
    • CommentTimeJul 11th 2017

    Thanks! I put in a section heading, since it’s not part of the definition of surjection.

    One also writes *|A|\empty \leq^* |A| for all sets AA, but this is a standalone definition, and doesn’t follow from a construction on SurjSurj.

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

    • CommentRowNumber35.
    • CommentAuthorDavidRoberts
    • CommentTimeJul 11th 2017

    @Mike: sure, using subquotients, which give, in the presence of LEM, an equivalent preorder to *\leq^* as defined in the piecemeal fashion.

    • CommentRowNumber36.
    • CommentAuthorMike Shulman
    • CommentTimeJul 11th 2017

    Good. I think we should give that definition, then, not the piecemeal one.

    • CommentRowNumber37.
    • CommentAuthorDavidRoberts
    • CommentTimeJul 12th 2017

    Did so, but left the set-theorists one in, but clarified how they are related.

    • CommentRowNumber38.
    • CommentAuthorMike Shulman
    • CommentTimeJul 12th 2017

    Thanks! I did some editing; in particular I removed the piecewise proof that BAB\le A implies B *AB \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=B=\emptyset is the same as “BB is not inhabited” even constructively.)