The model category structure on topological spaces

Stream: maths

[Joël Riou]

I have just finished the formalization of the Quillen model category structure on TopCat, which should enable future developments of the formalization of homotopy theory in Lean/mathlib. https://github.com/joelriou/topcat-model-category (For stupid technical reasons, this is currently only for TopCat.{0}.)
The main result is :

example : ModelCategory TopCat.{0} := inferInstance

https://github.com/joelriou/topcat-model-category/blob/155c90fff56eb12770be21d5dd43e223463e31a7/TopCatModelCategory/ModelCategoryTopCat.lean#L157-L158

[Joël Riou]

This is a major step towards the construction of the Quillen model category structure on the category of simplicial sets. My approach mostly follows the book Simplicial homotopy theory by Goerss and Jardine. In a few places, I had to look at original papers/books by Kan, Gabriel-Zisman and Hovey.

[Joël Riou]

Previously, @Reid Barton made significant work formalizing homotopy theory. In his attempt at constructing the Quillen model category structure on topological spaces https://github.com/rwbarton/lean-model-categories/blob/top-dev/src/model_top.lean the only missing step was that if p : E ⟶ B is a Serre fibration between topological spaces, then it is a weak homotopy equivalence iff if has the lifting properties with respect to "boundary inclusions" (e.g. inclusions of spheres in balls).

[Joël Riou]

The most significant improvement in my work is that I have formalised this characterization of "trivial fibrations" (fibrations that are also weak equivalences) in terms of lifting properties. I have done this as a consequence of a similar characterization of trivial fibrations between Kan complexes (i.e. fibrant simplicial sets): this proceeds from the development of the homotopy theory of Kan complexes (e.g. the homotopy sequence of a fibration), which was made possible through the basic (and quite technical) study of the class of morphisms that are Gabriel-Zisman anodyne extensions (this is a closure of the family of "horn inclusions").
https://github.com/joelriou/topcat-model-category/blob/155c90fff56eb12770be21d5dd43e223463e31a7/TopCatModelCategory/SSet/KanComplexKeyLemma.lean#L318-L323

[Joël Riou]

There is a similar characterization of trivial fibrations between arbitrary simplicial sets, and this is the only remaining sorry towards the definition of the Quillen model category structure on simplicial sets.
https://github.com/joelriou/topcat-model-category/blob/155c90fff56eb12770be21d5dd43e223463e31a7/TopCatModelCategory/ModelCategorySSet.lean#L117-L119
The proof shall be more difficult, even though I have already obtained one of the major ingredients which is the existence theorem for minimal fibrations.
https://github.com/joelriou/topcat-model-category/blob/155c90fff56eb12770be21d5dd43e223463e31a7/TopCatModelCategory/SSet/MinimalFibrations.lean#L673-L677

[Joël Riou]

Similarly as in @Reid Barton's work, the small object argument -- which we have both formalised, and is now in mathlib https://leanprover-community.github.io/mathlib4_docs/Mathlib/CategoryTheory/SmallObject/Basic.html -- plays an important role in the verification of the axioms of model category structures. Several references omit most of the details about "smallness" lemmas for topological spaces (e.g. a map from a compact space to a CW-complex factors through a finite subcomplex): it was helpful for me to find in @Reid Barton's code a reference to the notion of "closed T₁ inclusion" which appears in the book Model categories by Mark Hovey.

[Robin Carlier]

Once the formalization for the model structure on simplicial sets will be done, how far do you expect it will be before being able to formalize the various models structures on simplicial (pre)sheaves, or on objects like simplicial algebraic gadgets (e.g simplicial rings, simplicial modules over simplicial rings, etc.)?

[Joël Riou]

Some additional work on locally presentable categories/accessible functors would be convenient in order to obtain the existence of certain Bousfield localizations.

[Robin Carlier]

Also, how much of your code do you expect could be reusable for the Joyal model structure on simplicial sets (which is very useful for higher category/theory "à la Lurie")?

[Robin Carlier]

Joël Riou said:

Some additional work on locally presentable categories/accessible functors would be convenient in order to obtain the existence of certain Bousfield localizations.

Would that entail taking up the daunting task of redoing the current "indization/ind-object" infrastructure in mathlib but with regular cardinals replacing omega?

[Joël Riou]

Robin Carlier said:

Would that entail taking up the daunting task of redoing the current "indization/ind-object" infrastructure in mathlib but with regular cardinals replacing omega?

I do not know what exactly you are referring to, but I already introduced some definitions, like https://leanprover-community.github.io/mathlib4_docs/Mathlib/CategoryTheory/Presentable/Basic.html

[Joël Riou]

Robin Carlier said:

Also, how much of your code do you expect could be reusable for the Joyal model structure on simplicial sets (which is very useful for higher category/theory "à la Lurie")?

I do not know the technical details about the Joyal model structure, but this seems to be almost completely unrelated to my work.

[Robin Carlier]

Joël Riou said:

I do not know the technical details about the Joyal model structure, but this seems to be almost completely unrelated to my work.

Cisinski’s book Higher categories and homotopical algebra, section 2.4 introduces a framework to produce model categories on simplicial objects capable of producing both the Kan-Quillen model structure and the Joyal one (thm 3.1.8 for the Kan-Quillen one, def 3.3.7 for the Joyal one), which is why I’m asking.

[Robin Carlier]

Joël Riou said:

Robin Carlier said:

Would that entail taking up the daunting task of redoing the current "indization/ind-object" infrastructure in mathlib but with regular cardinals replacing omega?

I do not know what exactly you are referring to, but I already introduced some definitions, like https://leanprover-community.github.io/mathlib4_docs/Mathlib/CategoryTheory/Presentable/Basic.html

One of the definition (or at least a characterization) of "locally presentable category" that I know of is that the category is
1) Cocomplete
2) k-accessible for a regular cardinal k.
The second point is by definition that it is equivalent to Ind_k(C) for a small category C, and Ind_k is the k-indization of C.

Do you mean you’d instead define them as accessible localization of categories of presheaves?

[Joël Riou]

I am not following Cisinski's approach because my goal is not just to get a model category structure, but to get a model category structure on simplicial sets that is Quillen equivalent to the model category structure on topological spaces.

[Joël Riou]

(And also, develop some standard homotopy theory tools, like the homotopy sequence of a fibration, etc.)

[Joël Riou]

Robin Carlier said:

Do you mean you’d instead define them as accessible localization of categories of presheaves?

For simplicial presheaves (with equivalences defined relative to a Grothendieck topology) and other model structures (e.g. Bousfield localizations), the most technical part is to show that there is a generating set of trivial cofibrations, and for this, the literature is sometimes sketchy, or wrong... In order to construct model categories, there is a general theorem by J. Smith which relies on notions of locally presentable categories and the solution set condition, but as far as I remember, even though I already have most of the ingredients in order to formalize a version of the theorem, it would require more work on accessible functors/categories in order to be able to use it (e.g. the WIP PR #20267, which is about the accessibility of comma categories).

[Emily Riehl]

Congrats @Joël Riou this is a monumental achievement.

As part of the infrastructure you've developed, can you say anything about pushout products of cofibrations and trivial cofibrations? For those following along, I'm referring to the monoidal model category axiom of Hovey extending Quillen's simplicial model categories.

[Joël Riou]

As part of the study of anodyne extensions following Gabriel and Zisman, I have shown https://github.com/joelriou/topcat-model-category/blob/155c90fff56eb12770be21d5dd43e223463e31a7/TopCatModelCategory/SSet/AnodyneExtensionsAdjunctions.lean#L350-L360 which says that if A is a subcomplex of X : SSet, B a subcomplex of Y, then the inclusion of the union of A ⊗ Y and X ⊗ B in X ⊗ Y is an anodyne extension if one of the two inclusions is. (Once we know these anodyne extensions are exactly the trivial cofibrations for the Quillen model category structure, the monoidal model category axiom will follow.)

[Emily Riehl]

Fantastic. Though now I'm curious about how you've defined the trivial cofibrations... :)

[Joël Riou]

I defined anodyne extensions in SSet as (fibrations _).llp (i.e. J.rlp.llp, where J are horn inclusions), because I had already formalized the small object argument (so that anodyneExtensions is also the closure of J with coproducts, pushouts, infinite or transfinite compositions and retracts). Once we have the model category axioms for the Quillen structure on SSet, it will follow that anodyne extensions are precisely trivial cofibrations (i.e. those cofibrations that are weak equivalences).

[Robin Carlier]

Joël Riou said:

Robin Carlier said:

Do you mean you’d instead define them as accessible localization of categories of presheaves?

For simplicial presheaves (with equivalences defined relative to a Grothendieck topology) and other model structures (e.g. Bousfield localizations), the most technical part is to show that there is a generating set of trivial cofibrations, and for this, the literature is sometimes sketchy, or wrong... In order to construct model categories, there is a general theorem by J. Smith which relies on notions of locally presentable categories and the solution set condition, but as far as I remember, even though I already have most of the ingredients in order to formalize a version of the theorem, it would require more work on accessible functors/categories in order to be able to use it (e.g. the WIP PR #20267, which is about the accessibility of comma categories).

I was not exactly referring to this (I was asking if you were avoiding the notion of Ind_k by defining locally presentable categories as reflective subcategories of categories of presheaves such that the reflection is accesible, which is what I was calling an "accessible localization"), but the PR you linked answers my questions anyways. Congratulation for this immense amount of work!

[Joël Riou]

I have managed to extend the results from TopCat.{0} to TopCat.{u} for any universe u:

example : ModelCategory TopCat.{u} := inferInstance

It follows from #27576 but also from additional results about left Kan extensions along the (ulifted) Yoneda functor:

lemma isLeftKanExtension_along_uliftYoneda_iff'
    [uliftYoneda.{w}.HasPointwiseLeftKanExtension A]
    (L : (Cᵒᵖ ⥤ Type (max w v₁)) ⥤ D)
    (α : A ⟶ uliftYoneda.{w} ⋙ L) :
    L.IsLeftKanExtension α ↔ IsIso α ∧
      ∀ (P : Cᵒᵖ ⥤ Type max w v₁),
        PreservesColimit (functorToRepresentables P) L := ...

https://github.com/joelriou/topcat-model-category/blob/b0837c5ac39dd7e77da3ae43d7538dadd2d60d33/TopCatModelCategory/LeftKanExtensionAlongUliftYoneda.lean#L138

[Blake Farman]

Joël Riou said:

Robin Carlier said:

Do you mean you’d instead define them as accessible localization of categories of presheaves?

For simplicial presheaves (with equivalences defined relative to a Grothendieck topology) and other model structures (e.g. Bousfield localizations), the most technical part is to show that there is a generating set of trivial cofibrations, and for this, the literature is sometimes sketchy, or wrong... In order to construct model categories, there is a general theorem by J. Smith which relies on notions of locally presentable categories and the solution set condition, but as far as I remember, even though I already have most of the ingredients in order to formalize a version of the theorem, it would require more work on accessible functors/categories in order to be able to use it (e.g. the WIP PR #20267, which is about the accessibility of comma categories).

Sorry to revive this older thread, but I’d like to get a sense of where things stand before diving in.

I’m interested in a formalization of Hovey’s Model Category Structures on Chain Complexes of Sheaves (arXiv:math/9909024) as a stepping stone toward formalizing some of my own work on derived categories of noncommutative projective schemes. The main technical ingredient there is Hovey's recognition theorem for cofibrantly generated model categories (Theorem 2.1.19 from Model Categories), which yields the injective model structure on chain complexes in a Grothendieck category.

Before I start working on this, I wanted to check if there has been any progress on formalizing the recognition theorem (if anyone is working along that direction) or the surrounding machinery. I’d like to avoid duplicating effort, especially since earlier comments suggested that related work may already be ongoing.

[Joël Riou]

Note that the small object argument is already completely formalized, so that the recognition principle should be relatively accessible. Actually, in my formalization https://github.com/joelriou/topcat-model-category/blob/master/TopCatModelCategory/ModelCategoryTopCat.lean of the model category structure on topological spaces, the proof follows the lines of the recognition principle (the key lemma is that a Serre fibration is a weak equivalence iff it has the right lifting property with respect to the generating cofibrations, and the formal part of the argument shall be the same for the model category structure on simplicial sets, so that it would be nice if the recognition principle is formalized).

In order to prove that the assumptions of the recognition principle are satisfied for unbounded complexes in a Grothendieck abelian category, note that we already have the Freyd-Mitchell embedding theorem and the Gabriel-Popescu localization theorem. In some future (but not the immediate future), I would intend to work on the formalization of some results in the paper Sheafifiable homotopy model categories by Tibor Beke https://arxiv.org/abs/math/0102087 which involves locally presentable categories and the solution set condition (see Theorem 1.7). Proposition 3.13 in this paper is the construction of the injective model category on unbounded complexes in a Grothendieck abelian category. Whether in Hovey's paper or via this approach, there must be some technicalities in order to prove that the assumptions of the recognition theorem hold... In the approach following Beke, there are a lot of prerequisites about locally presentable/accessible categories, which I may work on in a reasonably near future.

[Joël Riou]

In both approaches in Beke's or Hovey's articles, there is a use of the Gabriel-Popescu theorem (already in mathlib) to say that the Grothendieck abelian category C that is considered is a localization (in a certain sense) of the category of modules over a ring R. Both argue using a result from the book by Bo Stenström, Rings and Modules of Quotients: the category C identifies to a "Giraud subcategory" of ModuleCat R, and theorem 10.2 p. 48 of this book classifies these Giraud subcategories in terms of "topologies" of R, which are families of ideals I in R satisfying certain properties. Then, C shall be the localization with respect to the inclusions I ⟶ R.
From this, Hovey deduces that all the objects in C satisfy a certain smallness property relatively to a cardinal, a condition which is (strictly?) weaker than the property satisfied by presentable objects (docs#CategoryTheory.IsCardinalPresentable). Beke shows the stronger result that C is a locally presentable category.
I have just formalised #30554 the "orthogonal reflection" theorem which is used by Beke which allows to deduce that C is locally presentable from the fact that ModuleCat R is locally presentable and that the "localization" is done with respect to a small family of morphisms (in this case this is a family of inclusions I ⟶ R of ideals).
Would you @Blake Farman be interested in formalizing this classification theorem of Giraud subcategories in ModuleCat R from Stenström's book?
(Apart from the recognition theorem for cofibrantly generated model categories, I believe that the rest of the construction of the "injective" model category on unbounded complexes would be subsumed by more general constructions from the theory of locally presentable and accessible categories as it appears in Beke's article and the book by Adámek and Rosický.)

[Blake Farman]

Thanks so much for the suggestion, @Joël Riou. This sounds really interesting, and I’d be glad to work on it. I’ll start digging into Stenström’s classification theorem and sketching things out in Lean. I'll report back once I have a clearer picture of the formalization. I might also pop back here with questions if I get stuck along the way.

[Robin Carlier]

Congratulations @Joël Riou for the milestone! I’m looking forward to reviewing the PRs! In your definition of anodyne extensions, did you go with the plan described in #Infinity-Cosmos > Functor quasi-categories are formalized @ 💬 to make life easier when working with inner anodyne extensions? I’m really looking forward using some of the infrastructure related to this formalization to the theory of quasi-categories (though, realistically, it’ll be a few month before I have the time to really work on this).

[Joël Riou]

I define anodyne extensions as the llp of the rlp of horn inclusions; and we may do the same for inner anodyne extensions. By the small object argument, this is the same as the completion under retracts of the class of transfinite compositions of pushouts of coproducts of (inner) horn inclusions. The strong (inner) anodyne extensions are those for which there is no need to take retracts.

In the definition of pairings #28332 (the combinatorial data describing a strong anodyne extensions), I have added a conditon IsInner, which, when I clean up the construction of the associated "relative cell complex" #28462 will show that we have a relative cell complex with cells that are inner horns. So yes, this "pairings" API will apply to both anodyne extensions (as initially defined by Gabriel and Zisman) and inner anodyne extensions.

For the applications to the model category structure, I was only interested in anodyne extensions (in particular : the subdivision functor preserves anodyne extensions) rather than strong anodyne extensions. If someone wants to develop the basic theory of strong (inner) anodyne extensions after #28462 is merged, they are very much welcome.

[Joël Riou]

As #28893 was merged today, the project https://github.com/joelriou/topcat-model-category now depends on the master branch of mathlib rather than on a custom branch.