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.

structure Physicslib4.AQFT.HaagKastler.Isotony (U : LocalNet) : Type u_1

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.

The family is chosen data, not an existence statement: the identity and composition laws below are equations between the maps themselves, so there is nothing to state unless the maps are fixed. An axiom of the form "for each inclusion there exists some monomorphism" cannot express functoriality at all.

map_self and map_comp say exactly that B ↦ 𝔘(B) is a functor on the inclusion order of basis sets. They are required rather than derived because they constrain the net's chosen embeddings, not the spacetime. Their payoff is that the local algebras form a genuine directed system, which is what gives the quasilocal algebra (def:quasilocal-algebra) its algebra structure.

• map ⦃B₁ B₂ : Set StandardMinkowskiSpacetime.Carrier⦄ : IsAlexandrovBasisSet B₁ → IsAlexandrovBasisSet B₂ → B₁ ⊆ B₂ → U.algebra B₁ →⋆ₐ[ℂ] U.algebra B₂

  The chosen unital *-monomorphism implementing each inclusion of basis sets. This is data, which is what makes the two laws below statable.

• injective ⦃B₁ B₂ : Set StandardMinkowskiSpacetime.Carrier⦄ (h₁ : IsAlexandrovBasisSet B₁) (h₂ : IsAlexandrovBasisSet B₂) (h : B₁ ⊆ B₂) : Function.Injective ⇑(self.map h₁ h₂ h)

  Each chosen embedding is injective, i.e. a monomorphism.

• map_self ⦃B : Set StandardMinkowskiSpacetime.Carrier⦄ (h : IsAlexandrovBasisSet B) : self.map h h ⋯ = StarAlgHom.id ℂ (U.algebra B)

  Identity law. The embedding along B ⊆ B is the identity.

• map_comp ⦃B₁ B₂ B₃ : Set StandardMinkowskiSpacetime.Carrier⦄ (h₁ : IsAlexandrovBasisSet B₁) (h₂ : IsAlexandrovBasisSet B₂) (h₃ : IsAlexandrovBasisSet B₃) (h₁₂ : B₁ ⊆ B₂) (h₂₃ : B₂ ⊆ B₃) : (self.map h₂ h₃ h₂₃).comp (self.map h₁ h₂ h₁₂) = self.map h₁ h₃ ⋯

  Composition law. The embedding along B₁ ⊆ B₃ factors through any intermediate B₂.

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