Physicslib4.Spacetime.Isometry

Isometries of a spacetime

This file develops the group of isometries of a Physicslib4.Spacetime, used to instantiate the abstract isometry group of the curved-spacetime Haag-Kastler axioms (def:isometric-covariance-in-curved-spacetime, Axiom 5).

Main definitions

• Physicslib4.Spacetime.Isometry: a diffeomorphism of the spacetime whose manifold differential mfderiv preserves the metric.
• Group (Isometry M) and MulAction (Isometry M) M.Carrier.

Modelling notes

An isometry is a genuine C^∞ diffeomorphism φ : M → M (bundled as a Diffeomorph, so smoothness of φ and of φ⁻¹ is built in) whose manifold derivative preserves the metric: g_{φ(x)}(dφ_x v, dφ_x w) = g_x(v, w), where dφ_x = mfderiv I I φ x. Composition and inverse preserve the metric via the manifold chain rule (mfderiv_comp); for the inverse we use that φ ∘ φ⁻¹ = id together with Filter.EventuallyEq.mfderiv_eq, exactly as Mathlib's PartialHomeomorph.MDifferentiable.comp_symm_deriv does. The isometries thus form a group acting on points.

On the identity-component restriction. Isometry M is the full metric-preserving diffeomorphism group. The blueprint's identity-component ("connected to the identity") restriction of Axiom 5 is captured downstream: Physicslib4/Spacetime/IsometryTopology.lean topologizes this group as a topological group and defines the identity-component subgroup Isometry.identityComponent := Subgroup.connectedComponentOfOne, and Isometry.orientedIdentityComponent (IsometryCausality.lean) intersects it with future-orientation preservation. That subgroup is the M.Isom supplied to the curved Haag-Kastler bridge toAbstractIdentityComponent. The full group is retained here as the substrate and for the axioms that hold under all isometries (e.g. microcausality).

structure Physicslib4.Spacetime.Isometry (M : Spacetime) : Type u_1

An isometry of a spacetime: a C^∞ diffeomorphism φ of M whose differential preserves the metric, g_(φ(x))(dφ_x v, dφ_x w) = g_x(v, w).

Isometries are the symmetries of the geometry; for Minkowski spacetime they include the Poincaré transformations. They form a group under composition, (φ * ψ)(x) = φ(ψ(x)), acting faithfully on the points of M (g • x). An isometry preserves the causal type of tangent vectors (isTimelike_mfderiv_iff), but it may reverse the time orientation. The isometries "connected to the identity" of Axiom 5 are the subgroup identityComponent, and those that also preserve the time orientation are orientedIdentityComponent.

Implementation note: the diffeomorphism is Mathlib's Diffeomorph, so smoothness of φ and φ⁻¹ is built in, and dφ_x is the manifold derivative mfderiv.

Blueprint: lmm:isometry-preserves-classification (isometries are described in lmm:isometry-pullback-metric)

• toDiffeo : Diffeomorph M.model M.model M.Carrier M.Carrier ↑⊤

  The diffeomorphism φ : M → M.

• preserves (x : M.Carrier) (v w : TangentSpace M.model x) : ((M.val (self.toDiffeo x)) ((mfderiv% ⇑self.toDiffeo x) v)) ((mfderiv% ⇑self.toDiffeo x) w) = ((M.val x) v) w

  φ preserves the metric: g_(φ(x))(dφ_x v, dφ_x w) = g_x(v, w), with dφ_x the manifold derivative mfderiv.

theorem Physicslib4.Spacetime.Isometry.ext_iff {M : Spacetime} {x y : M.Isometry} : x = y ↔ x.toDiffeo = y.toDiffeo

theorem Physicslib4.Spacetime.Isometry.ext {M : Spacetime} {x y : M.Isometry} (toDiffeo : x.toDiffeo = y.toDiffeo) : x = y

@[instance_reducible]

noncomputable instance Physicslib4.Spacetime.Isometry.instGroup {M : Spacetime} : Group M.Isometry

Equations

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

@[instance_reducible]

noncomputable instance Physicslib4.Spacetime.Isometry.instMulActionCarrier {M : Spacetime} : MulAction M.Isometry M.Carrier

The action of the isometry group on spacetime points, by applying the underlying diffeomorphism.

Equations

• Physicslib4.Spacetime.Isometry.instMulActionCarrier = { smul := fun (g : M.Isometry) (x : M.Carrier) => g.toDiffeo x, mul_smul := ⋯, one_smul := ⋯ }

@[simp]

theorem Physicslib4.Spacetime.Isometry.smul_def {M : Spacetime} (g : M.Isometry) (x : M.Carrier) : g • x = g.toDiffeo x

instance Physicslib4.Spacetime.Isometry.instFaithfulSMulCarrier {M : Spacetime} : FaithfulSMul M.Isometry M.Carrier

The isometry group acts faithfully on the spacetime: an isometry is determined by its action on points.

Invariance of the causal classification

An isometry preserves the metric square of a tangent vector, hence preserves the timelike/null/spacelike classification. These are the basic facts linking the isometry group to the causal structure underlying Axiom 5.

theorem Physicslib4.Spacetime.Isometry.preserves_self {M : Spacetime} (g : M.Isometry) (x : M.Carrier) (v : TangentSpace M.model x) : ((M.val (g.toDiffeo x)) ((mfderiv% ⇑g.toDiffeo x) v)) ((mfderiv% ⇑g.toDiffeo x) v) = ((M.val x) v) v

An isometry preserves the metric square g(v,v) of a tangent vector.

theorem Physicslib4.Spacetime.Isometry.isTimelike_mfderiv_iff {M : Spacetime} (g : M.Isometry) (x : M.Carrier) (v : TangentSpace M.model x) : M.IsTimelike ((mfderiv% ⇑g.toDiffeo x) v) ↔ M.IsTimelike v

An isometry preserves timelike vectors.

theorem Physicslib4.Spacetime.Isometry.isNull_mfderiv_iff {M : Spacetime} (g : M.Isometry) (x : M.Carrier) (v : TangentSpace M.model x) : M.IsNull ((mfderiv% ⇑g.toDiffeo x) v) ↔ M.IsNull v

An isometry preserves null vectors.

theorem Physicslib4.Spacetime.Isometry.isSpacelike_mfderiv_iff {M : Spacetime} (g : M.Isometry) (x : M.Carrier) (v : TangentSpace M.model x) : M.IsSpacelike ((mfderiv% ⇑g.toDiffeo x) v) ↔ M.IsSpacelike v

An isometry preserves spacelike vectors.