Axiom 2 (Isotony), curved spacetime

This file formalises the blueprint declaration def:isotony-in-curved-spacetime (Axiom 2 of the Haag-Kastler axioms on a Lorentzian spacetime, Chapter 10 (sections/sec10/10-4_haag-kastler-axioms-in-curved-spacetime) of the AQFT-in-Lean blueprint):

If 𝐁₁ ⊆ 𝐁₂ (Alexandrov-basis sets) then the inclusion induces a unital *-monomorphism i : 𝔘(𝐁₁) ↪ 𝔘(𝐁₂).

Main definitions

• Physicslib4.AQFT.HaagKastlerCurved.Isotony: a Prop-valued predicate on a LocalNet M asserting Axiom 2.

This is the verbatim curved analogue of the Minkowski Isotony (def:isotony); only the carrier and basis predicate change to the abstract interface M.

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

Axiom 2 (Isotony), curved spacetime. A local net U on a Lorentzian spacetime M satisfies isotony if every inclusion B₁ ⊆ B₂ between Alexandrov-basis sets is implemented by a unital *-monomorphism 𝔘(B₁) ↪ 𝔘(B₂).

Blueprint reference: def:isotony-in-curved-spacetime.

Equations

• Physicslib4.AQFT.HaagKastlerCurved.Isotony U = ∀ ⦃B₁ B₂ : Set M.Carrier⦄, M.IsBasisSet B₁ → M.IsBasisSet B₂ → B₁ ⊆ B₂ → ∃ (φ : U.algebra B₁ →⋆ₐ[ℂ] U.algebra B₂), Function.Injective ⇑φ

theorem Physicslib4.AQFT.HaagKastlerCurved.exists_injective_self {M : LorentzianSpacetime} (U : LocalNet M) {B : Set M.Carrier} : ∃ (φ : U.algebra B →⋆ₐ[ℂ] U.algebra B), Function.Injective ⇑φ

Isotony is reflexive. Every Alexandrov-basis set embeds into itself via the identity unital *-monomorphism, independently of any isotony hypothesis.

theorem Physicslib4.AQFT.HaagKastlerCurved.Isotony.trans {M : LorentzianSpacetime} {U : LocalNet M} (h : Isotony U) ⦃B₁ B₂ B₃ : Set M.Carrier⦄ (hB₁ : M.IsBasisSet B₁) (hB₂ : M.IsBasisSet B₂) (hB₃ : M.IsBasisSet B₃) (h₁₂ : B₁ ⊆ B₂) (h₂₃ : B₂ ⊆ B₃) : ∃ (φ : U.algebra B₁ →⋆ₐ[ℂ] U.algebra B₃), Function.Injective ⇑φ

Isotony is transitive. Given inclusions B₁ ⊆ B₂ ⊆ B₃ of Alexandrov-basis sets, the isotony embeddings compose to a unital *-monomorphism 𝔘(B₁) ↪ 𝔘(B₃).