Physicslib4.AQFT.HaagKastlerCurved.IdentityComponent

The identity-component bridge: faithfulness and satisfiability

The concrete-to-abstract bridge Physicslib4.Spacetime.LorentzianSpacetime.toAbstractIdentityComponent (Physicslib4/AQFT/HaagKastlerCurved/Concrete.lean) instantiates the abstract interface's isometry group Isom with the oriented identity component of the isometry group, matching the blueprint's "isometries connected to the identity" in Axiom 5 (def:isometric-covariance-in-curved-spacetime). This file records that the identity component acts faithfully and that the curved Haag-Kastler axioms are jointly satisfiable over the bridge.

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.)

theorem Physicslib4.Spacetime.LorentzianSpacetime.isometricCovariance_trivial_identityComponent (L : LorentzianSpacetime) : AQFT.HaagKastlerCurved.IsometricCovariance (AQFT.HaagKastlerCurved.trivialLocalNet L.toAbstractIdentityComponent) (AQFT.HaagKastlerCurved.trivialLocalNetIsotony 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).

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

The curved-spacetime Haag–Kastler axioms are consistent over every geometric Lorentzian spacetime.

The group of Axiom 5 is that of toAbstractIdentityComponent, the isometries of L connected to the identity. The witness is the trivial net, which assigns ℂ to every region; the statement specialises Physicslib4.AQFT.HaagKastlerCurved.nonempty_haagKastlerNet to the interface of L.

Implementation note: the net has its algebras in universe 0, because the witness is built from ℂ, which lives in Type.

Blueprint: thrm:haag-kastler-net-in-curved-spacetime-nonempty