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)

@[implicit_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 subgroup of the isometry group: the isometries connected to the identity, formalising the group used in Axiom 5 (def:isometric-covariance-in-curved-spacetime). It is the connected component of 1, a (normal) subgroup of the topological group.

Equations

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