Commit 2025-07-21 14:23 b6e1a5c4

feat: define Riemannian manifolds (#27250) We introduce typeclasses to deal with Riemannian manifolds:

• In a fiber bundle whose fibers are already endowed with an inner product space structure, [IsContinuousRiemannianBundle F E] registers the fact the inner product depends continuously on the base point. This is a Prop-valued class, on top of existing data [∀ x, NormedAddCommGroup (E x)] [∀ x, InnerProductSpace ℝ (E x)].
• We also register [IsContMDiffRiemannianBundle n IB F E] similarly.
• There is an issue when the fibers already have a topological structure (for instance the tangent spaces), because adding an assumption [∀ x, NormedAddCommGroup (TangentSpace I x)] would create a diamond. Instead, we introduce another typeclass [RiemannianBundle E] containing the data of an inner product space on the fibers, compatible with the preexisting topology. From this class, we register instances of inner product space structures on the fibers, whose topology is defeq to the original one.
• We make sure that registering concrete instances of [RiemannianBundle E] registers automatically [IsContinuousRiemannianBundle F E] and/or [IsContMDiffRiemannianBundle n IB F E] in terms of the regularity of the metric.
• Under the assumptions [RiemannianBundle (fun (b : M) -> TangentSpace I b)] and [EMetricSpace M], we register a Prop-valued typeclass [IsRiemannianManifold I M] registering the fact that the edist coincides with the infimum of the lengths of paths, measured using the normed space structure in the tangent spaces. With this design, one can develop the general theory of Riemannian bundles and Riemannian manifolds, and also define concrete instances. When working with a generic Riemannian manifold, the typeclasses will include (in addition to the usual one for manifolds, replacing the topological space one with an emetric space one) the assumptions [RiemannianBundle (fun (b : M) -> TangentSpace I b)] [IsContinuousRiemannianBundle E (fun (b : M) -> TangentSpace I b)] [IsContMDiffRiemannianBundle n I E (fun (b : M) -> TangentSpace I b)].