Riemannian metrics as positive symmetric sections #
The native Bundle.ContMDiffRiemannianMetric carrier embeds into the vector space of C^n
bilinear sections. Its image is exactly the positive-definite symmetric sections when the model
fibre is finite-dimensional. Thus the linear space of sections provides an ambient carrier for
studying spaces of metrics, with no choice of a background metric on the fibres.
TauCeti.Manifold.positiveDefiniteBilinearSections is the convex cone of such sections, and
Bundle.ContMDiffRiemannianMetric.positiveDefiniteSectionEquiv gives the comparison in both
directions. The reverse construction proves the native bounded-unit-set condition from finite
dimensionality; positivity alone would not suffice in infinite dimensions. The forward map and
convexity do not require finite dimensionality. All results allow boundary charts and arbitrary
regularity n.
The same comparison holds in the vector bundle fun x ↦ symmetricBilinearMaps ℝ (V x) ℝ of
symmetric bilinear forms, which for the tangent bundle is Sym²(T*M).
TauCeti.Manifold.positiveDefiniteSymmetricSections is the convex cone of its positive-definite
C^n sections, and Bundle.ContMDiffRiemannianMetric.positiveDefiniteSymmetricSectionEquiv
identifies it with the native metrics, through the identification
TauCeti.Manifold.symmetricBilinearSectionEquiv of C^n sections of the symmetric bundle with
symmetric C^n bilinear sections.
def
TauCeti.Manifold.positiveDefiniteBilinearSections
{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]
(V : B → Type u_5)
[TopologicalSpace (Bundle.TotalSpace F V)]
[(x : B) → TopologicalSpace (V x)]
[(x : B) → AddCommGroup (V x)]
[(x : B) → Module ℝ (V x)]
[FiberBundle F V]
[VectorBundle ℝ F V]
:
Set (BilinearSection IB F V ℝ n)
The cone of symmetric C^n bilinear sections positive on every nonzero diagonal vector.
Instances For
@[simp]
theorem
TauCeti.Manifold.mem_positiveDefiniteBilinearSections
{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]
{V : B → Type u_5}
[TopologicalSpace (Bundle.TotalSpace F V)]
[(x : B) → TopologicalSpace (V x)]
[(x : B) → AddCommGroup (V x)]
[(x : B) → Module ℝ (V x)]
[FiberBundle F V]
[VectorBundle ℝ F V]
(b : BilinearSection IB F V ℝ n)
:
b ∈ positiveDefiniteBilinearSections IB n F V ↔ b ∈ symmetricBilinearSections ∧ ∀ (x : B) (v : V x), v ≠ 0 → 0 < ((b x) v) v
Membership in the metric cone consists of symmetry and strict diagonal positivity.
theorem
TauCeti.Manifold.convex_positiveDefiniteBilinearSections
{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]
{V : B → Type u_5}
[TopologicalSpace (Bundle.TotalSpace F V)]
[(x : B) → TopologicalSpace (V x)]
[(x : B) → AddCommGroup (V x)]
[(x : B) → Module ℝ (V x)]
[FiberBundle F V]
[VectorBundle ℝ F V]
:
Convex ℝ (positiveDefiniteBilinearSections IB n F V)
Positive-definite symmetric sections are closed under convex combinations.
The cone in the bundle of symmetric bilinear forms #
def
TauCeti.Manifold.positiveDefiniteSymmetricSections
{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]
(V : B → Type u_5)
[TopologicalSpace (Bundle.TotalSpace F V)]
[(x : B) → TopologicalSpace (V x)]
[(x : B) → AddCommGroup (V x)]
[(x : B) → Module ℝ (V x)]
[FiberBundle F V]
[VectorBundle ℝ F V]
:
Set (ContMDiffSection IB (↥(symmetricBilinearMaps ℝ F ℝ)) n fun (x : B) => ↥(symmetricBilinearMaps ℝ (V x) ℝ))
The cone of C^n sections of the bundle of symmetric bilinear forms that are positive on
every nonzero vector. For the tangent bundle these are the metrics as sections of Sym²(T*M).
Instances For
@[simp]
theorem
TauCeti.Manifold.mem_positiveDefiniteSymmetricSections
{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]
{V : B → Type u_5}
[TopologicalSpace (Bundle.TotalSpace F V)]
[(x : B) → TopologicalSpace (V x)]
[(x : B) → AddCommGroup (V x)]
[(x : B) → Module ℝ (V x)]
[FiberBundle F V]
[VectorBundle ℝ F V]
(σ : ContMDiffSection IB (↥(symmetricBilinearMaps ℝ F ℝ)) n fun (x : B) => ↥(symmetricBilinearMaps ℝ (V x) ℝ))
:
Membership in the cone of positive-definite symmetric sections is strict diagonal positivity.
theorem
TauCeti.Manifold.symmetricBilinearSectionEquiv_mem_positiveDefiniteBilinearSections_iff
{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]
{V : B → Type u_5}
[TopologicalSpace (Bundle.TotalSpace F V)]
[(x : B) → TopologicalSpace (V x)]
[(x : B) → AddCommGroup (V x)]
[(x : B) → Module ℝ (V x)]
[FiberBundle F V]
[VectorBundle ℝ F V]
(σ : ContMDiffSection IB (↥(symmetricBilinearMaps ℝ F ℝ)) n fun (x : B) => ↥(symmetricBilinearMaps ℝ (V x) ℝ))
:
↑((symmetricBilinearSectionEquiv IB n) σ) ∈ positiveDefiniteBilinearSections IB n F V ↔ σ ∈ positiveDefiniteSymmetricSections IB n F V
Identifying sections of the symmetric bundle with symmetric bilinear sections matches the two cones of positive-definite sections.
theorem
TauCeti.Manifold.convex_positiveDefiniteSymmetricSections
{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]
{V : B → Type u_5}
[TopologicalSpace (Bundle.TotalSpace F V)]
[(x : B) → TopologicalSpace (V x)]
[(x : B) → AddCommGroup (V x)]
[(x : B) → Module ℝ (V x)]
[FiberBundle F V]
[VectorBundle ℝ F V]
:
Convex ℝ (positiveDefiniteSymmetricSections IB n F V)
Positive-definite sections of the symmetric bundle are closed under convex combinations.
def
Bundle.ContMDiffRiemannianMetric.toBilinearSection
{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]
{V : B → Type u_5}
[TopologicalSpace (TotalSpace F V)]
[(x : B) → TopologicalSpace (V x)]
[(x : B) → AddCommGroup (V x)]
[(x : B) → Module ℝ (V x)]
[FiberBundle F V]
[VectorBundle ℝ F V]
(g : ContMDiffRiemannianMetric IB n F V)
:
TauCeti.Manifold.BilinearSection IB F V ℝ n
The bilinear section underlying a native C^n Riemannian metric.
Instances For
@[simp]
theorem
Bundle.ContMDiffRiemannianMetric.toBilinearSection_apply
{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]
{V : B → Type u_5}
[TopologicalSpace (TotalSpace F V)]
[(x : B) → TopologicalSpace (V x)]
[(x : B) → AddCommGroup (V x)]
[(x : B) → Module ℝ (V x)]
[FiberBundle F V]
[VectorBundle ℝ F V]
(g : ContMDiffRiemannianMetric IB n F V)
(x : B)
(v w : V x)
:
theorem
Bundle.ContMDiffRiemannianMetric.toBilinearSection_injective
{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]
{V : B → Type u_5}
[TopologicalSpace (TotalSpace F V)]
[(x : B) → TopologicalSpace (V x)]
[(x : B) → AddCommGroup (V x)]
[(x : B) → Module ℝ (V x)]
[FiberBundle F V]
[VectorBundle ℝ F V]
:
The underlying bilinear section determines a Riemannian metric.
@[simp]
theorem
Bundle.ContMDiffRiemannianMetric.toBilinearSection_mem
{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]
{V : B → Type u_5}
[TopologicalSpace (TotalSpace F V)]
[(x : B) → TopologicalSpace (V x)]
[(x : B) → AddCommGroup (V x)]
[(x : B) → Module ℝ (V x)]
[FiberBundle F V]
[VectorBundle ℝ F V]
(g : ContMDiffRiemannianMetric IB n F V)
:
The bilinear section of a Riemannian metric belongs to the positive symmetric cone.
noncomputable def
Bundle.ContMDiffRiemannianMetric.toSymmetricSection
{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]
{V : B → Type u_5}
[TopologicalSpace (TotalSpace F V)]
[(x : B) → TopologicalSpace (V x)]
[(x : B) → AddCommGroup (V x)]
[(x : B) → Module ℝ (V x)]
[FiberBundle F V]
[VectorBundle ℝ F V]
(g : ContMDiffRiemannianMetric IB n F V)
:
ContMDiffSection IB (↥(TauCeti.symmetricBilinearMaps ℝ F ℝ)) n fun (x : B) => ↥(TauCeti.symmetricBilinearMaps ℝ (V x) ℝ)
A native C^n Riemannian metric as a C^n section of the bundle of symmetric bilinear
forms.
Instances For
@[simp]
theorem
Bundle.ContMDiffRiemannianMetric.coe_toSymmetricSection_apply
{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]
{V : B → Type u_5}
[TopologicalSpace (TotalSpace F V)]
[(x : B) → TopologicalSpace (V x)]
[(x : B) → AddCommGroup (V x)]
[(x : B) → Module ℝ (V x)]
[FiberBundle F V]
[VectorBundle ℝ F V]
(g : ContMDiffRiemannianMetric IB n F V)
(x : B)
:
@[simp]
theorem
Bundle.ContMDiffRiemannianMetric.symmetricBilinearSectionEquiv_toSymmetricSection
{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]
{V : B → Type u_5}
[TopologicalSpace (TotalSpace F V)]
[(x : B) → TopologicalSpace (V x)]
[(x : B) → AddCommGroup (V x)]
[(x : B) → Module ℝ (V x)]
[FiberBundle F V]
[VectorBundle ℝ F V]
(g : ContMDiffRiemannianMetric IB n F V)
:
Under the identification of sections of the symmetric bundle with symmetric bilinear sections, the section of a metric is its bilinear section.
theorem
Bundle.ContMDiffRiemannianMetric.toSymmetricSection_injective
{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]
{V : B → Type u_5}
[TopologicalSpace (TotalSpace F V)]
[(x : B) → TopologicalSpace (V x)]
[(x : B) → AddCommGroup (V x)]
[(x : B) → Module ℝ (V x)]
[FiberBundle F V]
[VectorBundle ℝ F V]
:
The section of the symmetric bundle determines a Riemannian metric.
@[simp]
theorem
Bundle.ContMDiffRiemannianMetric.toSymmetricSection_mem
{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]
{V : B → Type u_5}
[TopologicalSpace (TotalSpace F V)]
[(x : B) → TopologicalSpace (V x)]
[(x : B) → AddCommGroup (V x)]
[(x : B) → Module ℝ (V x)]
[FiberBundle F V]
[VectorBundle ℝ F V]
(g : ContMDiffRiemannianMetric IB n F V)
:
The section of a Riemannian metric belongs to the positive-definite symmetric cone.
def
Bundle.ContMDiffRiemannianMetric.ofPositiveDefiniteSection
{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]
{V : B → Type u_5}
[TopologicalSpace (TotalSpace F V)]
[(x : B) → TopologicalSpace (V x)]
[(x : B) → AddCommGroup (V x)]
[(x : B) → Module ℝ (V x)]
[FiberBundle F V]
[VectorBundle ℝ F V]
[FiniteDimensional ℝ F]
(b : TauCeti.Manifold.BilinearSection IB F V ℝ n)
(hb : b ∈ TauCeti.Manifold.positiveDefiniteBilinearSections IB n F V)
:
ContMDiffRiemannianMetric IB n F V
A positive-definite symmetric section determines a native Riemannian metric. The bounded-unit-set condition follows from finite dimensionality of the model fibre.
Instances For
@[simp]
theorem
Bundle.ContMDiffRiemannianMetric.ofPositiveDefiniteSection_inner
{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]
{V : B → Type u_5}
[TopologicalSpace (TotalSpace F V)]
[(x : B) → TopologicalSpace (V x)]
[(x : B) → AddCommGroup (V x)]
[(x : B) → Module ℝ (V x)]
[FiberBundle F V]
[VectorBundle ℝ F V]
[FiniteDimensional ℝ F]
(b : TauCeti.Manifold.BilinearSection IB F V ℝ n)
(hb : b ∈ TauCeti.Manifold.positiveDefiniteBilinearSections IB n F V)
(x : B)
(v w : V x)
:
@[simp]
theorem
Bundle.ContMDiffRiemannianMetric.ofPositiveDefiniteSection_toBilinearSection
{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]
{V : B → Type u_5}
[TopologicalSpace (TotalSpace F V)]
[(x : B) → TopologicalSpace (V x)]
[(x : B) → AddCommGroup (V x)]
[(x : B) → Module ℝ (V x)]
[FiberBundle F V]
[VectorBundle ℝ F V]
[FiniteDimensional ℝ F]
(g : ContMDiffRiemannianMetric IB n F V)
:
Recovering a metric from its section preserves the original metric.
@[simp]
theorem
Bundle.ContMDiffRiemannianMetric.toBilinearSection_ofPositiveDefiniteSection
{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]
{V : B → Type u_5}
[TopologicalSpace (TotalSpace F V)]
[(x : B) → TopologicalSpace (V x)]
[(x : B) → AddCommGroup (V x)]
[(x : B) → Module ℝ (V x)]
[FiberBundle F V]
[VectorBundle ℝ F V]
[FiniteDimensional ℝ F]
(b : TauCeti.Manifold.BilinearSection IB F V ℝ n)
(hb : b ∈ TauCeti.Manifold.positiveDefiniteBilinearSections IB n F V)
:
Recovering a metric from a positive symmetric section preserves that section.
def
Bundle.ContMDiffRiemannianMetric.positiveDefiniteSectionEquiv
{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]
{V : B → Type u_5}
[TopologicalSpace (TotalSpace F V)]
[(x : B) → TopologicalSpace (V x)]
[(x : B) → AddCommGroup (V x)]
[(x : B) → Module ℝ (V x)]
[FiberBundle F V]
[VectorBundle ℝ F V]
[FiniteDimensional ℝ F]
:
Native finite-rank C^n metrics are exactly positive-definite symmetric C^n sections.
Instances For
@[simp]
theorem
Bundle.ContMDiffRiemannianMetric.positiveDefiniteSectionEquiv_apply
{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]
{V : B → Type u_5}
[TopologicalSpace (TotalSpace F V)]
[(x : B) → TopologicalSpace (V x)]
[(x : B) → AddCommGroup (V x)]
[(x : B) → Module ℝ (V x)]
[FiberBundle F V]
[VectorBundle ℝ F V]
[FiniteDimensional ℝ F]
(g : ContMDiffRiemannianMetric IB n F V)
:
@[simp]
theorem
Bundle.ContMDiffRiemannianMetric.positiveDefiniteSectionEquiv_symm_apply
{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]
{V : B → Type u_5}
[TopologicalSpace (TotalSpace F V)]
[(x : B) → TopologicalSpace (V x)]
[(x : B) → AddCommGroup (V x)]
[(x : B) → Module ℝ (V x)]
[FiberBundle F V]
[VectorBundle ℝ F V]
[FiniteDimensional ℝ F]
(b : ↑(TauCeti.Manifold.positiveDefiniteBilinearSections IB n F V))
:
theorem
Bundle.ContMDiffRiemannianMetric.range_toBilinearSection
{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]
{V : B → Type u_5}
[TopologicalSpace (TotalSpace F V)]
[(x : B) → TopologicalSpace (V x)]
[(x : B) → AddCommGroup (V x)]
[(x : B) → Module ℝ (V x)]
[FiberBundle F V]
[VectorBundle ℝ F V]
[FiniteDimensional ℝ F]
:
The image of the native metric carrier in the space of sections is the metric cone.
noncomputable def
Bundle.ContMDiffRiemannianMetric.ofPositiveDefiniteSymmetricSection
{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]
{V : B → Type u_5}
[TopologicalSpace (TotalSpace F V)]
[(x : B) → TopologicalSpace (V x)]
[(x : B) → AddCommGroup (V x)]
[(x : B) → Module ℝ (V x)]
[FiberBundle F V]
[VectorBundle ℝ F V]
[FiniteDimensional ℝ F]
(σ :
ContMDiffSection IB (↥(TauCeti.symmetricBilinearMaps ℝ F ℝ)) n fun (x : B) =>
↥(TauCeti.symmetricBilinearMaps ℝ (V x) ℝ))
(hσ : σ ∈ TauCeti.Manifold.positiveDefiniteSymmetricSections IB n F V)
:
ContMDiffRiemannianMetric IB n F V
A positive-definite section of the bundle of symmetric bilinear forms determines a native Riemannian metric.
Instances For
@[simp]
theorem
Bundle.ContMDiffRiemannianMetric.ofPositiveDefiniteSymmetricSection_inner
{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]
{V : B → Type u_5}
[TopologicalSpace (TotalSpace F V)]
[(x : B) → TopologicalSpace (V x)]
[(x : B) → AddCommGroup (V x)]
[(x : B) → Module ℝ (V x)]
[FiberBundle F V]
[VectorBundle ℝ F V]
[FiniteDimensional ℝ F]
(σ :
ContMDiffSection IB (↥(TauCeti.symmetricBilinearMaps ℝ F ℝ)) n fun (x : B) =>
↥(TauCeti.symmetricBilinearMaps ℝ (V x) ℝ))
(hσ : σ ∈ TauCeti.Manifold.positiveDefiniteSymmetricSections IB n F V)
(x : B)
:
@[simp]
theorem
Bundle.ContMDiffRiemannianMetric.ofPositiveDefiniteSymmetricSection_toSymmetricSection
{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]
{V : B → Type u_5}
[TopologicalSpace (TotalSpace F V)]
[(x : B) → TopologicalSpace (V x)]
[(x : B) → AddCommGroup (V x)]
[(x : B) → Module ℝ (V x)]
[FiberBundle F V]
[VectorBundle ℝ F V]
[FiniteDimensional ℝ F]
(g : ContMDiffRiemannianMetric IB n F V)
:
Recovering a metric from its section of the symmetric bundle preserves the original metric.
@[simp]
theorem
Bundle.ContMDiffRiemannianMetric.toSymmetricSection_ofPositiveDefiniteSymmetricSection
{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]
{V : B → Type u_5}
[TopologicalSpace (TotalSpace F V)]
[(x : B) → TopologicalSpace (V x)]
[(x : B) → AddCommGroup (V x)]
[(x : B) → Module ℝ (V x)]
[FiberBundle F V]
[VectorBundle ℝ F V]
[FiniteDimensional ℝ F]
(σ :
ContMDiffSection IB (↥(TauCeti.symmetricBilinearMaps ℝ F ℝ)) n fun (x : B) =>
↥(TauCeti.symmetricBilinearMaps ℝ (V x) ℝ))
(hσ : σ ∈ TauCeti.Manifold.positiveDefiniteSymmetricSections IB n F V)
:
Recovering a metric from a positive-definite section of the symmetric bundle preserves that section.
noncomputable def
Bundle.ContMDiffRiemannianMetric.positiveDefiniteSymmetricSectionEquiv
{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]
{V : B → Type u_5}
[TopologicalSpace (TotalSpace F V)]
[(x : B) → TopologicalSpace (V x)]
[(x : B) → AddCommGroup (V x)]
[(x : B) → Module ℝ (V x)]
[FiberBundle F V]
[VectorBundle ℝ F V]
[FiniteDimensional ℝ F]
:
Native finite-rank C^n metrics are exactly the positive-definite C^n sections of the
bundle of symmetric bilinear forms.
Instances For
@[simp]
theorem
Bundle.ContMDiffRiemannianMetric.positiveDefiniteSymmetricSectionEquiv_apply
{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]
{V : B → Type u_5}
[TopologicalSpace (TotalSpace F V)]
[(x : B) → TopologicalSpace (V x)]
[(x : B) → AddCommGroup (V x)]
[(x : B) → Module ℝ (V x)]
[FiberBundle F V]
[VectorBundle ℝ F V]
[FiniteDimensional ℝ F]
(g : ContMDiffRiemannianMetric IB n F V)
:
@[simp]
theorem
Bundle.ContMDiffRiemannianMetric.positiveDefiniteSymmetricSectionEquiv_symm_apply
{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]
{V : B → Type u_5}
[TopologicalSpace (TotalSpace F V)]
[(x : B) → TopologicalSpace (V x)]
[(x : B) → AddCommGroup (V x)]
[(x : B) → Module ℝ (V x)]
[FiberBundle F V]
[VectorBundle ℝ F V]
[FiniteDimensional ℝ F]
(σ : ↑(TauCeti.Manifold.positiveDefiniteSymmetricSections IB n F V))
:
theorem
Bundle.ContMDiffRiemannianMetric.range_toSymmetricSection
{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]
{V : B → Type u_5}
[TopologicalSpace (TotalSpace F V)]
[(x : B) → TopologicalSpace (V x)]
[(x : B) → AddCommGroup (V x)]
[(x : B) → Module ℝ (V x)]
[FiberBundle F V]
[VectorBundle ℝ F V]
[FiniteDimensional ℝ F]
:
The image of the native metric carrier in the sections of the symmetric bundle is the positive-definite cone.