Cerf's theorem: every self-diffeomorphism of S3 is smoothly isotopic to a linear isometry
Problem statement
Notes: Cerf's 1968 theorem, the X = point (unparameterized) case of the Smale conjecture. Stated as the existence of a smooth isotopy [0,1] x S3 -> S3 from f to a linear isometry, witnessed by a smooth slice-inverse to encode the diffeomorphism property of each slice without needing a topology on Diffeomorph.
Source: J. Cerf, Sur les diffeomorphismes de la sphere de dimension trois, Lecture Notes in Mathematics 53, Springer (1968).
Informal solution: Cerf's original proof uses pseudo-isotopy theory: a self-diffeomorphism of S3 extends to a pseudo-isotopy of D4, and Cerf's theorem on the triviality of pi_0 of the pseudo-isotopy space in dimension 4 implies the extension is isotopic to a genuine isotopy. Hatcher (1983) reproved this as a corollary of the full Smale conjecture using configurations of 2-spheres.
theorem declaration uses `sorry`cerf_gamma_four (f : sphere (0 : EuclideanSpace ℝ (Fin 4)) 1 ≃ₘ⟮𝓡 3, 𝓡 3⟯
sphere (0 : EuclideanSpace ℝ (Fin 4)) 1) :
∃ (A : Matrix.orthogonalGroup (Fin 4) ℝ)
(F F' : unitInterval × sphere (0 : EuclideanSpace ℝ (Fin 4)) 1 →
sphere (0 : EuclideanSpace ℝ (Fin 4)) 1),
ContMDiff ((𝓡∂ 1).prod (𝓡 3)) (𝓡 3) ∞ F ∧
ContMDiff ((𝓡∂ 1).prod (𝓡 3)) (𝓡 3) ∞ F' ∧
(∀ t p, F (t, F' (t, p)) = p) ∧
(∀ t p, F' (t, F (t, p)) = p) ∧
(∀ p, F (0, p) = f p) ∧
(∀ p, (F (1, p) : EuclideanSpace ℝ (Fin 4)) =
Matrix.UnitaryGroup.toLinearEquiv A
(p : EuclideanSpace ℝ (Fin 4))) := f:↑(sphere 0 1) ≃ₘ⟮𝓡 3, 𝓡 3⟯ ↑(sphere 0 1)⊢ ∃ A F F',
ContMDiff ((𝓡∂ 1).prod (𝓡 3)) (𝓡 3) ∞ F ∧
ContMDiff ((𝓡∂ 1).prod (𝓡 3)) (𝓡 3) ∞ F' ∧
(∀ (t : ↑unitInterval) (p : ↑(sphere 0 1)), F (t, F' (t, p)) = p) ∧
(∀ (t : ↑unitInterval) (p : ↑(sphere 0 1)), F' (t, F (t, p)) = p) ∧
(∀ (p : ↑(sphere 0 1)), F (0, p) = f p) ∧
∀ (p : ↑(sphere 0 1)), (↑(F (1, p))).ofLp = (Matrix.UnitaryGroup.toLinearEquiv A) (↑p).ofLp
All goals completed! 🐙