Homeomorphism and diffeomorphism groups of spheres
TheoremCerf's theorem \(\Gamma_4 = 0\)#●ready to prove
Let \(S^3 \subset \mathbb{R}^4\) be the unit sphere. Every smooth diffeomorphism \(f\) of \(S^3\) is smoothly isotopic to the restriction of a linear isometry of \(\mathbb{R}^4\): there are an orthogonal matrix \(A \in O(4)\) and smooth maps \(F, F' : [0, 1] \times S^3 \to S^3\) such that for every \(t \in [0, 1]\) the maps \(F(t, \cdot)\) and \(F'(t, \cdot)\) are inverse to each other, and \(F(0, p) = f(p)\) and \(F(1, p) = Ap\) for all \(p \in S^3\).
public theorem_wanted 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)))Sources
- J. Cerf, Sur les diffeomorphismes de la sphere de dimension trois, Lecture Notes in Mathematics 53, Springer (1968). Problem
cerf_gamma_fourof the lean-eval benchmark.
TheoremNormal subgroups of the identity component of the homeomorphism group of a sphere#●ready to prove
Let \(n \ne 4\) be a natural number and let \(S^n\) be the unit sphere in \(\mathbb{R}^{n+1}\). Give the group \(\mathrm{Homeo}(S^n)\) of homeomorphisms of \(S^n\) the topology induced by the embedding \(h \mapsto (h, h^{-1})\) into pairs of continuous self-maps of \(S^n\) with the compact-open topology, and let \(G_0\) be the connected component of the identity in \(\mathrm{Homeo}(S^n)\). If \(N\) is a subgroup of \(\mathrm{Homeo}(S^n)\) contained in \(G_0\) such that \(h k h^{-1} \in N\) for all \(h \in G_0\) and \(k \in N\), then either \(N\) is the trivial subgroup or \(G_0 \subseteq N\). In other words, the only normal subgroups of \(G_0\) are the trivial one and \(G_0\) itself.
This is Ulam's Problem 29 of the Scottish Book, which asked the question for every \(n\); the case \(n = 4\) is excluded here. The restriction \(n \ne 4\) is the caveat attached to the sphere case in the Encyclopedia of Mathematics; Epstein's theorem itself is stated for manifolds in general.
theorem_wanted identity_component_of_sphere_homeomorphism_group_simple :
∀ (n : ℕ), n ≠ 4 →
∀ (N : Subgroup (↥(Metric.sphere (0 : EuclideanSpace ℝ (Fin (n + 1))) 1) ≃ₜ
↥(Metric.sphere (0 : EuclideanSpace ℝ (Fin (n + 1))) 1))),
(∀ h ∈ N, h ∈ connectedComponent 1) →
(∀ h ∈ connectedComponent 1, ∀ k ∈ N, h * k * h⁻¹ ∈ N) →
N = ⊥ ∨ ∀ h, h ∈ connectedComponent 1 → h ∈ NSources
- S. Ulam, Problem 29 of the Scottish Book; D. B. A. Epstein, The simplicity of certain groups of homeomorphisms, Compositio Mathematica 22 (1970), 165-173; see the commentary in R. D. Mauldin (ed.), The Scottish Book, 2nd ed. (Birkhäuser, 2015).
TheoremSmale conjecture (Hatcher), relative parametrized form#●ready to prove
Let \(n \ge 1\) and let \(X\) be a compact, Hausdorff, second-countable smooth manifold with boundary modelled on the \(n\)-dimensional half-space, with boundary \(\partial X\). Write \(S^3\) for the unit sphere of \(\mathbb{R}^4\) and let the orthogonal group \(O(4)\) act linearly on it. Let \(F, F' : X \times S^3 \to S^3\) be smooth maps with \(F(x, F'(x, p)) = p\) and \(F'(x, F(x, p)) = p\) for all \(x \in X\) and \(p \in S^3\), and let \(\psi_\partial : \partial X \to O(4)\) be a continuous map with \(F(b, p) = \psi_\partial(b)\, p\) for all \(b \in \partial X\) and \(p \in S^3\). Then there are a continuous map \(\psi : X \to O(4)\) that agrees with \(\psi_\partial\) on \(\partial X\) and smooth maps \(H, H' : X \times [0, 1] \times S^3 \to S^3\) such that for all \(x \in X\), \(t \in [0, 1]\) and \(p \in S^3\) we have \(H(x, t, H'(x, t, p)) = p\), \(H'(x, t, H(x, t, p)) = p\), \(H(x, 0, p) = F(x, p)\) and \(H(x, 1, p) = \psi(x)\, p\), and \(H(b, t, p) = F(b, p)\) whenever \(b \in \partial X\).
Thus each \(F(x, \cdot)\) is a diffeomorphism of \(S^3\), and \(H\) is a smooth isotopy through diffeomorphisms, relative to \(\partial X\), from the family \(F\) to the linear family \(\psi\).
MathlibExt.Topology.SmaleConjectureWanted.Topology.smale_conjecture · 36 lines
public theorem_wanted 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))Sources
- A. Hatcher, A proof of the Smale conjecture, Diff(S3) = O(4), Ann. of Math. 117 (1983). Problem
smale_conjectureof the lean-eval benchmark.
TheoremThe four-dimensional Smale conjecture is false (Watanabe)#●ready to prove
Write \(S^4\) for the unit sphere of \(\mathbb{R}^5\) and let the orthogonal group \(O(5)\) act linearly on it. There are an \(n \ge 1\), a compact, Hausdorff, second-countable smooth manifold \(X\) with boundary modelled on the \(n\)-dimensional half-space, with boundary \(\partial X\), smooth maps \(F, F' : X \times S^4 \to S^4\) with \(F(x, F'(x, p)) = p\) and \(F'(x, F(x, p)) = p\) for all \(x \in X\) and \(p \in S^4\), and a continuous map \(\psi_\partial : \partial X \to O(5)\) with \(F(b, p) = \psi_\partial(b)\, p\) for all \(b \in \partial X\) and \(p \in S^4\), such that the following fails: there are a continuous map \(\psi : X \to O(5)\) that agrees with \(\psi_\partial\) on \(\partial X\) and smooth maps \(H, H' : X \times [0, 1] \times S^4 \to S^4\) such that for all \(x \in X\), \(t \in [0, 1]\) and \(p \in S^4\) we have \(H(x, t, H'(x, t, p)) = p\), \(H'(x, t, H(x, t, p)) = p\), \(H(x, 0, p) = F(x, p)\) and \(H(x, 1, p) = \psi(x)\, p\), and \(H(b, t, p) = F(b, p)\) whenever \(b \in \partial X\).
In other words, the relative parametrized form of the statement that \(O(5) \to \mathrm{Diff}(S^4)\) is a homotopy equivalence, the analogue of Hatcher's theorem for \(S^3\), does not hold.
MathlibExt.Topology.WatanabeSmaleDisproofWanted.Topology.watanabe_four_dim_smale_disproof · 36 lines
public theorem_wanted 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)))Sources
- 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). Problem
watanabe_four_dim_smale_disproofof the lean-eval benchmark.
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.