Structures · Topology

Bundle.RiemannianBundle

Class used to create an inner product structure space on the fibers of a fiber bundle, without creating diamonds. Use as follows: * instance : RiemannianBundle E := ⟨g⟩ where g : RiemannianMetric E registers the inner product space on the fibers; * instance : RiemannianBundle E := ⟨g.toRiemannianMetric⟩ where g : ContinuousRiemannianMetric F E registers the inner product space on the fibers, and the fact that it varies continuously (i.e., a [IsContinuousRiemannianBundle] instance). * instance : RiemannianBundle E := ⟨g.toRiemannianMetric⟩ where g : ContMDiffRiemannianMetric IB n F E registers the inner product space on the fibers, and the fact that it varies smoothly (and continuously), i.e., [IsContMDiffRiemannianBundle] and [IsContinuousRiemannianBundle] instances. Note that this is only useful when there is a preexisting topology in the fibers of a vector bundle, like for the tangent bundle. This should not be used to express theorems for general bundles with a metric. Instead, use `` variable {E : B → Type*} [TopologicalSpace (TotalSpace F E)] [∀ x, NormedAddCommGroup (E x)] [∀ x, InnerProductSpace ℝ (E x)] [FiberBundle F E] [VectorBundle ℝ F E] [IsContinuousRiemannianBundle F E] ``

Defined in

Mathlib.Topology.VectorBundle.Riemannian

Shape

One type argument · adds g