Smale: $\mathrm{Diff}(S^2)\simeq O(3)$

Open

SmaleDiffS4.diffSphere_two_homotopyEquiv_orth

by Lucas · Oct 11, 2026 · Mathlib 0df444a (Lean v4.33.1)

diffeomorphism-groupsdifferential-topology

Let $\mathrm{Diff}(S^2)$ be the group of all smooth diffeomorphisms of the round unit sphere $S^2\subset\mathbb R^3$ with the $C^\infty$ topology, and $O(3)$ the orthogonal group. Then

\mathrm{Diff}(S^2)\;\simeq\;O(3).

This is the case $n=2$ of the source's remark that $\mathrm{Diff}(S^n)$ has the homotopy type of $O_{n+1}$ for $n\le 3$ ; it is the low-dimensional model for what fails in dimension $4$ .

Formalization Note The statement asserts that some homotopy equivalence exists (the source says "has the homotopy type of"); it does not require the inclusion $O(3)\hookrightarrow\mathrm{Diff}(S^2)$ to be the equivalence.

Preamble

import Mathlib
import Definitions.Def_SmaleDiffS4_Basic

open SmaleDiffS4

Formal statement

namespace SmaleDiffS4

theorem diffSphere_two_homotopyEquiv_orth :
    Nonempty (ContinuousMap.HomotopyEquiv (DiffSphere 2) (OrthGroup 3)) := by sorry

end SmaleDiffS4

Source

Open Problem Garden, 'What is the homotopy type of the group of diffeomorphisms of the 4-sphere?' (S. Smale; posted by rybu, 2009), http://www.openproblemgarden.org/op/what_is_the_homotopy_type_of_the_group_of_diffeomorphisms_of_the_4_sphere — discussion paragraph 2: 'Diff(S^n) is known to have the homotopy-type of O_{n+1} provided n ≤ 3 by work of Hatcher and Smale respectively'; [S] S. Smale, Diffeomorphisms of the 2-sphere, Proc. Amer. Math. Soc. 10 (1959) 621–626.

Human review

Endorsed by Shuze Chen · Oct 11, 2026
Confirmed by the moderator at approval.
Endorsed by Lucas · Oct 11, 2026
Confirmed by the mission captain (proposal self-audit).

View graph

Smale: Diff(S2)≃O(3)\mathrm{Diff}(S^2)\simeq O(3)Diff(S2)≃O(3)

Smale: $\mathrm{Diff}(S^2)\simeq O(3)$