Axiom 2: Isotony

This file formalises the blueprint declaration def:isotony (Axiom 2 of the "sharpened" Haag-Kastler axioms, section 10.3 of the AQFT-in-Lean blueprint):

If 𝐁₁ ⊆ 𝐁₂ (basis sets of the Alexandrov topology) then the inclusion induces a unital *-monomorphism 𝔘(𝐁₁) ↪ 𝔘(𝐁₂) between the corresponding local algebras.

Main definitions

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

Modelling notes

• The blueprint statement is the existence of an injective unital *-homomorphism for every inclusion of basis sets. Mathlib's StarAlgHom ℂ A B is unital by virtue of preserving the Algebra ℂ-structure (and in particular 1), so requiring a StarAlgHom together with Function.Injective captures the blueprint's "unital *-monomorphism".

• We keep the basis-set restriction explicit: Axiom 2 only mentions basis sets of the Alexandrov topology, so the quantifier ranges over B₁, B₂ satisfying IsAlexandrovBasisSet.

def Physicslib4.AQFT.HaagKastler.Isotony (U : LocalNet) : Prop

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

Blueprint reference: def:isotony.

Equations

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

theorem Physicslib4.AQFT.HaagKastler.exists_injective_self (U : LocalNet) {B : Set StandardMinkowskiSpacetime.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.HaagKastler.Isotony.trans {U : LocalNet} (h : Isotony U) ⦃B₁ B₂ B₃ : Set StandardMinkowskiSpacetime.Carrier⦄ (hB₁ : IsAlexandrovBasisSet B₁) (hB₂ : IsAlexandrovBasisSet B₂) (hB₃ : IsAlexandrovBasisSet 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₃).