change of basepoint for homotopy groups `π_ n`

Stream: Is there code for X?

[Jiazhen Xia]

In the header of Topology/Homotopy/HomotopyGroup.lean (link here), it is stated that path-induced homomorphisms have not been formalized.

I'd be glad to help if this is needed in Mathlib. As part of my formalization for Whitehead theorem, I implemented the change-of-base-point maps for π_ n (link here).

Related PR: #33108 @Junyan Xu

[Joël Riou]

I did formalize the action of the fundamental groupoid on higher homotopy groups in the case of Kan complexes https://github.com/joelriou/topcat-model-category/blob/202ea039d99ada0d4bc1d8223d2bf4f51d8208f5/TopCatModelCategory/SSet/FundamentalGroupoidAction.lean#L434 (arguably, this action for topological spaces is a particular case).
For topological spaces, it was done in Lean 3 by @Reid Barton https://github.com/rwbarton/lean-homotopy-theory/blob/lean-3.4.2/src/homotopy_theory/topological_spaces/pi_n.lean
It would certainly be useful to have this in mathlib!

[Jiazhen Xia]

Hi Prof. Riou, I just watched your presentation at Lean Together 2026, and I'm happy to learn that your work neatly gives the Whitehead theorem as a corollary. I also completed a formalization of Whitehead theorem (link here), but I worked directly with topological spaces most of the time; your model category approach is indeed cleaner and more extensible. (I wrote up my formalization into a Master's thesis in computer science at Zhejiang University, and I did mention your approach in the introduction chapter.)

Do you plan to transfer your work into mathlib? Maybe I can help with that, and then specialize to the action for topological spaces.

[Joël Riou]

Yes, I plan to upstream almost 100% of my formalization of the model category structures on topological spaces (and simplicial sets). The model structure on TopCat uses a lot of results about Kan complexes. In your formalization, it seems you use arguments based on the homotopy extension property in order to define the transport of elements in homotopy groups along a path. This homotopy extension property is very much related to the lifting properties of Kan fibrations with respect to anodyne extensions between simplicial sets that I am using in my formalization, and the topological case should be a particular case of these results in the case of Kan complexes (if X is a topological space, we may apply these to the Kan complex Sing X).
If you had used explicit (painful!) formulas in order to define the action, it would have definitely been very interesting to have this approach as well, but as both our formalizations rely on the same basic principles, it is probably easier to use on the "anodyne extensions" approach.
The only thing that I am not completely sure about is how to relate the simplicial homotopy groups of a Kan complex (or a topological space) to the "cubical" homotopy groups (which is the definition that we have in mathlib for topological spaces): there are various ways to compare them, and I am not sure yet what is the best strategy.

[Jiazhen Xia]

Joël Riou said:

it seems you use arguments based on the homotopy extension property in order to define the transport of elements in homotopy groups along a path

That's right (the exact location in my code is here). But I did use explicit formulas (i.e., this, this, and this) to prove the homotopy extension property. These formulas define the radial projection (see figure below) in Hatcher's proposition 0.16. With these, it's not too difficult to re-write my definition of the action to avoid Classical.choose.

image.png