Higher homotopy groups of a torus

Every homotopy group of an indexed product is the indexed product of the homotopy groups of its factors. Since the homotopy groups of a real circle vanish in dimensions at least two, the same is true for any indexed product of real circles. In particular, all higher homotopy groups of the finite-dimensional torus Tᵏ vanish.

Together with the fundamental-group computation in TauCeti.AlgebraicTopology.UniversalCover.Torus.FundamentalGroup, this completes the π_n(Tᵏ) application in TauCetiRoadmap/UniversalCovers/README.md, Stage 4, item 13.

Main declarations

• AddCircle.subsingleton_homotopyGroup_pi: every homotopy group in dimension at least two of an indexed product of real circles is trivial.
• AddCircle.homotopyGroup_pi_eq_one, AddCircle.homotopyGroupPi_pi_eq_one: the corresponding equality statements.

instance AddCircle.subsingleton_homotopyGroup_pi {N : Type u_1} {ι : Type u_2} [Nontrivial N] (p : ι → ℝ) (x : (i : ι) → AddCircle (p i)) : Subsingleton (HomotopyGroup N ((i : ι) → AddCircle (p i)) x)

Every higher homotopy group of an indexed product of real circles is trivial. The index type N being nontrivial expresses that the homotopy dimension is at least two.

theorem AddCircle.homotopyGroup_pi_eq_one {N : Type u_1} {ι : Type u_2} [Nontrivial N] (p : ι → ℝ) (x : (i : ι) → AddCircle (p i)) [DecidableEq N] (a : HomotopyGroup N ((i : ι) → AddCircle (p i)) x) : a = 1

Every higher homotopy class of an indexed product of real circles is the identity.

theorem AddCircle.homotopyGroupPi_pi_eq_one {ι : Type u_2} (p : ι → ℝ) (x : (i : ι) → AddCircle (p i)) (n : ℕ) (a : HomotopyGroup.Pi (n + 2) ((i : ι) → AddCircle (p i)) x) : a = 1

Every element of π_(n + 2) of an indexed product of real circles is the identity.