Manifold structure on the sphere #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
This file defines stereographic projection from the sphere in an inner product space E, and uses
it to put a smooth manifold structure on the sphere.
Main results #
For a unit vector v in E, the definition stereographic gives the stereographic projection
centred at v, a local homeomorphism from the sphere to (ℝ ∙ v)ᗮ (the orthogonal complement of
v).
For finite-dimensional E, we then construct a smooth manifold instance on the sphere; the charts
here are obtained by composing the local homeomorphisms stereographic with arbitrary isometries
from (ℝ ∙ v)ᗮ to Euclidean space.
We prove two lemmas about smooth maps:
cont_mdiff_coe_spherestates that the coercion map from the sphere intoEis smooth; this is a useful tool for constructing smooth maps from the sphere.cont_mdiff.cod_restrict_spherestates that a map from a manifold into the sphere is smooth if its lift to a map toEis smooth; this is a useful tool for constructing smooth maps to the sphere.
As an application we prove cont_mdiff_neg_sphere, that the antipodal map is smooth.
Finally, we equip the circle (defined in analysis.complex.circle to be the sphere in ℂ
centred at 0 of radius 1) with the following structure:
- a charted space with model space
euclidean_space ℝ (fin 1)(inherited frommetric.sphere) - a Lie group with model with corners
𝓡 1
We furthermore show that exp_map_circle (defined in analysis.complex.circle to be the natural
map λ t, exp (t * I) from ℝ to circle) is smooth.
Implementation notes #
The model space for the charted space instance is euclidean_space ℝ (fin n), where n is a
natural number satisfying the typeclass assumption [fact (finrank ℝ E = n + 1)]. This may seem a
little awkward, but it is designed to circumvent the problem that the literal expression for the
dimension of the model space (up to definitional equality) determines the type. If one used the
naive expression euclidean_space ℝ (fin (finrank ℝ E - 1)) for the model space, then the sphere in
ℂ would be a manifold with model space euclidean_space ℝ (fin (2 - 1)) but not with model space
euclidean_space ℝ (fin 1).
Construction of the stereographic projection #
Stereographic projection, forward direction. This is a map from an inner product space E to
the orthogonal complement of an element v of E. It is smooth away from the affine hyperplane
through v parallel to the orthogonal complement. It restricts on the sphere to the stereographic
projection.
Auxiliary function for the construction of the reverse direction of the stereographic
projection. This is a map from the orthogonal complement of a unit vector v in an inner product
space E to E; we will later prove that it takes values in the unit sphere.
For most purposes, use stereo_inv_fun, not stereo_inv_fun_aux.
Stereographic projection, reverse direction. This is a map from the orthogonal complement of a
unit vector v in an inner product space E to the unit sphere in E.
Equations
- stereo_inv_fun hv w = ⟨stereo_inv_fun_aux v ↑w, _⟩
Stereographic projection from the unit sphere in E, centred at a unit vector v in E; this
is the version as a local homeomorphism.
Equations
- stereographic hv = {to_local_equiv := {to_fun := stereo_to_fun v ∘ coe, inv_fun := stereo_inv_fun hv, source := {⟨v, _⟩}ᶜ, target := set.univ ↥(Span {v})ᗮ, map_source' := _, map_target' := _, left_inv' := _, right_inv' := _}, open_source := _, open_target := _, continuous_to_fun := _, continuous_inv_fun := _}
Charted space structure on the sphere #
In this section we construct a charted space structure on the unit sphere in a finite-dimensional
real inner product space E; that is, we show that it is locally homeomorphic to the Euclidean
space of dimension one less than E.
The restriction to finite dimension is for convenience. The most natural charted_space
structure for the sphere uses the stereographic projection from the antipodes of a point as the
canonical chart at this point. However, the codomain of the stereographic projection constructed
in the previous section is (ℝ ∙ v)ᗮ, the orthogonal complement of the vector v in E which is
the "north pole" of the projection, so a priori these charts all have different codomains.
So it is necessary to prove that these codomains are all continuously linearly equivalent to a fixed normed space. This could be proved in general by a simple case of Gram-Schmidt orthogonalization, but in the finite-dimensional case it follows more easily by dimension-counting.
Variant of the stereographic projection, for the sphere in an n + 1-dimensional inner product
space E. This version has codomain the Euclidean space of dimension n, and is obtained by
composing the original sterographic projection (stereographic) with an arbitrary linear isometry
from (ℝ ∙ v)ᗮ to the Euclidean space.
Equations
The unit sphere in an n + 1-dimensional inner product space E is a charted space
modelled on the Euclidean space of dimension n.
Equations
- metric.sphere.charted_space = {atlas := {f : local_homeomorph ↥(metric.sphere 0 1) (euclidean_space ℝ (fin n)) | ∃ (v : ↥(metric.sphere 0 1)), f = stereographic' n v}, chart_at := λ (v : ↥(metric.sphere 0 1)), stereographic' n (-v), mem_chart_source := _, chart_mem_atlas := _}
Smooth manifold structure on the sphere #
The unit sphere in an n + 1-dimensional inner product space E is a smooth manifold,
modelled on the Euclidean space of dimension n.
The inclusion map (i.e., coe) from the sphere in E to E is smooth.
If a cont_mdiff function f : M → E, where M is some manifold, takes values in the
sphere, then it restricts to a cont_mdiff function from M to the sphere.
The antipodal map is smooth.
Consider the differential of the inclusion of the sphere in E at the point v as a continuous
linear map from tangent_space (𝓡 n) v to E. The range of this map is the orthogonal complement
of v in E.
Note that there is an abuse here of the defeq between E and the tangent space to E at (v:E).
In general this defeq is not canonical, but in this case (the tangent space of a vector space) it is
canonical.
Consider the differential of the inclusion of the sphere in E at the point v as a continuous
linear map from tangent_space (𝓡 n) v to E. This map is injective.
The unit circle in ℂ is a charted space modelled on euclidean_space ℝ (fin 1). This
follows by definition from the corresponding result for metric.sphere.
Equations
The unit circle in ℂ is a Lie group.
The map λ t, exp (t * I) from ℝ to the unit circle in ℂ is smooth.