Physicslib4.AQFT.HaagKastlerCurved.IsometricCovariance

Axiom 5 (Isometric Covariance), curved spacetime #

This file formalises the blueprint declaration def:isometric-covariance-in-curved-spacetime (Axiom 5 of the Haag-Kastler axioms on a Lorentzian spacetime, Chapter 10 (sections/sec10/haag-kastler-axioms-in-curved-spacetime) of the AQFT-in-Lean blueprint):

A member Ο† of the group of isometries of M connected to the identity acts on π”˜(𝐁) via a unital *-isomorphism Ξ±_Ο† : π”˜(𝐁) β†’ π”˜(Ο†(𝐁)), where Ο†(𝐁) is the image of the basis set. The action satisfies (1) Ξ±_πŸ™ = id, (2) Ξ±_{Ο†'Β·Ο†} = Ξ±_{Ο†'} ∘ Ξ±_Ο†, and (3) it commutes with the isotony monomorphism i (Axiom 2).

Main definitions #

Modelling notes #

source
def Physicslib4.AQFT.HaagKastlerCurved.IsometricCovariance {M : LorentzianSpacetime} (U : LocalNet M) (i : Isotony U) :
Prop

Axiom 5 in curved spacetime (isometric covariance): the isometries connected to the identity act on the net, compatibly with isotony.

In curved spacetime the PoincarΓ© group of the Minkowski axioms is replaced by the symmetries the spacetime actually has: the group M.Isom of isometries of M connected to the identity. A generic spacetime has no isometries other than the identity, and then the axiom says little. The axiom asks for a unital *-isomorphism Ξ±_Ο† : π”˜(B) β†’ π”˜(Ο†(B)) for every such isometry Ο† and every region B, where Ο†(B) is the image of B under Ο†, such that

  1. Ξ±_1 is the identity;
  2. Ξ±_(Ο†'Ο†) = Ξ±_Ο†' ∘ Ξ±_Ο†; and
  3. Ξ±_Ο† commutes with the isotony family i of Axiom 2: whenever B₁ βŠ† Bβ‚‚ are basis sets, Ξ±_Ο† ∘ i(B₁, Bβ‚‚) = i(Ο†(B₁), Ο†(Bβ‚‚)) ∘ Ξ±_Ο†.

In condition 3, Ο†(B₁) and Ο†(Bβ‚‚) are basis sets with Ο†(B₁) βŠ† Ο†(Bβ‚‚) because isometries preserve basis sets (the interface field LorentzianSpacetime.isBasisSet_smul) and images preserve inclusions (Set.smul_set_mono), so no further hypothesis is needed. The predicate takes the isotony family as a parameter, so the action respects the net's own embeddings. HaagKastlerNet.covEquiv chooses the maps Ξ±_Ο†. There is no quasilocal algebra for them to act on; on a region fixed by Ο† they give automorphisms of its algebra (HaagKastlerNet.stabAut).

Implementation note: π”˜(1 β€’ B) and π”˜(B), and π”˜((Ο†'Ο†) β€’ B) and π”˜(Ο†' β€’ (Ο† β€’ B)), are different types that are equal only propositionally, so conditions 1 and 2 transport along those equalities (one_smul, mul_smul) with Eq.mp. For a geometric spacetime, M.Isom is the oriented identity component of its isometry group (toAbstractIdentityComponent).

Blueprint: def:isometric-covariance-in-curved-spacetime

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