mathlib documentation

geometry.manifold.instances.sphere

Manifold structure on the sphere #

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.

Finally, two lemmas about smooth maps:

As an application we prove times_cont_mdiff_neg_sphere, that the antipodal map 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 (findim ℝ 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 (findim ℝ 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 #

def stereo_to_fun {E : Type u_1} [inner_product_space E] (v : E) [complete_space E] (x : E) :

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.

Equations
@[simp]
theorem stereo_to_fun_apply {E : Type u_1} [inner_product_space E] {v : E} [complete_space E] (x : E) :
def stereo_inv_fun_aux {E : Type u_1} [inner_product_space E] (v w : E) :
E

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.

Equations
@[simp]
theorem stereo_inv_fun_aux_apply {E : Type u_1} [inner_product_space E] {v : E} (w : E) :
stereo_inv_fun_aux v w = (w ^ 2 + 4)⁻¹ (4 w + (w ^ 2 - 4) v)
theorem stereo_inv_fun_aux_mem {E : Type u_1} [inner_product_space E] {v : E} (hv : v = 1) {w : E} (hw : w (submodule.span {v})) :
def stereo_inv_fun {E : Type u_1} [inner_product_space E] {v : E} (hv : v = 1) (w : (submodule.span {v})) :

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
@[simp]
theorem stereo_inv_fun_apply {E : Type u_1} [inner_product_space E] {v : E} (hv : v = 1) (w : (submodule.span {v})) :
(stereo_inv_fun hv w) = (w ^ 2 + 4)⁻¹ (4 w + (w ^ 2 - 4) v)
theorem stereo_inv_fun_ne_north_pole {E : Type u_1} [inner_product_space E] {v : E} (hv : v = 1) (w : (submodule.span {v})) :
stereo_inv_fun hv w v, _⟩
theorem continuous_stereo_inv_fun {E : Type u_1} [inner_product_space E] {v : E} (hv : v = 1) :
theorem stereo_left_inv {E : Type u_1} [inner_product_space E] {v : E} [complete_space E] (hv : v = 1) {x : (metric.sphere 0 1)} (hx : x v) :
theorem stereo_right_inv {E : Type u_1} [inner_product_space E] {v : E} [complete_space E] (hv : v = 1) (w : (submodule.span {v})) :

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
@[simp]
theorem stereographic_source {E : Type u_1} [inner_product_space E] {v : E} [complete_space E] (hv : v = 1) :
@[simp]

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
@[instance]

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

Smooth manifold structure on the sphere #

@[instance]

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.

theorem times_cont_mdiff.cod_restrict_sphere {E : Type u_1} [inner_product_space E] {F : Type u_2} [normed_group F] [normed_space F] {H : Type u_3} [topological_space H] {I : model_with_corners F H} {M : Type u_4} [topological_space M] [charted_space H M] [smooth_manifold_with_corners I M] {n : } [fact (finite_dimensional.findim E = n + 1)] {m : with_top } {f : M → E} (hf : times_cont_mdiff I 𝓘(, E) m f) (hf' : ∀ (x : M), f x metric.sphere 0 1) :

If a times_cont_mdiff function f : M → E, where M is some manifold, takes values in the sphere, then it restricts to a times_cont_mdiff function from M to the sphere.