Isometries and the causal structure of curves #
This file proves basis-set preservation for Axiom 5
(def:isometric-covariance-in-curved-spacetime): a future-orientation-
preserving isometry g carries trips to trips, hence chronological
precedence, chronological futures and pasts, and Alexandrov diamonds, to
their images.
The construction starts from the pushforward of a smooth path g ∘ μ
under an isometry g, together with the chain-rule description of its
tangent vector, and builds up through geodesics, chronological futures and
pasts, and Alexandrov diamonds to alexandrovBasis_image and isBasisSet_smul.
Main definitions / results #
Physicslib4.Spacetime.Isometry.pushforwardPath.Physicslib4.Spacetime.Isometry.orientedIdentityComponent: the subgroup of isometries that preserve a time orientation and lie in the identity component.Physicslib4.Spacetime.Isometry.alexandrovBasis_image: an isometry carries Alexandrov diamonds to Alexandrov diamonds.Physicslib4.Spacetime.LorentzianSpacetime.isBasisSet_smul: basis-set preservation under the action oforientedIdentityComponent.
Chain rule for the tangent vector of g ∘ μ along the parameter space:
the derivative of the composite is the differential of the isometry applied
to the derivative of μ.
Metric preservation plays no role, so this is the instance ψ := g.toDiffeo of
Spacetime.mfderivWithin_comp_diffeo
(lmm:cross-metric-pushforward-path-tangent).
The pushforward of a smooth path μ under an isometry g: the composite
g ∘ μ on the same parameter space.
None of the data of the pushforward path depends on the metric, so this is by
definition the instance ψ := g.toDiffeo of Spacetime.pushforwardPath
(lmm:cross-metric-pushforward-path) rather than a second copy of the same
construction; in particular the accessors below remain rfl.
Equations
Instances For
The tangent vector of the pushforward path is the differential of the
isometry applied to the tangent vector of μ.
The pushforward of a timelike path is timelike: isometries preserve the timelike condition along a path.
The pushforward of a causal path is causal.
A past endpoint of μ is carried by g to a past endpoint of the
pushforward path.
A future endpoint of μ is carried by g to a future endpoint of the
pushforward path.
Preservation of future orientation, trips and chronological precedence #
A general isometry preserves the metric and hence the timelike/null/spacelike
classification, but it need not preserve the chosen time orientation t. We
isolate the property that it preserves future-pointing-ness and show that,
under this hypothesis, the pushforward carries trips to trips and therefore
chronological precedence forward. Whether every identity-component isometry
has this property is not decided here; orientedIdentityComponent includes
it as a condition.
An isometry g preserves the future orientation t: its differential sends future-pointing tangent vectors to future-pointing tangent vectors.
Such an isometry carries trips to trips, so p ≪ q implies g(p) ≪ g(q)
(chronologicallyPrecedes_pushforward). The property holds for the identity and is closed under
composition; the subgroup asks it of g and of g⁻¹ (futureOrientationPreserving).
Blueprint: lmm:isometry-preserves-chronology
Equations
- g.PreservesFutureOrientation t = ∀ (x : M.Carrier) (v : TangentSpace M.model x), M.IsFuturePointing t v → M.IsFuturePointing t ((mfderiv% ⇑g.toDiffeo x) v)
Instances For
The identity isometry preserves the future orientation.
Future-orientation preservation is closed under composition.
The subgroup of isometries g such that g and g⁻¹ both preserve the future orientation t.
Implementation note: asking the condition of g⁻¹ as well makes this a subgroup using only the
identity and composition lemmas, with no appeal to the group topology. Its intersection with
identityComponent is orientedIdentityComponent, the group of Axiom 5.
Blueprint: lmm:isometry-preserves-basis-sets
Equations
- One or more equations did not get rendered due to their size.
Instances For
The oriented identity component: the isometries in the identity component that preserve the time orientation t.
This is the group of "isometries connected to the identity" of Axiom 5 in curved spacetime, the
group Isom of LorentzianSpacetime.toAbstractIdentityComponent. Its members carry trips to
trips and chronological diamonds to chronological diamonds, with
φ(I⁺(p) ∩ I⁻(q)) = I⁺(φ(p)) ∩ I⁻(φ(q))
(alexandrovBasis_image_of_mem_orientedIdentityComponent), which is what makes the Axiom 5 maps
𝔘(B) → 𝔘(φ(B)) well defined.
Implementation note: the group is identityComponent intersected with
futureOrientationPreserving. Every isometry in the identity component preserves the future
orientation, so the intersection is the whole identity component, but the proof needs a
Myers–Steenrod-type rigidity theorem that Mathlib does not provide, so orientation preservation
is part of the definition instead.
Blueprint: lmm:isometry-preserves-basis-sets
Equations
Instances For
Under future-orientation preservation, the pushforward of a future-oriented path is future-oriented.
The differential of an isometry g undoes the pullback of a vector field along g.
The metric pairing of pullbacks along an isometry is the pullback of the pairing.
Chain rule for the metric pairing of pulled-back vector fields along an isometry.
Naturality of the Lie bracket under an isometry, paired with the metric.
An isometry preserves the Levi-Civita connection: dg(∇_{g^*A} g^*B) = ∇_A B ∘ g.
Blueprint reference: lmm:isometry-preserves-levi-civita.
Isometries map geodesics to geodesics. An isometry φ preserves the Levi-Civita
connection (lmm:isometry-preserves-levi-civita), so it carries a vector field extending the
velocity of μ to one extending the velocity of φ ∘ μ, and the geodesic condition transfers.
Blueprint reference: lmm:isometry-preserves-geodesics.
Under future-orientation preservation, an isometry carries a single trip segment forward.
Under future-orientation preservation, an isometry carries chronological
precedence forward: p ≪ q implies g p ≪ g q. A trip is a finite chain of
trip segments, so this lifts segmentPrecedes_pushforward along the transitive
closure (Relation.TransGen.lift).
Under future-orientation preservation, the image of a chronological future is contained in the chronological future of the image point.
When both g and g⁻¹ preserve the future orientation, the image of a
chronological future is exactly the chronological future of the image point:
g(I⁺(p)) = I⁺(g p).
Under future-orientation preservation, the image of a chronological past is contained in the chronological past of the image point.
When both g and g⁻¹ preserve the future orientation, the image of a
chronological past is exactly the chronological past of the image point:
g(I⁻(p)) = I⁻(g p).
Basis-set preservation. When both g and g⁻¹ preserve the future
orientation, the isometry carries Alexandrov-basis sets to Alexandrov-basis
sets: g(I⁺(p) ∩ I⁻(q)) = I⁺(g p) ∩ I⁻(g q). This is the geometric content
behind Axiom 5's action 𝔘(𝐁) → 𝔘(φ(𝐁)).
Unconditional basis-set preservation for a future-orientation-preserving isometry: it carries Alexandrov-basis sets to Alexandrov-basis sets.
Basis-set preservation for the oriented identity component. Every
isometry in the oriented identity component carries Alexandrov-basis sets to
Alexandrov-basis sets - the geometric input behind Axiom 5's action
𝔘(𝐁) → 𝔘(φ(𝐁)), with no further hypothesis.
Basis-set preservation in pointwise-action form: a future-orientation-
preserving isometry sends Alexandrov-basis sets to basis sets, with the action
written as g • B.
Basis-set preservation on a Lorentzian spacetime (image form). An
isometry of L.toSpacetime in the oriented identity component carries
IsBasisSet sets to IsBasisSet sets.
Basis-set preservation on a Lorentzian spacetime (pointwise-action form).
The same statement written with the pointwise action g • B, as used by the
abstract Axiom 5 interface.