Cross-metric isometries #
This file formalises the second half of the blueprint subsection Pullback metrics and cross-metric isometries (section 10.2 of the AQFT-in-Lean blueprint).
General covariance compares two different metrics on one carrier, related by
pulling back along a diffeomorphism, so the causal-transport statements of
Physicslib4/Spacetime/IsometryCausality.lean — which compare a spacetime with
itself — have to be redone cross-metric. This file supplies that geometry and
concludes with the pullback of a LorentzianSpacetime.
Main definitions #
Physicslib4.Spacetime.CrossIsometry(def:cross-metric-isometry): a diffeomorphismψbetween the manifolds of two spacetimes withψ^*g₂ = g₁. The single-metricSpacetime.Isometryis the caseN = M.Physicslib4.homeomorphOfGenerateFrom(lmm:bijection-generated-topology-homeomorphism): a bijection matching two generating families is a homeomorphism for the generated topologies.Physicslib4.Spacetime.LorentzianSpacetime.pullback(thrm:pullback-is-lorentzian-spacetime).
Modelling notes #
The blueprint phrases these statements as "two metrics g₁, g₂ on the same
manifold M". Formally they are stated here for two Spacetime structures
M, N and a diffeomorphism Diffeo M N of the underlying manifolds — a
strict generalisation, and the one the type system supports without transport
along carrier equalities. The blueprint's situation is the instance
M := M₀.pullback ψ, N := M₀, whose carriers and models are definitionally
those of M₀; Spacetime.pullbackDiffeo performs that reading of ψ.
Continuity for generated topologies, forward direction
(lmm:bijection-generated-topology-homeomorphism, first half).
If every member of the generating family T of the target pulls back into the
generating family S of the source, then f is continuous for the two generated
topologies. This is continuous_generateFrom_iff together with
TopologicalSpace.isOpen_generateFrom_of_mem.
Note that continuous_generateFrom_iff writes only the source topology
explicitly, as an implicit variable, so it has to be instantiated by hand — at
the application sites below the source is the carrier of a spacetime, which
already carries its manifold topology as an instance, and letting that be
inferred yields a well-typed but wrong statement. That is exactly why the
statement here writes both topologies with @.
Continuity for generated topologies, inverse direction
(lmm:bijection-generated-topology-homeomorphism, second half).
The same argument applied to e.symm, using that e.symm ⁻¹' s = e '' s because
e is a bijection; this is where the hypothesis hfS on images is spent.
A bijection matching generating families is a homeomorphism
(lmm:bijection-generated-topology-homeomorphism).
If e : X ≃ Y is a bijection carrying the family S into T and pulling T
back into S, it is a homeomorphism for the topologies generated by S and
T. Purely topological, with no geometry involved: the two continuity
obligations are continuous_generateFrom_of_preimage_mem and
continuous_symm_generateFrom_of_image_mem.
The bijection is taken as a bundled Equiv rather than as a function together
with Function.Bijective, so that the inverse of the resulting homeomorphism is
the given inverse e.symm and not the choice-based Function.surjInv
produced by Equiv.ofBijective. Consumers such as
Spacetime.pullbackAlexandrovHomeomorph need to compute with that inverse.
Equations
- Physicslib4.homeomorphOfGenerateFrom e S T hfS hfT = { toEquiv := e, continuous_toFun := ⋯, continuous_invFun := ⋯ }
Instances For
Isometries between two metrics #
Isometry between two metrics on one manifold (def:cross-metric-isometry).
A C^∞ diffeomorphism ψ from the manifold of M to that of N is an
isometry from (M, g₁) to (N, g₂) when ψ^*g₂ = g₁, that is when
g₂(dψ_x v, dψ_x w) = g₁(v, w) for every x and all v, w ∈ T_xM.
The usual single-metric notion — Spacetime.Isometry M — is exactly the case
N = M, and ψ is tautologically an isometry from M.pullback ψ to M; see
pullbackCrossIsometry.
- toDiffeo : M.Diffeo N
The underlying
C^∞diffeomorphism of the two underlying manifolds. - preserves (x : M.Carrier) (v w : TangentSpace M.model x) : ((N.val (self.toDiffeo x)) ((mfderiv% ⇑self.toDiffeo x) v)) ((mfderiv% ⇑self.toDiffeo x) w) = ((M.val x) v) w
Cross-metric preservation:
g₂(dψ_x v, dψ_x w) = g₁(v, w).
Instances For
ψ is tautologically an isometry from the pullback spacetime ψ^*(M,g) to
(M,g): the defining equation reads ψ^*g = ψ^*g.
Equations
- M.pullbackCrossIsometry ψ = { toDiffeo := M.pullbackDiffeo ψ, preserves := ⋯ }
Instances For
A single-metric Spacetime.Isometry is the case N = M of a cross-metric
isometry (def:cross-metric-isometry): its defining equation is literally the
preserves field of CrossIsometry M M.
The bridge points from the special case to the general one, so it cannot be used
in the other direction: it does not let the already-proved single-metric
statements of Physicslib4/Spacetime/Isometry.lean and
Physicslib4/Spacetime/IsometryCausality.lean discharge the cross-metric results
below (CrossIsometry.preserves_self, CrossIsometry.isTimelike_mfderiv_iff and
the chronology family), which are genuinely more general and have to be proved
in that generality. What the bridge does give is the converse traffic: once
proved, the cross-metric results specialise back to isometries by instantiating
Ψ := g.toCrossIsometry, so the single-metric statements need never be reproved
cross-metric. The genuinely metric-free ingredients, where duplication is
avoidable and avoided, are factored out instead into
Physicslib4/Spacetime/Diffeo.lean and
Physicslib4/Spacetime/DiffeoPath.lean.
Equations
- g.toCrossIsometry = { toDiffeo := g.toDiffeo, preserves := ⋯ }
Instances For
The single-metric future-orientation condition of
Physicslib4/Spacetime/IsometryCausality.lean is the two-metric
Spacetime.PreservesFutureOrientation at t₁ = t₂ = t, so the cross-metric
transport lemmas below apply verbatim to isometries.
The inverse of a cross-metric isometry is a cross-metric isometry
(lmm:cross-metric-isometry-symm), pointwise form:
g₁(d(ψ⁻¹)_y u, d(ψ⁻¹)_y u') = g₂(u, u').
This is not the defining equation of def:cross-metric-isometry read
backwards — reading it backwards gives an equation about dψ, not about
d(ψ⁻¹) — and passing between the two is exactly mfderiv_symm_cancel_left.
The inverse of a cross-metric isometry, as a cross-metric isometry in the
opposite direction (lmm:cross-metric-isometry-symm).
This is noncomputable of necessity, not by oversight: Diffeomorph.symm takes
the NontriviallyNormedField ℝ instance as an explicit argument, and on ℝ that
instance factors through the noncomputable Real.denselyNormedField, so the
compiler cannot generate code for Ψ.toDiffeo.symm. Contrast
Isometry.toCrossIsometry, which only repackages existing fields and so is
computable.
Instances For
The metric square is preserved
(lmm:cross-metric-isometry-preserves-classification, equation part).
A cross-metric isometry preserves timelikeness
(lmm:cross-metric-isometry-preserves-classification). The single-metric
Isometry.isTimelike_mfderiv_iff does not apply: source and target metrics
differ here.
A cross-metric isometry preserves nullness
(lmm:cross-metric-isometry-preserves-classification).
A cross-metric isometry preserves spacelikeness
(lmm:cross-metric-isometry-preserves-classification).
Pushforward of a path #
The pushforward ψ ∘ μ of a path, the chain rule for its tangent vector and the
transport of endpoints depend on the diffeomorphism only and not on either metric,
so they are not stated here at all: they live in
Physicslib4/Spacetime/DiffeoPath.lean, low enough in the import graph that the
single-metric Isometry.pushforwardPath is defined as an instance of them.
What remains here are the statements that genuinely consume metric preservation.
The pushforward preserves the timelike condition
(lmm:cross-metric-pushforward-path-causal): if μ is timelike for g₁ then
ψ ∘ μ is timelike for g₂.
The pushforward preserves the causal condition
(lmm:cross-metric-pushforward-path-causal).
Under future-orientation preservation the pushforward of a future-oriented path is future-oriented.
Transport of chronology #
A cross-metric isometry preserving the future orientation carries a single trip segment forward.
Cross-metric isometries transport chronological precedence
(lmm:cross-metric-isometry-preserves-chronology): p ≪₁ q implies
ψ p ≪₂ ψ q. A trip is a finite chain of trip segments, so this lifts
CrossIsometry.segmentPrecedes along the transitive closure
(Relation.TransGen.lift).
Image of the chronological future
(lmm:cross-metric-chronological-future-image): ψ(I⁺₁(p)) = I⁺₂(ψ p).
The ⊆ half is CrossIsometry.chronologicallyPrecedes; the ⊇ half applies the
same lemma to ψ⁻¹, which is a cross-metric isometry in the opposite direction
by CrossIsometry.symm and preserves the future orientation by the second half
of the two-sided hypothesis.
Image of the chronological past
(lmm:cross-metric-chronological-past-image): ψ(I⁻₁(p)) = I⁻₂(ψ p).
Cross-metric isometries preserve basis sets
(lmm:cross-metric-isometry-preserves-basis-sets), diamond form:
ψ(I⁺₁(p) ∩ I⁻₁(q)) = I⁺₂(ψ p) ∩ I⁻₂(ψ q).
The image of an intersection under an injective map is the intersection of the
images, and the two factors are CrossIsometry.chronologicalFuture_image and
CrossIsometry.chronologicalPast_image.
Cross-metric isometries preserve basis sets
(lmm:cross-metric-isometry-preserves-basis-sets), membership form.
The pullback Alexandrov topology #
ψ carries pullback Alexandrov basis sets to Alexandrov basis sets
(lmm:pullback-alexandrov-homeomorphism, forward matching hypothesis).
This is CrossIsometry.alexandrovBasis_image applied to pullbackCrossIsometry,
whose two-sided orientation hypothesis is
pullback_preservesFutureOrientationTwoSided.
ψ⁻¹ carries Alexandrov basis sets to pullback Alexandrov basis sets
(lmm:pullback-alexandrov-homeomorphism, backward matching hypothesis).
This is CrossIsometry.alexandrovBasis_image applied to
(pullbackCrossIsometry M ψ).symm together with the second half of
pullback_preservesFutureOrientationTwoSided, the preimage under ψ being the
image under ψ⁻¹.
The pullback Alexandrov topology (lmm:pullback-alexandrov-homeomorphism).
ψ is a homeomorphism from ψ^*(M,g) carrying the Alexandrov topology of
ψ^*g and ψ^*t to (M,g) carrying the Alexandrov topology of g and t.
This is homeomorphOfGenerateFrom applied to the two families of Alexandrov
diamonds, whose matching-up is pullback_alexandrovBasis_image and
pullback_alexandrovBasis_preimage; the proof of this node is pure citation and
introduces no obligation of its own.
Equations
- M.pullbackAlexandrovHomeomorph ψ t = Physicslib4.homeomorphOfGenerateFrom (M.pullbackDiffeo ψ).toEquiv ((M.pullback ψ).alexandrovBasis (M.pullbackTimeOrientation ψ t)) (M.alexandrovBasis t) ⋯ ⋯
Instances For
The homeomorphism of lmm:pullback-alexandrov-homeomorphism is ψ itself.
The pullback Alexandrov topology is Hausdorff
(thrm:pullback-is-lorentzian-spacetime, the only obligation of that node).
It transports from the Hausdorffness of the Alexandrov topology of (M,g,t)
along pullbackAlexandrovHomeomorph by Homeomorph.t2Space.
The pullback of a Lorentzian spacetime is a Lorentzian spacetime
(thrm:pullback-is-lorentzian-spacetime).
The underlying spacetime is Spacetime.pullback, the time orientation is
Spacetime.pullbackTimeOrientation and the Hausdorff condition on the Alexandrov
topology is LorentzianSpacetime.pullback_alexandrov_t2.
This is what makes "the net over ψ^*(M,g)" meaningful in
def:general-covariance-in-curved-spacetime.
Equations
- L.pullback ψ = { toSpacetime := L.toSpacetime.pullback ψ, timeOrientation := L.toSpacetime.pullbackTimeOrientation ψ L.timeOrientation, alexandrov_t2 := ⋯ }