Pullback of a spacetime metric along a diffeomorphism #
This file formalises the first half of the blueprint subsection
Pullback metrics and cross-metric isometries (section 10.2 of the
AQFT-in-Lean blueprint): the pullback metric ψ^*g, the fact that it is again
a spacetime metric, and the pullback of a time orientation together with the
two-sided transport of future-pointing-ness.
The cross-metric isometry theory built on top of this lives in
Physicslib4/Spacetime/CrossMetricIsometry.lean.
The purely differential-geometric input — the type Physicslib4.Spacetime.Diffeo
of C^∞ diffeomorphisms, the differential mfderivEquiv as a continuous linear
equivalence, the round-trip cancellations and the formal inverse — lives in
Physicslib4/Spacetime/Diffeo.lean, which mentions no metric and is therefore
imported by the single-metric isometry theory as well.
Main definitions #
Physicslib4.Spacetime.pullbackVal(def:pullback-metric): the field of continuous bilinear forms(ψ^*g)_x = g_{ψ x}(dψ_x ·, dψ_x ·), realised as an inhabitant of the bundled type viaContinuousLinearMap.bilinearComp.Physicslib4.Spacetime.pullback(thrm:pullback-is-spacetime): the pullback spacetimeψ^*(M,g), keeping all manifold data ofMand replacing the metric bypullbackVal.Physicslib4.Spacetime.PreservesFutureOrientationandPreservesFutureOrientationTwoSided(def:preserves-future-orientation): the cross-metric orientation conditions on a bare diffeomorphism, generalising the single-metricIsometry.PreservesFutureOrientation.Physicslib4.Spacetime.pullbackTimeOrientation(lmm:pullback-time-orientation): the pullback time orientationψ^*t = (dψ_x)⁻¹ t_{ψ x}, i.e.VectorField.mpullback.
Modelling notes #
The blueprint states the pullback only for a diffeomorphism ψ : M → M of one
spacetime. The purely differential-geometric statements are stated in
Physicslib4/Spacetime/Diffeo.lean for a diffeomorphism between the manifolds
of two spacetimes, since the cross-metric isometry theory downstream needs
exactly that generality and the single-spacetime case is the instance N := M.
The genuinely metric-level constructions (pullbackVal, pullback,
pullbackTimeOrientation) are stated for ψ : Diffeo M M, matching the
blueprint.
The pullback metric #
Two-slot precomposition of a continuous bilinear form on the model space
ℝ⁴ with a continuous linear map, i.e. ContinuousLinearMap.bilinearComp read
on SpacetimeModel.
This auxiliary step is needed because Mathlib's bilinearComp requires
SeminormedAddCommGroup instances on its source spaces, while
TangentSpace I x is not reducible and carries only topological-module
instances; the two families of instances are definitionally equal, so the
form is built on the model space and transported to the tangent spaces in
pullbackVal (exactly the device used for the constant metric in
Physicslib4/Spacetime/Minkowski.lean).
Equations
Instances For
The pullback of a spacetime metric (def:pullback-metric).
(ψ^*g)_x(v,w) = g_{ψ x}(dψ_x v, dψ_x w), realised as an inhabitant of the
bundled type T_xM →L[ℝ] T_xM →L[ℝ] ℝ by precomposing g_{ψ x} with dψ_x in
both slots (bilinearPrecomp, i.e. ContinuousLinearMap.bilinearComp).
Continuity and bilinearity are then structural rather than facts to be proved,
and pullbackVal_apply recovers the displayed formula.
This node is data only; that ψ^*g satisfies the metric obligations of
def:spacetime is Physicslib4.Spacetime.pullback.
Equations
- M.pullbackVal ψ x = Physicslib4.Spacetime.bilinearPrecomp (M.val (ψ x)) (mfderiv% ⇑ψ x)
Instances For
The pullback metric is symmetric (lmm:pullback-metric-symm).
The pullback metric is non-degenerate
(lmm:pullback-metric-nondegenerate): if (ψ^*g)_x(v,w) = 0 for all w then
v = 0.
The pullback metric is Lorentzian (lmm:pullback-metric-lorentzian):
at every x there is a basis of T_xM whose Gram matrix under (ψ^*g)_x is
diag(-1,1,1,1). The signature basis is transported from T_{ψ x}M along the
inverse of mfderivEquiv by Module.Basis.map; this is where the existential
formulation of the Lorentzian condition in def:spacetime is essential.
The pullback metric is a smooth section of the bilinear-form bundle
(lmm:pullback-metric-smooth-in-charts).
The contMDiff field of def:spacetime for ψ^*g, at the same regularity
index ∞ as Spacetime.contMDiff itself. The label name is historical: the
statement is entirely in the bundle-section idiom and nothing chart-local
remains.
The pullback of a spacetime is a spacetime (thrm:pullback-is-spacetime).
ψ^*(M,g) keeps the carrier set, topology, Hausdorff and connectedness
properties, charts, model with corners, smooth structure and tangent-space
finite-dimensionality of (M,g) unchanged, and replaces the metric field by
pullbackVal. The four metric obligations are discharged by
pullbackVal_symm, pullbackVal_nondegenerate, pullbackVal_lorentzian and
pullbackVal_contMDiff.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The carrier of the pullback spacetime is that of M. Deliberately not
@[simp]: this is an equality of Types, so rewriting with it inside a
dependent goal produces motive-correctness failures rather than progress; the
two carriers are definitionally equal and should be used as such.
ψ regarded as a diffeomorphism from the pullback spacetime to M. The two
types are definitionally equal, since pullback changes only the metric field;
this is the coercion used whenever ψ has to be read cross-metric.
Equations
- M.pullbackDiffeo ψ = ψ
Instances For
Two-sided preservation of the future orientation #
Preservation of the future orientation, cross-metric
(def:preserves-future-orientation, one-sided half).
A diffeomorphism ψ from the manifold of M (with time orientation t₁) to
that of N (with time orientation t₂) preserves the future orientation when
dψ_x carries vectors that are future-pointing for (g₁,t₁) to vectors that are
future-pointing for (g₂,t₂).
Nothing here refers to the metrics beyond the two orientations, so this is a
condition on a diffeomorphism and a pair of oriented metrics, stated
independently of any isometry hypothesis. The single-metric case N = M,
t₂ = t₁ is Isometry.PreservesFutureOrientation.
Equations
- Physicslib4.Spacetime.PreservesFutureOrientation ψ t₁ t₂ = ∀ (x : M.Carrier) (v : TangentSpace M.model x), M.IsFuturePointing t₁ v → N.IsFuturePointing t₂ ((mfderiv% ⇑ψ x) v)
Instances For
The two-sided orientation hypothesis (def:preserves-future-orientation):
both ψ preserves the future orientation from (g₁,t₁) to (g₂,t₂) and ψ⁻¹
preserves it from (g₂,t₂) back to (g₁,t₁).
Equations
- One or more equations did not get rendered due to their size.
Instances For
The pullback time orientation #
The pullback of a bundle-smooth vector field along a diffeomorphism is
bundle-smooth (lmm:mpullback-vectorField-contMDiff-of-diffeo).
The hypothesis hV is literally the smooth field of
Spacetime.TimeOrientation, and the conclusion is literally the smooth field
to be produced for ψ^*t, so no conversion happens on either side. This is
ContMDiff.mpullback_vectorField, whose hf' hypothesis is supplied by
isInvertible_mfderiv and whose exponent gap ∞ + 1 ≤ ∞ is discharged by
simp, since ∞ + 1 = ∞ in ℕ∞.
Following the policy of the module docstring, and matching the generality of
ContMDiff.mpullback_vectorField itself, this is stated for a diffeomorphism
between the manifolds of two spacetimes; the blueprint's case is the instance
N := M, used by pullbackTimeOrientation.
The pullback time orientation is nowhere vanishing
(lmm:pullback-time-orientation-ne-zero): (ψ^*t)_x = (dψ_x)⁻¹ t_{ψ x} ≠ 0.
This needs inverse_mfderiv_eq_symm: off the invertible case
ContinuousLinearMap.inverse returns the junk value 0 and is not
injective.
The metric square of the pullback time orientation is the metric square of
t at the image point (lmm:pullback-time-orientation-timelike, equation
part):
(ψ^*g)_x((ψ^*t)_x, (ψ^*t)_x) = g_{ψ x}(t_{ψ x}, t_{ψ x}).
The pullback time orientation is everywhere timelike
(lmm:pullback-time-orientation-timelike).
Pullback of a time orientation (lmm:pullback-time-orientation).
ψ^*t : x ↦ (dψ_x)⁻¹ t_{ψ x}, which is Mathlib's VectorField.mpullback, is a
time orientation of the pullback spacetime: smoothness is
contMDiff_mpullback_vectorField applied at V = t.field, non-vanishing is
mpullback_field_ne_zero and timelikeness is isTimelike_mpullback_field.
Equations
- M.pullbackTimeOrientation ψ t = { field := VectorField.mpullback M.model M.model (⇑ψ) t.field, nonvanishing := ⋯, timelike_at := ⋯, smooth := ⋯ }
Instances For
The mixed metric identity underlying the transport of future-pointing-ness
(lmm:pullback-future-pointing-timelike, equation part):
(ψ^*g)_x((ψ^*t)_x, v) = g_{ψ x}(t_{ψ x}, dψ_x v).
Transport of future-pointing timelike vectors
(lmm:pullback-future-pointing-timelike). For v timelike for ψ^*g, v is
future-pointing for (ψ^*g, ψ^*t) if and only if dψ_x v is future-pointing
for (g,t).
Transport of future-pointing null vectors
(lmm:pullback-future-pointing-null). For v null for ψ^*g the condition is
not a sign condition but the existence of an approximating sequence of
future-pointing timelike vectors, so the witnessing sequence is transported
along the continuous linear map dψ_x (and back along its inverse).
The pullback preserves the future orientation two-sidedly
(lmm:pullback-preserves-future-orientation).
ψ, regarded as carrying (ψ^*g, ψ^*t) to (g,t), satisfies the two-sided
orientation hypothesis of def:preserves-future-orientation. A future-pointing
vector is timelike or null, and each of the two transport lemmas above is an
equivalence, so it yields both the forward direction for ψ and the forward
direction for ψ⁻¹; the ψ⁻¹ half is where mfderiv_symm_cancel_left is
spent.