Riemannian manifolds

StructureRiemannian/bundle metric#

A family of inner product space structures on the fibers of a fiber bundle, defining the same topology as the already existing one. This family is not assumed to be continuous or smooth: to guarantee continuity, resp. smoothness, of the inner product as a function of the base point, use ContinuousRiemannianMetric or ContMDiffRiemannianMetric.

This structure is used through RiemannianBundle for typeclass inference, to register the inner product space structure on the fibers without creating diamonds.

Bundle.RiemannianMetric.{u_4, u_6} {B : Type u_4} (E : B → Type u_6)
  [(b : B) → TopologicalSpace (E b)] [(b : B) → AddCommGroup (E b)]
  [(b : B) → _root_.Module ℝ (E b)] : Type (max u_4 u_6)

Sources

• Mathlib documentation: Bundle.RiemannianMetric
• Source of Bundle.RiemannianMetric in Mathlib/Topology/VectorBundle/Riemannian.lean
• Mathlib overview: Geometry › Riemannian manifolds

MathlibBundle.RiemannianMetric

Uses 4 · Used by 1

Statement usesAssociative algebra over a commutative ring · Continuous linear map · Metric space · Topological ring

Used byRiemannian manifold

StructureSmooth bundle metric#

A family of inner product space structures on the fibers of a fiber bundle, defining the same topology as the already existing one, and varying continuously with the base point. See also ContinuousRiemannianMetric for a continuous version.

This structure is used through RiemannianBundle for typeclass inference, to register the inner product space structure on the fibers without creating diamonds.

Bundle.ContMDiffRiemannianMetric.{u_1, u_2, u_3, u_4, u_5} {EB : Type u_1} [NormedAddCommGroup EB]
  [NormedSpace ℝ EB] {HB : Type u_2} [TopologicalSpace HB] (IB : ModelWithCorners ℝ EB HB)
  (n : WithTop ℕ∞) {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) → _root_.Module ℝ (E b)] [FiberBundle F E]
  [VectorBundle ℝ F E] : Type (max u_3 u_5)

Sources

• Mathlib documentation: Bundle.ContMDiffRiemannianMetric
• Source of Bundle.ContMDiffRiemannianMetric in Mathlib/Geometry/Manifold/VectorBundle/Riemannian.lean
• Mathlib overview: Geometry › Riemannian manifolds

MathlibBundle.ContMDiffRiemannianMetric

Uses 5

Statement usesInner product space, over \(R\) or \(C\) · Smooth map between manifolds · Topological module · Topological ring · Topological vector bundle

ClassRiemannian manifold#

Consider a manifold in which the tangent spaces are already endowed with an inner product, and the space is already endowed with an extended distance. We say that this is a Riemannian manifold if the distance is given by the infimum of the lengths of C^1 paths, measured using the norm in the tangent spaces.

This is a Prop-valued typeclass, on top of existing data.

If you need to construct a distance using a Riemannian structure, see EMetricSpace.ofRiemannianMetric.

IsRiemannianManifold.{u_1, u_2, u_3} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E]
  {H : Type u_2} [TopologicalSpace H] (I : ModelWithCorners ℝ E H) (M : Type u_3)
  [TopologicalSpace M] [PseudoEMetricSpace M] [ChartedSpace H M]
  [Bundle.RiemannianBundle fun x => TangentSpace I x] : Prop

Sources

• Mathlib documentation: IsRiemannianManifold
• Source of IsRiemannianManifold in Mathlib/Geometry/Manifold/Riemannian/Basic.lean
• Mathlib overview: Geometry › Riemannian manifolds

MathlibIsRiemannianManifold

Uses 7

Statement usesInner product space, over \(R\) or \(C\) · Integral of positive measurable functions · Lebesgue measure (Measure theory) · Norm · Norms \(\lVert\cdot\rVert_p\) on \(\R^n\) and \(\C^n\) · Riemannian/bundle metric · Smooth map between manifolds

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.