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 comma 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 finite 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 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.
    • CommentAuthorDavid_Corfield
    • CommentTimeSep 11th 2021

    Thought I’d start something in the hope that experts will say more.

    v1, current

    • CommentRowNumber2.
    • CommentAuthorTim_Porter
    • CommentTimeSep 11th 2021

    David. Have you seen this?

    • CommentRowNumber3.
    • CommentAuthorDavid_Corfield
    • CommentTimeSep 11th 2021

    Thanks. Have added that in, and some more comments.

    diff, v2, current

    • CommentRowNumber4.
    • CommentAuthorvarkor
    • CommentTimeOct 9th 2021

    Mention KZ doctrines and remove duplicate link.

    diff, v4, current

    • CommentRowNumber5.
    • CommentAuthorUrs
    • CommentTimeOct 13th 2021
    • (edited Oct 13th 2021)

    I have edited this entry a fair bit:

    Have touched the original text to make it flow better (I hope) and added some crucial cross-links, such as with ETCC and with 2-topos.

    Then I added paragraphs on how:

    • in one direction, this “formal category theory” is the categorification of the discussion of set theory via the topos of sets,

    • while, in the other direction, it further categorifies to the untrodden territory of formal \infty-category theory seen in the full (,2)(\infty,2)-topos Cat (,1)Cat_{(\infty,1)}

    • which however is already interesting in Verity & Riehl’s “formal \infty-category theory” seen in “just” 2Ho(Cat (,1))2Ho\big( Cat_{(\infty,1)}\big),

    • (which, at least for the case of presentable \infty-categories, is accessible already as 2Ho(ComModCat).)

    As one source I found for exactly this terminology, I added pointer to:

    diff, v5, current

    • CommentRowNumber6.
    • CommentAuthorUrs
    • CommentTimeMay 8th 2022

    added publication data and hyperlinks to:

    diff, v8, current

    • CommentRowNumber7.
    • CommentAuthorvarkor
    • CommentTimeMay 8th 2022

    Formal category theory should be taken to be an axiomatisation of the properties of VCat, not Cat. This is an important distinction, because Cat has some unusual structure that is not enjoyed more generally by 2-categories of enriched categories. In particular, it has a “nice” Yoneda structure (i.e. it satisfies Axiom 3* of Street and Walters). Therefore, I don’t think it’s accurate to say that formal category theory is directly related to 2-topos theory, because the evidence suggests that only nice Yoneda structures form 2-toposes (as studied by Weber). I haven’t made any changes accordingly yet, because I want to leave this open for discussion, but I think it’s a subtle but important point.

    • CommentRowNumber8.
    • CommentAuthorUrs
    • CommentTimeMay 8th 2022

    Why not consider adding demand for nice Yoneda structure to the axioms of formal category theory?

    • CommentRowNumber9.
    • CommentAuthorvarkor
    • CommentTimeMay 8th 2022

    Because then you don’t capture 2-categories of enriched categories for most bases of enrichment, which is a motivating class of examples. Nice Yoneda structures are generally those arising from internal categories, which tend to be “better behaved” than enriched categories.

    • CommentRowNumber10.
    • CommentAuthorUrs
    • CommentTimeMay 8th 2022

    Maybe what you really want to do is add to the entry a line saying that there is an extra axiom which one may add to reduce formal category theory of general enriched categories to that of SetSet-enriched categories.

    • CommentRowNumber11.
    • CommentAuthorvarkor
    • CommentTimeMay 9th 2022

    I’ll try to figure out a clear way to put it and update the page accordingly.

    • CommentRowNumber12.
    • CommentAuthorDavid_Corfield
    • CommentTimeOct 18th 2022

    Added a reference

    diff, v10, current

    • CommentRowNumber14.
    • CommentAuthormaxsnew
    • CommentTimeOct 18th 2022

    Thanks for the reference.

    It’s not clear to me what the line between formal category theory and synthetic category theory is (if there even is one). Dan and I were calling our proofs “synthetic” until recently when we changed the name to emphasize the continuity with prior work.

    • CommentRowNumber15.
    • CommentAuthorJohn Baez
    • CommentTimeOct 12th 2023

    Added overview by Nathaniel Arkor (on non-public portion of the Category Theory Community Server, so not easily citable).

    diff, v14, current

    • CommentRowNumber16.
    • CommentAuthorUrs
    • CommentTimeOct 12th 2023
    • (edited Oct 12th 2023)

    I have adjusted the wording and fixed formatting, referencing and hyperlinking of the new material.

    Notice that the first new paragraph was essentially a duplicate of what the entry already had under “Details”. I have merged this.

    diff, v15, current

    • CommentRowNumber17.
    • CommentAuthorDavid_Corfield
    • CommentTimeOct 12th 2023

    Added

    diff, v17, current

    • CommentRowNumber18.
    • CommentAuthorRoald
    • CommentTimeOct 12th 2023
    The following is a comment on Nathanael's comment "Technically, augmented virtual equipments generalise virtual equipments, but it is not clear that there are examples captured by the former that cannot be captured by the latter by making appropriate modifications." in the overview of [15].

    I came up with augmented virtual double categories mostly for "book-keeping" purposes. For example the formal notion of a Yoneda morphism y: A -> PA in an augmented virtual double category does not require first specifying a class of "admissible morphisms", like a Yoneda structure on a 2-category does. In an augmented virtual double category one simply regards all horizontal morphisms as admissible; a vertical morphism is then admissible iff it has a companion and an object is admissible iff it has a horizontal unit. I don't see how this can be (smoothly) done in a virtual double category. And this goes quite far: (roughly) one can define an object A to be "formally small" whenever all composites of horizontal morphisms X -|-> A and A -|-> Y exist and prove that presheaf objects PA are cocomplete with respect to that formal notion of smallness.

    Also I wouldn't be surprised if Nathanael's assessment is correct. Roughly, I guess that in the end augmented virtual double categories are to unital virtual double categories somewhat like semicategories are to categories and that, like in the latter case, any augmented virtual double category can be turned into a unital virtual double category by adding in horizontal units. But like semicategories, double categories without horizontal units do appear naturally (see e.g. Prop. 8.1.6 of Riehl and Verity's Elements of infinity-category theory), so also in this sense using the augmented notion might be more natural.

    Let me finish by adding that to me the advantages of using a virtual equipment over a 2-category with Yoneda structure, for formal category theory, are clear. For instance a Yoneda morphism y: A -> PA in the former induces an equivalence of the slice categories of horizontal morphisms A -|-> B and vertical morphisms B -> PA and I don't know how to obtain something similar using the Yoneda morphisms of a Yoneda structure (especially without requiring further structure).
    • CommentRowNumber19.
    • CommentAuthorvarkor
    • CommentTimeOct 13th 2023

    I don’t feel the message in the Category Theory Zulip server was entirely suited to placing wholesale on the nLab, as it was intended specifically as a response to someone who wanted a starting point for learning about formal category theory. In particular, there is often a trade-off between the simplicity of an approach, and its expressivity. For instance, (augmented) virtual equipments are more complicated structures than proarrow equipments, but are also much more expressive (for instance, in capturing enriched category theory without assumptions on the base of enrichment). So if one wishes to work very generally, it is better to work in the (augmented) virtual setting, and it seems reasonable to suggest these approaches to someone learning formal category theory.

    However, the trade-off between virtual equipments and augmented virtual equipments is a little more subtle since, from what I have understood, many of the natural examples of augmented virtual equipments naturally reside inside a larger (non-augmented) virtual equipment (e.g. for instance, (Set, Set’)-Prof resides within Set’-Prof). So here the trade-off has a different flavour, less about examples, and more about simplicity of definitions and proofs: a prime example being the additional complexity of an augmented virtual double category, versus the simplicity of admissibility in that setting (an analogous development in a virtual equipment necessitating specifying some class of admissible proarrows).

    Really it would be helpful to rework this nLab page entirely and give a more detailed introduction to these ideas and their trade-offs. Perhaps I shall find the time to do so. Part of the difficulty is that any such discussion is necessarily somewhat hand-wavy, because there are many aspects of formal category theory that have not yet been established in any one setting, making it impossible to give a precise comparison by reference to the literature (though this situation has been steadily improving, in no small part due to Roald’s work).

    (I should finally mention that there were some misspellings of people’s names on Zulip and consequently in the nLab page. These have now been fixed.)

    • CommentRowNumber20.
    • CommentAuthorvarkor
    • CommentTimeOct 13th 2023

    I’ve edited the text regarding the approaches slightly. It needs a bigger rework, but this is in a slightly more appropriate form for the nLab.

    diff, v20, current

    • CommentRowNumber21.
    • CommentAuthorUrs
    • CommentTimeOct 13th 2023

    Looks good.

    What is maybe still missing is an indication that all these tools are needed to do something more ambitious than what the Idea-section currently advertises:

    The idea section currently just speaks about using a plain old 2-category CatCat in order to do formal theory of plain categories.

    Somewhere there should be a line saying that one can also consider more ambitious projects like “formal enriched category theory” which then require an ambient context richer than a plain 2-category. Or something like this.

    • CommentRowNumber22.
    • CommentAuthorvarkor
    • CommentTimeOct 13th 2023

    Rephrase the introduction so that it no longer talks about the 2-category Cat, and instead highlights that more structure is needed than simply a 2-category.

    diff, v20, current

    • CommentRowNumber23.
    • CommentAuthorvarkor
    • CommentTimeOct 13th 2023

    I will try to clean this up a little more this evening.

    • CommentRowNumber24.
    • CommentAuthorUrs
    • CommentTimeOct 13th 2023

    Thanks.

    I have just swapped your paragraph withe the previous one, so that its lead-in via “This is analogous to…” still makes sense.

    diff, v21, current

    • CommentRowNumber25.
    • CommentAuthorUrs
    • CommentTimeOct 13th 2023

    Would it make sense to speak of formal enriched category theory, for definiteness?

    • CommentRowNumber26.
    • CommentAuthorvarkor
    • CommentTimeOct 13th 2023

    Formal category theory is intended to capture all flavours of (one-dimensional) category theory, e.g. ordinary category theory, internal category theory, enriched category theory, fibred category theory, internal category theory, etc. Enriched category theory is notable only because it is a useful and widely used flavour, and because there are subtleties in the enriched setting that are not visible in ordinary or internal category theory (e.g. not every weighted colimit may be expressed as a conical colimit). I shall try to expand upon this in the introduction.

    • CommentRowNumber27.
    • CommentAuthorvarkor
    • CommentTimeOct 13th 2023

    Perhaps the references to formal (infinity, 1)-category theory should be moved to synthetic (infinity,1)-category theory. “Formal” and “synthetic” appear to be being used in the same context, which is unfortunate. It would be better to have a single name.

    • CommentRowNumber28.
    • CommentAuthorUrs
    • CommentTimeOct 13th 2023

    You wanna take care of that, or shall I?

    By the way, while we have the momentum:

    What the entry badly needs after presenting the heavy machinery is to show some output:

    What are useful theorems in formal category theory which make the machinery worthwhile?

    • CommentRowNumber29.
    • CommentAuthorvarkor
    • CommentTimeOct 13th 2023

    Rewrote the introduction and approaches section. (More to follow.)

    diff, v23, current

    • CommentRowNumber30.
    • CommentAuthorvarkor
    • CommentTimeOct 13th 2023

    Re. #28: I will bring the (infinity, 1)-categorical page into line with this one, and also give some references to theorems that have been proven in formal category theory. (I will continue editing in a couple of hours.)

    • CommentRowNumber31.
    • CommentAuthorUrs
    • CommentTimeOct 13th 2023

    Thanks, looks good.

    Maybe some of the original Idea-section was not completely useless? :-)

    Such as the comparison to “formal set theory” one dimension down?

    • CommentRowNumber32.
    • CommentAuthorvarkor
    • CommentTimeOct 13th 2023

    Moved content on formal (infinity, 1)-category theory to a standalone page.

    diff, v24, current

    • CommentRowNumber33.
    • CommentAuthorvarkor
    • CommentTimeOct 13th 2023

    Added reference to Trimble’s epistemologies.

    diff, v24, current

    • CommentRowNumber34.
    • CommentAuthorvarkor
    • CommentTimeOct 13th 2023
    • (edited Oct 13th 2023)

    Add some mention of theorems. This is a rather biased selection at the moment; I will try to add more later. (The references on codiscrete cofibration are relevant, for instance, as are the many papers on the monads-and-bimodules construction.)

    diff, v24, current

    • CommentRowNumber35.
    • CommentAuthorvarkor
    • CommentTimeOct 13th 2023

    Added further references. These references are of a different nature, in that they develop the theory of proarrow equipments (or other formalisms for formal category theory), rather than developing category theory inside such a formalism. However, they still fall very much within the purview of formal category theory, as their motivation is to study the structure of categories. To explain this distinction, I’ve introduced two terms: “intramural” (to refer to doing category theory inside a 2-dimensional structure) and “extramural” (to refer to studying the theory of such 2-dimensional structures). There may be good existing terms for this distinction, or better alternatives. Feel free to offer suggestions. Even in the 1-dimensional case, I’m not sure I’ve seen this distinction being drawn explicitly, but I think it can be helpful.

    diff, v25, current

    • CommentRowNumber36.
    • CommentAuthorUrs
    • CommentTimeOct 14th 2023
    • (edited Oct 14th 2023)

    Thanks for adding the long list of theorems.

    What I was after are theorems recognizable outside the area of formal category theory itself. Imagine somebody who is into category theory but without background in formal category theory, what can the latter offer them?

    Such people might well be in need of an adjoint functor, say, in a given situation. So they follow your link to Arkor et al 23, Theorem 2.16

    This sounds like a great statement, but it may require serious work to unwind what it is saying for a concrete situation.

    Can we extract from this a tangible corollary, of the kind:

    “For example in the case that the lax-idempotent pseudomonads RR and II are taken to be such-and-such, this theorem positively answers the question of existence of adjoints which was previously left-open in …”

    ?

    • CommentRowNumber37.
    • CommentAuthorvarkor
    • CommentTimeOct 14th 2023

    Add a sentence about one motivation for the development of formal category theory.

    diff, v27, current

    • CommentRowNumber38.
    • CommentAuthorvarkor
    • CommentTimeOct 14th 2023
    • (edited Oct 14th 2023)

    Re. #36:

    What I was after are theorems recognizable outside the area of formal category theory itself. Imagine somebody who is into category theory but without background in formal category theory, what can the latter offer them?

    Many of these references play a similar role, say, to Kelly’s Basic Concepts of Enriched Category Theory. That is, they are useful when someone is working in a context whose category theory has not been well developed (such as enriched category theory without symmetry/cocompleteness) and they want to know that the fundamental theorems of category theory hold in this setting, rather than having to derive the results from scratch in their particular setting. For example, Gordon and Power have a series of papers in which they develop enough bicategory-enriched category theory to be sufficient for their applications in computer science (e.g. Algebraic structure for bicategory enriched categories), because a general theory was not available. However, now many of these results may be derived from analogous results in formal category theory. Another example is Shulman’s Enriched indexed categories, in which he develops much basic category theory in this new setting, but whose results follow from analogous results in formal category theory (as he notes this in that paper), though at that time many of the requisite results had not been established.

    Formal category theory has also been established with specific applications in mind, e.g. in Wood et al’s work on constructive complete distributivity, but I think the main motivation is to provide a general framework for doing “category-like theory”, so as to be of use to category theorists generally.

    Formal category theory is more useful the earlier it is developed, since it prevents a proliferation of references on different flavours of category theory with essentially the same definitions and proofs. (Take, for example, the recent introduction of categories enriched in a skew-monoidal category, whose theory may now be derived from formal category theory, rather than needing to carry out a Kelly-like programme in slight additional generality.)

    This sounds like a great statement, but it may require serious work to unwind what it is saying for a concrete situation.

    That paper in particular includes a number of concrete examples that show how to unwind it for specific situations, though I imagine it is probably easier for the reader to look at the paper directly for that. The purpose of the paper was less to prove some conjecture, and rather to show that a number of isolated adjoint functor theorems in the literature were instances of a more general theorem, making it easier to come up with new variants as applications demand, without needing to reprove each variant individually. However, the theorems in question, that were previously in the literature, are all in the setting of ordinary categories; whereas the general theorem in that paper can immediately be specialised to enriched categories, etc.

    • CommentRowNumber39.
    • CommentAuthorUrs
    • CommentTimeOct 14th 2023

    I see, thanks.

    I picked that example at random, just feeling that in a given situation it might well be easier to directly check some kind of solution set condition than to first come up with and check the existence of no less than two idempotent pseudomonads, just to start with. But I am just speaking superficially here and may be way off, just sharing my user-experience.

    But here is a question I actually care about (which may be comparatively trivial, please bear with me):

    With a formal theory of relative monads in hand, do we get a nice relative analog of the classical fact that for a monad on a symmetric closed category to lift to an enriched/internal monad is equivalent to it having symmetric monoidal monad structure?

    I see vague allusion to this on p. 3 of Arkor & McDermott 2023a, but I am not sure if the question can be extracted from the discussion there.

    • CommentRowNumber40.
    • CommentAuthorvarkor
    • CommentTimeOct 16th 2023

    I picked that example at random, just feeling that in a given situation it might well be easier to directly check some kind of solution set condition than to first come up with and check the existence of no less than two idempotent pseudomonads, just to start with. But I am just speaking superficially here and may be way off, just sharing my user-experience.

    If one is interested in ordinary adjointness, as opposed to something like multiadjointness, then it suffices only to have one lax idempotent pseudomonad PP around, which would typically be the appropriate notion of free small cocompletion in that context. The adjoint functor theorem in this context says that a 1-cell is left adjoint if and only if it preserves PP-colimits, and is “PP-admissible”, i.e. admits a nerve with respect to PP, which is the formal analogue of the solution set condition.

    With a formal theory of relative monads in hand, do we get a nice relative analog of the classical fact that for a monad on a symmetric closed category to lift to an enriched/internal monad is equivalent to it having symmetric monoidal monad structure?

    I believe this should follow from formal considerations. I imagine the correspondence between strong and enriched monads follows from an equivalence between the equipment of actions of a monoidal category, and the equipment of enriched categories, under suitable assumptions on the monoidal category VV (along the lines of Enrichment through variation): this equivalence would then preserve relative monads. However, I’ve not yet checked the details.

    • CommentRowNumber41.
    • CommentAuthorUrs
    • CommentTimeOct 18th 2023

    Just to say thanks for again taking the time to reply.

    I am now distracted with something else, but I’ll come back to this.

    • CommentRowNumber42.
    • CommentAuthorvarkor
    • CommentTimeDec 21st 2023

    Added Michał Przybyłek’s thesis.

    diff, v28, current