Smooth nondegenerate metrics on a manifold #
This file bundles a smooth field of symmetric nondegenerate real bilinear forms on the tangent bundle. Positivity is not required.
The metric is stored as a native ContMDiffSection of the bundle of continuous bilinear forms.
When the model space is finite-dimensional, its pointwise nondegeneracy produces flat and sharp
musical isomorphisms through LinearMap.BilinForm.toDual. Every smooth Riemannian metric gives
such a nondegenerate metric, which connects this general carrier to Mathlib's positive-definite
Riemannian carrier.
These objects are the algebraic and smooth carrier needed to state the Koszul construction of the Levi-Civita connection for an indefinite metric.
Main definitions and results #
TauCeti.Manifold.ContMDiffNondegenerateMetric: a smooth symmetric nondegenerate tangent bilinear form.TauCeti.Manifold.tangentBilinFormInCoordinates: a tangent bilinear form read in a tangent-bundle trivialization, with its symmetry and nondegeneracy on the base set.TauCeti.Manifold.ContMDiffNondegenerateMetric.inCoordinates: the metric read in a tangent-bundle trivialization, with its symmetry, nondegeneracy and smoothness on the base set.TauCeti.Manifold.ContMDiffNondegenerateMetric.chartMetric: the metric read in the chart at a point, a field of symmetric nondegenerate bilinear forms on the chart target, smooth there.TauCeti.Manifold.ContMDiffNondegenerateMetric.flat: its fibrewise flat musical equivalence, for a finite-dimensional model space.TauCeti.Manifold.ContMDiffNondegenerateMetric.sharp: the inverse musical equivalence, for a finite-dimensional model space.TauCeti.Manifold.ContMDiffNondegenerateMetric.ofRiemannianBundle: the metric of a smooth Riemannian bundle instance on the tangent bundle, as a smooth nondegenerate metric.Bundle.ContMDiffRiemannianMetric.toNondegenerateMetric: the positive-definite specialization.
References #
- J. M. Lee, Introduction to Riemannian Manifolds, 2nd ed., Springer GTM 176 (2018), Chapters 2 and 5.
A smooth field of symmetric nondegenerate real bilinear forms on the tangent bundle.
The form is a native smooth section of the continuous-bilinear-form bundle. Nondegeneracy is the
native algebraic predicate on its underlying LinearMap.BilinForm; it does not impose positivity
or choose any signature.
- toContMDiffSection : ContMDiffSection I (E →L[ℝ] E →L[ℝ] ℝ) ↑⊤ fun (x : M) => TangentSpace I x →L[ℝ] TangentSpace I x →L[ℝ] ℝ
The smooth section of continuous bilinear forms.
- symm (x : M) : (self.toContMDiffSection x).toBilinForm.IsSymm
The bilinear form in every tangent fibre is symmetric.
- nondegenerate (x : M) : (self.toContMDiffSection x).toBilinForm.Nondegenerate
The bilinear form in every tangent fibre is nondegenerate.
Instances For
The underlying field of bilinear forms is smooth.
Pairing two differentiable vector fields with a smooth nondegenerate metric is differentiable.
Evaluation of a smooth nondegenerate metric is symmetric in its tangent arguments.
Smooth nondegenerate metrics are equal when all their fibrewise pairings agree.
Tangent bilinear forms read in a trivialization #
A bilinear form ϕ on the tangent space at x, read in the trivialization of the tangent
bundle at a: a continuous bilinear form on the model space. It is meaningful for x in the base
set of that trivialization.
Instances For
The tangent bilinear-form coordinate map is the canonical coordinate map for hom bundles.
On the base set of the trivialization at a, a tangent bilinear form read in that
trivialization pairs two vectors of the model space as the form pairs the tangent vectors with
these coordinates.
On the base set of the trivialization at a, a tangent bilinear form read in that
trivialization is the congruence of the form by the trivialization's linear equivalence.
A symmetric tangent bilinear form read in a trivialization is symmetric on its base set.
A nondegenerate tangent bilinear form read in a trivialization is nondegenerate on its base set.
A family of tangent bilinear forms that is continuous at y₀, as a map into the total space
of the tangent bilinear-form bundle, is continuous at y₀ when read in the trivialization at its
base point at y₀.
The metric read in a trivialization #
The metric g at x, read in the trivialization of the tangent bundle at a: a continuous
bilinear form on the model space. It is meaningful for x in the base set of that
trivialization.
Instances For
Reading the metric in a trivialization is the general tangent bilinear-form coordinate construction applied to its value at the point.
On the base set of the trivialization at a, the metric read in that trivialization pairs two
vectors of the model space as g pairs the tangent vectors with these coordinates.
On the base set of the trivialization at a, the metric read in that trivialization is the
congruence of the metric by the trivialization's linear equivalence.
The metric read in a trivialization is symmetric on its base set.
The metric read in a trivialization is nondegenerate on its base set.
The metric read in the trivialization at a is smooth at every point of its base set.
The metric read in a chart #
The metric g read in the chart at x₀: at a point z of the model space, the bilinear form
on E obtained by reading g at (extChartAt I x₀).symm z in the trivialization of the tangent
bundle at x₀. It is meaningful on the chart target (extChartAt I x₀).target.
Instances For
The chart metric is the tangent coordinate metric composed with the inverse base chart.
At a point z of the chart target, the chart metric pairs two vectors of the model space as
g pairs the tangent vectors at (extChartAt I x₀).symm z with these coordinates.
At the chart image of a point y of the chart domain, the chart metric pairs two vectors of
the model space as g pairs the tangent vectors at y with these coordinates.
At the chart image of a point y of the chart domain, the chart metric pairs two vectors of a
basis b of the model space as g pairs the corresponding vectors at y of the coordinate frame
of b.
The chart metric is symmetric at every point of the chart target.
The chart metric is nondegenerate at every point of the chart target.
The chart metric is smooth on the chart target.
The chart metric is smooth at the chart image of every point of the chart domain lying in the interior of the model.
The flat musical isomorphism induced by a smooth nondegenerate metric at x. Its inverse is
the sharp musical isomorphism.
Instances For
The flat musical isomorphism is Mathlib's dual equivalence of the fibrewise bilinear form.
The sharp musical isomorphism induced by a smooth nondegenerate metric at x.
Instances For
The inverse of the flat musical isomorphism is the sharp musical isomorphism.
Flat undoes sharp.
Sharp undoes flat.
The flat musical isomorphism evaluates as the metric pairing.
The sharp representative of a covector pairs against every vector to give that covector.
By symmetry, the sharp representative also represents a covector in the second argument.
A vector is the sharp representative of a covector exactly when contraction with the metric gives that covector.
A smooth positive-definite Riemannian metric, viewed as a smooth symmetric nondegenerate metric without forgetting its fibrewise values.
Instances For
Viewing a Riemannian metric as a nondegenerate metric preserves its pointwise pairing.
The metric of a smooth Riemannian bundle structure on the tangent bundle, viewed as a smooth symmetric nondegenerate metric.
Instances For
The metric of a Riemannian bundle structure pairs tangent vectors by their inner product.