Theorems · Inductive type · algebraic topology

Bundle.RiemannianBundle

{B : Type u_4} →
  (E : B → Type u_6) →
    [(b : B) → TopologicalSpace (E b)] →
      [inst : (b : B) → AddCommGroup (E b)] → [(b : B) → Module ℝ (E b)] → Type (max u_4 u_6)

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

Cited by

12 results in Mathlib

Foundations

Depth 95 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

TopologicalSpaceAddCommGroupModule