The orthogonal group acts on the sphere by diffeomorphisms #
A linear isometry equivalence of a real inner product space E preserves norms, so it restricts
to a self-map of the unit sphere; this file shows that restriction is a diffeomorphism of the
sphere as an analytic manifold, and assembles the restrictions into a group homomorphism
(E ≃ₗᵢ[ℝ] E) →* Diff (𝓡 n) (sphere (0 : E) 1) m into the self-diffeomorphism group of
TauCeti.Geometry.Diffeomorphism.Group. Taking E = EuclideanSpace ℝ (Fin (n + 1)), whose
linear isometry group is the orthogonal group O(n + 1), this is the reference inclusion
O(n + 1) → Diff(Sⁿ).
The inclusion is continuous for the subspace topology on O(n + 1) and the weak Whitney C^m
topology on the diffeomorphism group, from TauCeti.Geometry.Diffeomorphism.Topology. More
generally, restricting a continuous family of linear isometry equivalences to the unit sphere
gives a continuous family of C^m maps. This is the map whose source and target the Smale
conjecture Diff(S³) ≃ O(4) ([Kir97, Problem 4.34], Hatcher) compares: the conjecture asserts
that TauCeti.orthogonalToDiffSphere 3 ω is a homotopy equivalence, a statement that needs the
continuity proved here.
Main definitions #
LinearIsometryEquiv.unitSphereEquiv: the self-equivalence of the unit sphere obtained by restricting a linear isometry equivalence.LinearIsometryEquiv.unitSphereDiffeomorph: that restriction as aC^mdiffeomorphism of the unit sphere, viewed as a manifold modelled on𝓡 n.LinearIsometryEquiv.unitSphereDiffHom: the group homomorphism(E ≃ₗᵢ[ℝ] E) →* Diff (𝓡 n) (sphere (0 : E) 1) m.TauCeti.orthogonalToDiffSphere: the reference inclusionO(n + 1) → Diff(Sⁿ), the caseE = EuclideanSpace ℝ (Fin (n + 1))ofunitSphereDiffHom.
Main results #
LinearIsometryEquiv.contMDiff_unitSphereEquiv: the restriction to the unit sphere isC^mfor every smoothness exponent, so the linear isometry group acts on the unit sphere byC^mmaps (aContMDiffConstSMulinstance).LinearIsometryEquiv.mvfderiv_coe_sphere_unitSphereEquiv: the differential of the restriction, read in the ambient spaces through the sphere inclusions, is the linear isometry itself.LinearIsometryEquiv.isometry_unitSphereEquiv: it is an isometry for the distance the sphere inherits fromE, so the action is by isometries of the round sphere.LinearIsometryEquiv.unitSphereDiffeomorph_neg_apply: the diffeomorphism induced by-1 ∈ O(n + 1)is the antipodal map.TauCeti.LinearMap.eq_of_eqOn_unitSphere: a linear map is determined by its values on the unit sphere, whenceLinearIsometryEquiv.unitSphereDiffHom_injectiveandTauCeti.orthogonalToDiffSphere_injective: the inclusion is injective, soO(n + 1)is realised as a subgroup ofDiff(Sⁿ).Continuous.toContMDiffMap_unitSphereDiffeomorph: the restriction to the unit sphere of a continuous family of linear isometry equivalences is continuous in the weak Whitney topology.TauCeti.continuous_orthogonalToDiffSphere: the reference inclusionO(n + 1) → Diff(Sⁿ)is continuous.TauCeti.continuousOrthogonalToDiffSphere: the reference inclusion packaged as a continuous map.
Implementation notes #
The declarations extending LinearIsometryEquiv here and in
TauCeti.Geometry.Sphere.LinearIsometry live in the root-level LinearIsometryEquiv namespace,
allowing receiver notation. The reference inclusion remains project-owned top-level API in
TauCeti; the auxiliary linear-map lemma remains in TauCeti.LinearMap as explained in the
generic file.
The restriction of a linear isometry equivalence to the unit sphere is C^m, for every
smoothness exponent m.
The differential of the restriction of a linear isometry to the unit spheres, read in the ambient space through the inclusion of the target sphere, is the linear isometry applied to the tangent vector read in the ambient space.
The diffeomorphism between unit spheres induced by a linear isometry equivalence.
Equations
- e.unitSphereDiffeomorph m = { toEquiv := e.unitSphereEquiv, contMDiff_toFun := ⋯, contMDiff_invFun := ⋯ }
Instances For
The antipodal map of the unit sphere is the diffeomorphism induced by -1, the element of
O(n + 1) given by LinearIsometryEquiv.neg. In particular Mathlib's contMDiff_neg_sphere is
the case e = -1 of contMDiff_unitSphereEquiv.
The inclusion of the linear isometry group of E into the group of self-diffeomorphisms of
its unit sphere. For E = EuclideanSpace ℝ (Fin (n + 1)) this is the reference inclusion
O(n + 1) → Diff(Sⁿ); see TauCeti.orthogonalToDiffSphere.
Equations
- LinearIsometryEquiv.unitSphereDiffHom m = { toFun := fun (e : E ≃ₗᵢ[ℝ] E) => e.unitSphereDiffeomorph m, map_one' := ⋯, map_mul' := ⋯ }
Instances For
The inclusion of the linear isometry group into the diffeomorphism group of the unit sphere is
injective, so O(n + 1) is realised as a subgroup of Diff(Sⁿ).
The linear isometry group of E acts on the unit sphere by C^m maps, for every smoothness
exponent m.
Continuity in the linear isometry #
The restriction of a linear isometry to the unit sphere depends continuously on the isometry,
for the weak Whitney topology on the C^m maps between the spheres.
The restriction to the unit sphere of a continuous family of linear isometry equivalences is
a continuous family of C^m maps between the spheres, for the weak Whitney topology. Continuity of
the family is asked for in the operator-norm topology.
The reference inclusion O(n + 1) → Diff(Sⁿ): an orthogonal transformation of ℝⁿ⁺¹
restricts to a diffeomorphism of the unit sphere Sⁿ, and this restriction is a group
homomorphism. It is injective by TauCeti.orthogonalToDiffSphere_injective.
Equations
Instances For
The reference inclusion O(n + 1) → Diff(Sⁿ) sends an orthogonal transformation to its
restriction to the unit sphere.
The reference inclusion O(n + 1) → Diff(Sⁿ) is injective, so O(n + 1) is realised as a
subgroup of Diff(Sⁿ).
The reference inclusion O(n + 1) → Diff(Sⁿ) is continuous, for the subspace topology on
the orthogonal group and the weak Whitney C^m topology on the diffeomorphism group.
The reference inclusion O(n + 1) → Diff(Sⁿ), packaged as a continuous map.
Equations
- TauCeti.continuousOrthogonalToDiffSphere n m = { toFun := ⇑(TauCeti.orthogonalToDiffSphere n m), continuous_toFun := ⋯ }