do we need Quillen model categories?

Stream: Infinity-Cosmos

[Kunhong Du]

@Emily Riehl
I got it! Thanks for the clarification.

I also have a question about the task plan: do we need the theory of Quillen's model category? I checked your book (Elements of $\infty$-Category Theory) and I believe some of the classical results are used but I am not sure about the plan for this project.

[Nima Rasekh]

Kunhong Du said:

Emily Riehl
I got it! Thanks for the clarification.

I also have a question about the task plan: do we need the theory of Quillen's model category? I checked your book (Elements of $\infty$-Category Theory) and I believe some of the classical results are used but I am not sure about the plan for this project.

I am not sure about the plan as well. However, model categories do provide a good source of examples for oo-cosmoi (see E.1.1. Proposition in Elements). Also certain results do rely on quasi-categorical manipulations, which can be seen as "something is true in a model category".Here the model category would usually be the Joyal model structure or a model structure for fibrations.

[Kunhong Du]

Nima Rasekh said:

Kunhong Du said:

Emily Riehl
I got it! Thanks for the clarification.

I also have a question about the task plan: do we need the theory of Quillen's model category? I checked your book (Elements of $\infty$-Category Theory) and I believe some of the classical results are used but I am not sure about the plan for this project.

I am not sure about the plan as well. However, model categories do provide a good source of examples for oo-cosmoi (see E.1.1. Proposition in Elements). Also certain results do rely on quasi-categorical manipulations, which can be seen as "something is true in a model category".Here the model category would usually be the Joyal model structure or a model structure for fibrations.

I see. So, on the other hand, the classical model structure of SSet is not so relevant here?

[Nima Rasekh]

Kunhong Du said:

Nima Rasekh said:

Kunhong Du said:

Emily Riehl
I got it! Thanks for the clarification.

I also have a question about the task plan: do we need the theory of Quillen's model category? I checked your book (Elements of $\infty$-Category Theory) and I believe some of the classical results are used but I am not sure about the plan for this project.

I am not sure about the plan as well. However, model categories do provide a good source of examples for oo-cosmoi (see E.1.1. Proposition in Elements). Also certain results do rely on quasi-categorical manipulations, which can be seen as "something is true in a model category".Here the model category would usually be the Joyal model structure or a model structure for fibrations.

I see. So, on the other hand, the classical model structure of SSet is not so relevant here?

If classical means "Kan-Quillen", then presumably less so. oo-cosmoi are by definition QCat enriched, so the most important model structure relevant for it would be the Joyal model structure.
On the other hand both model structures are defined on the same category and so developing simplicial methods would be useful for both, I presume?
Also, Kan complexes do help recover the "discrete oo-categories" in an oo-cosmos (see 1.2.26. Definition in Elements), which we should think of as the oo-groupoids in that setting, so for that part Kan complexes (i.e. the fibrant objects in that model structure) are certainly important.

[Kunhong Du]

Nima Rasekh said:

Kunhong Du said:

Nima Rasekh said:

Kunhong Du said:

Emily Riehl
I got it! Thanks for the clarification.

I also have a question about the task plan: do we need the theory of Quillen's model category? I checked your book (Elements of $\infty$-Category Theory) and I believe some of the classical results are used but I am not sure about the plan for this project.

I am not sure about the plan as well. However, model categories do provide a good source of examples for oo-cosmoi (see E.1.1. Proposition in Elements). Also certain results do rely on quasi-categorical manipulations, which can be seen as "something is true in a model category".Here the model category would usually be the Joyal model structure or a model structure for fibrations.

I see. So, on the other hand, the classical model structure of SSet is not so relevant here?

If classical means "Kan-Quillen", then presumably less so. oo-cosmoi are by definition QCat enriched, so the most important model structure relevant for it would be the Joyal model structure.
On the other hand both model structures are defined on the same category and so developing simplicial methods would be useful for both, I presume?
Also, Kan complexes do help recover the "discrete oo-categories" in an oo-cosmos (see 1.2.26. Definition in Elements), which we should think of as the oo-groupoids in that setting, so for that part Kan complexes (i.e. the fibrant objects in that model structure) are certainly important.

That sounds nice! Actually I've been working with Kan complexes and Kan fibrations for my projects. I have to deal with some lifting property, which may be better handled in the setting of model category. If it's also useful in this project, I'll be more motivated to tackle them rather than try my best to circumvent them. :)

[Emily Riehl]

We don't quite need the full Joyal model structure on simplicial sets. But to show that quasi-categories define an $\infty$-cosmos, we need various pieces of it, some of which I expect will be quite annoying to establish.

[Emily Riehl]

But let's start with the good news. Mathlib has a folder "LiftingProperties" under "CategoryTheory" that has some todos which would be helpful for us right away and might not be too too painful. If this is of interest to @Kunhong Du , @Nima Rasekh, @Zeyi Zhao or anyone else, we can divvy them up.

[Emily Riehl]

(Aside: what is the best way to reference specific mathlib files here? I haven't mastered this.)

[Emily Riehl]

In the Basic file, maps characterized by a right lifting property are shown to be closed under composition and contain the isomorphisms. But they don't prove closure under retract, pullback, product, or inverse limit of towers, all of which would be great to have.

[Emily Riehl]

A more involved project would be to explain the relationship between lifting properties and two variable adjunctions. I don't believe mathlib has a definition of a two variable adjunction, so this will require some preliminary work to even state the result correctly. A goal would be to prove Exercise C.2.v.

[Notification Bot]

11 messages were moved here from #Infinity-Cosmos > welcome! by Emily Riehl.

[Emily Riehl]

Kevin Buzzard said:

(someone should move this interesting conversation to a thread with a better title, for easier searchability later; I believe any user can do this as long as it stays within the same channel, which is the case here)

Thanks @Kevin Buzzard for the suggestion. I didn't know this could be done.

[Emily Riehl]

Now for the bad news: Elements section 1.1 contains some results that were cut from the blueprint (section 1.2) because I thought they would be too hard to formalize. Indeed the proofs don't actually appear until appendix D.

[Emily Riehl]

Specifically it would be helpful to know various closure properties of the isofibrations (= Joyal model structure fibrations between quasi-categories). Some of these follow immediately from the fact that these are characterized by a right lifting property but others are more subtle, holding essentially because the Joyal model structure is cartesian closed, so isofibrations are closed under pullback exponential with monomorphisms. This is the relative generalization of the fact that if $A$ is a quasi-category and $X$ is a simplicial set, then $X^A$ is a quasi-category.

[Emily Riehl]

Question for @Jack McKoen: are these definitions in our repository on the way into mathlib (or already there)?

/-- left lifting property with respect to a class of morphisms -/
def llp (T : MorphismProperty C) : MorphismProperty C := fun _ _ f ↦
  ∀ ⦃X Y : C⦄ ⦃g : X ⟶ Y⦄ (_ : T g), HasLiftingProperty f g

/-- rlp wrt a class of morphisms -/
def rlp (T : MorphismProperty C) : MorphismProperty C := fun _ _ f ↦
  ∀ ⦃X Y : C⦄ ⦃g : X ⟶ Y⦄ (_ : T g), HasLiftingProperty g f

[Kim Morrison]

Emily Riehl said:

(Aside: what is the best way to reference specific mathlib files here? I haven't mastered this.)

file#Mathlib/CategoryTheory/LiftingProperties/Basic

[Nima Rasekh]

@Emily Riehl Is there a proof of the Cartesian closure that doesn't go through some sort of the "saturated classes" argument? If not, then formalizing it shouldn't be straightforward

[Kunhong Du]

@Emily Riehl I don't think retract exists in Mathlib yet, unless it's named something other than "retract" so I couldn't find it. So I have defined it myself in my experimental file to define model structures. I'll prove rlp is closed under retract and also pullbacks (actually already proved that for Kan fibrations in my repesoitory).

[Emily Riehl]

Nima Rasekh said:

Emily Riehl Is there a proof of the Cartesian closure that doesn't go through some sort of the "saturated classes" argument? If not, then formalizing it shouldn't be straightforward

Could you rephrase this with fewer negatives?

[Nima Rasekh]

Well, I want to show that the pushout product of inner horn inclusions and cofibrations are categorical equivalences. The proof I know reduces the cofibrations to boundary inclusions, at which point it is a direct calculation. The way I know how to do the reduction is to use the theory of saturated classes. My question is, do you know a way that avoids that? If not then formalizing this result would require a bunch of stuff about saturated classes to be formalized first
Is my question clearer now?

[Joël Riou]

Emily Riehl said:

But let's start with the good news. Mathlib has a folder "LiftingProperties" under "CategoryTheory" that has some todos which would be helpful for us right away and might not be too too painful. If this is of interest to Kunhong Du , Nima Rasekh, Zeyi Zhao or anyone else, we can divvy them up.

I have already formalized model categories (in lean 3 https://github.com/joelriou/homotopical_algebra/blob/main/src/for_mathlib/algebraic_topology/homotopical_algebra/model_category.lean) until the fundamental lemma of homotopical algebra. I may port/clean the code if there is a need.

[Joël Riou]

I am also in the process of PRing general results on the small object argument. https://leanprover-community.github.io/mathlib4_docs/Mathlib/CategoryTheory/SmallObject/Iteration/Basic.html

[Jack McKoen]

Emily Riehl said:

Question for Jack McKoen: are these definitions in our repository on the way into mathlib (or already there)?

/-- left lifting property with respect to a class of morphisms -/
def llp (T : MorphismProperty C) : MorphismProperty C := fun _ _ f ↦
  ∀ ⦃X Y : C⦄ ⦃g : X ⟶ Y⦄ (_ : T g), HasLiftingProperty f g

/-- rlp wrt a class of morphisms -/
def rlp (T : MorphismProperty C) : MorphismProperty C := fun _ _ f ↦
  ∀ ⦃X Y : C⦄ ⦃g : X ⟶ Y⦄ (_ : T g), HasLiftingProperty g f

These are not in mathlib yet AFAIK. I'm not in a rush to get anything into mathlib while I work on finishing my thesis project though

Edit: I will actually make a PR for this and some related things soon

[Jack McKoen]

Nima Rasekh said:

Well, I want to show that the pushout product of inner horn inclusions and cofibrations are categorical equivalences. The proof I know reduces the cofibrations to boundary inclusions, at which point it is a direct calculation. The way I know how to do the reduction is to use the theory of saturated classes. My question is, do you know a way that avoids that? If not then formalizing this result would require a bunch of stuff about saturated classes to be formalized first
Is my question clearer now?

This is almost exactly what I've been working on in my repo. I'm doing a lot of work with saturated classes at the moment, which may be of use here?

[Jack McKoen]

Kunhong Du said:

Emily Riehl I'll prove rlp is closed under retract and also pullbacks (actually already proved that for Kan fibrations in my repesoitory).

I've already proved rlp is closed under retracts and pullbacks (with dual statements for llp). I guess I should really make some pull requests : /

[Jack McKoen]

For posterity: https://github.com/mckoen/quasicategory/blob/master/Quasicategory/MorphismProperty.lean

[Joël Riou]

Emily Riehl said:

A more involved project would be to explain the relationship between lifting properties and two variable adjunctions. I don't believe mathlib has a definition of a two variable adjunction, so this will require some preliminary work to even state the result correctly. A goal would be to prove Exercise C.2.v.

Until yesterday, I did not know that "adjunctions of two variables" were a thing, but I did formalize this equivalence for lifting properties in #22828 and #22834 in the situation of what we may call an "adjunction between (two) bifunctors". (In the case of "adjunctions of two variables" which involve three bifunctors, it suffices to apply the lemma Adjunction₂.hasLiftingProperty_iff twice.)

[Joël Riou]

Also, about the homotopy theory of simplicial sets, I am very close to formalising the proof by Gabriel and Zisman that any Kan fibration has a fibrewise deformation retract which is a minimal fibration.

[Emily Riehl]

Joël Riou said:

Emily Riehl said:

A more involved project would be to explain the relationship between lifting properties and two variable adjunctions. I don't believe mathlib has a definition of a two variable adjunction, so this will require some preliminary work to even state the result correctly. A goal would be to prove Exercise C.2.v.

Until yesterday, I did not know that "adjunctions of two variables" were a thing, but I did formalize this equivalence for lifting properties in #22828 and #22834 in the situation of what we may call an "adjunction between (two) bifunctors". (In the case of "adjunctions of two variables" which involve three bifunctors, it suffices to apply the lemma Adjunction₂.hasLiftingProperty_iff twice.)

Great! I'll have a look when I have a moment. In the case you consider, I prefer the name "parametrized adjunction" which I believe is what Mac Lane uses.

[Joël Riou]

Joël Riou said:

Also, about the homotopy theory of simplicial sets, I am very close to formalising the proof by Gabriel and Zisman that any Kan fibration has a fibrewise deformation retract which is a minimal fibration.

Modulo a few relatively basic lemmas about anodyne extensions, I have just formalized the existence theorem for minimal fibrations:

lemma SSet.MinimalFibration.existence {E B : SSet.{u}} (p : E ⟶ B) [Fibration p] :
    ∃ (A : E.Subcomplex) (_ : A.RelativeDeformationRetract p),
      MinimalFibration (A.ι ≫ p) :=

https://github.com/joelriou/topcat-model-category/blob/master/TopCatModelCategory/SSet/MinimalFibrations.lean

[Emily Riehl]

Congrats!