Three Whitehead theorems

Stream: maths

[Johan Commelin]

@Dean Young It's great that you outlined your project over here: https://leanprover.zulipchat.com/#narrow/stream/113486-announce/topic/Whitehead.20Theorem
Since #announce isn't suited for longer discussions, I'm starting a thread here. You talk about an extensive outline for the project. Is that publicly available?

[Dean Young]

@Johan Commelin ,

thanks so much for making this space for the idea, and good question. The information about the project is publicly available at https://linearlibrary.net/ThreeWhiteheadTheorems/October11th.pdf. I'd also like to mention that any notation in the October11th file is pretty flexible going forward.

[Joël Riou]

As I do not know much about infinity categories, it is very difficult for me to relate to anything that is in this document. If I were actively trying to prove any version of Whitehead theorems I know of, I would proceed basically like this:

• formalize Serre fibrations of topological spaces (various equivalent definitions, construction of the homotopy sequence of a Serre fibration)
• formalize the axioms of model categories (which a few of us already know how to do): then any weak equivalence between fibrant and cofibrant objects are homotopy equivalences (this is a Whitehead type theorem, which I believe I have already formalised in Lean3)
• formalize the Quillen model category structure on topological spaces
• formalize the model category structure on simplicial sets

How does your strategy intersect with the constructions above?

[Dean Young]

Hi Joël,

Great question.

The core of the Whitehead theorem typically uses an extension property (HEP) such as the one in Hatcher's text on page 346. You're no doubt familiar with how such extension theorems lead to model structures, and so to answer your question I would like to illustrate the extension property that we will show.

Firstly, instead of CW-complexes we use a quite similar object formed by attaching objects Δⁿ along their boundaries ∂Δⁿ instead of discs Dₙ along their boundaries Sⁿ. We show the theorem by induction, reducing to the case of a "jar filling lemma" which extends a homotopy along a single attachment. Maybe you see why I want to call this HEP a "jar filling lemma": the jar shape is created by gluing (∂Δⁿ × I) with Δⁿ along ∂Δⁿ. The existence of the extension uses the quasi-category lifting condition by extending one simplex at a time (followed by a lid which completes the desired homotopy extension).

I hope this brief explanation of the relevant lifting lemma answers your question.

Unfortunately the October11th file does not feature this detail since I had only recently decided on a particular model. I also like the models you mention, and it would be great to hear your thoughts as to which model you think would be most useful or integrated.

[Joël Riou]

I did not mention CW-complexes!

[Joël Riou]

My question was more: do you intend to prove that topological spaces and simplicial sets have a model category structure (and there is a Quillen equivalence between the two)?

[Dean Young]

We don't prove any model structures for either. That part was the closest it came because of how it suggests a weak factorization system involving maps from a CW-complex to a point and their relative analogues.

However if it's something that would be useful for you then we can go ahead and add a model structure for topological spaces in.

[Joël Riou]

I only wish that while you develop your approach, we do not eventually get only an "isolated" theorem but also the relevant API. For example, it seems likely that what you suggest about "jars" is related to some classical results from Gabriel-Zisman Calculus of fractions and homotopy theory about different characterizations of the saturation of horns in the category of simplicial sets (IV.2 Anodyne extensions).

[Dean Young]

Consider the demonstration that two maps of chain complexes f, g : C𛲔 ⭢ D𛲔 with C𛲔 a chain complex of projectives bounded below, and such that (∀ n : Int), Hₙ f = Hₙ g, are homotopy equivalent. This proof typically accompanies "weak equivalent replacement with a projective complex". Similarly, our proof of Wa (Whitehead theorem a) features two parts: replacement (REPa) and homotopy extension (HEPa). I just wanted to mention that to clarify how such two-fold proofs can get by without proving a model structure.

Having mentioned that, I think it's a good idea to fill out the whole of various model structures involved, and including basics on anodyne maps seems like a good way to attract more users too.

Based on your suggestions, here are six fundamental definitions, suggesting three different model structures, which might make a good addition to the project:

• a left fibration if f has the right lifting property with respect to all
horn inclusions Λni ⊆ ∆n, 0 ≤ i < n.
• a right fibration if f has the right lifting property with respect to all
horn inclusions Λni ⊆ ∆n, 0 < i ≤ n.
• an inner fibration if f has the right lifting property with respect to all
horn inclusions Λni ⊆ ∆n, 0 < i < n.
A morphism of simplicial sets i : A → B is
• left anodyne if i has the left lifting property with respect to all left fibrations.
• right anodyne if i has the left lifting property with respect to all right fibrations.
• inner anodyne if i has the left lifting property with respect to all inner fibrations.

(See Lurie's HTT page 53.)

What do you think about the inclusion of three model structures involved in the above?

[Joël Riou]

For the standard model category structure on simplicial sets (the one which is the most useful for homotopy), the fibrations are Kan fibrations, which is a stronger condition than left/right/inner fibrations.

(Note that in case of homological algebra, I have mostly verified the axioms of model categories in the dual situation: the case of bounded below complexes in a category with enough injectives https://leanprover.zulipchat.com/#narrow/stream/335062-homology/topic/Derived.20functors . I am not completely sure that the exact phrasing of the lemma on projectives you mention is correct though.)