Functor quasi-categories are formalized

Stream: Infinity-Cosmos

[Jack McKoen]

I'm happy to say my repo https://github.com/mckoen/quasicategory now contains a sorry-free proof that the internal hom between a simplicial set and a quasi-category is a quasi-category. I'll be cleaning up the code in the next few weeks (and eventually pushing to mathlib).

[Jack McKoen]

The main result can be found in https://github.com/mckoen/quasicategory/blob/master/Quasicategory/QCat.lean, where I've used it to show the category of quasi-categories is enriched over itself.

[Emily Riehl]

Woohoo! What an accomplishment. Congratulations!

[Emily Riehl]

This is a huge accomplishment. Once the PRs are in the queue, will you let us know so we can help with the reviewing. In the immediate term, this means we'll be able to start developing the theory of co/limits in a quasi-category so it will be great to have.

[Johan Commelin]

Last week @Shane Kelly taught me the concept of a weighted (co)limit. Maybe that's a reasonable path?

[Emily Riehl]

Weighted co/limits are awesome and we should add them to the enriched category theory stuff. But my vision for co/limits of quasi-categories is much simpler: all we need is that the 2-category of quasi-categories is cartesian closed and @Jack McKoen's result gives us that.

Which reminds me, @Jack McKoen have you announced this on main? Because you should.

[Jack McKoen]

@Emily Riehl how far off are we from defining the infinity-cosmos of quasi-categories?

[Robin Carlier]

A question about your formalization: did you focus on internal hom, or did you formalize the more general https://kerodon.net/tag/01BT and https://kerodon.net/tag/01F1 as well?

[Robin Carlier]

A related question is: how much of the Joyal model structure your formalization (more or less implicitly) defines? I saw that you defined inner fibrations and inner anodyne extensions at the very least.

[Jack McKoen]

I focused exclusively on the internal hom, but 01BT should follow immediately from some of the results I've shown and results already in mathlib (CategoryTheory.ParametrizedAdjunction.hasLiftingProperty_iff). 01F1 is not attainable as I don't even have a definition of isofibrations in my repository. Likewise for the Joyal model structure, I've essentially only done work on monomorphisms and inner anodyne extensions.

[Emily Riehl]

So it sounds like your results would also cover the case of $i : A \to B$ and an inner fibration $q : X \to S$, in which case we want to know that the Leibniz thing is a trivial fibration. This all gets us pretty close. We just need to add the inclusion of the endpoint in the coherent isomorphism to the generating left maps. I say ``just'' without any sense of how hard it will be to extend to this case.

[Joël Riou]

The main technical lemma in Jack's formalization is that the inclusion of the union of Λ[2, 1] ⊗ Δ[n] and Δ[2] ⊗ ∂Δ[n] in Δ[2] ⊗ Δ[n] is an inner anodyne extension (see https://github.com/mckoen/quasicategory/blob/f4c9210337cf459447813c7431640cef2e5d65f5/Quasicategory/_007F.lean#L274). This is similar to what I initially did for the original definition of anodyne extensions (but with extra complications as the simplices have to be added in a more intricate order).

[Joël Riou]

I have formalized a very significantly different approach using the very interesting work by Sean Moss, Another approach to the Kan–Quillen model structure https://link.springer.com/article/10.1007/s40062-019-00247-y who gives a complete combinatorial description of strong anodyne extensions (same as anodyne extensions, but without taking the closure under retracts). The idea is that if a subcomplex A of X is such that X is obtained from A by attaching simplices along horns, then the nondegenerate simplices of X not in A come by pairs (a simplex, along with the face which does not belong to the corresponding horn). In order to show that the inclusion A ⟶ X is a strong anodyne extension, it suffices to produce such a "pairing", and show that a certain ancestrality relation is well founded (in order to be able to add a simplex, we need to know that all faces but one are already in our subcomplex).

[Joël Riou]

I have formalized this approach initially in order to show that the subdivision functor preserves anodyne extensions (the basic case is done there https://github.com/joelriou/topcat-model-category/blob/8aedab5a642e7630e14be6df196a645d1cfbf723/TopCatModelCategory/SSet/PairingSubdivision.lean#L558 which corresponds to Proposition 19 in Moss's article), but I have just formalized the essential case of Lemma 17 in Moss's article, which is that the incusion of Λ[m, k] ⊗ Δ[n] and Δ[m] ⊗ ∂Δ[n] in Δ[m] ⊗ Δ[n] is a strong anodyne extension (when m is non zero). I have completely done the case k < m (but the case k = m could probably be deduced by using a certain symmetry). When we have 0 < k < m, I have verified that only inner horns are used, which will allow a more conceptual proof of the verification that in the case m = 2, k = 1, we have a strong inner anodyne extension.

[Joël Riou]

https://github.com/joelriou/topcat-model-category/blob/8aedab5a642e7630e14be6df196a645d1cfbf723/TopCatModelCategory/SSet/PairingUnionProd.lean#L738

[Jack McKoen]

Robin Carlier said:

A question about your formalization: did you focus on internal hom, or did you formalize the more general https://kerodon.net/tag/01BT and https://kerodon.net/tag/01F1 as well?

I've had some spare time recently so I have nearly formalized https://kerodon.net/tag/01BT, modulo one smaller lemma. Some of the things I needed went towards defining a symmetric monoidal structure on the arrow category of SSet (and more general categories), where the product is given by the pushout-product Leibniz thing.

I'm going to start PRing stuff very soon, but my laptop's SSD died yesterday so I won't be writing any code for a bit.

[Emily Riehl]

This is very exciting! What are the prospects of formalizing the corresponding statements involving trivial fibrations?

Let us know when you need reviewers (and good luck sorting out the laptop issue).

[Jack McKoen]

Which statements specifically would you want?

[Emily Riehl]

Both statements in 1.1.29 of this.

[Jack McKoen]

Right, so the first statement (mono and trivial fibration gives trivial fibration) is immediate, but the second statement will take some nontrivial work.