Higher homotopy groups of the circle

The real line covers every real additive circle AddCircle p. This file combines that covering with the invariance of higher homotopy groups under covering maps to show that all homotopy groups of a circle in dimensions at least two are trivial. The complex unit circle Circle is homeomorphic to AddCircle (2 * π), and the unit circle of EuclideanSpace ℝ (Fin 2) is homeomorphic to Circle, so the higher homotopy groups of those two models vanish as well.

The only calculation needed in the total space is elementary: any two generalized loops in a real topological vector space are homotopic relative to the cube boundary, so all homotopy groups of such a space are subsingletons (HomotopyGroup.subsingleton_of_topologicalVectorSpace). Applying the covering-map isomorphism for ℝ → AddCircle p gives the circle calculation.

This proves Stage 4, item 11 of the Tau Ceti universal-covers roadmap (TauCetiRoadmap/UniversalCovers/README.md): π_n(S¹) = 0 for n ≥ 2.

Main declarations

• AddCircle.subsingleton_homotopyGroup: π_N(AddCircle p) is trivial when N has at least two elements; instance resolution specializes it to π_(n + 2).
• AddCircle.homotopyGroup_eq_one, AddCircle.homotopyGroupPi_eq_one: the corresponding equalities.
• Circle.subsingleton_homotopyGroup, Circle.homotopyGroup_eq_one and Circle.homotopyGroupPi_eq_one: the same statements for the complex unit circle.
• TauCeti.EuclideanSpace.subsingleton_homotopyGroup_sphere, TauCeti.EuclideanSpace.homotopyGroup_sphere_eq_one and TauCeti.EuclideanSpace.homotopyGroupPi_sphere_eq_one: the same statements for the unit circle of EuclideanSpace ℝ (Fin 2), the model in which the Euclidean spheres are stated.

The covering map is Junyan Xu's AddCircle.isCoveringMap_coe in Mathlib.Topology.Covering.AddCircle.

instance AddCircle.subsingleton_homotopyGroup {N : Type u_1} [Nontrivial N] (p : ℝ) (x : AddCircle p) : Subsingleton (HomotopyGroup N (AddCircle p) x)

Every higher homotopy group of a real circle is trivial. The index type N being nontrivial expresses that the dimension is at least two.

theorem AddCircle.homotopyGroup_eq_one {N : Type u_1} [Nontrivial N] (p : ℝ) (x : AddCircle p) [DecidableEq N] (a : HomotopyGroup N (AddCircle p) x) : a = 1

Every higher homotopy class of a real circle is the identity.

theorem AddCircle.homotopyGroupPi_eq_one (p : ℝ) (x : AddCircle p) (n : ℕ) (a : HomotopyGroup.Pi (n + 2) (AddCircle p) x) : a = 1

Every element of π_(n + 2) of a real circle is the identity.

instance Circle.subsingleton_homotopyGroup {N : Type u_1} [Nontrivial N] (z : Circle) : Subsingleton (HomotopyGroup N Circle z)

Every higher homotopy group of the complex unit circle is trivial.

theorem Circle.homotopyGroup_eq_one {N : Type u_1} [Nontrivial N] (z : Circle) [DecidableEq N] (a : HomotopyGroup N Circle z) : a = 1

Every higher homotopy class of the complex unit circle is the identity.

theorem Circle.homotopyGroupPi_eq_one (z : Circle) (n : ℕ) (a : HomotopyGroup.Pi (n + 2) Circle z) : a = 1

Every element of π_(n + 2) of the complex unit circle is the identity.

instance TauCeti.EuclideanSpace.subsingleton_homotopyGroup_sphere {N : Type u_1} [Nontrivial N] (y : ↑(Metric.sphere 0 1)) : Subsingleton (HomotopyGroup N (↑(Metric.sphere 0 1)) y)

Every higher homotopy group of the unit circle of EuclideanSpace ℝ (Fin 2) is trivial.

theorem TauCeti.EuclideanSpace.homotopyGroup_sphere_eq_one {N : Type u_1} [Nontrivial N] (y : ↑(Metric.sphere 0 1)) [DecidableEq N] (a : HomotopyGroup N (↑(Metric.sphere 0 1)) y) : a = 1

Every higher homotopy class of the unit circle of EuclideanSpace ℝ (Fin 2) is the identity.

theorem TauCeti.EuclideanSpace.homotopyGroupPi_sphere_eq_one (y : ↑(Metric.sphere 0 1)) (n : ℕ) (a : HomotopyGroup.Pi (n + 2) (↑(Metric.sphere 0 1)) y) : a = 1

Every element of π_(n + 2) of the unit circle of EuclideanSpace ℝ (Fin 2) is the identity.