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 partial 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 partial homeomorphisms stereographic with arbitrary isometries from (ℝ ∙ v)ᗮ to Euclidean space.

We prove two lemmas about smooth maps:

• contMDiff_coe_sphere states that the coercion map from the sphere into E is smooth; this is a useful tool for constructing smooth maps from the sphere.
• contMDiff.codRestrict_sphere states that a map from a manifold into the sphere is smooth if its lift to a map to E is smooth; this is a useful tool for constructing smooth maps to the sphere.

As an application we prove contMdiffNegSphere, 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 EuclideanSpace ℝ (Fin 1) (inherited from Metric.Sphere)
• a Lie group with model with corners 𝓡 1

We furthermore show that expMapCircle (defined in Analysis.Complex.Circle to be the natural map fun t ↦ exp (t * I) from ℝ to circle) is smooth.

Implementation notes

The model space for the charted space instance is EuclideanSpace ℝ (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 EuclideanSpace ℝ (Fin (finrank ℝ E - 1)) for the model space, then the sphere in ℂ would be a manifold with model space EuclideanSpace ℝ (Fin (2 - 1)) but not with model space EuclideanSpace ℝ (Fin 1).

TODO

Relate the stereographic projection to the inversion of the space.

Construction of the stereographic projection

def stereoToFun {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (v : E) (x : E) : ↥(Submodule.span ℝ {v})ᗮ

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

• stereoToFun v x = (2 / (1 - ((innerSL ℝ) v) x)) • (orthogonalProjection (Submodule.span ℝ {v})ᗮ) x

@[simp]

theorem stereoToFun_apply {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {v : E} (x : E) : stereoToFun v x = (2 / (1 - ((innerSL ℝ) v) x)) • (orthogonalProjection (Submodule.span ℝ {v})ᗮ) x

theorem contDiffOn_stereoToFun {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {v : E} : ContDiffOn ℝ ⊤ (stereoToFun v) {x : E | ((innerSL ℝ) v) x ≠ 1}

theorem continuousOn_stereoToFun {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {v : E} : ContinuousOn (stereoToFun v) {x : E | ((innerSL ℝ) v) x ≠ 1}

def stereoInvFunAux {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (v : E) (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 stereoInvFun, not stereoInvFunAux.

Equations

• stereoInvFunAux v w = (‖w‖ ^ 2 + 4)⁻¹ • (4 • w + (‖w‖ ^ 2 - 4) • v)

@[simp]

theorem stereoInvFunAux_apply {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {v : E} (w : E) : stereoInvFunAux v w = (‖w‖ ^ 2 + 4)⁻¹ • (4 • w + (‖w‖ ^ 2 - 4) • v)

theorem stereoInvFunAux_mem {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {v : E} (hv : ‖v‖ = 1) {w : E} (hw : w ∈ (Submodule.span ℝ {v})ᗮ) : stereoInvFunAux v w ∈ Metric.sphere 0 1

theorem hasFDerivAt_stereoInvFunAux {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (v : E) : HasFDerivAt (stereoInvFunAux v) (ContinuousLinearMap.id ℝ E) 0

theorem hasFDerivAt_stereoInvFunAux_comp_coe {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (v : E) : HasFDerivAt (stereoInvFunAux v ∘ Subtype.val) (Submodule.span ℝ {v})ᗮ.subtypeL 0

theorem contDiff_stereoInvFunAux {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {v : E} : ContDiff ℝ ⊤ (stereoInvFunAux v)

def stereoInvFun {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {v : E} (hv : ‖v‖ = 1) (w : ↥(Submodule.span ℝ {v})ᗮ) : ↑(Metric.sphere 0 1)

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

• stereoInvFun hv w = ⟨stereoInvFunAux v ↑w, ⋯⟩

@[simp]

theorem stereoInvFun_apply {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {v : E} (hv : ‖v‖ = 1) (w : ↥(Submodule.span ℝ {v})ᗮ) : ↑(stereoInvFun hv w) = (‖w‖ ^ 2 + 4)⁻¹ • (4 • ↑w + (‖w‖ ^ 2 - 4) • v)

theorem stereoInvFun_ne_north_pole {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {v : E} (hv : ‖v‖ = 1) (w : ↥(Submodule.span ℝ {v})ᗮ) : stereoInvFun hv w ≠ ⟨v, ⋯⟩

theorem continuous_stereoInvFun {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {v : E} (hv : ‖v‖ = 1) : Continuous (stereoInvFun hv)

theorem stereo_left_inv {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {v : E} (hv : ‖v‖ = 1) {x : ↑(Metric.sphere 0 1)} (hx : ↑x ≠ v) : stereoInvFun hv (stereoToFun v ↑x) = x

theorem stereo_right_inv {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {v : E} (hv : ‖v‖ = 1) (w : ↥(Submodule.span ℝ {v})ᗮ) : stereoToFun v ↑(stereoInvFun hv w) = w

def stereographic {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {v : E} (hv : ‖v‖ = 1) : PartialHomeomorph ↑(Metric.sphere 0 1) ↥(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 partial homeomorphism.

Equations

• One or more equations did not get rendered due to their size.

theorem stereographic_apply {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {v : E} (hv : ‖v‖ = 1) (x : ↑(Metric.sphere 0 1)) : ↑(stereographic hv) x = (2 / (1 - ⟪v, ↑x⟫_ℝ)) • (orthogonalProjection (Submodule.span ℝ {v})ᗮ) ↑x

@[simp]

theorem stereographic_source {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {v : E} (hv : ‖v‖ = 1) : (stereographic hv).source = {⟨v, ⋯⟩}ᶜ

@[simp]

theorem stereographic_target {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {v : E} (hv : ‖v‖ = 1) : (stereographic hv).target = Set.univ

@[simp]

theorem stereographic_apply_neg {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (v : ↑(Metric.sphere 0 1)) : ↑(stereographic ⋯) (-v) = 0

@[simp]

theorem stereographic_neg_apply {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (v : ↑(Metric.sphere 0 1)) : ↑(stereographic ⋯) v = 0

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 ChartedSpace 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.

def stereographic' {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (n : ℕ) [Fact (FiniteDimensional.finrank ℝ E = n + 1)] (v : ↑(Metric.sphere 0 1)) : PartialHomeomorph (↑(Metric.sphere 0 1)) (EuclideanSpace ℝ (Fin n))

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

• stereographic' n v = (stereographic ⋯).trans (OrthonormalBasis.fromOrthogonalSpanSingleton n ⋯).repr.toHomeomorph.toPartialHomeomorph

@[simp]

theorem stereographic'_source {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {n : ℕ} [Fact (FiniteDimensional.finrank ℝ E = n + 1)] (v : ↑(Metric.sphere 0 1)) : (stereographic' n v).source = {v}ᶜ

@[simp]

theorem stereographic'_target {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {n : ℕ} [Fact (FiniteDimensional.finrank ℝ E = n + 1)] (v : ↑(Metric.sphere 0 1)) : (stereographic' n v).target = Set.univ

instance EuclideanSpace.instChartedSpaceSphere {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {n : ℕ} [Fact (FiniteDimensional.finrank ℝ E = n + 1)] : ChartedSpace (EuclideanSpace ℝ (Fin n)) ↑(Metric.sphere 0 1)

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

• One or more equations did not get rendered due to their size.

instance instChartedSpaceEuclideanSpaceRealFinElemHAddNatOfNatSphere (n : ℕ) : ChartedSpace (EuclideanSpace ℝ (Fin n)) ↑(Metric.sphere 0 1)

Equations

• instChartedSpaceEuclideanSpaceRealFinElemHAddNatOfNatSphere n = let_fun this := ⋯; EuclideanSpace.instChartedSpaceSphere

theorem sphere_ext_iff {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (u : ↑(Metric.sphere 0 1)) (v : ↑(Metric.sphere 0 1)) : u = v ↔ ⟪↑u, ↑v⟫_ℝ = 1

theorem stereographic'_symm_apply {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {n : ℕ} [Fact (FiniteDimensional.finrank ℝ E = n + 1)] (v : ↑(Metric.sphere 0 1)) (x : EuclideanSpace ℝ (Fin n)) : ↑(↑(stereographic' n v).symm x) = let U := (OrthonormalBasis.fromOrthogonalSpanSingleton n ⋯).repr; (‖↑(U.symm x)‖ ^ 2 + 4)⁻¹ • 4 • ↑(U.symm x) + (‖↑(U.symm x)‖ ^ 2 + 4)⁻¹ • (‖↑(U.symm x)‖ ^ 2 - 4) • ↑v

Smooth manifold structure on the sphere

instance EuclideanSpace.instSmoothManifoldWithCornersSphere {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {n : ℕ} [Fact (FiniteDimensional.finrank ℝ E = n + 1)] : SmoothManifoldWithCorners (modelWithCornersSelf ℝ (EuclideanSpace ℝ (Fin n))) ↑(Metric.sphere 0 1)

The unit sphere in an n + 1-dimensional inner product space E is a smooth manifold, modelled on the Euclidean space of dimension n.

Equations

• ⋯ = ⋯

instance instSmoothManifoldWithCornersRealEuclideanSpaceFinModelWithCornersSelfElemHAddNatOfNatSphere (n : ℕ) : SmoothManifoldWithCorners (modelWithCornersSelf ℝ (EuclideanSpace ℝ (Fin n))) ↑(Metric.sphere 0 1)

Equations

• ⋯ = ⋯

theorem contMDiff_coe_sphere {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {n : ℕ} [Fact (FiniteDimensional.finrank ℝ E = n + 1)] : ContMDiff (modelWithCornersSelf ℝ (EuclideanSpace ℝ (Fin n))) (modelWithCornersSelf ℝ E) ⊤ Subtype.val

The inclusion map (i.e., coe) from the sphere in E to E is smooth.

theorem ContMDiff.codRestrict_sphere {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners ℝ F H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] [SmoothManifoldWithCorners I M] {n : ℕ} [Fact (FiniteDimensional.finrank ℝ E = n + 1)] {m : ℕ∞} {f : M → E} (hf : ContMDiff I (modelWithCornersSelf ℝ E) m f) (hf' : ∀ (x : M), f x ∈ Metric.sphere 0 1) : ContMDiff I (modelWithCornersSelf ℝ (EuclideanSpace ℝ (Fin n))) m (Set.codRestrict f (Metric.sphere 0 1) hf')

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

theorem contMDiff_neg_sphere {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {n : ℕ} [Fact (FiniteDimensional.finrank ℝ E = n + 1)] : ContMDiff (modelWithCornersSelf ℝ (EuclideanSpace ℝ (Fin n))) (modelWithCornersSelf ℝ (EuclideanSpace ℝ (Fin n))) ⊤ fun (x : ↑(Metric.sphere 0 1)) => -x

The antipodal map is smooth.

theorem range_mfderiv_coe_sphere {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {n : ℕ} [Fact (FiniteDimensional.finrank ℝ E = n + 1)] (v : ↑(Metric.sphere 0 1)) : LinearMap.range (mfderiv (modelWithCornersSelf ℝ (EuclideanSpace ℝ (Fin n))) (modelWithCornersSelf ℝ E) Subtype.val v) = (Submodule.span ℝ {↑v})ᗮ

Consider the differential of the inclusion of the sphere in E at the point v as a continuous linear map from TangentSpace (𝓡 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.

theorem mfderiv_coe_sphere_injective {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {n : ℕ} [Fact (FiniteDimensional.finrank ℝ E = n + 1)] (v : ↑(Metric.sphere 0 1)) : Function.Injective ⇑(mfderiv (modelWithCornersSelf ℝ (EuclideanSpace ℝ (Fin n))) (modelWithCornersSelf ℝ E) Subtype.val v)

Consider the differential of the inclusion of the sphere in E at the point v as a continuous linear map from TangentSpace (𝓡 n) v to E. This map is injective.

theorem finrank_real_complex_fact' : Fact (FiniteDimensional.finrank ℝ ℂ = 1 + 1)

instance instChartedSpaceEuclideanSpaceRealFinOfNatNatSubtypeComplexMemSubmonoidCircle : ChartedSpace (EuclideanSpace ℝ (Fin 1)) ↥circle

The unit circle in ℂ is a charted space modelled on EuclideanSpace ℝ (Fin 1). This follows by definition from the corresponding result for Metric.Sphere.

Equations

• instChartedSpaceEuclideanSpaceRealFinOfNatNatSubtypeComplexMemSubmonoidCircle = EuclideanSpace.instChartedSpaceSphere

instance instSmoothManifoldWithCornersRealEuclideanSpaceFinOfNatNatModelWithCornersSelfSubtypeComplexMemSubmonoidCircle : SmoothManifoldWithCorners (modelWithCornersSelf ℝ (EuclideanSpace ℝ (Fin 1))) ↥circle

Equations

• instSmoothManifoldWithCornersRealEuclideanSpaceFinOfNatNatModelWithCornersSelfSubtypeComplexMemSubmonoidCircle = ⋯

instance instLieGroupRealEuclideanSpaceFinOfNatNatModelWithCornersSelfSubtypeComplexMemSubmonoidCircle : LieGroup (modelWithCornersSelf ℝ (EuclideanSpace ℝ (Fin 1))) ↥circle

The unit circle in ℂ is a Lie group.

Equations

• instLieGroupRealEuclideanSpaceFinOfNatNatModelWithCornersSelfSubtypeComplexMemSubmonoidCircle = ⋯

theorem contMDiff_expMapCircle : ContMDiff (modelWithCornersSelf ℝ ℝ) (modelWithCornersSelf ℝ (EuclideanSpace ℝ (Fin 1))) ⊤ ⇑expMapCircle

The map fun t ↦ exp (t * I) from ℝ to the unit circle in ℂ is smooth.