The height function on the unit sphere is a Morse function

The height function x ↦ ⟪x, v⟫ on the unit sphere of an (n + 1)-dimensional real inner product space, for a unit vector v, is the standard first example of a Morse function: it is smooth, its only critical points are the north pole v and the south pole -v, and these are nondegenerate, of Morse index n and 0 respectively. Morse homology reads the homology of the sphere off this function, one generator in degree 0 and one in degree n, so it is the first test case for a Morse complex.

The manifold structure on the sphere is Mathlib's, charted by stereographic projection. In the chart centred at the north pole v, which projects from -v, the height function is the explicit rational function stereographicHeight w = (4 - ‖w‖ ^ 2) / (‖w‖ ^ 2 + 4) of the chart coordinate w. Its Hessian at the origin is minus the inner product, which is what makes v a nondegenerate critical point of index n. The chart centred at -v sees the negative of the same function, so the south pole is a nondegenerate critical point of index 0. The critical points are located through the manifold derivative: the differential of the height function at x is the inner product with v restricted to the tangent space (ℝ ∙ x)ᗮ, which vanishes exactly when v is a multiple of x.

Main declarations

• TauCeti.stereographicHeight: the height function in the stereographic chart at the north pole, with TauCeti.isNondegenerateCriticalPoint_stereographicHeight_zero and TauCeti.morseIndex_stereographicHeight_zero computing its Morse data at the origin.
• TauCeti.sphereHeight: the height function on the unit sphere in the direction of a unit vector.
• TauCeti.sphereHeight_comp_extChartAt_symm: in the preferred chart at the north pole it is stereographicHeight.
• TauCeti.mvfderiv_sphereHeight_eq_zero_iff and TauCeti.mfderiv_sphereHeight_eq_zero_iff: its critical points are the two poles.
• TauCeti.sphereHeight_lt_self and TauCeti.sphereHeight_neg_lt: the north pole is its strict global maximum and the south pole its strict global minimum.
• TauCeti.isMorse_sphereHeight: the height function is a Morse function.
• TauCeti.manifoldMorseIndex_sphereHeight_self and TauCeti.manifoldMorseIndex_sphereHeight_neg: the north pole has index n and the south pole has index 0.
• TauCeti.criticalPoints_sphereHeight: the critical points of the height function are the poles.
• TauCeti.ncard_setOf_sphereHeight_eq_zero: the equator of the circle has two points.
• TauCeti.infinite_setOf_sphereHeight_eq_zero: the equator of a sphere of dimension at least 2 is infinite.

References

• M. Audin and M. Damian, Morse Theory and Floer Homology, Springer Universitext, 2014, Chapter 1.

The height function in the stereographic chart

noncomputable def TauCeti.stereographicHeight {F : Type u_1} [NormedAddCommGroup F] (w : F) : ℝ

The height function of the unit sphere, read in the stereographic chart centred at the north pole: the point with chart coordinate w has height (4 - ‖w‖ ^ 2) / (‖w‖ ^ 2 + 4).

@[simp]

theorem TauCeti.stereographicHeight_apply {F : Type u_1} [NormedAddCommGroup F] (w : F) : stereographicHeight w = (4 - ‖w‖ ^ 2) / (‖w‖ ^ 2 + 4)

theorem TauCeti.contDiff_stereographicHeight {F : Type u_1} [NormedAddCommGroup F] [InnerProductSpace ℝ F] {n : WithTop ℕ∞} : ContDiff ℝ n stereographicHeight

The chart height function is smooth.

theorem TauCeti.hasFDerivAt_stereographicHeight {F : Type u_1} [NormedAddCommGroup F] [InnerProductSpace ℝ F] (w : F) : HasFDerivAt stereographicHeight ((-16 / (‖w‖ ^ 2 + 4) ^ 2) • (innerSL ℝ) w) w

The derivative of the chart height function.

theorem TauCeti.fderiv_stereographicHeight {F : Type u_1} [NormedAddCommGroup F] [InnerProductSpace ℝ F] (w : F) : fderiv ℝ stereographicHeight w = (-16 / (‖w‖ ^ 2 + 4) ^ 2) • (innerSL ℝ) w

The Fréchet derivative of the chart height function at w is -16 / (‖w‖ ^ 2 + 4) ^ 2 times the inner product with w.

theorem TauCeti.hasGradientAt_stereographicHeight {F : Type u_1} [NormedAddCommGroup F] [InnerProductSpace ℝ F] [CompleteSpace F] (w : F) : HasGradientAt stereographicHeight ((-16 / (‖w‖ ^ 2 + 4) ^ 2) • w) w

The gradient of the chart height function.

theorem TauCeti.gradient_stereographicHeight {F : Type u_1} [NormedAddCommGroup F] [InnerProductSpace ℝ F] [CompleteSpace F] (w : F) : gradient stereographicHeight w = (-16 / (‖w‖ ^ 2 + 4) ^ 2) • w

The gradient of the chart height function at w is -16 / (‖w‖ ^ 2 + 4) ^ 2 times w.

@[simp]

theorem TauCeti.gradient_stereographicHeight_zero {F : Type u_1} [NormedAddCommGroup F] [InnerProductSpace ℝ F] [CompleteSpace F] : gradient stereographicHeight 0 = 0

The origin is a critical point of the chart height function.

theorem TauCeti.hasFDerivAt_gradient_stereographicHeight_zero {F : Type u_1} [NormedAddCommGroup F] [InnerProductSpace ℝ F] [CompleteSpace F] : HasFDerivAt (gradient stereographicHeight) (-ContinuousLinearMap.id ℝ F) 0

The Hessian of the chart height function at the origin is minus the identity.

theorem TauCeti.hessianOperator_stereographicHeight_zero {F : Type u_1} [NormedAddCommGroup F] [InnerProductSpace ℝ F] [CompleteSpace F] : hessianOperator stereographicHeight 0 = -ContinuousLinearMap.id ℝ F

The Hessian operator of the chart height function at the origin is minus the identity.

theorem TauCeti.hessianQuadraticForm_stereographicHeight_zero {F : Type u_1} [NormedAddCommGroup F] [InnerProductSpace ℝ F] (w : F) : (hessianQuadraticForm stereographicHeight 0) w = -‖w‖ ^ 2

The Hessian quadratic form of the chart height function at the origin is minus the squared norm.

theorem TauCeti.isNondegenerateCriticalPoint_stereographicHeight_zero {F : Type u_1} [NormedAddCommGroup F] [InnerProductSpace ℝ F] [CompleteSpace F] : IsNondegenerateCriticalPoint stereographicHeight 0

The origin is a nondegenerate critical point of the chart height function.

theorem TauCeti.morseIndex_stereographicHeight_zero {F : Type u_1} [NormedAddCommGroup F] [InnerProductSpace ℝ F] [FiniteDimensional ℝ F] : morseIndex stereographicHeight 0 = Module.finrank ℝ F

The Morse index of the chart height function at the origin is the dimension of the chart space.

The height function on the sphere

def TauCeti.sphereHeight {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (v x : ↑(Metric.sphere 0 1)) : ℝ

The height function on the unit sphere in the direction of the unit vector v: the inner product with v. It is the standard Morse function on the sphere, with the poles v and -v as its only critical points.

@[simp]

theorem TauCeti.sphereHeight_apply {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (v x : ↑(Metric.sphere 0 1)) : sphereHeight v x = inner ℝ ↑x ↑v

theorem TauCeti.sphereHeight_eq_innerSL_comp {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (v : ↑(Metric.sphere 0 1)) : sphereHeight v = ⇑((innerSL ℝ) ↑v) ∘ Subtype.val

The height function is the inner product with v composed with the inclusion of the sphere.

@[simp]

theorem TauCeti.sphereHeight_neg {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (v : ↑(Metric.sphere 0 1)) : sphereHeight (-v) = -sphereHeight v

Reversing the direction negates the height function.

theorem TauCeti.contMDiff_sphereHeight {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {n : ℕ} [Fact (Module.finrank ℝ E = n + 1)] {m : WithTop ℕ∞} (v : ↑(Metric.sphere 0 1)) : ContMDiff (modelWithCornersSelf ℝ (EuclideanSpace ℝ (Fin n))) (modelWithCornersSelf ℝ ℝ) m (sphereHeight v)

The height function is smooth.

@[simp]

theorem TauCeti.mvfderiv_sphereHeight_eq_zero_iff {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {n : ℕ} [Fact (Module.finrank ℝ E = n + 1)] (v x : ↑(Metric.sphere 0 1)) : d% (sphereHeight v) x = 0 ↔ x = v ∨ x = -v

The critical points of the height function are exactly the north and south poles.

@[simp]

theorem TauCeti.mfderiv_sphereHeight_eq_zero_iff {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {n : ℕ} [Fact (Module.finrank ℝ E = n + 1)] (v x : ↑(Metric.sphere 0 1)) : mfderiv% (sphereHeight v) x = 0 ↔ x = v ∨ x = -v

The critical points of the height function, stated with mfderiv, are the two poles.

theorem TauCeti.sphereHeight_lt_self {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {v x : ↑(Metric.sphere 0 1)} (hx : x ≠ v) : sphereHeight v x < sphereHeight v v

The north pole is the strict global maximum of the height function.

theorem TauCeti.sphereHeight_neg_lt {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {v x : ↑(Metric.sphere 0 1)} (hx : x ≠ -v) : sphereHeight v (-v) < sphereHeight v x

The south pole is the strict global minimum of the height function.

theorem TauCeti.sphereHeight_self {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (v : ↑(Metric.sphere 0 1)) : sphereHeight v v = 1

The height of the north pole is 1.

theorem TauCeti.sphereHeight_neg_self {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (v : ↑(Metric.sphere 0 1)) : sphereHeight v (-v) = -1

The height of the south pole is -1.

theorem TauCeti.sphereHeight_le_one {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (v x : ↑(Metric.sphere 0 1)) : sphereHeight v x ≤ 1

The height function is at most 1, its value at the north pole.

theorem TauCeti.neg_one_le_sphereHeight {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (v x : ↑(Metric.sphere 0 1)) : -1 ≤ sphereHeight v x

The height function is at least -1, its value at the south pole.

theorem TauCeti.sphereHeight_eq_one_iff {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {v x : ↑(Metric.sphere 0 1)} : sphereHeight v x = 1 ↔ x = v

The north pole is the only point of height 1.

theorem TauCeti.sphereHeight_eq_neg_one_iff {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {v x : ↑(Metric.sphere 0 1)} : sphereHeight v x = -1 ↔ x = -v

The south pole is the only point of height -1.

theorem TauCeti.sphereHeight_comp_chartAt_symm {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {n : ℕ} [Fact (Module.finrank ℝ E = n + 1)] (v : ↑(Metric.sphere 0 1)) : sphereHeight v ∘ ↑(chartAt (EuclideanSpace ℝ (Fin n)) v).symm = stereographicHeight

In the chart centred at the north pole v, the height function in the direction v is stereographicHeight.

theorem TauCeti.sphereHeight_comp_extChartAt_symm {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {n : ℕ} [Fact (Module.finrank ℝ E = n + 1)] (v : ↑(Metric.sphere 0 1)) : sphereHeight v ∘ ↑(extChartAt (modelWithCornersSelf ℝ (EuclideanSpace ℝ (Fin n))) v).symm = stereographicHeight

In the preferred extended chart at the north pole v, the height function in the direction v is stereographicHeight.

theorem TauCeti.isManifoldNondegenerateCriticalPoint_sphereHeight_self {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {n : ℕ} [Fact (Module.finrank ℝ E = n + 1)] (v : ↑(Metric.sphere 0 1)) : IsManifoldNondegenerateCriticalPoint (modelWithCornersSelf ℝ (EuclideanSpace ℝ (Fin n))) (sphereHeight v) v

The north pole is a nondegenerate critical point of the height function.

theorem TauCeti.isManifoldNondegenerateCriticalPoint_sphereHeight_neg {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {n : ℕ} [Fact (Module.finrank ℝ E = n + 1)] (v : ↑(Metric.sphere 0 1)) : IsManifoldNondegenerateCriticalPoint (modelWithCornersSelf ℝ (EuclideanSpace ℝ (Fin n))) (sphereHeight v) (-v)

The south pole is a nondegenerate critical point of the height function.

theorem TauCeti.isMorse_sphereHeight {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {n : ℕ} [Fact (Module.finrank ℝ E = n + 1)] (v : ↑(Metric.sphere 0 1)) : IsMorse (modelWithCornersSelf ℝ (EuclideanSpace ℝ (Fin n))) (sphereHeight v)

The height function on the sphere is a Morse function.

@[simp]

theorem TauCeti.manifoldMorseIndex_sphereHeight_self {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {n : ℕ} [Fact (Module.finrank ℝ E = n + 1)] (v : ↑(Metric.sphere 0 1)) : manifoldMorseIndex (modelWithCornersSelf ℝ (EuclideanSpace ℝ (Fin n))) (sphereHeight v) v = n

The Morse index of the height function at the north pole is n.

@[simp]

theorem TauCeti.manifoldMorseIndex_sphereHeight_neg {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {n : ℕ} [Fact (Module.finrank ℝ E = n + 1)] (v : ↑(Metric.sphere 0 1)) : manifoldMorseIndex (modelWithCornersSelf ℝ (EuclideanSpace ℝ (Fin n))) (sphereHeight v) (-v) = 0

The Morse index of the height function at the south pole is 0.

@[simp]

theorem TauCeti.criticalPoints_sphereHeight {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {n : ℕ} [Fact (Module.finrank ℝ E = n + 1)] (v : ↑(Metric.sphere 0 1)) : criticalPoints (modelWithCornersSelf ℝ (EuclideanSpace ℝ (Fin n))) (sphereHeight v) = {v, -v}

The critical points of the height function on the sphere are the north pole v and the south pole -v.

theorem TauCeti.ncard_setOf_sphereHeight_eq_zero {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (hE : Module.finrank ℝ E = 2) (v : ↑(Metric.sphere 0 1)) : {x : ↑(Metric.sphere 0 1) | sphereHeight v x = 0}.ncard = 2

The equator of the circle has two points. In a two-dimensional real inner product space, exactly two points of the unit circle have height zero in the direction of a unit vector v.

theorem TauCeti.infinite_setOf_sphereHeight_eq_zero {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (hE : 3 ≤ Module.finrank ℝ E) (v : ↑(Metric.sphere 0 1)) : {x : ↑(Metric.sphere 0 1) | sphereHeight v x = 0}.Infinite

The equator is infinite in dimension at least two. If E has dimension at least 3, the points of the unit sphere of height zero in the direction of a unit vector v form an infinite set.