The Smale conjecture for the three-sphere

The reference homomorphism from the orthogonal group of ℝ⁴ to the smooth self-diffeomorphisms of the round three-sphere is already continuous for the weak Whitney topology. This file records the sharp Smale conjecture: that this particular inclusion, rather than merely some homotopy equivalence between the two spaces, is itself a homotopy equivalence.

The proposition is the formal shape of Hatcher's theorem. It records the canonical map whose homotopy inverse compares the homotopy type of Diff (S³) with that of O(4). Continuity of the displayed map is supplied by TauCeti.continuous_orthogonalToDiffSphere.

Main definitions

• TauCeti.SmaleConjecture: the inclusion O(4) → Diff(S³) is a homotopy equivalence.

References

• A. Hatcher, A proof of the Smale conjecture, Diff(S³) ≃ O(4), Ann. of Math. 117 (1983), 553–607.
• R. Kirby, Problems in Low-Dimensional Topology, Problem 4.34.

def TauCeti.SmaleConjecture : Prop

Smale's conjecture for the three-sphere: the canonical continuous inclusion of the orthogonal group O(4) into the weak-Whitney space of smooth self-diffeomorphisms of the round three-sphere is a homotopy equivalence.

theorem TauCeti.smaleConjecture_iff_exists_homotopyInverse : SmaleConjecture ↔ ∃ (g : C(Diff (modelWithCornersSelf ℝ (EuclideanSpace ℝ (Fin 3))) ↑(Metric.sphere 0 1) ↑⊤, ↥(Matrix.orthogonalGroup (Fin 4) ℝ))), (g.comp (continuousOrthogonalToDiffSphere 3 ↑⊤)).Homotopic (ContinuousMap.id ↥(Matrix.orthogonalGroup (Fin (3 + 1)) ℝ)) ∧ ((continuousOrthogonalToDiffSphere 3 ↑⊤).comp g).Homotopic (ContinuousMap.id (Diff (modelWithCornersSelf ℝ (EuclideanSpace ℝ (Fin 3))) ↑(Metric.sphere 0 1) ↑⊤))

Characterize Smale's conjecture by a continuous inverse for the canonical inclusion and the two homotopies witnessing its inverse laws.