Documentation

Physicslib4.AQFT.HaagKastlerCurved.IdentityComponent

Bridging via the identity-component isometry group #

This file provides the variant of the concrete-to-abstract bridge (Physicslib4.Spacetime.LorentzianSpacetime.toAbstract) that instantiates the abstract interface's isometry group Isom with the identity component of the isometry group, matching the blueprint's "isometries connected to the identity" in Axiom 5 (def:isometric-covariance-in-curved-spacetime).

Main definitions #

Modelling notes #

The isometry group is a topological group under the (map, inverse)-induced topology (see Physicslib4/Spacetime/IsometryTopology.lean), so the identity-component subgroup is unconditional and this bridge yields the abstract interface with Isom the genuine identity-component subgroup (isometries connected to the identity).

source
noncomputable def Physicslib4.Spacetime.LorentzianSpacetime.toAbstractIdentityComponent (L : LorentzianSpacetime) :
AQFT.HaagKastlerCurved.LorentzianSpacetime

The abstract Haag-Kastler interface induced by a concrete Lorentzian spacetime, with the isometry group taken to be the oriented identity component (identity-component isometries that also preserve the future orientation), as in Axiom 5. Using the oriented component makes basis-set preservation φ(𝐁) a theorem (toAbstractIdentityComponent_isBasisSet_smul) rather than an unprovable consequence of the bare (C⁰) group topology.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem Physicslib4.Spacetime.LorentzianSpacetime.toAbstractIdentityComponent_Carrier (L : LorentzianSpacetime) :
    L.toAbstractIdentityComponent.Carrier = L.Carrier
    source
    @[simp]
    theorem Physicslib4.Spacetime.LorentzianSpacetime.toAbstractIdentityComponent_IsBasisSet (L : LorentzianSpacetime) :
    L.toAbstractIdentityComponent.IsBasisSet = L.IsBasisSet
    source
    @[simp]
    theorem Physicslib4.Spacetime.LorentzianSpacetime.toAbstractIdentityComponent_Isom (L : LorentzianSpacetime) :
    L.toAbstractIdentityComponent.Isom = ↥(Isometry.orientedIdentityComponent L.toSpacetime L.timeOrientation)

    The abstract isometry group of the bridge is, definitionally, the oriented identity component. Exposed as a simp lemma so abstract-interface statements can be rewritten to the concrete subgroup.

    source
    @[implicit_reducible]
    noncomputable instance Physicslib4.Spacetime.LorentzianSpacetime.instTopologicalSpaceToAbstractIsom (L : LorentzianSpacetime) :
    TopologicalSpace L.toAbstract.Isom

    The abstract isometry group of the toAbstract bridge inherits the topological-group topology of the concrete isometry group. This discharges the [TopologicalSpace M.Isom] hypothesis of the curved covariance/KMS results (e.g. the strongly continuous stabilizer GNS unitary) automatically for a net over a concrete Lorentzian spacetime — no explicit topology argument is needed.

    Equations
    • One or more equations did not get rendered due to their size.
    source
    @[implicit_reducible]
    noncomputable instance Physicslib4.Spacetime.LorentzianSpacetime.instTopologicalSpaceToAbstractIdentityComponentIsom (L : LorentzianSpacetime) :
    TopologicalSpace L.toAbstractIdentityComponent.Isom

    The abstract isometry group of the toAbstractIdentityComponent bridge inherits the subspace topology of the oriented identity-component subgroup, discharging [TopologicalSpace M.Isom] automatically over a concrete spacetime.

    Equations
    • One or more equations did not get rendered due to their size.
    source
    theorem Physicslib4.Spacetime.LorentzianSpacetime.toAbstractIdentityComponent_isBasisSet_smul (L : LorentzianSpacetime) (φ : L.toAbstractIdentityComponent.Isom) {B : Set L.toAbstractIdentityComponent.Carrier} (hB : L.toAbstractIdentityComponent.IsBasisSet B) :
    L.toAbstractIdentityComponent.IsBasisSet (φ • B)

    Axiom 5 basis-set preservation, stated over the abstract bridge. Every isometry φ of the abstract spacetime carries Alexandrov-basis sets to basis sets: φ(𝐁) = φ • 𝐁 is again a basis set. This is what makes the Axiom 5 action 𝔘(𝐁) → 𝔘(φ(𝐁)) well-defined.

    source
    theorem Physicslib4.Spacetime.LorentzianSpacetime.identityComponent_faithfulSMul (L : LorentzianSpacetime) :
    FaithfulSMul (↥(Isometry.identityComponent L.toSpacetime)) L.toSpacetime.Carrier

    The identity-component isometry group acts faithfully on the spacetime: an identity-component isometry is determined by its action on points. (Inherited from the faithful action of the full isometry group.)

    source
    theorem Physicslib4.Spacetime.LorentzianSpacetime.isometricCovariance_trivial_identityComponent (L : LorentzianSpacetime) :
    AQFT.HaagKastlerCurved.IsometricCovariance (AQFT.HaagKastlerCurved.trivialLocalNet L.toAbstractIdentityComponent)

    Relating back to Axiom 5 over the concrete spacetime. The trivial net over the concrete Lorentzian spacetime — with Isom the genuine identity-component isometry group — satisfies isometric covariance (def:isometric-covariance-in-curved-spacetime).

    source
    theorem Physicslib4.Spacetime.LorentzianSpacetime.nonempty_haagKastlerNet_identityComponent (L : LorentzianSpacetime) :
    Nonempty (AQFT.HaagKastlerCurved.HaagKastlerNet L.toAbstractIdentityComponent)

    Over the concrete spacetime (with the identity-component isometry group), the full set of curved-spacetime Haag-Kastler axioms is jointly satisfiable.

    source
    theorem Physicslib4.AQFT.HaagKastlerCurved.HaagKastlerNet.commute_of_spacelike_mono_identityComponent {L : Spacetime.LorentzianSpacetime} (N : HaagKastlerNet L.toAbstractIdentityComponent) ⦃B₁ B₂ B₁' B₂' B : Set L.toAbstractIdentityComponent.Carrier⦄ (hB₁' : L.toAbstractIdentityComponent.IsBasisSet B₁') (hB₂' : L.toAbstractIdentityComponent.IsBasisSet B₂') (hB : L.toAbstractIdentityComponent.IsBasisSet B) (hs : L.toAbstractIdentityComponent.IsCompletelySpacelike B₁ B₂) (hsub₁ : B₁' ⊆ B₁) (hsub₂ : B₂' ⊆ B₂) (h₁ : B₁ ⊆ B) (h₂ : B₂ ⊆ B) (a : N.algebra B₁') (b : N.algebra B₂') :
    Commute ((N.commIsotony hB₁' hB ⋯) a) ((N.commIsotony hB₂' hB ⋯) b)

    Monotonicity of local commutativity over the identity-component bridge. The identity-component analogue of commute_of_spacelike_mono_geometric: for a Haag-Kastler net over the abstract interface induced by a concrete Lorentzian spacetime L with Isom the oriented identity component, the spacelike-monotonicity hypothesis is discharged automatically by Spacetime.LorentzianSpacetime.isCompletelySpacelike_mono (the bridge's IsCompletelySpacelike is, definitionally, that of L). This is the physically faithful form: the symmetry group is the isometries connected to the identity, as in Axiom 5.