Physicslib4.Spacetime.IsometryTopology

Topology on the isometry group and the identity component

This file makes the isometry group Physicslib4.Spacetime.Isometry M a topological group and carves out the identity-component subgroup — the isometries "connected to the identity" used by Axiom 5 of the curved-spacetime Haag-Kastler axioms (def:isometric-covariance-in-curved-spacetime).

Main definitions / results

• TopologicalSpace (Isometry M): the topology induced from the inclusion g ↦ (g, g⁻¹) into C(M, M) × C(M, M) (the standard topological-group topology on a transformation group).
• IsTopologicalGroup (Isometry M).
• Physicslib4.Spacetime.Isometry.identityComponent: the identity-component subgroup Subgroup.connectedComponentOfOne (Isometry M).

Modelling notes

Taking the bare compact-open topology (induced from the forward map alone) does not obviously make inversion continuous (the Arens problem). The standard remedy, used here, is to induce the topology from both the map and its inverse, g ↦ (g, g⁻¹) ∈ C(M,M) × C(M,M):

• Inversion g ↦ g⁻¹ corresponds to swapping the two coordinates, hence is continuous by construction.
• Multiplication is continuous because a finite-dimensional manifold M is locally compact (ChartedSpace.locallyCompactSpace), so composition C(M,M) × C(M,M) → C(M,M) is continuous (ContinuousMap.continuous_comp').

This is exactly the Arens-style construction, and it discharges IsTopologicalGroup outright, so the identity-component subgroup is unconditional.

instance Physicslib4.Spacetime.Isometry.instLocallyCompactSpace {M : Spacetime} : LocallyCompactSpace M.Carrier

A finite-dimensional manifold is locally compact, since its model space ℝ⁴ is.

noncomputable def Physicslib4.Spacetime.Isometry.toContinuousMap {M : Spacetime} (g : M.Isometry) : C(M.Carrier, M.Carrier)

An isometry as a continuous self-map of the spacetime (its underlying diffeomorphism, which is continuous).

Equations

• g.toContinuousMap = { toFun := ⇑g.toDiffeo, continuous_toFun := ⋯ }

noncomputable def Physicslib4.Spacetime.Isometry.toProd {M : Spacetime} (g : M.Isometry) : C(M.Carrier, M.Carrier) × C(M.Carrier, M.Carrier)

An isometry as the pair of its underlying continuous self-map and the map of its inverse. The group topology is induced from this inclusion into C(M,M) × C(M,M).

Equations

• g.toProd = (g.toContinuousMap, g⁻¹.toContinuousMap)

@[instance_reducible]

noncomputable instance Physicslib4.Spacetime.Isometry.instTopologicalSpace {M : Spacetime} : TopologicalSpace M.Isometry

The topological-group topology on the isometry group, induced from the inclusion g ↦ (g, g⁻¹) into C(M,M) × C(M,M).

Equations

• Physicslib4.Spacetime.Isometry.instTopologicalSpace = TopologicalSpace.induced Physicslib4.Spacetime.Isometry.toProd inferInstance

theorem Physicslib4.Spacetime.Isometry.continuous_toProd {M : Spacetime} : Continuous toProd

theorem Physicslib4.Spacetime.Isometry.continuous_toContinuousMap {M : Spacetime} : Continuous toContinuousMap

theorem Physicslib4.Spacetime.Isometry.continuous_toContinuousMap_inv {M : Spacetime} : Continuous fun (g : M.Isometry) => g⁻¹.toContinuousMap

theorem Physicslib4.Spacetime.Isometry.toContinuousMap_mul {M : Spacetime} (a b : M.Isometry) : (a * b).toContinuousMap = a.toContinuousMap.comp b.toContinuousMap

The forward map of a product is the composition of the forward maps.

instance Physicslib4.Spacetime.Isometry.instContinuousInv {M : Spacetime} : ContinuousInv M.Isometry

instance Physicslib4.Spacetime.Isometry.instContinuousMul {M : Spacetime} : ContinuousMul M.Isometry

instance Physicslib4.Spacetime.Isometry.instIsTopologicalGroup {M : Spacetime} : IsTopologicalGroup M.Isometry

instance Physicslib4.Spacetime.Isometry.instContinuousSMul {M : Spacetime} : ContinuousSMul M.Isometry M.Carrier

The isometry group acts continuously on spacetime. The action (g, x) ↦ g • x = g.toDiffeo x is jointly continuous: it factors as the evaluation (g, x) ↦ (toContinuousMap g) x, and evaluation C(M,M) × M → M is continuous since M is locally compact (Continuous.eval). This is the standard continuity companion to the topological-group structure, used by any continuity argument over the isometry group.

noncomputable def Physicslib4.Spacetime.Isometry.identityComponent (M : Spacetime) : Subgroup M.Isometry

The identity component of the isometry group: the connected component of the identity, for the compact-open group topology.

These are the isometries "connected to the identity" of Axiom 5 in curved spacetime. For Minkowski spacetime they are the proper orthochronous Poincaré transformations, while parity and time reversal lie in other components (a standard fact, not formalised here). Every isometry in the identity component preserves the time orientation, but the proof needs a Myers–Steenrod-type rigidity theorem that Mathlib does not provide; the axioms therefore use orientedIdentityComponent, which is the same group with orientation preservation built into its definition.

Implementation note: the group topology is induced by g ↦ (g, g⁻¹) into C(M, M) × C(M, M), with the compact-open topology on each factor; using both g and g⁻¹ makes inversion continuous, and local compactness of M makes composition continuous, so IsTopologicalGroup holds and the connected component of 1 is a subgroup (Subgroup.connectedComponentOfOne).

Equations

• Physicslib4.Spacetime.Isometry.identityComponent M = Subgroup.connectedComponentOfOne M.Isometry