Homotopy groups of spheres

TheoremThe fundamental group of the circle is infinite cyclic#●ready to prove

The fundamental group of the unit circle in \(\mathbb{C}\) based at \(1\) is isomorphic, as a group, to the additive group \(\mathbb{Z}\).

public theorem_wanted pi1_circle_mulEquiv_int :
    Nonempty (HomotopyGroup.Pi 1 Circle (1 : Circle) ≃* Multiplicative ℤ)

Sources

• Classical theorem in algebraic topology. Problem pi1_circle_mulEquiv_int of the lean-eval benchmark.

TheoremThe sixth homotopy group of the 3-sphere#●ready to prove

Let \(S^3\) be the unit sphere in Euclidean space \(\mathbb{R}^4\). For every point \(x \in S^3\), the homotopy group \(\pi_6(S^3, x)\) is isomorphic as a group to the cyclic group \(\mathbb{Z}/12\).

public theorem_wanted pi6_sphere_three_mulEquiv_zmod_twelve
    (x : Metric.sphere (0 : EuclideanSpace ℝ (Fin 4)) 1) :
    Nonempty
      (HomotopyGroup.Pi 6 (Metric.sphere (0 : EuclideanSpace ℝ (Fin 4)) 1) x ≃*
        Multiplicative (ZMod 12))

Sources

• H. Toda, 'Composition Methods in Homotopy Groups of Spheres', Annals of Mathematics Studies 49, Princeton University Press, 1962. The value pi_6(S^3) = Z/12 also appears in the tables of A. Hatcher, 'Algebraic Topology', Section 4.1. Problem pi6_sphere_three_mulEquiv_zmod_twelve of the lean-eval benchmark.

2 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.