Isotopy classes of orthogonal transformations of a sphere

The reference inclusion TauCeti.orthogonalToDiffSphere : O(n + 1) → Diff(Sⁿ) induces an injective map on path components, for every dimension n and every smoothness exponent m of the weak Whitney topology: two orthogonal transformations of ℝⁿ⁺¹ are isotopic as diffeomorphisms of Sⁿ exactly when they have the same determinant. A path of diffeomorphisms is a homotopy of maps, because evaluation is continuous for the weak Whitney topology, and an orthogonal transformation acts on the reduced homology Hₙ(Sⁿ; ℤ) ≅ ℤ by the sign of its determinant; conversely matrices of equal determinant are joined in the orthogonal group (TauCeti.Matrix.joined_orthogonalGroup_iff_det_eq). In particular a reflection of Sⁿ is not isotopic to the identity, and Diff(Sⁿ) is never path-connected.

Main results

• TauCeti.det_eq_of_joined_orthogonalToDiffSphere: orthogonal transformations isotopic as diffeomorphisms of Sⁿ have the same determinant.
• TauCeti.joined_orthogonalToDiffSphere_iff: they are isotopic exactly when their determinants agree.
• TauCeti.not_joined_one_orthogonalToDiffSphere_of_det_eq_neg_one: an orthogonal transformation of determinant -1 is not isotopic to the identity.
• TauCeti.not_pathConnectedSpace_diff_sphere: the diffeomorphism group of a sphere is not path-connected.

theorem TauCeti.det_eq_of_joined_orthogonalToDiffSphere {n : ℕ} {m : WithTop ℕ∞} {A B : ↥(Matrix.orthogonalGroup (Fin (n + 1)) ℝ)} (h : Joined ((orthogonalToDiffSphere n m) A) ((orthogonalToDiffSphere n m) B)) : (↑A).det = (↑B).det

Isotopic orthogonal transformations have the same determinant. If the restrictions of two orthogonal transformations of ℝⁿ⁺¹ to the unit sphere Sⁿ are joined by a path of C^m diffeomorphisms, for the weak Whitney topology, then the two matrices have the same determinant.

theorem TauCeti.joined_orthogonalToDiffSphere_iff {n : ℕ} {m : WithTop ℕ∞} {A B : ↥(Matrix.orthogonalGroup (Fin (n + 1)) ℝ)} : Joined ((orthogonalToDiffSphere n m) A) ((orthogonalToDiffSphere n m) B) ↔ (↑A).det = (↑B).det

The isotopy classes of orthogonal transformations of a sphere. The restrictions of two orthogonal transformations of ℝⁿ⁺¹ to Sⁿ are joined by a path of C^m diffeomorphisms exactly when the two matrices have the same determinant. So the map π₀ O(n + 1) → π₀ Diff(Sⁿ) is injective, and its image consists of two path components.

theorem TauCeti.not_joined_one_orthogonalToDiffSphere_of_det_eq_neg_one {n : ℕ} {m : WithTop ℕ∞} {A : ↥(Matrix.orthogonalGroup (Fin (n + 1)) ℝ)} (hA : (↑A).det = -1) : ¬Joined 1 ((orthogonalToDiffSphere n m) A)

An orthogonal transformation of determinant -1, such as a reflection, is not isotopic to the identity as a diffeomorphism of the sphere.

theorem TauCeti.not_pathConnectedSpace_diff_sphere {n : ℕ} {m : WithTop ℕ∞} : ¬PathConnectedSpace (Diff (modelWithCornersSelf ℝ (EuclideanSpace ℝ (Fin n))) (↑(Metric.sphere 0 1)) m)

The diffeomorphism group of a sphere is not path-connected, for the weak Whitney C^m topology: a reflection of Sⁿ is not isotopic to the identity.