The quasilocal colimit: index type and directed system #
This file begins the construction of the quasilocal algebra from the net alone, as the directed colimit of the local algebras along the Axiom 2 isotony family, later completed. It supplies the two foundational ingredients that everything downstream needs:
- the index type of Alexandrov diamonds, ordered by inclusion, together with the
fact that it is directed (blueprint
lmm:alexandrov-diamonds-isDirected); - the isotony family as a
DirectedSystemin Mathlib's sense (blueprintlmm:isotony-directed-system).
Modelling notes #
Mathlib's DirectLimit API is indexed by a Preorder and takes the transition
maps in the shape f : ∀ i j (h : i ≤ j), T h, where T h is a FunLike type.
Isotony.map is indexed instead by subsets together with a proof of
IsAlexandrovBasisSet, so the index is packaged here as the subtype Diamond,
whose order is the inclusion order inherited from Set. IsAlexandrovBasisSet B
is by definition B ∈ Spacetime.alexandrovBasis .., so the geometry proved in
Physicslib4/Spacetime/MinkowskiDirected.lean applies to it unchanged.
The transition maps are kept as StarAlgHoms rather than bare functions, since
StarAlgHom is FunLike and satisfies the RingHomClass/StarHomClass/
AlgHomClass/LinearMapClass hypotheses under which DirectLimit carries its
Ring, StarRing, Algebra and StarModule structures.
The Alexandrov diamonds of standard Minkowski spacetime, as a type, ordered by inclusion. This is the index type of the directed system of local algebras.
Blueprint reference: lmm:alexandrov-diamonds-isDirected.
Equations
Instances For
The Alexandrov diamonds are directed under inclusion (set-level form):
any two basis diamonds are contained in a common one. This is the order-theoretic
repackaging of Physicslib4.Spacetime.alexandrovBasis_directed.
Blueprint reference: lmm:alexandrov-diamonds-isDirected.
The Alexandrov diamonds are directed under inclusion (subtype form).
This is the instance the colimit construction consumes, so that downstream nodes
can cite an instance instead of restating a ∀∃ statement.
Blueprint reference: lmm:alexandrov-diamonds-isDirected.
The transition maps of the directed system of local algebras, in the
Mathlib's DirectLimit expects: explicit index binders, with the map itself a
StarAlgHom.
Equations
- Physicslib4.AQFT.HaagKastler.transitionHom U i D₁ D₂ h = i.map ⋯ ⋯ h
Instances For
The isotony family is a directed system. Mathlib's DirectedSystem is a
two-field class whose fields are exactly Axiom 2's identity and composition laws,
so the instance is built by supplying Isotony.map_self and Isotony.map_comp.
Blueprint reference: lmm:isotony-directed-system.
The colimit of the local algebras along the Axiom 2 isotony family: the
directed colimit lim_{→ 𝐁} 𝔘(𝐁), taken over the Alexandrov diamonds ordered by
inclusion.
Mathlib supplies its algebraic structure (Ring, StarRing, Algebra ℂ,
StarModule ℂ) but puts no norm on any colimit; that is built by hand below.
Equations
Instances For
The isotony embeddings are isometric. A *-homomorphism of complex
C*-algebras is isometric as soon as it is injective, and Axiom 2(a) supplies
injectivity. This is what makes the colimit norm well defined.
Blueprint reference: lmm:quasilocal-colimit-norm-well-defined.
The colimit norm. ‖[a]‖ := ‖a‖ for any representative a. It is well
defined precisely because the transition maps are isometric
(norm_transitionHom): the universal property of the colimit takes that isometry
as its compatibility obligation.
Blueprint reference: lmm:quasilocal-colimit-norm-well-defined.
Equations
- Physicslib4.AQFT.HaagKastler.colimitNorm U i = DirectLimit.lift (Physicslib4.AQFT.HaagKastler.transitionHom U i) (fun (x : Physicslib4.AQFT.HaagKastler.Diamond) (a : U.algebra ↑x) => ‖a‖) ⋯
Instances For
The colimit norm of a class is the norm of any representative: the defining
equation of colimitNorm, and the reason the node is stated as a
well-definedness claim.
Common representatives for two colimit elements. Any two elements of the colimit are the classes of two elements of one and the same diamond. This is what lets the binary algebraic and norm identities be checked on representatives, and it is available exactly because the index type is directed.
Blueprint reference: lmm:quasilocal-colimit-common-representatives.
There is at least one Alexandrov diamond. Every set of the form
I⁺(p) ∩ I⁻(q) is a basis element, so the index type is inhabited.
This is needed as an instance, not merely as a fact: the colimit's Zero and
One are built by choosing a component (DirectLimit.map₀ picks
Classical.arbitrary ι), so Mathlib's algebraic instances on the colimit all
carry [Nonempty ι]. Without it none of Ring, Module ℂ or Algebra ℂ
resolves on the colimit.
The colimit norm is a ring norm. Its five RingNorm fields are the first
five clauses of the blueprint node: map_zero' and neg' come from
AddGroupSeminorm, add_le' and mul_le' are subadditivity and
submultiplicativity, and eq_zero_of_map_eq_zero' is positive definiteness.
Each is checked on common representatives (exists_common_representatives) and
transported by colimitNorm_mk. Positive definiteness is the only clause with
real content: it is where injectivity of the canonical maps into the colimit is
spent, via DirectLimit.mk_injective fed by Axiom 2(a).
Blueprint reference: lmm:quasilocal-colimit-norm-axioms.
Equations
- Physicslib4.AQFT.HaagKastler.colimitRingNorm U i = { toFun := Physicslib4.AQFT.HaagKastler.colimitNorm U i, map_zero' := ⋯, add_le' := ⋯, neg' := ⋯, mul_le' := ⋯, eq_zero_of_map_eq_zero' := ⋯ }
Instances For
The colimit as a NormedRing, obtained from colimitRingNorm.
RingNorm.toNormedRing packages the five clauses just checked into the norm and
metric structure that everything downstream consumes.
Absolute homogeneity of the colimit norm, ‖c • x‖ = ‖c‖ * ‖x‖. It is stated
separately from the RingNorm fields because a RingNorm knows nothing about the
scalars; its role is to supply the norm_smul_le field of NormedSpace ℂ over
the NormedRing structure just obtained.
Blueprint reference: lmm:quasilocal-colimit-norm-axioms.
The NormedRing norm on the colimit is the norm of colimitNorm, by
construction. This is the bridge that lets the representative-level lemmas above
be used against the ambient ‖·‖.
The colimit is a normed algebra over ℂ. Together with the StarRing and
StarModule ℂ instances, which Mathlib's DirectLimit supplies by typeclass
inference from the corresponding structures on each local algebra, this is the
normed *-algebra structure the blueprint node asserts.
NormedAlgebra has no field beyond Algebra other than norm_smul_le, which is
absolute homogeneity (colimitNorm_smul) weakened to an inequality. It is stated
in the NormedAlgebra form because that is what the completion hypotheses consume
downstream.
Blueprint reference: lmm:quasilocal-union-normed-star-algebra.
Equations
- Physicslib4.AQFT.HaagKastler.colimitNormedAlgebra U i = { toAlgebra := DirectLimit.instAlgebra, norm_smul_le := ⋯ }
The colimit satisfies the C*-inequality ‖x‖ * ‖x‖ ≤ ‖x⋆ * x‖.
Only the inequality is asserted, because it is literally the single field
norm_mul_self_le of Mathlib's CStarRing, so establishing it is establishing
the instance. The familiar equality ‖x⋆ * x‖ = ‖x‖ ^ 2 then comes back free from
CStarRing.norm_star_mul_self, and ‖x⋆‖ = ‖x‖ from
CStarRing.to_normedStarGroup; neither needs a proof of its own.
Note CStarRing does not require completeness, which is why this holds on the
colimit even though the colimit is in general not a C*-algebra. Only one
element is involved, so no directedness is needed: take a representative a, note
x⋆ * x has representative a⋆ * a in the same local algebra, and apply the
CStarRing instance there.
Blueprint reference: lmm:quasilocal-colimit-cstar-identity.
The quasilocal algebra built from the net: the completion of the colimit of the local algebras along the Axiom 2 isotony family.
This is the object the blueprint claims exists, constructed from the net alone, with no ambient C*-algebra presupposed anywhere.
Equations
Instances For
The completion of the quasilocal colimit is a C*-algebra
(lmm:quasilocal-completion-cstar).
This is the general completion theory of Physicslib4/Analysis/CStarCompletion.lean
instantiated at the colimit. Its five standing hypotheses — NormedRing,
StarRing, NormedAlgebra ℂ, StarModule ℂ and CStarRing — are exactly what
the colimit development above establishes, so the C*-algebra structure follows by
instance resolution with nothing further to prove.
In particular isometry of the involution is not a separate obligation: it comes
from the C*-inequality through CStarRing.to_normedStarGroup.
The colimit insertion as a *-algebra homomorphism
(lmm:quasilocal-embedding).
Mathlib's canonical map from a component into the colimit,
DirectLimit.Algebra.of, is bundled only as an AlgHom; there is no
StarAlgHom-valued version of it, so the one missing StarAlgHom field,
map_star', is supplied by hand. It holds by definition of the involution on the
colimit, DirectLimit.star_def, which sends the class of ⟨D, a⟩ to the class
of ⟨D, a⋆⟩.
Equations
Instances For
Applying colimitStarOf to an element of a local algebra gives its class in
the colimit.
The canonical embedding into the quasilocal algebra
(lmm:quasilocal-embedding).
For each Alexandrov diamond D, the composite ι_D := η ∘ ρ of the colimit
insertion colimitStarOf with the completion coercion
Physicslib4.coeStarAlgHom is a unital *-algebra homomorphism over ℂ, both
factors being bundled StarAlgHoms.
Equations
Instances For
Applying quasilocalEmbedding to an element of a local algebra gives the
completion class of its class in the colimit.
The colimit is the union of the images of its insertions
(lmm:quasilocal-colimit-union-of-insertions).
Every element of the colimit is the class of a pair ⟨D, a⟩ (DirectLimit.exists_eq_mk),
hence lies in the range of the insertion colimitStarOf U i D. This is what
identifies the range of the insertions with the whole colimit, and is the pivot of
the density argument.
The canonical embeddings form a cocone (lmm:quasilocal-embedding-cocone).
For diamonds D₁ ≤ D₂, embedding after transporting along isotony equals
embedding directly: ι_{D₂} ∘ i_{D₁ D₂} = ι_{D₁}. This is the cocone condition
that makes the embeddings well defined on the colimit.
The identity for the colimit insertions is DirectLimit.mk_apply, Mathlib's
compatibility of insertions with transition maps; applying the completion coercion
η to both sides is a congrArg.
The Images of the Canonical Embeddings are Dense (lmm:quasilocal-embeddings-dense).
The union of the ranges of the quasilocal embeddings ι_B, taken over all
Alexandrov-basis diamonds, is dense in the completion of the colimit: this is
the density clause the quasilocal algebra requires. The range of the completion
coercion η is dense by UniformSpace.Completion.denseRange_coe, and every
colimit element lies in the range of some insertion
(exists_eq_colimitStarOf), so the range of η is contained in the displayed
union; density transfers by Dense.mono.
It is stated in the basis-set-indexed form — pairs ⟨B, hB⟩ of a set and a proof
that it is an Alexandrov basis set — on purpose, so that the statement matches, verbatim, the
dense_range field of QuasilocalAlgebra, which this lemma discharges.
The colimit insertion is injective (lmm:quasilocal-embedding-injective).
Every transition map of the directed system is injective by Axiom 2(a)
(Isotony.injective), so Mathlib's DirectLimit.mk_injective gives injectivity
of the insertion of each diamond into the colimit. This is the step flagged in
the blueprint as the place where Axiom 2(a) is spent.