Riemannian vector bundles #
Given a vector bundle over a manifold whose fibers are all endowed with a scalar product, we say that this bundle is Riemannian if the scalar product depends smoothly on the base point.
We introduce a typeclass [IsContMDiffRiemannianBundle IB n F E] registering this property.
Under this assumption, we show that the scalar product of two smooth maps into the same fibers of
the bundle is a smooth function.
If the fibers of a bundle E have a preexisting topology (like the tangent bundle), one can not
assume additionally [∀ b, InnerProductSpace ℝ (E b)] as this would create diamonds. Instead,
use [RiemannianBundle E], which endows the fibers with a scalar product while ensuring that
there is no diamond. We provide a constructor for [RiemannianBundle E] from a smooth family
of metrics, which registers automatically [IsContMDiffRiemannianBundle IB n F E].
The following code block is the standard way to say "Let E be a smooth vector bundle equipped with
a C^n Riemannian structure over a C^n manifold B":
variable
{EB : Type*} [NormedAddCommGroup EB] [NormedSpace ℝ EB]
{HB : Type*} [TopologicalSpace HB] {IB : ModelWithCorners ℝ EB HB} {n : WithTop ℕ∞}
{B : Type*} [TopologicalSpace B] [ChartedSpace HB B]
{F : Type*} [NormedAddCommGroup F] [NormedSpace ℝ F]
{E : B → Type*} [TopologicalSpace (TotalSpace F E)] [∀ x, NormedAddCommGroup (E x)]
[∀ x, InnerProductSpace ℝ (E x)] [FiberBundle F E] [VectorBundle ℝ F E]
[IsManifold IB n B] [ContMDiffVectorBundle n F E IB]
[IsContMDiffRiemannianBundle IB n F E]
class
IsContMDiffRiemannianBundle
{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)]
[(x : B) → NormedAddCommGroup (E x)]
[(x : B) → InnerProductSpace ℝ (E x)]
[FiberBundle F E]
[VectorBundle ℝ F E]
:
Consider a real vector bundle in which each fiber is endowed with a scalar product.
We that the bundle is Riemannian if the scalar product depends smoothly on the base point.
This assumption is spelled IsContMDiffRiemannianBundle IB n F E where IB is the model space of
the base, n is the smoothness, F is the model fiber, and E : B → Type* is the bundle.
Instances
theorem
IsContMDiffRiemannianBundle.of_le
{EB : Type u_1}
[NormedAddCommGroup EB]
[NormedSpace ℝ EB]
{HB : Type u_2}
[TopologicalSpace HB]
{IB : ModelWithCorners ℝ EB HB}
{n 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)]
[(x : B) → NormedAddCommGroup (E x)]
[(x : B) → InnerProductSpace ℝ (E x)]
[FiberBundle F E]
[VectorBundle ℝ F E]
[h : IsContMDiffRiemannianBundle IB n F E]
(h' : n' ≤ n)
:
IsContMDiffRiemannianBundle IB n' F E
instance
instIsContMDiffRiemannianBundleOfSomeENatTopOfLEInfty
{EB : Type u_1}
[NormedAddCommGroup EB]
[NormedSpace ℝ EB]
{HB : Type u_2}
[TopologicalSpace HB]
{IB : ModelWithCorners ℝ EB HB}
{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)]
[(x : B) → NormedAddCommGroup (E x)]
[(x : B) → InnerProductSpace ℝ (E x)]
[FiberBundle F E]
[VectorBundle ℝ F E]
{a : WithTop ℕ∞}
[IsContMDiffRiemannianBundle IB (↑⊤) F E]
[h : ENat.LEInfty a]
:
IsContMDiffRiemannianBundle IB a F E
instance
instIsContMDiffRiemannianBundleOfTopWithTopENat
{EB : Type u_1}
[NormedAddCommGroup EB]
[NormedSpace ℝ EB]
{HB : Type u_2}
[TopologicalSpace HB]
{IB : ModelWithCorners ℝ EB HB}
{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)]
[(x : B) → NormedAddCommGroup (E x)]
[(x : B) → InnerProductSpace ℝ (E x)]
[FiberBundle F E]
[VectorBundle ℝ F E]
{a : WithTop ℕ∞}
[IsContMDiffRiemannianBundle IB ⊤ F E]
:
IsContMDiffRiemannianBundle IB a F E
instance
instIsContMDiffRiemannianBundleOfNatWithTopENat
{EB : Type u_1}
[NormedAddCommGroup EB]
[NormedSpace ℝ EB]
{HB : Type u_2}
[TopologicalSpace HB]
{IB : ModelWithCorners ℝ EB HB}
{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)]
[(x : B) → NormedAddCommGroup (E x)]
[(x : B) → InnerProductSpace ℝ (E x)]
[FiberBundle F E]
[VectorBundle ℝ F E]
[IsContMDiffRiemannianBundle IB 1 F E]
:
IsContMDiffRiemannianBundle IB 0 F E
instance
instIsContMDiffRiemannianBundleOfNatWithTopENat_1
{EB : Type u_1}
[NormedAddCommGroup EB]
[NormedSpace ℝ EB]
{HB : Type u_2}
[TopologicalSpace HB]
{IB : ModelWithCorners ℝ EB HB}
{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)]
[(x : B) → NormedAddCommGroup (E x)]
[(x : B) → InnerProductSpace ℝ (E x)]
[FiberBundle F E]
[VectorBundle ℝ F E]
[IsContMDiffRiemannianBundle IB 2 F E]
:
IsContMDiffRiemannianBundle IB 1 F E
instance
instIsContMDiffRiemannianBundleOfNatWithTopENat_2
{EB : Type u_1}
[NormedAddCommGroup EB]
[NormedSpace ℝ EB]
{HB : Type u_2}
[TopologicalSpace HB]
{IB : ModelWithCorners ℝ EB HB}
{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)]
[(x : B) → NormedAddCommGroup (E x)]
[(x : B) → InnerProductSpace ℝ (E x)]
[FiberBundle F E]
[VectorBundle ℝ F E]
[IsContMDiffRiemannianBundle IB 3 F E]
:
IsContMDiffRiemannianBundle IB 2 F E
instance
instIsContMDiffRiemannianBundleTrivial
{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_6}
[NormedAddCommGroup F₁]
[InnerProductSpace ℝ F₁]
:
IsContMDiffRiemannianBundle IB n F₁ (Bundle.Trivial B F₁)
A trivial vector bundle, in which the model fiber has a scalar product, is a Riemannian bundle.
theorem
ContMDiffWithinAt.inner_bundle
{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)]
[(x : B) → NormedAddCommGroup (E x)]
[(x : B) → InnerProductSpace ℝ (E x)]
[FiberBundle F E]
[VectorBundle ℝ F E]
{EM : Type u_6}
[NormedAddCommGroup EM]
[NormedSpace ℝ EM]
{HM : Type u_7}
[TopologicalSpace HM]
{IM : ModelWithCorners ℝ EM HM}
{M : Type u_8}
[TopologicalSpace M]
[ChartedSpace HM M]
[h : IsContMDiffRiemannianBundle IB n F E]
{b : M → B}
{v w : (x : M) → E (b x)}
{s : Set M}
{x : M}
(hv : ContMDiffWithinAt IM (IB.prod (modelWithCornersSelf ℝ F)) n (fun (m : M) => { proj := b m, snd := v m }) s x)
(hw : ContMDiffWithinAt IM (IB.prod (modelWithCornersSelf ℝ F)) n (fun (m : M) => { proj := b m, snd := w m }) s x)
:
ContMDiffWithinAt IM (modelWithCornersSelf ℝ ℝ) n (fun (m : M) => inner ℝ (v m) (w m)) s x
Given two smooth maps into the same fibers of a Riemannian bundle, their scalar product is smooth.
theorem
ContMDiffAt.inner_bundle
{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)]
[(x : B) → NormedAddCommGroup (E x)]
[(x : B) → InnerProductSpace ℝ (E x)]
[FiberBundle F E]
[VectorBundle ℝ F E]
{EM : Type u_6}
[NormedAddCommGroup EM]
[NormedSpace ℝ EM]
{HM : Type u_7}
[TopologicalSpace HM]
{IM : ModelWithCorners ℝ EM HM}
{M : Type u_8}
[TopologicalSpace M]
[ChartedSpace HM M]
[h : IsContMDiffRiemannianBundle IB n F E]
{b : M → B}
{v w : (x : M) → E (b x)}
{x : M}
(hv : ContMDiffAt IM (IB.prod (modelWithCornersSelf ℝ F)) n (fun (m : M) => { proj := b m, snd := v m }) x)
(hw : ContMDiffAt IM (IB.prod (modelWithCornersSelf ℝ F)) n (fun (m : M) => { proj := b m, snd := w m }) x)
:
ContMDiffAt IM (modelWithCornersSelf ℝ ℝ) n (fun (b_1 : M) => inner ℝ (v b_1) (w b_1)) x
Given two smooth maps into the same fibers of a Riemannian bundle, their scalar product is smooth.
theorem
ContMDiffOn.inner_bundle
{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)]
[(x : B) → NormedAddCommGroup (E x)]
[(x : B) → InnerProductSpace ℝ (E x)]
[FiberBundle F E]
[VectorBundle ℝ F E]
{EM : Type u_6}
[NormedAddCommGroup EM]
[NormedSpace ℝ EM]
{HM : Type u_7}
[TopologicalSpace HM]
{IM : ModelWithCorners ℝ EM HM}
{M : Type u_8}
[TopologicalSpace M]
[ChartedSpace HM M]
[h : IsContMDiffRiemannianBundle IB n F E]
{b : M → B}
{v w : (x : M) → E (b x)}
{s : Set M}
(hv : ContMDiffOn IM (IB.prod (modelWithCornersSelf ℝ F)) n (fun (m : M) => { proj := b m, snd := v m }) s)
(hw : ContMDiffOn IM (IB.prod (modelWithCornersSelf ℝ F)) n (fun (m : M) => { proj := b m, snd := w m }) s)
:
ContMDiffOn IM (modelWithCornersSelf ℝ ℝ) n (fun (b_1 : M) => inner ℝ (v b_1) (w b_1)) s
Given two smooth maps into the same fibers of a Riemannian bundle, their scalar product is smooth.
theorem
ContMDiff.inner_bundle
{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)]
[(x : B) → NormedAddCommGroup (E x)]
[(x : B) → InnerProductSpace ℝ (E x)]
[FiberBundle F E]
[VectorBundle ℝ F E]
{EM : Type u_6}
[NormedAddCommGroup EM]
[NormedSpace ℝ EM]
{HM : Type u_7}
[TopologicalSpace HM]
{IM : ModelWithCorners ℝ EM HM}
{M : Type u_8}
[TopologicalSpace M]
[ChartedSpace HM M]
[h : IsContMDiffRiemannianBundle IB n F E]
{b : M → B}
{v w : (x : M) → E (b x)}
(hv : ContMDiff IM (IB.prod (modelWithCornersSelf ℝ F)) n fun (m : M) => { proj := b m, snd := v m })
(hw : ContMDiff IM (IB.prod (modelWithCornersSelf ℝ F)) n fun (m : M) => { proj := b m, snd := w m })
:
Given two smooth maps into the same fibers of a Riemannian bundle, their scalar product is smooth.
structure
Bundle.ContMDiffRiemannianMetric
{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 (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_3 u_5)
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.
The scalar product along the fibers of the bundle.
Instances For
def
Bundle.ContMDiffRiemannianMetric.toContinuousRiemannianMetric
{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 (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 : ContMDiffRiemannianMetric IB n F E)
:
A smooth Riemannian metric defines in particular a continuous Riemannian metric.
Equations
- g.toContinuousRiemannianMetric = { inner := g.inner, symm := ⋯, pos := ⋯, isVonNBounded := ⋯, continuous := ⋯ }
Instances For
def
Bundle.ContMDiffRiemannianMetric.toRiemannianMetric
{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 (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 : ContMDiffRiemannianMetric IB n F E)
:
A smooth Riemannian metric defines in particular a Riemannian metric.
Instances For
instance
Bundle.instIsContMDiffRiemannianBundle
{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 (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 : ContMDiffRiemannianMetric IB n F E)
:
IsContMDiffRiemannianBundle IB n F E