Local isometries of nondegenerate metrics #
Let g and g' be smooth symmetric nondegenerate metrics on M and N, of any signature. A
local isometry f : M → N from g to g' is a smooth map whose differential at every point is
invertible and pulls g' back to g:
g'_{f x}(df_x v, df_x w) = g_x(v, w).
It need not be injective or surjective: a diffeomorphism preserving the metrics is a local isometry, and so is a covering map whose target metric pulls back to the source metric.
The Levi-Civita connection is natural under local isometries: if ∇ and ∇' are Levi-Civita
connections of g and g', then for a vector field Y on N differentiable at f x,
df_x (∇_v (f^* Y)) = ∇'_{df_x v} Y,
where f^* Y = VectorField.mpullback I J f Y is the pullback vector field. The proof transports
the Koszul expression along f and concludes by the nondegeneracy of g'. Since a Levi-Civita
connection of a nondegenerate metric is unique on differentiable vector fields, this determines
how any construction of it behaves under metric-preserving diffeomorphisms.
For metrics coming from Riemannian bundle instances, local isometries are exactly the local
Riemannian isometries TauCeti.IsLocalRiemannianIsometry.
Main definitions and results #
In the namespace TauCeti.Manifold.ContMDiffNondegenerateMetric:
IsLocalIsometry: a smooth map with invertible differentials pulling one nondegenerate metric back to another.IsLocalIsometry.mfderiv_apply_mpullback: the differential cancels the pullback of a vector field.IsLocalIsometry.idandIsLocalIsometry.comp: the identity and composites.isLocalIsometry_ofRiemannianBundle_iff: for Riemannian metrics, local isometries are the local Riemannian isometries.IsLocalIsometry.koszul_mpullback: the Koszul expression is natural under local isometries.IsLocalIsometry.two_apply_mfderiv_eq_koszul: the Koszul formula of a Levi-Civita connection of the source metric, read in the target through the differential; it needs no connection of the target metric.IsLocalIsometry.mfderiv_apply_mpullback_of_isLeviCivitaConnection: naturality of Levi-Civita connections under local isometries.IsLocalIsometry.mpullback_apply_mpullback_of_isLeviCivitaConnection: the vector-field form∇_{f^* Y} (f^* Z) = f^* (∇'_Y Z).
References #
- B. O'Neill, Semi-Riemannian Geometry with Applications to Relativity, Academic Press, 1983, Ch. 3 (isometries preserve Levi-Civita connections).
- J. M. Lee, Introduction to Riemannian Manifolds, 2nd ed., Springer GTM 176 (2018), Prop. 5.13.
TauCeti.Geometry.Manifold.Riemannian.Isometry.LeviCivita: the positive-definite argument for local Riemannian isometries, adapted here with the inner product replaced bygand positivity by nondegeneracy.
A smooth map f : M → N is a local isometry from the nondegenerate metric g on M to the
nondegenerate metric g' on N if its differential at every point is invertible and pulls g'
back to g.
A local isometry is smooth.
- isInvertible_mfderiv (x : M) : (mfderiv% f x).IsInvertible
The differential of a local isometry is invertible at every point.
- apply_mfderiv (x : M) (v w : TangentSpace I x) : ((g'.toContMDiffSection (f x)) ((mfderiv% f x) v)) ((mfderiv% f x) w) = ((g.toContMDiffSection x) v) w
The differential of a local isometry pulls the target metric back to the source metric.
Instances For
The differential of a local isometry sends the pullback of a vector field at x to the value
of the field at f x.
Pulling back vector fields along a local isometry preserves their pointwise pairing.
The identity map is a local isometry from a nondegenerate metric to itself.
The composite of two local isometries of nondegenerate metrics is a local isometry.
For the metrics of smooth Riemannian bundle instances, a local isometry is exactly a local Riemannian isometry.
Pulling back a vector field differentiable at f x along a local isometry gives a vector
field differentiable at x.
Naturality of the Koszul expression. The Koszul expression of g on the pullbacks of three
vector fields along a local isometry f is the Koszul expression of g' on the fields themselves,
evaluated at the image point.
The Koszul formula through a local isometry. Let ∇ be a Levi-Civita connection of g
and f a local isometry from g to g'. For vector fields X, Y, Z on N differentiable
at f x with X (f x) = df_x v, 2 g'(df_x (∇_v (f^* Y)), Z) at f x is the Koszul expression
of g' on X, Y, Z at f x. No Levi-Civita connection of g' is needed.
Naturality of Levi-Civita connections under local isometries. If ∇ and ∇' are
Levi-Civita connections of the nondegenerate metrics g and g' and f is a local isometry from
g to g', then df_x (∇_v (f^* Y)) = ∇'_{df_x v} Y for every vector field Y on N
differentiable at f x.
The covariant derivative of a pulled-back vector field in a pulled-back direction is the
pullback of the covariant derivative: ∇_{f^* Y} (f^* Z) = f^* (∇'_Y Z) at x, for Levi-Civita
connections ∇ and ∇' of g and g' and a local isometry f from g to g'.