Model categories

Stream: Infinity-Cosmos

[Jakob von Raumer]

Happy to contribute a bit around the fringes, like infrastructure on model categories or on simplicial sets. @Joël Riou do you already have instances for model categories locally? I could start implementing these based on #19158, or start some infrastructure on functors preserving the morphism classes en route to have Quillen adjunctions

[Joël Riou]

I am currently working on basic facts about simplicial sets in order to construct the standard model category structure (both on simplicial sets and topological spaces), but the first instance of a model category which may appear in mathlib will probably be the one on bounded below complexes in an abelian category with enough injectives (I have already formalized the most tricky factorization axioms CM5, and CM4 is slightly easier).
I have a lean 3 formalization of the fundamental lemma of homotopical algebra (which describes morphisms in the (localized) homotopy category), K. S. Brown lemma, and a few other things which should be useful in order to construct derived functors between homotopy categories.
If you want to formalize Quillen adjunctions, you may certainly do so; I have not done anything in this area.

[Emily Riehl]

@Joël Riou my favorite definition of a model structure in Joyal's: on a bicomplete category it is given by three classes of maps $C$, $F$, $W$ so that $W$ has the 2 of 3 property and $(C \cap W, F)$ and $(C, F \cap W)$ are weak factorization systems. Is this perspective helpful in any (small) way?

[Jakob von Raumer]

Referencing weak factorization systems in the definition of model structures would make it a bit more modular and reduce some of the doublings

[Joël Riou]

I know this definition, but for the constructions I know (simplicial sets, topological spaces, simplicial presheaves [on a category with a topology], etc) as far as I know, we shall build the instances corresponding to the "traditional" axioms CM1/2/3/4/5 step by step, and then from these axioms, we can deduce that cofibrations are exactly the maps with the llp with respect to trivial fibrations, etc (see #20210).

From my perspective, it would be inefficient to have wfs as the definition of model categories. We may have an alternate constructor though!

[Jakob von Raumer]

With enough infrastructure it shouldn't make too much of a difference, I guess

[Joël Riou]

The mathematical issue I see with the wfs definition is that the burden of proof is stronger when we want to verify the axioms.
When we have a definition of wfs, we may deduce easily the wfs version of model category axioms from the work I have already done using the retract argument, and providing the alternate constructor for ModelCategory would be trivial (again, because the wfs axioms are kind of stronger than the traditional axioms).
The other way, the code would be much more messy, because if we were to define model categories using wfs, we would still have to phrase all the instances that I have formalized as axioms, and you would still have to prove that the traditional axioms implies the wfs version (again, because the wfs definition is not directly suitable for constructions), and if you think about it, that would be much more ugly than the path I am suggesting...

[Joël Riou]

In #24144, given an adjunction I obtain the derived adjunction between the left and right derived functors, under the assumption that these are absolute derived functors (this is a generalization by Georges Maltsiniotis of the theorem by Quillen for adjunctions between model categories).

[Emily Riehl]

I love that proof! And also that he explains is so clearly I could even understand it in French.