Hatcher: $\mathrm{Diff}(S^3)\simeq O(4)$

Open

SmaleDiffS4.diffSphere_three_homotopyEquiv_orth

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

diffeomorphism-groupsdifferential-topology

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

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

This is Hatcher's proof of the Smale conjecture, the case $n=3$ of the source's remark that $\mathrm{Diff}(S^n)\simeq O_{n+1}$ for $n\le 3$ . The analogous statement for $n=4$ is false (Watanabe).

Formalization Note As for $n=2$ , only the existence of some homotopy equivalence is asserted.

Preamble

import Mathlib
import Definitions.Def_SmaleDiffS4_Basic

open SmaleDiffS4

Formal statement

namespace SmaleDiffS4

theorem diffSphere_three_homotopyEquiv_orth :
    Nonempty (ContinuousMap.HomotopyEquiv (DiffSphere 3) (OrthGroup 4)) := 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; [H] A. Hatcher, A proof of a Smale conjecture, Diff(S^3) ≃ O(4), Ann. of Math. (2) 117 (1983), no. 3, 553–607.

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

Hatcher: Diff(S3)≃O(4)\mathrm{Diff}(S^3)\simeq O(4)Diff(S3)≃O(4)

Hatcher: $\mathrm{Diff}(S^3)\simeq O(4)$