homotopy theory

Stream: maths

[Dean Young]

Does mathlib4 have a model category type? I am trying to show that something is Quillen equivalent to CW-complexes.

[Yury G. Kudryashov]

Please create a new topic instead of posting to an unrelevant one.

[Dean Young]

Does math lib have the homotopy category?

[Dean Young]

Can somebody help me out a bit? I am looking for the math lib constructions of

• homotopy colimits
• homotopy pullback
• pi0
• CW-complexes

[Notification Bot]

4 messages were moved here from #mathlib4 > lean4#2074 (new-style structures) by Yury G. Kudryashov.

[Yury G. Kudryashov]

@Kind Bubble I moved your messages to a new topic. Please don't post to a random topic next time.

[Yury G. Kudryashov]

Did you search for the word "homotopy" in the mathlib repo?

[Yury G. Kudryashov]

Note that you should use the Lean 3 version because many "advanced" files were not ported to mathlib 4 yet.

[Adam Topaz]

We don't have model categories. But we do have many people who thought about formalizing model categories.

[Dean Young]

What about a model of the homotopy category?

[Adam Topaz]

What do you want exactly?

[Dean Young]

Preferably CW-complexes.

[Adam Topaz]

We don't have CW complexes

[Dean Young]

What about point-set topological spaces?

[Adam Topaz]

Yes, we have those of course. We also have geometric realizations of simplicial sets.

[Dean Young]

can you give me a link to where this is built up? Is there a point-set-topological-space-for-Lean tutorial?

[Adam Topaz]

If you can explain what you're trying to prove more precisely, then it would be easier to say whether it is feasible or not

[Adam Topaz]

docs#topological_space

[Adam Topaz]

Your lean experience would be much smoother if you figure out how to use the api search

[Adam Topaz]

https://leanprover-community.github.io/mathlib_docs

[Dean Young]

Thanks so much Adam. What's the API search?

[Adam Topaz]

See the last link above

[Dean Young]

I have a model for the homotopy category- that much is already done. But the main goal is to show quillen equivalence with whatever the most mainstream one is.

[Adam Topaz]

I think the category of simplicial sets would be the most natural choice for that

[Adam Topaz]

docs#sSet

[Adam Topaz]

What model did you construct?

[Dean Young]

I think with simplicial sets I would need recourse to topological spaces unless I restricted to the ones which have the lifting conditions of an ∞-groupoid. Whitehead's theorem and the cellular approximation theorem are major milestones. Unfortunately the model I made is kind of involved so I can't describe it at the moment. Usually they involve something which demands that the space of double base point preserving maps f: [0, 1] -> [0, 1] v ... v [0, 1] is contractible.

[Adam Topaz]

Stating the infinity groupoid condition is easy, since we have horns already in mathlib. As I said above, we also have the geometric realization functor from sSet to Top

[Adam Topaz]

The whole formalism necessary to state the concept of a Quillen adjunction still needs to be developed though.

[Reid Barton]

See also https://github.com/rwbarton/lean-model-categories/tree/top-dev which got most of the way through constructing the model category Top, but it's for an ancient version of mathlib

[Joël Riou]

In https://github.com/joelriou/homotopical_algebra/tree/main/src/for_mathlib/algebraic_topology/homotopical_algebra, I have obtained some basic results on model categories, like the fundamental lemma of homotopical algebra (computation of morphisms in the localized category using homotopy classes of morphisms...). I have been thinking recently about total (left/right) derived functors, so that stating what a Quillen adjunction is should not be very hard. However, proving that there is a Quillen equivalence requires that we already know both categories are model categories... I am afraid the hardest parts should be more about constructing these model category structures rather than about getting an equivalence. I would suggest starting with topological spaces (or compactly generated hausdorff spaces?).