Smale conjecture (Hatcher) in relative parameterized form
Problem statement
Notes: Hatcher's 1983 theorem that Diff(S3) is homotopy equivalent to O(4), stated in the relative-parameterized-family form (families on a compact manifold-with-boundary X whose boundary already factors through O(4) deform rel boundary to a family fully factoring through O(4)). Mathlib does not yet carry the C-infinity topology on Diffeomorph, which would be needed for the direct homotopy-equivalence formulation.
Source: A. Hatcher, A proof of the Smale conjecture, Diff(S3) = O(4), Ann. of Math. 117 (1983).
Informal solution: Hatcher proves Diff(S3) is homotopy equivalent to O(4) by analyzing configurations of 2-spheres in S3 (the bigon criterion) and deducing by induction that every self-diffeomorphism is isotopic to a linear one, with all higher parameterized versions handled by the same incompressible-surface machinery.
theorem declaration uses `sorry`smale_conjecture {n : ℕ} [NeZero n]
(X : Type) [TopologicalSpace X] [T2Space X] [SecondCountableTopology X]
[ChartedSpace (EuclideanHalfSpace n) X] [IsManifold (𝓡∂ n) ∞ X]
[CompactSpace X]
(F F' : X × sphere (0 : EuclideanSpace ℝ (Fin 4)) 1 →
sphere (0 : EuclideanSpace ℝ (Fin 4)) 1)
(hF : ContMDiff ((𝓡∂ n).prod (𝓡 3)) (𝓡 3) ∞ F)
(hF' : ContMDiff ((𝓡∂ n).prod (𝓡 3)) (𝓡 3) ∞ F')
(hFinv₁ : ∀ x p, F (x, F' (x, p)) = p)
(hFinv₂ : ∀ x p, F' (x, F (x, p)) = p)
(ψ_bdry : (𝓡∂ n).boundary X → Matrix.orthogonalGroup (Fin 4) ℝ)
(hψ_bdry_cont : Continuous ψ_bdry)
(hF_bdry : ∀ (b : (𝓡∂ n).boundary X)
(p : sphere (0 : EuclideanSpace ℝ (Fin 4)) 1),
(F ((b : X), p) : EuclideanSpace ℝ (Fin 4)) =
Matrix.UnitaryGroup.toLinearEquiv (ψ_bdry b)
(p : EuclideanSpace ℝ (Fin 4))) :
∃ (ψ : X → Matrix.orthogonalGroup (Fin 4) ℝ)
(H H' : X × unitInterval × sphere (0 : EuclideanSpace ℝ (Fin 4)) 1 →
sphere (0 : EuclideanSpace ℝ (Fin 4)) 1),
Continuous ψ ∧
(∀ b : (𝓡∂ n).boundary X, ψ (b : X) = ψ_bdry b) ∧
ContMDiff ((𝓡∂ n).prod ((𝓡∂ 1).prod (𝓡 3))) (𝓡 3) ∞ H ∧
ContMDiff ((𝓡∂ n).prod ((𝓡∂ 1).prod (𝓡 3))) (𝓡 3) ∞ H' ∧
(∀ x t p, H (x, t, H' (x, t, p)) = p) ∧
(∀ x t p, H' (x, t, H (x, t, p)) = p) ∧
(∀ x p, H (x, 0, p) = F (x, p)) ∧
(∀ x (p : sphere (0 : EuclideanSpace ℝ (Fin 4)) 1),
(H (x, 1, p) : EuclideanSpace ℝ (Fin 4)) =
Matrix.UnitaryGroup.toLinearEquiv (ψ x)
(p : EuclideanSpace ℝ (Fin 4))) ∧
(∀ (b : (𝓡∂ n).boundary X)
(t : unitInterval)
(p : sphere (0 : EuclideanSpace ℝ (Fin 4)) 1),
H ((b : X), t, p) = F ((b : X), p)) := n:ℕinst✝⁶:NeZero nX:Typeinst✝⁵:TopologicalSpace Xinst✝⁴:T2Space Xinst✝³:SecondCountableTopology Xinst✝²:ChartedSpace (EuclideanHalfSpace n) Xinst✝¹:IsManifold (𝓡∂ n) ∞ Xinst✝:CompactSpace XF:X × ↑(sphere 0 1) → ↑(sphere 0 1)F':X × ↑(sphere 0 1) → ↑(sphere 0 1)hF:ContMDiff ((𝓡∂ n).prod (𝓡 3)) (𝓡 3) ∞ FhF':ContMDiff ((𝓡∂ n).prod (𝓡 3)) (𝓡 3) ∞ F'hFinv₁:∀ (x : X) (p : ↑(sphere 0 1)), F (x, F' (x, p)) = phFinv₂:∀ (x : X) (p : ↑(sphere 0 1)), F' (x, F (x, p)) = pψ_bdry:↑(ModelWithCorners.boundary X) → ↥(Matrix.orthogonalGroup (Fin 4) ℝ)hψ_bdry_cont:Continuous ψ_bdryhF_bdry:∀ (b : ↑(ModelWithCorners.boundary X)) (p : ↑(sphere 0 1)),
(↑(F (↑b, p))).ofLp = (Matrix.UnitaryGroup.toLinearEquiv (ψ_bdry b)) (↑p).ofLp⊢ ∃ ψ H H',
Continuous ψ ∧
(∀ (b : ↑(ModelWithCorners.boundary X)), ψ ↑b = ψ_bdry b) ∧
ContMDiff ((𝓡∂ n).prod ((𝓡∂ 1).prod (𝓡 3))) (𝓡 3) ∞ H ∧
ContMDiff ((𝓡∂ n).prod ((𝓡∂ 1).prod (𝓡 3))) (𝓡 3) ∞ H' ∧
(∀ (x : X) (t : ↑unitInterval) (p : ↑(sphere 0 1)), H (x, t, H' (x, t, p)) = p) ∧
(∀ (x : X) (t : ↑unitInterval) (p : ↑(sphere 0 1)), H' (x, t, H (x, t, p)) = p) ∧
(∀ (x : X) (p : ↑(sphere 0 1)), H (x, 0, p) = F (x, p)) ∧
(∀ (x : X) (p : ↑(sphere 0 1)),
(↑(H (x, 1, p))).ofLp = (Matrix.UnitaryGroup.toLinearEquiv (ψ x)) (↑p).ofLp) ∧
∀ (b : ↑(ModelWithCorners.boundary X)) (t : ↑unitInterval) (p : ↑(sphere 0 1)),
H (↑b, t, p) = F (↑b, p)
All goals completed! 🐙