Isometries and the causal structure of curves

This file begins the basis-set-preservation chain for Axiom 5 (def:isometric-covariance-in-curved-spacetime): an isometry should carry trips to trips, hence chronological precedence forward, hence chronological futures forward.

The first step is the pushforward of a smooth path g ∘ μ under an isometry g, together with the chain-rule description of its tangent vector.

Main definitions

• Physicslib4.Spacetime.Isometry.pushforwardPath.

theorem Physicslib4.Spacetime.Isometry.mfderivWithin_comp_diffeo {M : Spacetime} (g : M.Isometry) (μ : M.SmoothPath) {s : ℝ} (hs : s ∈ μ.parameterSpace) : (mfderiv[μ.parameterSpace] (⇑g.toDiffeo ∘ μ.toFun) s) 1 = (mfderiv% ⇑g.toDiffeo (μ.toFun s)) ((mfderiv[μ.parameterSpace] μ.toFun s) 1)

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 μ.

noncomputable def Physicslib4.Spacetime.Isometry.pushforwardPath {M : Spacetime} (g : M.Isometry) (μ : M.SmoothPath) : M.SmoothPath

The pushforward of a smooth path μ under an isometry g: the composite g ∘ μ on the same parameter space. Smoothness is inherited from the composition of the smooth path with the (smooth) isometry, and the tangent vector is non-vanishing because the differential of an isometry is a linear isomorphism.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Physicslib4.Spacetime.Isometry.pushforwardPath_parameterSpace {M : Spacetime} (g : M.Isometry) (μ : M.SmoothPath) : (g.pushforwardPath μ).parameterSpace = μ.parameterSpace

@[simp]

theorem Physicslib4.Spacetime.Isometry.pushforwardPath_toFun {M : Spacetime} (g : M.Isometry) (μ : M.SmoothPath) : (g.pushforwardPath μ).toFun = ⇑g.toDiffeo ∘ μ.toFun

theorem Physicslib4.Spacetime.Isometry.pushforwardPath_tangent {M : Spacetime} (g : M.Isometry) (μ : M.SmoothPath) {s : ℝ} (hs : s ∈ μ.parameterSpace) : (g.pushforwardPath μ).tangent s = (mfderiv% ⇑g.toDiffeo (μ.toFun s)) (μ.tangent s)

The tangent vector of the pushforward path is the differential of the isometry applied to the tangent vector of μ.

theorem Physicslib4.Spacetime.Isometry.pushforwardPath_isTimelike {M : Spacetime} (g : M.Isometry) (μ : M.SmoothPath) (h : SmoothPath.IsTimelike M μ) : SmoothPath.IsTimelike M (g.pushforwardPath μ)

The pushforward of a timelike path is timelike: isometries preserve the timelike condition along a path.

theorem Physicslib4.Spacetime.Isometry.pushforwardPath_isCausal {M : Spacetime} (g : M.Isometry) (μ : M.SmoothPath) (h : SmoothPath.IsCausal M μ) : SmoothPath.IsCausal M (g.pushforwardPath μ)

The pushforward of a causal path is causal.

theorem Physicslib4.Spacetime.Isometry.pushforwardPath_isPastEndpoint {M : Spacetime} (g : M.Isometry) (μ : M.SmoothPath) {p : M.Carrier} (h : M.IsPastEndpoint μ p) : M.IsPastEndpoint (g.pushforwardPath μ) (g.toDiffeo p)

A past endpoint of μ is carried by g to a past endpoint of the pushforward path.

theorem Physicslib4.Spacetime.Isometry.pushforwardPath_isFutureEndpoint {M : Spacetime} (g : M.Isometry) (μ : M.SmoothPath) {p : M.Carrier} (h : M.IsFutureEndpoint μ p) : M.IsFutureEndpoint (g.pushforwardPath μ) (g.toDiffeo p)

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. The remaining step toward Axiom 5 is to show that identity-component isometries satisfy this property (a connectedness argument), which is recorded as future work.

def Physicslib4.Spacetime.Isometry.PreservesFutureOrientation {M : Spacetime} (g : M.Isometry) (t : M.TimeOrientation) : Prop

An isometry g preserves the future orientation t if its differential sends future-pointing tangent vectors to future-pointing tangent vectors.

Equations

• g.PreservesFutureOrientation t = ∀ (x : M.Carrier) (v : TangentSpace M.model x), M.IsFuturePointing t v → M.IsFuturePointing t ((mfderiv% ⇑g.toDiffeo x) v)

theorem Physicslib4.Spacetime.Isometry.preservesFutureOrientation_one {M : Spacetime} (t : M.TimeOrientation) : PreservesFutureOrientation 1 t

The identity isometry preserves the future orientation.

theorem Physicslib4.Spacetime.Isometry.preservesFutureOrientation_mul {M : Spacetime} {g h : M.Isometry} {t : M.TimeOrientation} (hg : g.PreservesFutureOrientation t) (hh : h.PreservesFutureOrientation t) : (g * h).PreservesFutureOrientation t

Future-orientation preservation is closed under composition.

noncomputable def Physicslib4.Spacetime.Isometry.futureOrientationPreserving (M : Spacetime) (t : M.TimeOrientation) : Subgroup M.Isometry

The future-orientation-preserving isometries: those g for which both g and g⁻¹ preserve the future orientation t. Bundling the inverse makes this a genuine subgroup using only the identity and composition lemmas, with no appeal to the (C⁰) group topology. This is the group over which Axiom 5's isometric covariance is intended to range.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Physicslib4.Spacetime.Isometry.mem_futureOrientationPreserving {M : Spacetime} {g : M.Isometry} {t : M.TimeOrientation} : g ∈ futureOrientationPreserving M t ↔ g.PreservesFutureOrientation t ∧ g⁻¹.PreservesFutureOrientation t

noncomputable def Physicslib4.Spacetime.Isometry.orientedIdentityComponent (M : Spacetime) (t : M.TimeOrientation) : Subgroup M.Isometry

The oriented identity component: the identity-component isometries that also preserve the future orientation. This folds orientation-preservation into the identity-component group of Axiom 5, sidestepping the (unprovable with the current C⁰ topology) statement that every identity-component isometry preserves orientation.

Equations

• Physicslib4.Spacetime.Isometry.orientedIdentityComponent M t = Physicslib4.Spacetime.Isometry.identityComponent M ⊓ Physicslib4.Spacetime.Isometry.futureOrientationPreserving M t

theorem Physicslib4.Spacetime.Isometry.pushforwardPath_isFutureOriented {M : Spacetime} (g : M.Isometry) (μ : M.SmoothPath) (t : M.TimeOrientation) (hg : g.PreservesFutureOrientation t) (h : SmoothPath.IsFutureOriented M μ t) : SmoothPath.IsFutureOriented M (g.pushforwardPath μ) t

Under future-orientation preservation, the pushforward of a future-oriented path is future-oriented.

theorem Physicslib4.Spacetime.Isometry.segmentPrecedes_pushforward {M : Spacetime} (g : M.Isometry) (t : M.TimeOrientation) (hg : g.PreservesFutureOrientation t) {p q : M.Carrier} (h : M.SegmentPrecedes t p q) : M.SegmentPrecedes t (g.toDiffeo p) (g.toDiffeo q)

Under future-orientation preservation, an isometry carries a single trip segment forward.

theorem Physicslib4.Spacetime.Isometry.chronologicallyPrecedes_pushforward {M : Spacetime} (g : M.Isometry) (t : M.TimeOrientation) (hg : g.PreservesFutureOrientation t) {p q : M.Carrier} (h : M.ChronologicallyPrecedes t p q) : M.ChronologicallyPrecedes t (g.toDiffeo p) (g.toDiffeo q)

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).

theorem Physicslib4.Spacetime.Isometry.chronologicalFuture_image_subset {M : Spacetime} (g : M.Isometry) (t : M.TimeOrientation) (hg : g.PreservesFutureOrientation t) (p : M.Carrier) : ⇑g.toDiffeo '' M.chronologicalFuture t p ⊆ M.chronologicalFuture t (g.toDiffeo p)

Under future-orientation preservation, the image of a chronological future is contained in the chronological future of the image point.

theorem Physicslib4.Spacetime.Isometry.toDiffeo_inv_apply {M : Spacetime} (g : M.Isometry) (x : M.Carrier) : g.toDiffeo (g⁻¹.toDiffeo x) = x

The underlying map of g cancels that of g⁻¹.

theorem Physicslib4.Spacetime.Isometry.inv_toDiffeo_apply {M : Spacetime} (g : M.Isometry) (x : M.Carrier) : g⁻¹.toDiffeo (g.toDiffeo x) = x

The underlying map of g⁻¹ cancels that of g.

theorem Physicslib4.Spacetime.Isometry.chronologicalFuture_image {M : Spacetime} (g : M.Isometry) (t : M.TimeOrientation) (hg : g.PreservesFutureOrientation t) (hg' : g⁻¹.PreservesFutureOrientation t) (p : M.Carrier) : ⇑g.toDiffeo '' M.chronologicalFuture t p = M.chronologicalFuture t (g.toDiffeo p)

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).

theorem Physicslib4.Spacetime.Isometry.chronologicalPast_image_subset {M : Spacetime} (g : M.Isometry) (t : M.TimeOrientation) (hg : g.PreservesFutureOrientation t) (p : M.Carrier) : ⇑g.toDiffeo '' M.chronologicalPast t p ⊆ M.chronologicalPast t (g.toDiffeo p)

Under future-orientation preservation, the image of a chronological past is contained in the chronological past of the image point.

theorem Physicslib4.Spacetime.Isometry.chronologicalPast_image {M : Spacetime} (g : M.Isometry) (t : M.TimeOrientation) (hg : g.PreservesFutureOrientation t) (hg' : g⁻¹.PreservesFutureOrientation t) (p : M.Carrier) : ⇑g.toDiffeo '' M.chronologicalPast t p = M.chronologicalPast t (g.toDiffeo p)

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).

theorem Physicslib4.Spacetime.Isometry.alexandrovBasis_image {M : Spacetime} (g : M.Isometry) (t : M.TimeOrientation) (hg : g.PreservesFutureOrientation t) (hg' : g⁻¹.PreservesFutureOrientation t) {B : Set M.Carrier} (hB : B ∈ M.alexandrovBasis t) : ⇑g.toDiffeo '' B ∈ M.alexandrovBasis t

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 𝔘(𝐁) → 𝔘(φ(𝐁)).

theorem Physicslib4.Spacetime.Isometry.alexandrovBasis_image_of_mem {M : Spacetime} (g : M.Isometry) (t : M.TimeOrientation) (hg : g ∈ futureOrientationPreserving M t) {B : Set M.Carrier} (hB : B ∈ M.alexandrovBasis t) : ⇑g.toDiffeo '' B ∈ M.alexandrovBasis t

Unconditional basis-set preservation for a future-orientation-preserving isometry: it carries Alexandrov-basis sets to Alexandrov-basis sets.

theorem Physicslib4.Spacetime.Isometry.alexandrovBasis_image_of_mem_orientedIdentityComponent {M : Spacetime} (g : M.Isometry) (t : M.TimeOrientation) (hg : g ∈ orientedIdentityComponent M t) {B : Set M.Carrier} (hB : B ∈ M.alexandrovBasis t) : ⇑g.toDiffeo '' B ∈ M.alexandrovBasis t

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 𝔘(𝐁) → 𝔘(φ(𝐁)), now unconditional.

theorem Physicslib4.Spacetime.Isometry.smul_set_eq_image {M : Spacetime} (g : M.Isometry) (B : Set M.Carrier) : g • B = ⇑g.toDiffeo '' B

The pointwise action of an isometry on a set is the image under its underlying map: g • B = g(B).

theorem Physicslib4.Spacetime.Isometry.alexandrovBasis_smul_of_mem {M : Spacetime} (g : M.Isometry) (t : M.TimeOrientation) (hg : g ∈ futureOrientationPreserving M t) {B : Set M.Carrier} (hB : B ∈ M.alexandrovBasis t) : g • B ∈ M.alexandrovBasis t

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.

theorem Physicslib4.Spacetime.LorentzianSpacetime.isBasisSet_image (L : LorentzianSpacetime) (g : L.toSpacetime.Isometry) (hg : g ∈ Isometry.orientedIdentityComponent L.toSpacetime L.timeOrientation) {B : Set L.Carrier} (hB : L.IsBasisSet B) : L.IsBasisSet (⇑g.toDiffeo '' 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.

theorem Physicslib4.Spacetime.LorentzianSpacetime.isBasisSet_smul (L : LorentzianSpacetime) (g : L.toSpacetime.Isometry) (hg : g ∈ Isometry.orientedIdentityComponent L.toSpacetime L.timeOrientation) {B : Set L.Carrier} (hB : L.IsBasisSet B) : L.IsBasisSet (g • B)

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.