The stereographic charts of the sphere, and the smooth embeddings of spheres induced by #

linear isometries

Mathlib charts the unit sphere of an (n + 1)-dimensional real inner product space by stereographic projection, the preferred chart at v projecting from the antipode -v (EuclideanSpace.instChartedSpaceSphere). This file records the facts about these charts that computations in a chart at a chosen point use: which stereographic projection the preferred chart is, that the extended chart at v sends v to the origin of the model space, and that the inverse of a stereographic chart is a smooth embedding of the model space into the sphere. Read in the ambient space, the inverse of stereographic projection has injective derivative, so it is a regular parametrization of the sphere minus a point. Stereographic projection from v is a diffeomorphism from the sphere minus v onto the model space, and from the sphere minus v and -v onto the punctured model space, since it sends exactly -v to the origin.

It then uses the charts to show that a linear isometry ι : F →ₗᵢ[ℝ] E restricts to a smooth embedding of unit spheres, LinearIsometry.unitSphereMap. Stereographic projection is defined from inner products and orthogonal projections, both of which ι preserves, so ι carries the stereographic chart at v to the stereographic chart at ι v: in those two charts, ι reads as a linear isometry LinearIsometry.stereographicModelMap of the model Euclidean spaces, and a linear isometry is the inclusion of a factor in a product decomposition (LinearIsometry.prodOrthogonalRangeEquiv). That is the normal form Mathlib's Manifold.IsImmersionAt asks for, and together with the isometric embedding of the spheres it makes the restriction a smooth embedding. Great circles, the geometric presentation of the unknot, are the case of a linear isometry ℂ →ₗᵢ[ℝ] E. A family of linear isometries depending smoothly on a parameter likewise acts smoothly on the sphere.

Finally, the covering map Circle.exp : ℝ → S¹ has injective derivative everywhere, so that a loop and its lift to ℝ have the same tangent lines, and its local inverse, the argument, is smooth away from -1. A differentiable path or loop in a sphere of dimension at least two omits a point, allowing the entire path or loop to be read in one stereographic chart.

Main results #

TauCeti.finrank_euclideanSpace_fin_succ_fact: the dimension of ℝⁿ⁺¹, in the form the stereographic charts of its unit sphere take it.
TauCeti.injective_fderiv_stereoInvFunAux_comp_coe: the inverse of stereographic projection from v, as a map from (ℝ ∙ v)ᗮ to the ambient space, has injective derivative.
TauCeti.fact_finrank_orthogonal_span_singleton_coe_sphere: the orthogonal complement v^⊥ of a point v of Sⁿ⁺¹ has dimension n + 1, so its unit sphere, the sphere of unit tangent vectors at v, is an n-dimensional manifold.
LinearIndependent.finCons_mvfderiv_coe_sphere: a point u of the sphere followed by the image in the ambient space of a linearly independent family of tangent vectors at u is linearly independent.
TauCeti.chartAt_sphere: the preferred chart at v is stereographic' n (-v).
TauCeti.extChartAt_sphere_apply_self: the preferred extended chart at v sends v to 0.
TauCeti.isSmoothEmbedding_stereographic'_symm: the inverse of a stereographic chart is a smooth embedding of the model space into the sphere.
TauCeti.coe_comp_stereographic'_symm, TauCeti.contDiff_coe_comp_stereographic'_symm, TauCeti.injective_fderiv_coe_comp_stereographic'_symm: read in the ambient space, the inverse of a stereographic chart is stereoInvFunAux precomposed with a linear isometry, so it is smooth with injective derivative.
TauCeti.compl_singleton_sup_compl_singleton_neg_eq_top: the complements of two antipodal points cover the sphere.
TauCeti.stereographicDiffeomorph, TauCeti.stereographicPuncturedDiffeomorph: stereographic projection from v as a diffeomorphism from the sphere minus v onto ℝⁿ, and from the sphere minus v and -v onto ℝⁿ \ {0}.
LinearIsometry.stereographic'_unitSphereMap: the stereographic charts read a linear isometry of unit spheres as a linear isometry of the model spaces.
LinearIsometry.isSmoothEmbedding_unitSphereMap: the restriction of a linear isometry to the unit spheres is a smooth embedding, at every differentiability order.
TauCeti.contMDiff_unitSphereEquiv_apply: a smooth family of linear isometries acts smoothly on the unit sphere.
TauCeti.injective_mfderiv_circleExp, TauCeti.surjective_mfderiv_circleExp: the derivative of Circle.exp : ℝ → S¹ is bijective.
TauCeti.contMDiffAt_circle_arg: the argument is smooth on the circle away from -1.
TauCeti.toSpanSingleton_deriv_comp_circleExp, TauCeti.toSpanSingleton_deriv_chart_comp_circleExp: the chain rule for a map of the circle read along Circle.exp, into a normed space or, through a chart, into a manifold.
TauCeti.contDiffOn_chart_comp_circleExp: a Cⁿ map of the circle, read in a chart of the maximal atlas along Circle.exp on an arc, is Cⁿ.
TauCeti.deriv_chart_comp_circleExp_eq, TauCeti.deriv_chart_comp_circleExp_ne_zero: two maps of the circle agreeing to first order at exp (t i) have the same velocity at t when read in a chart of the maximal atlas along Circle.exp, and that velocity is nonzero for an immersion.
TauCeti.mfderiv_eq_of_deriv_comp_circleExp_eq: two maps of the circle into a normed space with the same velocity at t along Circle.exp have the same derivative at exp (t i).
TauCeti.deriv_comp_circleExp_ne_zero_and_range_mfderiv: lifting a C¹ immersed circle along Circle.exp gives a nonzero derivative spanning its tangent line.
TauCeti.injective_mfderiv_of_deriv_comp_circleExp_ne_zero: conversely, a map of the circle whose lift along Circle.exp has nonzero derivative at t has injective derivative at exp (t i).
TauCeti.smul_deriv_coe_comp_circleExp: the chain rule for a loop in a sphere read along Circle.exp in the ambient space.
TauCeti.inner_deriv_coe_comp_circleExp_eq_zero, TauCeti.deriv_coe_comp_circleExp_ne_zero: the velocity of a loop in a sphere, read along Circle.exp in the ambient space, is tangent to the sphere, and nonzero where the loop is immersive.
TauCeti.mfderiv_eq_of_deriv_coe_comp_circleExp_eq, TauCeti.deriv_coe_comp_circleExp_eq_of_mfderiv_eq: two loops in a sphere through the same point have the same derivative there exactly when they have the same velocity, read along Circle.exp.
TauCeti.mfderiv_eq_of_deriv_comp_circleExp_eq_prod: two maps of S¹ × ℝ into Sⁿ × ℝ which agree on a line {z₀} × ℝ have the same derivative at (z₀, t) when their slices at time t have the same velocity at z₀ along Circle.exp.
TauCeti.deriv_coe_fst_comp_circleExp_ne_zero: for such a map which is the line s ↦ (y, s) over z₀ and has injective derivative, the sphere component of the slice has nonzero velocity.
TauCeti.exists_contMDiff_circle_hasDerivAt: an arbitrarily small smooth function on the circle vanishing at a given point with velocity 1 there along Circle.exp.
TauCeti.exists_notMem_range_circle_sphere: a differentiable loop in a sphere of dimension at least two omits a point.
TauCeti.contMDiff_coe_sphere_compl_zero, TauCeti.contMDiff_normalize_sphere: the inclusion of the unit sphere into the punctured space E \ {0} and the radial projection x ↦ x / ‖x‖ back onto the sphere are smooth; TauCeti.contMDiff_normalize_compl_zero is the radial projection read in E.
TauCeti.conjSphere, TauCeti.contMDiff_conjSphere: complex conjugation on the unit circle of ℂ, a smooth involution.

The stereographic charts of the sphere, and the smooth embeddings of spheres induced by #

Main results #

Smooth embeddings of spheres induced by linear isometries #

Smooth families of linear isometries acting on the sphere #

The derivative of the circle exponential #

Loops in a sphere read along Circle.exp #

Maps of the cylinder over the circle, read along Circle.exp #

Points omitted by differentiable loops #

The unit sphere in the punctured space #

Complex conjugation on the unit circle #

Loops in a sphere read along `Circle.exp` #

Maps of the cylinder over the circle, read along `Circle.exp` #