Watanabe's disproof of the 4-dimensional Smale conjecture
watanabe_four_dim_smale_disproof
Submitter: Kim Morrison.
Notes: Resolves [Kir97, Problems 4.34 and 4.126] negatively: the 4-dimensional generalized Smale conjecture (O(5) ↪ Diff(S⁴) is a homotopy equivalence, equivalently Diff(D⁴ rel ∂) is contractible) is false. Watanabe showed πₖ(Diff(D⁴ rel ∂)) ⊗ ℚ ≠ 0 for many k, including k = 1, via configuration-space integrals. We state this as the negation of the exact four-dimensional analogue of the (true) S³ Smale conjecture in SmaleConjecture.lean — relative parameterized form, because Mathlib has no C^∞ topology on diffeomorphism groups yet.
Source: T. Watanabe, *Some exotic nontrivial elements of the rational homotopy groups of Diff(S⁴)*, arXiv:1812.02448 (2018). Pairs with the positive S³ statement of Hatcher (Ann. of Math. 117, 1983) in SmaleConjecture.lean.
Informal solution: No formalization is feasible today: this needs the C^∞ topology on diffeomorphism groups, configuration-space integrals / Kontsevich classes, and the graph-cohomology machinery Watanabe uses. The statement is the negation of the parameterized homotopy-equivalence claim, which Watanabe's nontriviality result refutes.
theorem declaration uses `sorry`watanabe_four_dim_smale_disproof :
¬ (∀ {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 5)) 1 →
sphere (0 : EuclideanSpace ℝ (Fin 5)) 1),
ContMDiff ((𝓡∂ n).prod (𝓡 4)) (𝓡 4) ∞ F →
ContMDiff ((𝓡∂ n).prod (𝓡 4)) (𝓡 4) ∞ F' →
(∀ x p, F (x, F' (x, p)) = p) →
(∀ x p, F' (x, F (x, p)) = p) →
∀ (ψ_bdry : (𝓡∂ n).boundary X → Matrix.orthogonalGroup (Fin 5) ℝ),
Continuous ψ_bdry →
(∀ (b : (𝓡∂ n).boundary X)
(p : sphere (0 : EuclideanSpace ℝ (Fin 5)) 1),
(F ((b : X), p) : EuclideanSpace ℝ (Fin 5)) =
Matrix.UnitaryGroup.toLinearEquiv (ψ_bdry b)
(p : EuclideanSpace ℝ (Fin 5))) →
∃ (ψ : X → Matrix.orthogonalGroup (Fin 5) ℝ)
(H H' : X × unitInterval × sphere (0 : EuclideanSpace ℝ (Fin 5)) 1 →
sphere (0 : EuclideanSpace ℝ (Fin 5)) 1),
Continuous ψ ∧
(∀ b : (𝓡∂ n).boundary X, ψ (b : X) = ψ_bdry b) ∧
ContMDiff ((𝓡∂ n).prod ((𝓡∂ 1).prod (𝓡 4))) (𝓡 4) ∞ H ∧
ContMDiff ((𝓡∂ n).prod ((𝓡∂ 1).prod (𝓡 4))) (𝓡 4) ∞ 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 5)) 1),
(H (x, 1, p) : EuclideanSpace ℝ (Fin 5)) =
Matrix.UnitaryGroup.toLinearEquiv (ψ x)
(p : EuclideanSpace ℝ (Fin 5))) ∧
(∀ (b : (𝓡∂ n).boundary X)
(t : unitInterval)
(p : sphere (0 : EuclideanSpace ℝ (Fin 5)) 1),
H ((b : X), t, p) = F ((b : X), p))) := ⊢ ¬∀ {n : ℕ} [inst : NeZero n] (X : Type) [inst_1 : TopologicalSpace X] [T2Space X] [SecondCountableTopology X]
[inst_4 : ChartedSpace (EuclideanHalfSpace n) X] [IsManifold (𝓡∂ n) ∞ X] [CompactSpace X]
(F F' : X × ↑(sphere 0 1) → ↑(sphere 0 1)),
ContMDiff ((𝓡∂ n).prod (𝓡 4)) (𝓡 4) ∞ F →
ContMDiff ((𝓡∂ n).prod (𝓡 4)) (𝓡 4) ∞ F' →
(∀ (x : X) (p : ↑(sphere 0 1)), F (x, F' (x, p)) = p) →
(∀ (x : X) (p : ↑(sphere 0 1)), F' (x, F (x, p)) = p) →
∀ (ψ_bdry : ↑(ModelWithCorners.boundary X) → ↥(Matrix.orthogonalGroup (Fin 5) ℝ)),
Continuous ψ_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 (𝓡 4))) (𝓡 4) ∞ H ∧
ContMDiff ((𝓡∂ n).prod ((𝓡∂ 1).prod (𝓡 4))) (𝓡 4) ∞ 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! 🐙Solved by
Not yet solved.