Existence of Riemannian metrics

Every C^n real vector bundle with finite-dimensional fibres over a σ-compact Hausdorff smooth manifold modelled on a finite-dimensional space carries a C^n Riemannian metric (TauCeti.nonempty_contMDiffRiemannianMetric). In particular, such a manifold carries a C^n Riemannian metric on its tangent bundle. Here n ranges over ℕ∞: the metric is built with smooth partitions of unity, so the analytic case is not covered.

The proof is the classical one. Over the base set of a trivialization e, pulling back a fixed inner product on the model fibre along e gives a local metric. The fibrewise conditions on a metric (symmetry, positive definiteness and a von Neumann bounded unit set) cut out a convex set of continuous bilinear forms on each fibre (TauCeti.convex_setOfPred_symm_pos_isVonNBounded), so the local metrics glue along a smooth partition of unity, by Mathlib's exists_contMDiffSection_forall_mem_convex_of_local.

A Riemannian metric is the input of the metric constructions of differential geometry: it splits the restriction of the tangent bundle of a manifold along a submanifold into tangent and normal parts, and it gives the exponential maps, distances and volumes built from a metric.

Main results

• TauCeti.nonempty_contMDiffRiemannianMetric: a C^n vector bundle with finite-dimensional fibres over a σ-compact Hausdorff smooth manifold modelled on a finite-dimensional space has a C^n Riemannian metric.

References

• J. M. Lee, Introduction to Smooth Manifolds, 2nd ed., Springer GTM 218 (2013), Proposition 13.3 (existence of Riemannian metrics, by partitions of unity); the same argument applies verbatim to an arbitrary vector bundle.

theorem TauCeti.nonempty_contMDiffRiemannianMetric {EB : Type u_1} [NormedAddCommGroup EB] [NormedSpace ℝ EB] {HB : Type u_2} [TopologicalSpace HB] {IB : ModelWithCorners ℝ EB HB} {n : ℕ∞} {B : Type u_3} [TopologicalSpace B] [ChartedSpace HB B] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] {E : B → Type u_5} [TopologicalSpace (Bundle.TotalSpace F E)] [(b : B) → TopologicalSpace (E b)] [(b : B) → AddCommGroup (E b)] [(b : B) → Module ℝ (E b)] [FiberBundle F E] [VectorBundle ℝ F E] [∀ (b : B), ContinuousConstSMul ℝ (E b)] [FiniteDimensional ℝ EB] [T2Space B] [SigmaCompactSpace B] [IsManifold IB (↑⊤) B] [FiniteDimensional ℝ F] [ContMDiffVectorBundle (↑n) F E IB] : Nonempty (Bundle.ContMDiffRiemannianMetric IB (↑n) F E)

Existence of Riemannian metrics. A C^n real vector bundle with finite-dimensional fibres over a σ-compact Hausdorff smooth manifold modelled on a finite-dimensional space carries a C^n Riemannian metric.