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).
    • CommentRowNumber1.
    • CommentAuthorRichard Williamson
    • CommentTimeMar 2nd 2018
    • (edited Mar 2nd 2018)

    Following from the discussion begun here, I thought I’d air a few simple ideas on how one might construct a ’free co-completion’ internally to a 2-category, without referring to a category of sets (the idea being that one could then define Set\mathsf{Set} to be the free co-completion of 11). I’ll try to add details gradually, but I thought I’d just share the ideas anyway; maybe people can develop them or see problems quicker than I will.

    So suppose that we have some 22-category CC (a prototypical example being CAT\mathsf{CAT}) with an object cc which we’ll think of as analogous to Cat\mathsf{Cat} in CAT\mathsf{CAT}. Let aa be some other object of CC. I wish to define the free co-completion of aa with respect to cc.

    To get some idea for what we should do, consider a functor F:D𝒜F : D \rightarrow \mathcal{A} between categories. How do we freely construct a colimit of FF in 𝒜\mathcal{A}? Well, it seems to me that we should be able to proceed by first forming the category CoCone\mathsf{Co-Cone} of co-cones of FF, and then formally add an initial object. The category of co-cones of FF is of course a certain comma category, i.e. a 2-limit in CAT\mathsf{CAT}. Adding an initial object is a certain 2-colimit in CAT\mathsf{CAT}, if I am not mistaken. Thus, for an individual functor, it seems that we can construct a free colimit of it internally to a 2-category.

    What we now need to do is to carry out this construction for all functors at once. In other words, we should apply some construction to the slice category Cat/𝒜\mathsf{Cat} / \mathcal{A} (which is again a certain 2-limit) which on objects recovers the construction of the previous paragraph. I don’t see any significant problems with doing this, but I’ll stop here for now.

    Thoughts very welcome!

    • CommentRowNumber2.
    • CommentAuthorMike Shulman
    • CommentTimeMar 2nd 2018

    It doesn’t seem to me to solve any problems if you define SetSet but assuming from the start that you’re given CatCat. I would want instead to characterize SetSet as a free cocompletion with respect to some given class of “small weights” in CC, either two-sided fibrations or proarrows in an equipment.

    • CommentRowNumber3.
    • CommentAuthorRichard Williamson
    • CommentTimeMar 3rd 2018
    • (edited Mar 3rd 2018)

    My thinking was that one is only allowed to use purely 2-categorical means to treat Cat/𝒜\mathsf{Cat} / \mathcal{A}, so that one could replace Cat\mathsf{Cat} by any sufficiently nice CC (or maybe any CC at all). The significance of Cat\mathsf{Cat} is only that in this case we should recover something which is exactly the classical free co-completion.

    Also, my feeling was that in a categorical foundations, it is reasonable to assume that one has universes, i.e. a copy of CAT\mathsf{CAT} living inside CAT\mathsf{CAT}, which we call Cat\mathsf{Cat} (and obviously there could be further levels if needed). Indeed, my thought is that one has to have some kind of universe if one is to get something like Set\mathsf{Set}: one cannot get something from nothing.

    As a third thought, for me at least, it would be interesting to have a purely 2-categorical treatment of free co-completion, even if it does not fully solve the kind of problem we are discussing.

    Thus I am very interested to understand your suggested characterisation. It may well improve significantly on what I have just described, and I would like to understand how! Would you be able to elaborate?

    • CommentRowNumber4.
    • CommentAuthorTodd_Trimble
    • CommentTimeMar 3rd 2018

    For what it’s worth, for many years I’ve wanted to explore the semantics of what I’ve called “epistemologies”, which essentially takes free cocompletion as basic. The basic set-up is a bicategory B\mathbf{B} (understood as playing a role of bicategory of enriched categories and bimodules/profunctors) for which the inclusion i:Ladj(B)Bi: Ladj(\mathbf{B}) \hookrightarrow \mathbf{B} of the subbicategory consisting of objects of B\mathbf{B}, left adjoint 1-cells, and 2-cells between them, has a right biadjoint p:BLadj(B)p: \mathbf{B} \to Ladj(\mathbf{B}), or better yet a Kock-Zoeberlein right biadjoint. I call a B\mathbf{B} with this property a potent bicategory. Here Ladj(B)Ladj(\mathbf{B}) is understood as playing a role of enriched categories and functors, and the monad pip i plays the role of a free cocompletion.

    Things get more and more interesting when we put more assumptions on B\mathbf{B}. For example, if B\mathbf{B} has a compact closed structure (in the bicategorical sense), then the object v=pi(1)v = p i(1), the free cocompletion of the monoidal unit, really does play a role of base of enrichment, and one can develop formal enriched category theory in this context. If B\mathbf{B} is moreover a cartesian bicategory, then I think things get more interesting still.

    I had wondered for a long time whether we could get an interesting semantics for potent compact closed cartesian bicategories by looking at the examples of “small complete small categories” in realizability toposes as possible bases of enrichment. Mike seemed to think this ought to work. I regret letting that discussion drop!

    • CommentRowNumber5.
    • CommentAuthorMike Shulman
    • CommentTimeMar 4th 2018

    My point was that if you’re going to assume universes anyway, what’s the point of assuming CatCat but not assuming SetSet?

    • CommentRowNumber6.
    • CommentAuthorRichard Williamson
    • CommentTimeMar 4th 2018
    • (edited Mar 4th 2018)

    Todd: interesting, thanks! I definitely think just taking free co-completion as basic is reasonable and promising as well.

    Mike: ah, I see, thanks for the clarification. My feeling was that there is a big difference between assuming Cat\mathsf{Cat} and assuming Set\mathsf{Set} in a categorical foundations (where by this I mean here one in which categories are primitive). I.e. if one is axiomatising the 2-category of categories, I think it is reasonable to have ’copies’ of that same axiomatisation living inside one another. To me it is actually not at all obvious that one easily get Set\mathsf{Set} given such a universe. If one is axiomatising Set\mathsf{Set} as well, then I would think that it is probably not a categorical foundations (in the same sense as I clarified in the earlier paranthesis) any more. On the other hand, it could be that Todd’s approach is better than the one I suggested, where one takes free co-completion more or less as primitive. But I’d be interested to know what kind of characterisation you had in mind.

    • CommentRowNumber7.
    • CommentAuthorMike Shulman
    • CommentTimeMar 5th 2018

    To me it makes much more sense to have SetSet as an object of the 2-category of categories than it does to have CatCat. For one thing, CatCat is really a 2-category, not a category, hence not really an object of the 2-category of categories but rather the 3-category of 2-categories.

    I think it should be fairly easy to obtain SetSet from CatCat as the discrete objects, e.g. those that are right orthogonal to 212\to 1.

    What I had in mind was a universal characterization of SetSet relative to a class of small profunctors, as in section 10 of this paper.

    • CommentRowNumber8.
    • CommentAuthorRichard Williamson
    • CommentTimeMar 5th 2018
    • (edited Mar 5th 2018)

    To me it makes much more sense to have SetSet as an object of the 2-category of categories than it does to have CatCat. For one thing, CatCat is really a 2-category, not a category, hence not really an object of the 2-category of categories but rather the 3-category of 2-categories.

    I see your point. I’m not completely sure I agree, because I think small categories as objects of a 1-category only are quite fundamental (Indeed the very thing we are discussing here, namely for formulating the notion of a diagram, is an example). I think if one had Set\mathsf{Set}, one would probably need to build Cat\mathsf{Cat}. But probably one could indeed build a perfectly good theory with Set\mathsf{Set} axiomatised one way or another, and maybe that it is indeed preferable.

    I think it should be fairly easy to obtain SetSet from CatCat as the discrete objects, e.g. those that are right orthogonal to 212\to 1.

    That’s interesting. My feeling was that it was not obvious how to do this, thanks for the suggestion of how to do it. I had not considered right orthogonality as part of the axiomatic setup I had in mind, but maybe it should be there.

    An interesting question (for me) would be whether we can show (or what we need to be able to show) that Set\mathsf{Set} defined in this way is the free co-completion of 11. Maybe one would end up needing something like the construction I was getting at in #1.

    What I had in mind was a universal characterization of SetSet relative to a class of small profunctors, as in section 10 of this paper.

    This looks interesting. I have not really digested it yet, but it may well be that this kind of thing would be much more interesting and useful than the construction I was getting at, which is after all rather simplistic.