Riemannian vector bundles

Given a real vector bundle over a topological space whose fibers are all endowed with an inner product, we say that this bundle is Riemannian if the inner product depends continuously on the base point.

We introduce a typeclass [IsContinuousRiemannianBundle F E] registering this property. Under this assumption, we show that the inner product of two continuous maps into the same fibers of the bundle is a continuous function.

If one wants to endow an existing vector bundle with a Riemannian metric, there is a subtlety: the inner product space structure on the fibers should give rise to a topology on the fibers which is defeq to the original one, to avoid diamonds. To do this, we introduce a class [RiemannianBundle E] containing the data of an inner product on the fibers defining the same topology as the original one. Given this class, we can construct NormedAddCommGroup and InnerProductSpace instances on the fibers, compatible in a defeq way with the initial topology. If the data used to register the instance RiemannianBundle E depends continuously on the base point, we register automatically an instance of [IsContinuousRiemannianBundle F E] (and similarly if the data is smooth).

The general theory should be built assuming [IsContinuousRiemannianBundle F E], while the [RiemannianBundle E] mechanism is only to build data in specific situations.

Keywords

Vector bundle, Riemannian metric

class IsContinuousRiemannianBundle {B : Type u_1} [TopologicalSpace B] (F : Type u_2) [NormedAddCommGroup F] [NormedSpace ℝ F] (E : B → Type u_3) [TopologicalSpace (Bundle.TotalSpace F E)] [(x : B) → NormedAddCommGroup (E x)] [(x : B) → InnerProductSpace ℝ (E x)] [FiberBundle F E] [VectorBundle ℝ F E] : Prop

Consider a real vector bundle in which each fiber is endowed with an inner product. We say that the bundle is Riemannian if the inner product depends continuously on the base point. This assumption is spelled IsContinuousRiemannianBundle F E where F is the model fiber, and E : B → Type* is the bundle.

• exists_continuous : ∃ (g : (x : B) → E x →L[ℝ] E x →L[ℝ] ℝ), (Continuous fun (x : B) => Bundle.TotalSpace.mk' (F →L[ℝ] F →L[ℝ] ℝ) x (g x)) ∧ ∀ (x : B) (v w : E x), inner ℝ v w = ((g x) v) w

  There exists a bilinear form, depending continuously on the basepoint and defining the inner product in the fibers. This is expressed as an existence statement so that it is Prop-valued in terms of existing data, the inner product on the fibers and the fiber bundle structure.

instance instIsContinuousRiemannianBundleTrivial {B : Type u_1} [TopologicalSpace B] {F₁ : Type u_4} [NormedAddCommGroup F₁] [InnerProductSpace ℝ F₁] : IsContinuousRiemannianBundle F₁ (Bundle.Trivial B F₁)

A trivial vector bundle, in which the model fiber has a inner product, is a Riemannian bundle.

theorem ContinuousWithinAt.inner_bundle {B : Type u_1} [TopologicalSpace B] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {E : B → Type u_3} [TopologicalSpace (Bundle.TotalSpace F E)] [(x : B) → NormedAddCommGroup (E x)] [(x : B) → InnerProductSpace ℝ (E x)] [FiberBundle F E] [VectorBundle ℝ F E] {M : Type u_4} [TopologicalSpace M] [h : IsContinuousRiemannianBundle F E] {b : M → B} {v w : (x : M) → E (b x)} {s : Set M} {x : M} (hv : ContinuousWithinAt (fun (m : M) => { proj := b m, snd := v m }) s x) (hw : ContinuousWithinAt (fun (m : M) => { proj := b m, snd := w m }) s x) : ContinuousWithinAt (fun (m : M) => Inner.inner ℝ (v m) (w m)) s x

Given two continuous maps into the same fibers of a continuous Riemannian bundle, their inner product is continuous. Version with ContinuousWithinAt.

theorem ContinuousAt.inner_bundle {B : Type u_1} [TopologicalSpace B] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {E : B → Type u_3} [TopologicalSpace (Bundle.TotalSpace F E)] [(x : B) → NormedAddCommGroup (E x)] [(x : B) → InnerProductSpace ℝ (E x)] [FiberBundle F E] [VectorBundle ℝ F E] {M : Type u_4} [TopologicalSpace M] [h : IsContinuousRiemannianBundle F E] {b : M → B} {v w : (x : M) → E (b x)} {x : M} (hv : ContinuousAt (fun (m : M) => { proj := b m, snd := v m }) x) (hw : ContinuousAt (fun (m : M) => { proj := b m, snd := w m }) x) : ContinuousAt (fun (b_1 : M) => Inner.inner ℝ (v b_1) (w b_1)) x

Given two continuous maps into the same fibers of a continuous Riemannian bundle, their inner product is continuous. Version with ContinuousAt.

theorem ContinuousOn.inner_bundle {B : Type u_1} [TopologicalSpace B] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {E : B → Type u_3} [TopologicalSpace (Bundle.TotalSpace F E)] [(x : B) → NormedAddCommGroup (E x)] [(x : B) → InnerProductSpace ℝ (E x)] [FiberBundle F E] [VectorBundle ℝ F E] {M : Type u_4} [TopologicalSpace M] [h : IsContinuousRiemannianBundle F E] {b : M → B} {v w : (x : M) → E (b x)} {s : Set M} (hv : ContinuousOn (fun (m : M) => { proj := b m, snd := v m }) s) (hw : ContinuousOn (fun (m : M) => { proj := b m, snd := w m }) s) : ContinuousOn (fun (b_1 : M) => Inner.inner ℝ (v b_1) (w b_1)) s

Given two continuous maps into the same fibers of a continuous Riemannian bundle, their inner product is continuous. Version with ContinuousOn.

theorem Continuous.inner_bundle {B : Type u_1} [TopologicalSpace B] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {E : B → Type u_3} [TopologicalSpace (Bundle.TotalSpace F E)] [(x : B) → NormedAddCommGroup (E x)] [(x : B) → InnerProductSpace ℝ (E x)] [FiberBundle F E] [VectorBundle ℝ F E] {M : Type u_4} [TopologicalSpace M] [h : IsContinuousRiemannianBundle F E] {b : M → B} {v w : (x : M) → E (b x)} (hv : Continuous fun (m : M) => { proj := b m, snd := v m }) (hw : Continuous fun (m : M) => { proj := b m, snd := w m }) : Continuous fun (b_1 : M) => Inner.inner ℝ (v b_1) (w b_1)

Given two continuous maps into the same fibers of a continuous Riemannian bundle, their inner product is continuous.

theorem eventually_norm_symmL_trivializationAt_self_comp_lt {B : Type u_1} [TopologicalSpace B] (F : Type u_2) [NormedAddCommGroup F] [NormedSpace ℝ F] (E : B → Type u_3) [TopologicalSpace (Bundle.TotalSpace F E)] [(x : B) → NormedAddCommGroup (E x)] [(x : B) → InnerProductSpace ℝ (E x)] [FiberBundle F E] [VectorBundle ℝ F E] [h : IsContinuousRiemannianBundle F E] (x : B) {r : ℝ} (hr : 1 < r) : ∀ᶠ (y : B) in nhds x, ‖(Trivialization.symmL ℝ (trivializationAt F E x) x).comp (Trivialization.continuousLinearMapAt ℝ (trivializationAt F E x) y)‖ < r

In a continuous Riemannian bundle, local changes of coordinates given by the trivialization at a point distort the norm by a factor arbitrarily close to 1.

theorem eventually_norm_trivializationAt_lt {B : Type u_1} [TopologicalSpace B] (F : Type u_2) [NormedAddCommGroup F] [NormedSpace ℝ F] (E : B → Type u_3) [TopologicalSpace (Bundle.TotalSpace F E)] [(x : B) → NormedAddCommGroup (E x)] [(x : B) → InnerProductSpace ℝ (E x)] [FiberBundle F E] [VectorBundle ℝ F E] [h : IsContinuousRiemannianBundle F E] (x : B) : ∃ C > 0, ∀ᶠ (y : B) in nhds x, ‖Trivialization.continuousLinearMapAt ℝ (trivializationAt F E x) y‖ < C

In a continuous Riemannian bundle, the trivialization at a point is locally bounded in norm.

theorem eventually_norm_symmL_trivializationAt_comp_self_lt {B : Type u_1} [TopologicalSpace B] (F : Type u_2) [NormedAddCommGroup F] [NormedSpace ℝ F] (E : B → Type u_3) [TopologicalSpace (Bundle.TotalSpace F E)] [(x : B) → NormedAddCommGroup (E x)] [(x : B) → InnerProductSpace ℝ (E x)] [FiberBundle F E] [VectorBundle ℝ F E] [h : IsContinuousRiemannianBundle F E] (x : B) {r : ℝ} (hr : 1 < r) : ∀ᶠ (y : B) in nhds x, ‖(Trivialization.symmL ℝ (trivializationAt F E x) y).comp (Trivialization.continuousLinearMapAt ℝ (trivializationAt F E x) x)‖ < r

In a continuous Riemannian bundle, local changes of coordinates given by the trivialization at a point distort the norm by a factor arbitrarily close to 1.

theorem eventually_norm_symmL_trivializationAt_lt {B : Type u_1} [TopologicalSpace B] (F : Type u_2) [NormedAddCommGroup F] [NormedSpace ℝ F] (E : B → Type u_3) [TopologicalSpace (Bundle.TotalSpace F E)] [(x : B) → NormedAddCommGroup (E x)] [(x : B) → InnerProductSpace ℝ (E x)] [FiberBundle F E] [VectorBundle ℝ F E] [h : IsContinuousRiemannianBundle F E] (x : B) : ∃ C > 0, ∀ᶠ (y : B) in nhds x, ‖Trivialization.symmL ℝ (trivializationAt F E x) y‖ < C

In a continuous Riemannian bundle, the inverse of the trivialization at a point is locally bounded in norm.

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

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.

• inner (b : B) : E b →L[ℝ] E b →L[ℝ] ℝ

  The inner product along the fibers of the bundle.

• symm (b : B) (v w : E b) : ((self.inner b) v) w = ((self.inner b) w) v
• pos (b : B) (v : E b) (hv : v ≠ 0) : 0 < ((self.inner b) v) v
• continuousAt (b : B) : ContinuousAt (fun (v : E b) => ((self.inner b) v) v) 0

  The continuity at 0 is automatic when E b is isomorphic to a normed space, but since we are not making this assumption here we have to include it.

• isVonNBounded (b : B) : Bornology.IsVonNBounded ℝ {v : E b | ((self.inner b) v) v < 1}

@[reducible]

noncomputable def Bundle.RiemannianMetric.toCore {B : Type u_4} {E : B → Type u_6} [(b : B) → TopologicalSpace (E b)] [(b : B) → AddCommGroup (E b)] [(b : B) → Module ℝ (E b)] (g : RiemannianMetric E) (b : B) : InnerProductSpace.Core ℝ (E b)

`Core structure associated to a family of inner products on the fibers of a fiber bundle. This is an auxiliary construction to endow the fibers with an inner product space structure without creating diamonds.

Warning: Do not use this Core structure if the space you are interested in already has a norm instance defined on it, otherwise this will create a second non-defeq norm instance!

Equations

• g.toCore b = { inner := fun (v w : E b) => ((g.inner b) v) w, conj_inner_symm := ⋯, re_inner_nonneg := ⋯, add_left := ⋯, smul_left := ⋯, definite := ⋯ }

class Bundle.RiemannianBundle {B : Type u_4} (E : B → Type u_6) [(b : B) → TopologicalSpace (E b)] [(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.

• g : RiemannianMetric E

  The family of inner products on the fibers

@[instance 80]

noncomputable instance Bundle.instNormedAddCommGroupOfRiemannianBundle {B : Type u_4} {E : B → Type u_6} [(b : B) → TopologicalSpace (E b)] [(b : B) → AddCommGroup (E b)] [(b : B) → Module ℝ (E b)] [∀ (b : B), IsTopologicalAddGroup (E b)] [∀ (b : B), ContinuousConstSMul ℝ (E b)] [h : RiemannianBundle E] (b : B) : NormedAddCommGroup (E b)

Equations

• Bundle.instNormedAddCommGroupOfRiemannianBundle b = InnerProductSpace.Core.toNormedAddCommGroupOfTopology ⋯ ⋯

@[instance 80]

noncomputable instance Bundle.instInnerProductSpaceReal {B : Type u_4} {E : B → Type u_6} [(b : B) → TopologicalSpace (E b)] [(b : B) → AddCommGroup (E b)] [(b : B) → Module ℝ (E b)] [∀ (b : B), IsTopologicalAddGroup (E b)] [∀ (b : B), ContinuousConstSMul ℝ (E b)] [h : RiemannianBundle E] (b : B) : InnerProductSpace ℝ (E b)

Equations

• Bundle.instInnerProductSpaceReal b = InnerProductSpace.ofCoreOfTopology (Bundle.RiemannianBundle.g.toCore b) ⋯ ⋯

structure Bundle.ContinuousRiemannianMetric {B : Type u_4} [TopologicalSpace B] (F : Type u_5) [NormedAddCommGroup F] [NormedSpace ℝ F] (E : B → Type u_6) [TopologicalSpace (TotalSpace F E)] [(b : B) → TopologicalSpace (E b)] [(b : B) → AddCommGroup (E b)] [(b : B) → Module ℝ (E b)] [FiberBundle F E] [VectorBundle ℝ F E] : Type (max u_4 u_6)

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 ContMDiffRiemannianMetric for a smooth version.

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

• inner (b : B) : E b →L[ℝ] E b →L[ℝ] ℝ

  The inner product along the fibers of the bundle.

• symm (b : B) (v w : E b) : ((self.inner b) v) w = ((self.inner b) w) v
• pos (b : B) (v : E b) (hv : v ≠ 0) : 0 < ((self.inner b) v) v
• isVonNBounded (b : B) : Bornology.IsVonNBounded ℝ {v : E b | ((self.inner b) v) v < 1}
• continuous : Continuous fun (b : B) => TotalSpace.mk' (F →L[ℝ] F →L[ℝ] ℝ) b (self.inner b)

def Bundle.ContinuousRiemannianMetric.toRiemannianMetric {B : Type u_4} [TopologicalSpace B] {F : Type u_5} [NormedAddCommGroup F] [NormedSpace ℝ F] {E : B → Type u_6} [TopologicalSpace (TotalSpace F E)] [(b : B) → TopologicalSpace (E b)] [(b : B) → AddCommGroup (E b)] [(b : B) → Module ℝ (E b)] [FiberBundle F E] [VectorBundle ℝ F E] (g : ContinuousRiemannianMetric F E) : RiemannianMetric E

A continuous Riemannian metric is in particular a Riemannian metric.

Equations

• g.toRiemannianMetric = { inner := g.inner, symm := ⋯, pos := ⋯, continuousAt := ⋯, isVonNBounded := ⋯ }

instance Bundle.instIsContinuousRiemannianBundle {B : Type u_4} [TopologicalSpace B] {F : Type u_5} [NormedAddCommGroup F] [NormedSpace ℝ F] {E : B → Type u_6} [TopologicalSpace (TotalSpace F E)] [(b : B) → TopologicalSpace (E b)] [(b : B) → AddCommGroup (E b)] [(b : B) → Module ℝ (E b)] [∀ (b : B), IsTopologicalAddGroup (E b)] [∀ (b : B), ContinuousConstSMul ℝ (E b)] [FiberBundle F E] [VectorBundle ℝ F E] (g : ContinuousRiemannianMetric F E) : IsContinuousRiemannianBundle F E

If a Riemannian bundle structure is defined using g.toRiemannianMetric where g is a ContinuousRiemannianMetric, then we make sure typeclass inference can infer automatically that the the bundle is a continuous Riemannian bundle.