Compact Riemannian manifolds are geodesically complete

A Riemannian manifold carries no distance of its own: it carries the manifold topology and the fibrewise inner products, and the Riemannian distance has to be installed from them. Installing the extended distance EMetricSpace.ofRiemannianMetric turns a compact Riemannian manifold into a compact extended metric space, hence into a complete one, and metric completeness gives geodesic completeness. So every maximal geodesic of a compact Riemannian manifold is defined for all time, and its exponential map is defined on the whole tangent space at every point.

Running the argument through the extended distance, which is available on any Riemannian manifold, rather than through the ordinary distance, which exists only once the Riemannian distance is known to be finite, keeps the conclusion free of any connectedness hypothesis. It therefore also covers a compact manifold with several components, where points of different components are at infinite Riemannian distance from each other.

Preconnectedness does enter the consequences drawn afterwards, which speak about the Riemannian distance itself and so need it to be finite: on a compact preconnected Riemannian manifold every point is the image exp_p v of a tangent vector whose norm is its distance to p, so exp_p is surjective, and the radial geodesic segment along that vector realizes the distance.

Main results

In the namespace TauCeti.Manifold:

• isGeodesicallyCompleteAt_of_compactSpace: a compact Riemannian manifold is geodesically complete, with isGeodesicCurveOnFrom_maximalGeodesic_univ_of_compactSpace the resulting all-time geodesics and expDomain_eq_univ_of_compactSpace the resulting everywhere-defined exponential map.
• exists_riemannianExp_eq_and_enorm_eq_riemannianEDist_of_compactSpace and surjective_riemannianExp_of_compactSpace: on a compact preconnected Riemannian manifold every point is reached from p by the exponential map, along a tangent vector whose norm is the Riemannian distance.
• exists_isGeodesicCurveOn_Icc_pathELength_eq_riemannianEDist_of_compactSpace: on a compact preconnected Riemannian manifold a minimizing geodesic segment joins p to every point.

References

• M. P. do Carmo, Riemannian Geometry, Birkhäuser, 1992, Ch. 7, §2, Cor. 2.9.
• J. M. Lee, Introduction to Riemannian Manifolds, Springer, 2018, Ch. 6.

theorem TauCeti.Manifold.isGeodesicallyCompleteAt_of_compactSpace {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [FiniteDimensional ℝ E] [I.Boundaryless] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] [IsManifold I (↑⊤) M] [IsContMDiffRiemannianBundle I (↑⊤) E fun (x : M) => TangentSpace I x] [T2Space M] [CompactSpace M] (p : M) : IsGeodesicallyCompleteAt I M p

A compact Riemannian manifold is geodesically complete: every maximal geodesic leaving a point p is defined for all time. This is do Carmo's corollary to the Hopf–Rinow theorem.

@[simp]

theorem TauCeti.Manifold.expDomain_eq_univ_of_compactSpace {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [FiniteDimensional ℝ E] [I.Boundaryless] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] [IsManifold I (↑⊤) M] [IsContMDiffRiemannianBundle I (↑⊤) E fun (x : M) => TangentSpace I x] [T2Space M] [CompactSpace M] (p : M) : expDomain I M p = Set.univ

The exponential map of a compact Riemannian manifold is everywhere defined, its domain being the whole tangent space at every point.

theorem TauCeti.Manifold.isGeodesicCurveOnFrom_maximalGeodesic_univ_of_compactSpace {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [FiniteDimensional ℝ E] [I.Boundaryless] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] [IsManifold I (↑⊤) M] [IsContMDiffRiemannianBundle I (↑⊤) E fun (x : M) => TangentSpace I x] [T2Space M] [CompactSpace M] (p : M) (v : TangentSpace I p) : IsGeodesicCurveOnFrom I (maximalGeodesic I M p v) Set.univ p v

In a compact Riemannian manifold the maximal geodesic with initial data (p, v) is a geodesic on the whole real line.

theorem TauCeti.Manifold.exists_riemannianExp_eq_and_enorm_eq_riemannianEDist_of_compactSpace {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [FiniteDimensional ℝ E] [I.Boundaryless] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] [IsManifold I (↑⊤) M] [IsContMDiffRiemannianBundle I (↑⊤) E fun (x : M) => TangentSpace I x] [T2Space M] [CompactSpace M] [PreconnectedSpace M] (p q : M) : ∃ (v : TangentSpace I p), riemannianExp I M p v = q ∧ ‖v‖ₑ = Manifold.riemannianEDist I p q

Every point of a compact preconnected Riemannian manifold is reached minimally from p by the exponential map: it is exp_p v for a tangent vector v whose norm is the Riemannian distance from p to it.

theorem TauCeti.Manifold.surjective_riemannianExp_of_compactSpace {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [FiniteDimensional ℝ E] [I.Boundaryless] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] [IsManifold I (↑⊤) M] [IsContMDiffRiemannianBundle I (↑⊤) E fun (x : M) => TangentSpace I x] [T2Space M] [CompactSpace M] [PreconnectedSpace M] (p : M) : Function.Surjective (riemannianExp I M p)

The exponential map of a compact preconnected Riemannian manifold is surjective.

theorem TauCeti.Manifold.exists_isGeodesicCurveOn_Icc_pathELength_eq_riemannianEDist_of_compactSpace {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [FiniteDimensional ℝ E] [I.Boundaryless] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] [IsManifold I (↑⊤) M] [IsContMDiffRiemannianBundle I (↑⊤) E fun (x : M) => TangentSpace I x] [T2Space M] [CompactSpace M] [PreconnectedSpace M] (p q : M) : ∃ (γ : ℝ → M), IsGeodesicCurveOn I γ (Set.Icc 0 1) ∧ γ 0 = p ∧ γ 1 = q ∧ Manifold.pathELength I γ 0 1 = Manifold.riemannianEDist I p q ∧ ∀ s ∈ Set.Icc 0 1, ∀ t ∈ Set.Icc 0 1, s ≤ t → Manifold.pathELength I γ s t = Manifold.riemannianEDist I (γ s) (γ t)

A minimizing geodesic segment joins p to every point of a compact preconnected Riemannian manifold: a geodesic on [0, 1] from p to q whose length is the Riemannian distance from p to q, and each of whose subsegments likewise realizes the distance between its endpoints.