Homotopy groups of spheres

Stream: mathlib4

[Aaron Liu]

I'm thinking of doing some Homotopy groups of spheres.

• What kind of stuff is in mathlib already? For example, do we have homotopy groups or a "standard sphere" I can use?
• How do I state theorems like π₄(S³) = ℤ/2ℤ?
• How much of this do we want in mathlib? I can't imagine having a whole table of homotopy groups but something like πₖ(Sⁿ) for k ≤ n could be useful.
• Are there any good references I could follow?

[Kenny Lau]

I would state it by either an IsHomotopyGroup predicate or a group isomorphism

[Junyan Xu]

• There's docs#HomotopyGroup and the standard S^n is probably sphere (0 : EuclideanSpace ℝ (Fin (n+1)) 1.
• The Hopf fibration has been discussed before #LftCM22 > Hopf fibration @ 💬 but apparently is still not in mathlib. We probably want to show that it's a generator of π₃(𝕊²) with infinite order so π₃(𝕊²) is isomorphic to ℤ, and that it's suspension generates π₄(𝕊³) and has order 2 (also in the stable homotopy group).
• πₖ(Sⁿ) for k < n shouldn't be hard, but for k = n we may need to wait for homology (?)
• I think the next thing to do about homotopy groups is https://en.wikipedia.org/wiki/Homotopy_group#Long_exact_sequence_of_a_fibration

[Joël Riou]

I have already formalized the long exact homotopy sequence of a fibration https://github.com/joelriou/topcat-model-category/blob/master/TopCatModelCategory/SSet/FibrationSequence.lean (this is for a Kan fibration of Kan simplicial sets, but this formally implies a similar result for a Serre fibration of topological spaces)