- Boxes
- definitions
- Ellipses
- theorems and lemmas
- Blue border
- the statement of this result is ready to be formalized; all prerequisites are done
- Orange border
- the statement of this result is not ready to be formalized; the blueprint needs more work
- Blue background
- the proof of this result is ready to be formalized; all prerequisites are done
- Green border
- the statement of this result is formalized
- Green background
- the proof of this result is formalized
- Dark green background
- the proof of this result and all its ancestors are formalized
- Dark green border
- this is in Mathlib
Let \(\mathfrak {U}_1\) be a C*-subalgebra of the C*-algebra \(\mathfrak {U}_2\). If \(a\) is an element of \(\mathfrak {U}_1\), then the spectrum \(\sigma _{\mathfrak {U}_1}(a)\) of \(a\) when viewed as an element of \(\mathfrak {U}_1\) is the same as the spectrum \(\sigma _{\mathfrak {U}_2}(a)\) of \(a\) when viewed as an element of \(\mathfrak {U}_2\)*
If \(\mathfrak {U}\) is a *-algebra and there exists a norm on \(\mathfrak {U}\) with the C*-norm property and with respect to which \(\mathfrak {U}\) is closed, then this norm is unique.
Let \(\mathcal{H}\) be a Hilbert space and \(\mathcal{S}\) a *-subalgebra of \(\mathcal{B}(\mathcal{H})\) that contains the identity. Then \(\mathcal{S}\) is strongly dense in \(\mathcal{S}''\).
Let \(V_1\) be a normed space and \(V_2\) a Banach space. Suppose \(W\) is a dense subspace of \(V_1\) and \(T: W \rightarrow V_2\) is a bounded linear map. Then there exists a unique bounded linear map \(\widetilde{T}: V_1 \rightarrow V_2\) such that \(\widetilde{T}|_W = T\). Furthermore, the norm of \(\widetilde{T}\) equals the norm of \(T\).
A non-zero Abelian C*-algebra \(\mathcal{A}\) is primitive if and only if \(\mathcal{A} = \mathbb {C} \mathbf{1}\).
A smooth manifold \(M\) admits a smooth Lorentz metric if and only if it admits a smooth, nowhere-vanishing global vector field.
Consider an open subset \(\mathbf{O}\) of a smooth, connected, four dimensional Hausdorff manifold \(M\) that is equipped with a Lorentzian metric. \(\mathbf{O}\) is said to be causally convex if for every \(p\) and \(r\) in \(\mathbf{O}\) and \(q\) in \(M\) the existence of a future-directed, time-like curve from \(p\) to \(q\) and a future-directed, time-like curve from \(q\) to \(r\) implies that \(q\) is a member of \(\mathbf{O}\).
Consider a smooth, connected, four dimensional Hausdorff manifold \(M\) that is equipped with a Lorentzian metric. \(M\) is said to be strongly causal at \(p \in M\) if \(p\) has arbitrarily small causally convex neighborhoods. \(M\) is said to be strongly causal if \(M\) is strongly causal at every \(p \in M\).
The following three conditions on a smooth, connected, four dimensional manifold \(M\) with Hausdorff manifold topology are equivalent:
\(M\) is strongly causal;
the Alexandrov Topology agrees with the manifold topology;
the Alexandrov Topology is Hausdorff.
A Lorentzian spacetime is a smooth, connected, four dimensional manifold equipped with a smooth, nowhere-vanishing global vector field \(t^a\) and associated Lorentzian metric. In addition it is equipped with an associated Hausdorff Alexandrov topology.
For Lorentzian spacetime \(M\) the image \(\pi _\omega (a)\) of a self-adjoint member \(a\) of the local algebra \(\mathfrak {U}(\mathbf{B})\) under the GNS *-homomorphism \(\pi _\omega \) of a state \(\omega \) on \(\mathfrak {U}(\mathbf{B})\) is self-adjoint and thus corresponds to an “observable”. Any “observable” corresponding to such a self-adjoint \(\pi _\omega (a)\) is called a local observable.
For a spacetime \(M\) and \(p\) in \(M\) the set \(J^+(p) = \{ q \in M : p \prec q\} \) is called the causal future of \(p\). \(J^-(p) = \{ q \in M : q \prec p\} \) is called the causal past of \(p\). The causal future of a set \(S \subset M\) is the union of the causal future of each element of the set
The causal past of \(S\) is defined similarly
A causal trip is a curve which is piecewise a future-oriented, causal geodesic. (Note a causal geodesic is possibly degenerate.) A causal trip from \(p\) to \(q\) is a causal trip with past endpoint \(p\) and future endpoint \(q\). We write \(p \prec q\) if and only if there exists a causal trip from \(p\) to \(q\).
For a spacetime \(M\) and \(p\) in \(M\) the set \(I^+(p) = \{ q \in M : p \ll q\} \) is called the chronological future of \(p\). \(I^-(p) = \{ q \in M : q \ll p\} \) is called the chronological past of \(p\). The chronological future of a set \(S \subset M\) is the union of the chronological future of each element of the set
The chronological past of \(S\) is defined similarly
Consider two sets \(\mathbf{O}_1\) and \(\mathbf{O}_2\) in a spacetime. \(\mathbf{O}_1\) and \(\mathbf{O}_2\) are completely spacelike with respect to each other if every \(p_1\) in \(\mathbf{O}_1\) is spacelike related to every \(p_2\) in \(\mathbf{O}_2\).
A covariant quasilocal algebra bundles a Haag-Kastler net (64), a quasilocal algebra of that net (59), and a proof that the embeddings are covariance-compatible for every Lorentz transformation. On such data the quasilocal lift (67) exists for every \(L\) by 69, yielding the covariance action \(L \mapsto \beta _L\) on the quasilocal algebra; the trivial net provides an instance. This is the natural home for the covariance dynamics: the compatibility hypothesis of 69 becomes structural data rather than a side condition.
Given a Haag-Kastler net (64), a covariant family of local states assigns to every region \(\mathbf{B}\) a state \(\omega _{\mathbf{B}}\) on the local algebra \(\mathfrak {U}(\mathbf{B})\) such that, for every Lorentz transformation \(L\) and every \(a \in \mathfrak {U}(\mathbf{B})\), one has \(\omega _{\mathbf{B}}(a) = \omega _{L\cdot \mathbf{B}}(\alpha _L a)\), where \(\alpha _L\) is the covariance isomorphism of 63. The local states are thus intertwined by the Lorentz action.
Given a Haag-Kastler net on a Lorentzian spacetime (81), a covariant family of local states assigns to every region \(\mathbf{B}\) a state \(\omega _{\mathbf{B}}\) on \(\mathfrak {U}(\mathbf{B})\) such that, for every identity-component isometry \(\varphi \) and every \(a \in \mathfrak {U}(\mathbf{B})\), \(\omega _{\mathbf{B}}(a) = \omega _{\varphi (\mathbf{B})}(\alpha _\varphi a)\), where \(\alpha _\varphi \) is the covariance isomorphism of 80.
A curve is an equivalence class of paths equivalent under homeomorphisms of the parameter space. A smooth curve is an equivalence class of smooth paths equivalent under diffeomorphisms of the parameter space.
Let \(\mathcal{A}\) be an algebra represented by the bounded operators \(\pi (\mathcal{A})\) on the Hilbert space \(\mathcal{H}\). A vector \(\Omega \) in \(\mathcal{H}\) is said to be a cyclic vector if the set
is dense in \(\mathcal{H}\).
A point \(p\) in a spacetime \(M\) is the endpoint of a path \(\mu \) or its associated curve if it is a member of the image \(\mu (\partial \Sigma )\) of the boundary \(\partial \Sigma \) of the parameter space under \(\mu \). If \(\mu \) is a smooth path and its associated smooth curve is timelike and future-oriented, then an endpoint \(p\) is a past endpoint if it is the image under \(\mu \) of the lesser of the two boundary components of \(\partial \Sigma \). It is a future endpoint if it is the image under \(\mu \) of the greater of the two boundary components of \(\partial \Sigma \).
A future-oriented smooth curve is a smooth curve with a tangent vector that is future-pointing at every point. A past-oriented smooth curve is a smooth curve with a tangent vector that is past-pointing at every point.
For any \(p\) in a spacetime \(M\) a timelike tangent vector \(v \in TM|_p\) is future-pointing if \(g|_p(t,v)\) is negative and past-pointing if \(g|_p(t,v)\) is positive. A null tangent vector \(n \in TM|_p\) is future-pointing if it is the limit of future-pointing timelike tangent vectors and it is past-pointing if it is the limit of past-pointing timelike tangent vectors.
A Haag-Kastler net on Minkowski spacetime is the bundling of the data of 57 together with the properties of 58, 60, 62, and 63. In the Lean formalization this is a single structure whose fields are the assignment \(\mathbf{B} \mapsto \mathfrak {U}(\mathbf{B})\) and proofs that this assignment satisfies the four remaining axioms. Theorems about AQFT take an instance of this structure as a hypothesis and invoke each axiom as a projection.
A Haag-Kastler net in curved spacetime on a Lorentzian spacetime is the bundling of the data of 75 together with the properties of 76, 77, 79, and 80. In the Lean formalization this is a single structure whose fields are the assignment \(\mathbf{B} \mapsto \mathfrak {U}(\mathbf{B})\) and proofs that this assignment satisfies the four remaining axioms. Theorems about AQFT in curved spacetime take an instance of this structure as a hypothesis and invoke each axiom as a projection.
A state \(\omega \) on the quasilocal algebra of a covariant quasilocal algebra (71) is (Poincaré-)invariant if it is a fixed point of the dual covariance action: \(\omega (\beta _L a) = \omega (a)\) for every Lorentz transformation \(L\) and observable \(a\). This is the invariance condition of a vacuum state; further conditions (e.g. the spectrum condition) are imposed separately.
Let \(\mathbf{B}\) be any basis element of the Alexandrov topology on a Lorentzian spacetime \(M\), i.e. any set of the form \(I^+(p) \cap I^-(q)\).
A member \(\varphi \) of the group of isometries of \(M\) connected to the identity acts on \(\mathfrak {U}(\mathbf{B})\) as follows
where \(\varphi (\mathbf{B})\) is the image of the basis element \(\mathbf{B}\) under the isometry \(\varphi \) and \(\alpha _\varphi \) is a unital *-isomorphism generated by \(\varphi \). The map \(\alpha _\varphi \) is such that (1) for the identity isometry \(\mathbf{1}\) it satisfies
(2) for all appropriate \(a\), \(\varphi \), and \(\varphi '\) it satisfies
and (3) for Alexandrov topology basis elements \(\mathbf{B}_\iota \subset \mathbf{B}_\kappa \) and the unital *-monomorphism \(i\) of Axiom 2 (Isotony) \(\alpha _\varphi \) commutes with \(i\). In other words the following diagram
commutes.
Let \(\mathbf{B}_1\) and \(\mathbf{B}_2\) be any two basis elements of the Alexandrov topology on Minkowski spacetime, i.e. any two sets of the form \(I^+(p_1) \cap I^-(q_1)\) and \(I^+(p_2) \cap I^-(q_2)\).
If \(\mathbf{B}_1 \subset \mathbf{B}_2\) then \(\mathfrak {U}(\mathbf{B}_1) \subset \mathfrak {U}(\mathbf{B}_2)\), where inclusion is implemented by
a unital *-monomorphism.
Let \(\mathbf{B}_1\) and \(\mathbf{B}_2\) be any two basis elements of the Alexandrov topology on a Lorentzian spacetime, i.e. any two sets of the form \(I^+(p_1) \cap I^-(q_1)\) and \(I^+(p_2) \cap I^-(q_2)\).
If \(\mathbf{B}_1 \subset \mathbf{B}_2\) then \(\mathfrak {U}(\mathbf{B}_1) \subset \mathfrak {U}(\mathbf{B}_2)\), where inclusion is implemented by
a unital *-monomorphism.
For any basis element \(\mathbf{B}\) of the Alexandrov topology on Minkowski spacetime, i.e. any set of the form \(I^+(p) \cap I^-(q)\), there is a corresponding abstract C*-algebra \(\mathfrak {U}(\mathbf{B})\)
and when \(\mathbf{B}\) is the empty set, we have the distinguished correspondence
where \(\mathbf{1}\) is the multiplicative identity in the abstract C*-algebra \(\mathbb {C} \mathbf{1}\).
For any basis element \(\mathbf{B}\) of the Alexandrov topology on a Lorentzian spacetime, i.e. any set of the form \(I^+(p) \cap I^-(q)\), there is a corresponding abstract C*-algebra \(\mathfrak {U}(\mathbf{B})\)
and when \(\mathbf{B}\) is the empty set, we have the distinguished correspondence
where \(\mathbf{1}\) is the multiplicative identity in the abstract C*-algebra \(\mathbb {C} \mathbf{1}\).
Let \(\mathbf{B}_1\) and \(\mathbf{B}_2\) be any two basis elements of the Alexandrov topology on Minkowski spacetime, i.e. any two sets of the form \(I^+(p_1) \cap I^-(q_1)\) and \(I^+(p_2) \cap I^-(q_2)\).
If \(\mathbf{B_1}\) and \(\mathbf{B_2}\) are completely spacelike, then \(\mathfrak {U}(\mathbf{B_1})\) and \(\mathfrak {U}(\mathbf{B_2})\) commute in the quasilocal algebra \(\mathfrak {U}\), i.e. for any \(a_1\) in \(\mathfrak {U}(\mathbf{B_1})\) and \(a_2\) in \(\mathfrak {U}(\mathbf{B_2})\) it follows that
in the quasilocal algebra \(\mathfrak {U}\).
Let \(\mathbf{B}_1\) and \(\mathbf{B}_2\) be any two basis elements of the Alexandrov topology on a Lorentzian spacetime, i.e. any two sets of the form \(I^+(p_1) \cap I^-(q_1)\) and \(I^+(p_2) \cap I^-(q_2)\).
If \(\mathbf{B_1}\) and \(\mathbf{B_2}\) are completely spacelike, for any Alexandrov topology basis element \(\mathbf{B}\) such that \(\mathbf{B_1}, \mathbf{B_2} \subseteq \mathbf{B}\) the algebras \(\mathfrak {U}(\mathbf{B_1})\) and \(\mathfrak {U}(\mathbf{B_2})\) commute in the C*-algebra \(\mathfrak {U}(\mathbf{B})\), i.e. for any \(a_1\) in \(\mathfrak {U}(\mathbf{B_1})\) and \(a_2\) in \(\mathfrak {U}(\mathbf{B_2})\) we have
in the C*-algebra \(\mathfrak {U}(\mathbf{B})\), where \(i\) is the unital *-monomorphism Axiom 2 (Isotony).
If no such \(\mathbf{B}\) exists, then it simply doesn’t make sense to consider if \(\mathfrak {U}(\mathbf{B_1})\) and \(\mathfrak {U}(\mathbf{B_2})\) commute as they are not in the same algebra.
For Lorentzian spacetime \(M\) the image \(\pi _\omega (a)\) of a self-adjoint member \(a\) of the local algebra \(\mathfrak {U}(\mathbf{B})\) under the GNS *-homomorphism \(\pi _\omega \) of a state \(\omega \) on \(\mathfrak {U}(\mathbf{B})\) is self-adjoint and thus corresponds to an “observable”. Any “observable” corresponding to such a self-adjoint \(\pi _\omega (a)\) is called a local observable.
Let \(\mathbf{B}\) be any basis element of the Alexandrov topology on Minkowski spacetime, i.e. any set of the form \(I^+(p) \cap I^-(q)\).
A member \(L\) of the inhomogeneous Lorentz group connected to the identity acts on \(\mathfrak {U}(\mathbf{B})\) as follows
where \(L\mathbf{B}\) is the image of the region \(\mathbf{B}\) under the transformation \(L\) and \(\alpha _L\) is a unital *-isomorphism generated by \(L\). The map \(\alpha _L\) is such that (1) for the identity element \(\mathbf{1}\) of the Lorentz group it satisfies
(2) for all appropriate \(a\), \(L\), and \(L'\) it satisfies
and (3) for basis elements \(\mathbf{B}_\iota \subset \mathbf{B}_\kappa \) and the unital *-monomorphism \(i\) of Axiom 2 (Isotony) \(\alpha _L\) commutes with \(i\). In other words the following diagram
commutes.
A path is a continuous map \(\mu :\Sigma \rightarrow M\) from the parameter space–a closed, connected subset \(\Sigma \) of \(\mathbb {R}\) that contains more than a single point–to a spacetime \(M\). A smooth path is a path \(\mu \) that is smooth and has a non-vanishing derivative.
Consider the set-theoretic union of all \(\mathfrak {U}(\mathbf{B})\). As previously proven, this set-theoretic union is a normed *-algebra. Also, as previously proven, taking its completion one obtains a C*-algebra denoted as \(\mathfrak {U}\). This C*-algebra \(\mathfrak {U}\) is called the quasilocal algebra.
A lift of the fiberwise Lorentz action of \(L\) to a quasilocal algebra \(\mathfrak {U}\) (59) is a \(*\)-automorphism \(\beta _L\) of \(\mathfrak {U}\) intertwining the local embeddings \(\iota _{\mathbf{B}}\) with the covariance isomorphisms: \(\beta _L(\iota _{\mathbf{B}} a) = \iota _{L\cdot \mathbf{B}}(\alpha _L a)\) for every Alexandrov-basis set \(\mathbf{B}\).
The image \(\pi _\omega (a)\) of a self-adjoint member \(a\) of the quasilocal algebra \(\mathfrak {U}\) under a GNS *-homomorphism \(\pi _\omega \) is self-adjoint and thus corresponds to an “observable”. Any “observable” corresponding to such a self-adjoint \(\pi _\omega (a)\) is called a quasilocal observable.
A spacetime is a real, four-dimensional, connected, smooth, Hausdorff manifold \(M\) with a globally defined smooth tensor field \(g\) of type \((0,2)\) which is non-degenerate and “Lorentzian”. By Lorentzian we mean that for any \(p \in M\) there is a basis of the tangent space \(TM|_p\) to \(M\) at \(p\) relative to which \(g|_p\) is zero in its non-diagonal entries and on the diagonal takes the form \(\text{diag}(-1,1,1,1)\).
Standard Minkowski spacetime is a spacetime in which the underlying real, four-dimensional, connected, smooth, Hausdorff manifold is \(\mathbb {R}^4\) with the Euclidean topology. In addition \(g\) takes the form \(g|_p=\text{diag}(-1,1,1,1)\) for all \(p\) in \(\mathbb {R}^4\) with respect to the standard coordinates on \(\mathbb {R}^4\).
Let \(\mathfrak {U}\) be an abstract C*-algebra. A state is an element \(\omega \) of the dual space \(\mathfrak {U}^*\) that is
Positive - for any \(a \in \mathfrak {U}\) we have \(0 \le \omega (a^*a)\) and
Normalized - the operator norm satisfies \(\| \omega \| =1\).
Furthermore, a state \(\omega \) is said to be faithful if for any non-zero \(a\) in \(\mathfrak {U}\), it follows that \(0 {\lt} \omega (a^*a)\).
A spacetime \(M\) is time-orientable if it admits a smooth, non-vanishing vector field \(t\) that is timelike. Such a smooth, non-vanishing vector field is called a time-orientation.
A timelike smooth curve is a smooth curve with a tangent vector that is timelike at every point along the smooth curve. A causal smooth curve is a smooth curve with a tangent vector that is timelike or null at every point along the smooth curve.
Let \(M\) be a spacetime, \(p\) a point in \(M\), and \(g\) the tensor field of type \((0,2)\) associated to \(M\). Any tangent vector \(v \in TM|_p\) is timelike, spacelike, or null if \(g|_p(v,v)\) is negative, positive, or zero respectively.
A trip is a curve which is piecewise a future-oriented, timelike geodesic. A trip from \(p\) to \(q\) is a trip with past endpoint \(p\) and future endpoint \(q\). We write \(p \ll q\) if and only if there exists a trip from \(p\) to \(q\).
Instantiating the abstract curved-spacetime interface with the oriented identity component, every isometry \(\varphi \) of the abstract spacetime carries Alexandrov-basis sets to basis sets, \(\varphi \cdot \mathbf{B}\) is again a basis set. This is exactly the well-definedness condition for the Axiom 5 action \(\mathfrak {U}(\mathbf{B}) \to \mathfrak {U}(\varphi (\mathbf{B}))\).
Let \(\mathcal{A}\) be a *-algebra and \(\omega \) a positive element of the dual space \(\mathcal{A}^*\), i.e. \(\omega \) is an element of the dual space \(\mathcal{A}^*\) such that for any \(a \in \mathcal{A}\) one has \(0 \le \omega (a^*a)\). Then
for all \(a\) and \(b\) in \(\mathcal{A}\).
Every tangent vector \(v \in TM|_p\) is exactly one of timelike, null, or spacelike. In particular the three classes are mutually exclusive, and the zero vector is null.
Every trip is a causal trip, so \(p \ll q\) implies \(p \prec q\). Consequently \(I^+(p) \subseteq J^+(p)\) and \(I^-(p) \subseteq J^-(p)\).
Complete spacelike separation is monotone under shrinking either region; the empty region is completely spacelike to any region; and a union of regions is completely spacelike to \(\mathbf{O}\) if and only if each part is. The same properties hold for the bundled Lorentzian spacetime.
- Physicslib4.Spacetime.isCompletelySpacelike_mono
- Physicslib4.Spacetime.isCompletelySpacelike_empty_left
- Physicslib4.Spacetime.isCompletelySpacelike_empty_right
- Physicslib4.Spacetime.isCompletelySpacelike_union_left
- Physicslib4.Spacetime.isCompletelySpacelike_union_right
- Physicslib4.Spacetime.LorentzianSpacetime.isCompletelySpacelike_mono
- Physicslib4.Spacetime.LorentzianSpacetime.isCompletelySpacelike_empty_left
- Physicslib4.Spacetime.LorentzianSpacetime.isCompletelySpacelike_empty_right
- Physicslib4.Spacetime.LorentzianSpacetime.isCompletelySpacelike_union_left
- Physicslib4.Spacetime.LorentzianSpacetime.isCompletelySpacelike_union_right
Spacelike relatedness is symmetric, and consequently complete spacelike separation is symmetric in its two regions: \(\mathbf{O}_1, \mathbf{O}_2\) are completely spacelike if and only if \(\mathbf{O}_2, \mathbf{O}_1\) are.
Let \(g\) be a symmetric Lorentzian bilinear form, \(t\) a timelike vector, and write \(t^\perp = \{ u : g(t,u) = 0\} \) for the spacelike complement. Then \(g\) is positive semidefinite on \(t^\perp \) (so the ordinary Cauchy-Schwarz inequality holds there), and consequently for any timelike \(v, w\) with \(g(t,v) {\lt} 0\) and \(g(t,w) {\lt} 0\) one has \(g(v,w) {\lt} 0\). In particular two timelike tangent vectors that are future-pointing with respect to a common time orientation have negative inner product; by time reversal the same holds for two past-pointing timelike vectors (with \(g(t,v) {\gt} 0\) and \(g(t,w) {\gt} 0\)).
The sum of two timelike future-pointing tangent vectors (with respect to a fixed time orientation) is again timelike and future-pointing. More generally, the sum of any two future-pointing tangent vectors – timelike or null – is future-pointing, so the full future cone, including its null boundary, is convex. Since a vector is past-pointing exactly when its negation is future-pointing, the past cone is convex as well. Downstream this packages as the statement that the future-pointing and past-pointing tangent vectors each form a convex cone: they are closed under positive scaling and, more generally, under positive linear combinations \(a v + b w\) with \(a, b {\gt} 0\).
- Physicslib4.Spacetime.isFuturePointing_add
- Physicslib4.Spacetime.exists_seq_of_isFuturePointing
- Physicslib4.Spacetime.inner_t_nonpos_of_future
- Physicslib4.Spacetime.inner_nonpos_of_future
- Physicslib4.Spacetime.isFuturePointing_add_general
- Physicslib4.Spacetime.isPastPointing_iff_isFuturePointing_neg
- Physicslib4.Spacetime.isPastPointing_add
- Physicslib4.Spacetime.isFuturePointing_smul_pos
- Physicslib4.Spacetime.isFuturePointing_pos_combination
- Physicslib4.Spacetime.isPastPointing_smul_pos
- Physicslib4.Spacetime.isPastPointing_pos_combination
The set-valued chronological and causal futures and pasts are monotone: if \(S \subseteq T\) then \(I^\pm (S) \subseteq I^\pm (T)\) and \(J^\pm (S) \subseteq J^\pm (T)\).
The future-orientation-preserving isometries (those \(\varphi \) with both \(\varphi \) and \(\varphi ^{-1}\) preserving the orientation) form a subgroup, and intersecting it with the identity component gives the oriented identity component. Every such isometry maps Alexandrov-basis diamonds to diamonds, \(\varphi (I^+(p) \cap I^-(q)) = I^+(\varphi (p)) \cap I^-(\varphi (q))\), both as an image and in pointwise-action form \(\varphi \cdot \mathbf{B}\), and this lifts to the bundled Lorentzian spacetime.
- Physicslib4.Spacetime.Isometry.futureOrientationPreserving
- Physicslib4.Spacetime.Isometry.orientedIdentityComponent
- Physicslib4.Spacetime.Isometry.alexandrovBasis_image
- Physicslib4.Spacetime.Isometry.alexandrovBasis_image_of_mem
- Physicslib4.Spacetime.Isometry.alexandrovBasis_image_of_mem_orientedIdentityComponent
- Physicslib4.Spacetime.Isometry.smul_set_eq_image
- Physicslib4.Spacetime.Isometry.alexandrovBasis_smul_of_mem
- Physicslib4.Spacetime.LorentzianSpacetime.isBasisSet_image
- Physicslib4.Spacetime.LorentzianSpacetime.isBasisSet_smul
Say an isometry \(\varphi \) preserves the future orientation if its differential sends future-pointing vectors to future-pointing vectors; this property holds for the identity and is closed under composition. Under it, \(\varphi \) carries trips to trips, so \(p \ll q\) implies \(\varphi (p) \ll \varphi (q)\), and the chronological futures and pasts satisfy \(\varphi (I^\pm (p)) = I^\pm (\varphi (p))\).
- Physicslib4.Spacetime.Isometry.PreservesFutureOrientation
- Physicslib4.Spacetime.Isometry.preservesFutureOrientation_one
- Physicslib4.Spacetime.Isometry.preservesFutureOrientation_mul
- Physicslib4.Spacetime.Isometry.pushforwardPath_isFutureOriented
- Physicslib4.Spacetime.Isometry.chronologicallyPrecedes_pushforward
- Physicslib4.Spacetime.Isometry.chronologicalFuture_image_subset
- Physicslib4.Spacetime.Isometry.chronologicalFuture_image
- Physicslib4.Spacetime.Isometry.chronologicalPast_image_subset
- Physicslib4.Spacetime.Isometry.chronologicalPast_image
An isometry \(\varphi \) of a spacetime preserves the metric square of a tangent vector, \(g_{\varphi (x)}(d\varphi _x v, d\varphi _x v) = g_x(v,v)\), and therefore \(d\varphi _x v\) is timelike, null, or spacelike if and only if \(v\) is.
Let \(\omega \) be a state over a unital C*-algebra \(\mathfrak {U}\). Then the set \(\mathcal{N}_1\) defined by
is equivalent to the set \(\mathcal{N}\) defined by
On a Lorentzian spacetime, complete spacelike separation of two regions is symmetric, and every basis set \(I^+(p) \cap I^-(q)\) is open in the Alexandrov topology.
A future-pointing or past-pointing vector is timelike or null. Moreover a timelike vector cannot be both future-pointing and past-pointing with respect to a fixed time orientation.
An isometry \(\varphi \) pushes a smooth path \(\mu \) forward to the smooth path \(\varphi \circ \mu \) on the same parameter space, with tangent vector \(d\varphi (\dot\mu )\). The pushforward preserves the timelike and causal conditions and carries the past and future endpoints of \(\mu \) to those of \(\varphi \circ \mu \).
- Physicslib4.Spacetime.Isometry.pushforwardPath
- Physicslib4.Spacetime.Isometry.pushforwardPath_tangent
- Physicslib4.Spacetime.Isometry.pushforwardPath_isTimelike
- Physicslib4.Spacetime.Isometry.pushforwardPath_isCausal
- Physicslib4.Spacetime.Isometry.pushforwardPath_isPastEndpoint
- Physicslib4.Spacetime.Isometry.pushforwardPath_isFutureEndpoint
The covariance action \(L \mapsto \beta _L\) of a covariant quasilocal algebra is a genuine action of the Lorentz group by \(*\)-automorphisms of the quasilocal algebra: \(\beta _{\mathbf{1}} = \mathrm{id}\) and \(\beta _{L'L} = \beta _{L'} \circ \beta _L\).
Let \(g\) be a symmetric Lorentzian bilinear form on a real four-dimensional vector space and let \(v, w\) be timelike, that is \(g(v,v) {\lt} 0\) and \(g(w,w) {\lt} 0\). Then the reverse Cauchy-Schwarz inequality holds:
In particular this applies pointwise to the metric \(g|_p\) of any spacetime \(M\) and any two timelike tangent vectors at a point \(p\).
A Lorentzian bilinear form is nondegenerate: if \(g(v,w) = 0\) for every \(w\), then \(v = 0\) (this is read off the signature basis, on which the Gram matrix \(\mathrm{diag}(-1,1,1,1)\) is invertible). Consequently \(g\) is positive definite on the spacelike complement: if \(t\) is timelike and \(u \ne 0\) satisfies \(g(t,u) = 0\), then \(g(u,u) {\gt} 0\), i.e. \(u\) is spacelike.
Let \(g\) be a symmetric Lorentzian bilinear form on a real four-dimensional vector space and let \(v, w\) be timelike and aligned, that is \(g(v,v) {\lt} 0\), \(g(w,w) {\lt} 0\) and \(g(v,w) \le 0\). Then \(v + w\) is timelike, and the reverse (Lorentzian) triangle inequality holds:
In particular the timelike vectors sharing a time cone (so that \(g(v,w) \le 0\)) form a convex cone, and this applies pointwise to the metric \(g|_p\) of any spacetime.
Let \(\omega \) be a state over a unital C*-algebra \(\mathfrak {U}\). One can then construct a Hilbert space \(\mathcal{H}_\omega \) and *-representation \(\pi _\omega \) of \(\mathfrak {U}\) by bounded operators on \(\mathcal{H}_\omega \) such that
As \(\mathfrak {U}\) is unital, there exists a cyclic vector \(\Omega \) in \(\mathcal{H}_\omega \) for the representation \(\pi _\omega \) such that
The triple \((\mathcal{H}_\omega , \pi _\omega , \Omega )\) is called the GNS triple associated to \((\mathfrak {U}, \omega )\) or the cyclic representation of \((\mathfrak {U}, \omega )\). Furthermore, if \(\omega \) is a faithful state, then the *-representation \(\pi _\omega \) is faithful. In addition the GNS triple associated to \((\mathfrak {U}, \omega )\) is unique up to unitary equivalence.
For an invariant state \(\omega \), the covariance action is implemented on the GNS Hilbert space by a family of unitaries \(U(L)\) satisfying \(U(L)\, \pi (a)\Omega = \pi (\beta _L a)\, \Omega \) and \(U(L)\Omega = \Omega \). The unitaries are obtained by extending the densely-defined isometry \(\pi (a)\Omega \mapsto \pi (\beta _L a)\Omega \) - isometric because \(\omega \) preserves the GNS inner product \(\langle \pi (a)\Omega , \pi (b)\Omega \rangle = \omega (a^* b)\) - to the whole GNS space.
For a covariance-compatible quasilocal algebra, the fiberwise Lorentz action extends to a \(*\)-automorphism of \(\mathfrak {U}\), so the lift of 67 exists. The intertwiner is defined on the directed union of local images (a dense \(*\)-subalgebra) and extended by uniform continuity; the inverse is supplied by \(L^{-1}\), and the group laws \(\beta _{L'L} = \beta _{L'}\circ \beta _L\) and \(\beta _{1} = \mathrm{id}\) furnish the two-sided inverse.