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.
Re #100: Dugger’s theorem does prove homotopical essential surjectivity, equivalently, essential surjectivity for 2-localizations like in Renaudin’s paper.
But what do you want to do for 1-morphisms and 2-morphisms? More generally, how do you intend to prove homotopical fully faithfulness?
In terms of hammock localizations, one would need to show that the induced inclusion of hammock localizations is a weak equivalence.
This is hardly obvious since a hammock between two left proper combinatorial model categories can pass through non-left proper combinatorial model categories.
Okay, I see. So it’s good that you are looking into this in detail!
Have adjusted the footnote at Ho(CombModCat) and copied it also to derivator.
But please feel invited to further edit as need be.
The draft is ready: https://dmitripavlov.org/comb.pdf. 31 pages!
Perhaps you could take a look and see whether the statement you wanted is present in one of the 4 theorems?
Ah, excellent! I have now read the introduction section 1. Looks good!
Yes, I was after your Theorem 1.4 with presentable quasicategories instead of derivators, but of course your theorems 1.1/1.2 are much stronger than what I was looking for.
Just to check if I am reading right: the items in theorems 1.1 and 1.2 are all DW-equivalent to each other, right? Since the lists share the first item, CMC (though in 1.2 it’s not referred to as CMC).
Re #104: Yes, certainly. Will fix this now.
Do you have any similar statements in mind that you would like to see included?
Maybe if you could just make explicit the corollary that, in particular, the homotopy 2-category of CMC is equivalent to that of PresCat, just so that the reader sees fully manifestly that you have, in particular, adapted Renaudin’s theorem from presentable derivators to presentable -categories.
Re #107: Done, see the new statement of Theorem 1.4 in the newly uploaded file.
Let me know if you can think of any other useful statements that could be added.
(The theorems that establish these results allow for a lot of variation.)
Looks good, thanks.
If I were to freely wish for more: How about locally cartesian closed presentable -categories and any of their model category presentations listed here?
Re #109: Yes, this appears to be true.
The argument continues to work in a similar way, except that a slightly different model must be chosen.
Looking at the proofs of Cisinski and Gepner–Kock, I see that their construction of rectification is similar to mine, but instead of presenting κ-compact objects as a small relative category and then taking simplicial presheaves and left Bousfield localizing to ind-complete, they present κ-compact objects as a small fibrant simplicial category, take simplicial presheaves, and left Bousfield localize to ind-complete.
So either one has to show that the proofs of Cisinski and Gepner–Kock continue to work in my setting (for instance, showing that Proposition 1.5 in the Gepner–Kock paper continues to work if we use presheaves on a relative category of κ-compact objects), or, alternatively, establish a variant of my theorem for their version of this construction, which requires writing a new variant of Section 7 in my paper (4 pages total).
Can you think of any applications that would justify writing this up as a separate note? Something from type theory, perhaps?
I should say that the reason I brought this up in the first place is that I want to use it:
We are writing something like a book on matters of cohesive -bundles and are facing the tension between being both reasonably self-contained as well as reasonably concise. But the content-module “model category theory” is meant to have been loaded already, and so I was thinking about the quickest way from here to actually and rigorously setting up modal -topos theory. So I need a quick yet correct way to characterize the homotopy 2-category of presentable -categories (and then of presentable LCC -categories, etc.) based on just model category theory (okay, and localization of -categories). Which is what you now provided! :-)
I am thinking that this way of laying working foundations for -category theory should be quite useful in general.
But maybe you are looking for a more specific application. Regarding homotopy type theory: I’d have to remind myself of the details of what this article accomplishes:
but broadly this should be the kind of consideration that would benefit from a good understanding of the simplicial localization of CMC and LCCMC. (Checking the citations this has picked up, I am getting the impression that this is still essentially the state of the art, but I haven’t been following closely).
Okay, this is something I could write up separately, although maybe not in 2021, but in 2022.
Okay, sounds good! :-)
It’s a little unfortunate that we ended up having this whole discussion here under “derivator”, when it all originated from (and now succeeded in) the quest at Ho(CombModCat) to go away from the case of derivators. In any case, I have now added pointer to your draft there. I hope we eventually get the main results recorded there.
It is now on arXiv: https://arxiv.org/abs/2110.04679
Good.
By the way, how hard would it be to enhance to an equivalence of homotopy 2-categories or -categories? (i.e. as opposed to just homotopy -categories or -categories)?
Re #116: Not difficult. In fact, I was thinking about adding the version with noninvertible 2-morphisms, but decided against it, because while straightforward to write it would make the paper longer.
Basically, you need to develop some (straightforward) stuff about relative 2-categories (or 2-relative 2-categories?), where the hom-object hom(X,Y) is a relative category (objects are 1-morphisms, morphisms are 2-morphism), and some 1-morphism and 2-morphisms are weak equivalence.
In our case, left Quillen equivalences are weak 1-equivalences and natural transformations that are weak equivalences on cofibrant objects are weak 2-equivalences.
So the 2-categorical statement is true, and not difficult to write up, but the paper was already 32 pages long, so I decided against it.
This can also be done as a separate paper, if there is interest in it.
That would be great to have the 2-category-version written up somewhere! As highlighted by Riehl-Verity, the homotopy 2-category of infinity-categories goes a long way. In particular it knows all about the adjoints, hence the modalities, that I’d particularly care about.
Regarding the “2-relative” in #117:
Renaudin speaks only about 2-localizing at 1-morphisms.
I am guessing the point is that this inverts the desired 2-morphisms (“Quillen homotopies”) because (his Prop. 2.1.4, p. 10) these are equivalently 1-morphisms into the arrow category of the domain, equipped with a suitable model structure (his modèle chemin in Sec. 2.1.1).
Is that right? I haven’t penetrated further into his proof.
(Nor yours for that matter. I did spend some time with your article yesterday, but it was a surprising lot of discussion of techniques for dealing with size issues, and I haven’t yet gotten beyond these to the bottom of the proof yet.)
But disregarding details of the proof, what’s the form of the statement to be expected? Is it the 2-localization of the 2-category of combinatorial model categories at the 1-morphisms that are left Quillen equivalences which is already going to be equivalent to the homotopy 2-category of presentable -categories? Or only after further 1-localizing this hom-category-wise at the Quillen homotopies?
Sorry, I am being stupid. After I wrote this comment I remembered that I had made a note on this in the entry here: Renaudin’s theorem 2.3.2 says that the 2-morphisms which are Quillen homotopies automatically get inverted once the 1-morphisms which are left Quillen euqivalences have been inverted.
Re #120: Indeed, even more directly, Proposition 2.1.4 shows how to convert Quillen homotopies to left Quillen functors into path model categories, whereas Corollary 2.1.5 immediately applies Proposition 2.1.4 to show that inverting left Quillen equivalences also inverts Quillen homotopies, since the “constant path” left Quillen functor is a left Quillen equivalence.
So indeed we only need a “1-relative 2-category”, where only left Quillen equivalences need to be inverted.
Now that I think about it, it can be even easier to prove than I thought.
I think hammock localizations can be easily adapted to work with 1-relative 2-categories (each square in a hammock now has to commute up to a possibly noninvertible 2-morphism), and the hammock construction now produces a category enriched in simplicial sets equipped with the Joyal model structure.
Thanks, great.
Let me just double check about the form of the theorem you think you can prove:
Let me write
for 2-localization of 2-categories at a class of 1-morphisms, as in Renaudin’s article
for the homotopy 2-category of an -category.
Then there ought to be an equivalence of 2-categories:
Re #122: Yes, and I think this equivalence of 2-categories is induced by taking the homotopy 2-categories of the analogous equivalence of (∞,2)-categories, modeled as categories enriched in simplicial sets with the Joyal model structure, where the homotopy 2-category construction replaces each hom-object with its fundamental category.
The hom-objects can be constructed like in the usual hammock localization, but with 2-morphisms thrown in for each commuting square.
Thanks, great.
Mulling further about how to use this, I come to think that what I really want is closed symmetric monoidal structure on the 1-category . That should be guaranteed as the 1-cat shadow of the closed symmetric structure on , though it would be nice to have explicit model category theoretic presentation for it. The (strict) 2-category structure would be implied.
(This is not meant to be in reply to anything, I am just thinking out loud.)
Added last night’s:
have hyperlinked the author name (here) and added the reference to his page: Nicola Di Vittorio