This chapter describes how the library encodes states on a C*-algebra, the GNS construction, and
the representation theory built on it. It corresponds to
Section 10.1
of the blueprint, which states and proves the GNS theorem, and to the subsections of
Section 10.6
that develop representation theory, mostly for an arbitrary C*-algebra: "Irreducibility and Schur's
Lemma" to "Direct Sums, Amplification, and Reducibility", and "The Separating Vector of a Faithful
State". The physics is introduced in
chapter 1 of the tutorial,
and chapter 3 builds the one state of
\mathbb{C} and runs the GNS construction on it; this chapter assumes both.
1.2. Design🔗
The universe of the GNS Hilbert space and the library's use of Mathlib's GNS space are
discussed in the conventions chapter, under Universes and
Implementation choices.
The blueprint is the specification, and its entries record the reasons for the choices below.
1.2.1. States are a structure🔗
Mathlib has positive linear maps and a GNS construction for them, but no type of states. The
library's State A is a structure that extends A →L[ℂ] ℂ with two fields, as in the blueprint's
def:state:
positivity, 0 \le \omega(a^*a), and normalisation, \|\omega\| = 1. The familiar
\omega(\mathbf{1}) = 1 is a theorem (State.apply_one), from \|\varphi\| = \mathrm{Re}\,\varphi(\mathbf{1})
for a positive functional (norm_eq_re_apply_one_of_positive). Continuity is part of the data,
so that the operator norm is defined; for a positive functional on a C*-algebra it would be
automatic.
Properties of a state are predicates on it (State.IsFaithful, IsPure,
State.IsExtremePoint), and operations on states are functions that return a state, with the
proof of positivity and normalisation inside (State.comp, State.precomp,
State.convexCombo).
1.2.2. The construction uses Mathlib's GNS space🔗
The blueprint proves the theorem in the textbook way: quotient A by the null space
N(\omega) = \{n : \omega(n^*n) = 0\}, complete A/N(\omega) for
\langle [a], [b] \rangle = \omega(a^*b), let A act by left multiplication, and take
\Omega = [\mathbf{1}]. The Lean proof of gns_construction uses Mathlib's GNS space of the
positive functional \omega instead (PositiveLinearMap.GNS): the completion of A with the
semi-inner product \omega(a^*b), in which the quotient by N(\omega) happens inside the
completion. The representation is Mathlib's PositiveLinearMap.gnsStarAlgHom, and \Omega is
the class of \mathbf{1}. The blueprint's lemmas (the Cauchy–Schwarz inequality, N(\omega)
as a closed subspace) are formalised separately and are not used by the construction (blueprint
thrm:gns-construction-theorem,
formalization note).
The theorem is an existential over a Hilbert space, which in Lean is a type with three instances.
An existential needs a fixed universe for that type, so gns_construction puts H in the universe
of A, where Mathlib's space lives. Uniqueness is the separate theorem gns_unique, since the
two Hilbert spaces it compares are different types, in any universes.
A representation is a unital *-homomorphism π : A →⋆ₐ[ℂ] (H →L[ℂ] H) into the bounded operators
on a complex Hilbert space. It is not wrapped in a structure, so H is an explicit type and
π a x is the operator \pi(a) applied to x.
1.2.3. Cyclic and separating vectors🔗
IsCyclicVector π Ω says that the vectors \pi(a)\Omega are dense in H. The blueprint states
it for any algebra; in Lean A is a unital C*-algebra, the case used throughout. There is no
separate definition of a separating vector: theorems state the condition inline. In this chapter
it is stated for the elements of A, \pi(a)\Omega = 0 \Rightarrow a = 0, not for the
von Neumann algebra \pi(A)''; the
Haag–Kastler chapter
states the operator form for the local von Neumann algebras.
1.2.4. Irreducibility, purity and the commutant🔗
Irreducibility has two textbook forms: no nontrivial closed invariant subspace, and a trivial
commutant, \pi(A)' = \mathbb{C}\mathbf{1}. They are equivalent: the projection onto a closed
invariant subspace lies in \pi(A)', and the von Neumann algebra \pi(A)' is generated by its
projections. The library uses the commutant form, as the blueprint does
(def:irreducible-representation):
IsIrreducible π says that every bounded operator commuting with all \pi(a) is a multiple of
\mathbf{1}. On the zero Hilbert space every operator is 0 = 0 \cdot \mathbf{1}, so every
representation on it satisfies IsIrreducible; results that need a nonzero space assume it, as
Nontrivial H or as a nonzero vector. A space carrying a vector that reproduces a state is never
zero, since \|\Omega\|^2 = \langle \Omega, \pi(\mathbf{1})\Omega \rangle = \omega(\mathbf{1}) = 1;
this is immediate from the reproducing condition at a = \mathbf{1}, and the library has no
separate lemma for it. So the zero case does not arise in isPure_iff_isIrreducible.
Purity is defined by domination
(def:pure-state):
every positive functional \psi with \psi(a^*a) \le \omega(a^*a) is a multiple of \omega.
This avoids normalising the parts of a mixture. The convex form, that \omega is not a
nontrivial mixture of two states, is State.IsExtremePoint, and the two are proved equivalent.
The equivalence of purity with irreducibility of the GNS representation goes through a
Radon–Nikodym operator rnOp, the element of \pi(A)' that represents a dominated \psi.
The state space appears in two topologies. stateSpace A, a subset of A →L[ℂ] ℂ with the norm
topology, carries convexity and Mathlib's extremePoints. weakStateSet, a subset of Mathlib's
WeakDual ℂ A, carries the weak-* topology and is compact. The existence of pure states, by the
Krein–Milman theorem applied to weakStateSet, is not proved: among the missing pieces, Mathlib
has no instance LocallyConvexSpace ℝ (WeakDual ℂ A), which its Krein–Milman theorem needs.
The von Neumann algebra \pi(A)'' is gnsVonNeumann π as a set of operators and
gnsVonNeumannAlgebra π bundled as Mathlib's VonNeumannAlgebra; the commutant is Mathlib's
Set.centralizer, and \pi(A)' bundled is commutantVonNeumann π. The names refer to the GNS
representation, but \pi is any representation.
1.2.5. Disjointness, quasi-equivalence and superselection🔗
As you will recall, the superselection sectors of a theory are labelled by unitary equivalence
classes of irreducible representations of its algebra of observables. The library compares representations in three ways, each a
proposition:
-
UnitaryEquiv π₁ π₂: a unitary U : H_1 \to H_2 with U\pi_1(a) = \pi_2(a)U;
-
QuasiEquiv π₁ π₂: a *-isomorphism \pi_1(A)'' \to \pi_2(A)'' with
\pi_1(a) \mapsto \pi_2(a);
-
AreDisjoint π₁ π₂: the only intertwiner from \pi_1 to \pi_2 is 0.
A unitary is a linear isometric equivalence H₁ ≃ₗᵢ[ℂ] H₂. Quasi-equivalence asks for a
*-isomorphism of the underlying *-algebras, with no normality condition, since a *-isomorphism of
von Neumann algebras is automatically normal. The quasi-equivalence of a representation with its
amplification is not proved: it needs the commutant of an amplification,
(\pi(A) \otimes \mathbf{1})' = \pi(A)' \mathbin{\bar\otimes} B(\ell^2(\iota)), which Mathlib does not provide.
1.2.6. Direct sums and amplification🔗
The direct sum of a family (\pi_i)_{i \in \iota} acts on Mathlib's \ell^2 space lp H 2 of a
family of Hilbert spaces H : ι → Type*, over an arbitrary index type, by the block-diagonal
operator with blocks \pi_i(a). It is bounded by \|a\| because a *-homomorphism of
C*-algebras is contractive. The amplification \iota \cdot \pi is the direct sum of the constant
family.
1.2.7. Covariance and unitary implementation🔗
Symmetries enter in two ways. First, a *-isomorphism \Phi : A \to B relabels observables. The
pullback \omega \circ \Phi of a state is State.comp, defined along any unital
*-homomorphism, and the GNS representation of \omega \circ \Phi is that of \omega composed
with \Phi, up to unitary equivalence. No new construction is needed: gns_unique applies to the
two cyclic representations of \omega \circ \Phi.
Second, a family of *-automorphisms \gamma_g that leaves \omega invariant is implemented on the
GNS space by unitaries U(g), the extension of \pi(a)\Omega \mapsto \pi(\gamma_g(a))\Omega. These
theorems are stated for any unital C*-algebra and any monoid G, with the action either as a function with
the composition laws or as a monoid homomorphism. They apply both to the quasilocal algebra with
the Poincaré action and to a local algebra with the stabiliser of its region. Strong continuity of
U follows from continuity of the matrix coefficients g \mapsto \omega(a^*\gamma_g(b)); it is
what Stone's theorem needs to produce self-adjoint generators, such as the Hamiltonian.
1.3. Main definitions and theorems🔗
Definitions are shown with their docstrings, which give the mathematics and the blueprint entry;
theorems with their statements, as Lean prints them, and a line or two of explanation. Each
subsection opens with the blueprint entries it covers. In the printed statements,
inner ℂ x y is the inner product \langle x, y \rangle, linear in the second argument, and
(π a) Ω is \pi(a)\Omega. For the declarations not shown here, see the
API documentation and
the files listed at the end of the chapter.
1.3.1. States🔗
Blueprint: def:state, lmm:cauchy-schwarz-inequality, lmm:lmm1,
lmm:lmm2.
🔗structure
A state on a unital C*-algebra A: a positive, normalised continuous linear functional ω : A → ℂ.
The number ω(a) is the expectation value of the observable a in the state ω. Positivity asks
that ω(a* a) ≥ 0 for every a ∈ A, that is, ω(a* a) is real and non-negative. Normalisation asks
that the operator norm ‖ω‖ is 1; for a positive functional on a nonzero algebra the norm is
Re ω(1) (norm_eq_re_apply_one_of_positive), so this is the familiar ω(1) = 1. A density matrix
ρ gives the state a ↦ tr(ρa) of the algebra of bounded operators on a Hilbert space, but the
definition needs no Hilbert space: the GNS construction (gns_construction) produces one from ω.
Implementation note: the structure extends A →L[ℂ] ℂ, and a FunLike instance lets one write
ω a. Positivity uses Mathlib's partial order on ℂ (ComplexOrder), in which 0 ≤ z means that
z is real and non-negative.
Blueprint: def:state
Fields
isPositive : ∀ (a : A), 0 ≤ self.toContinuousLinearMap (star a * a)
Positivity: ω(a* a) is real and non-negative for every a ∈ A.
🔗def
A faithful state: ω(a* a) > 0 for every nonzero a ∈ A.
Since ω(a* a) ≥ 0 always, this says that ω(a* a) = 0 only for a = 0: no nonzero observable has
vanishing expectation of a* a. A faithful state has an injective GNS representation
(gns_construction), and its cyclic vector is separating (separating_of_faithful). On a
matrix algebra the Gibbs state a ↦ tr(e^(−βH) a)/Z is faithful, while a vector state
a ↦ ⟨ψ, aψ⟩ is not: it vanishes on a* a whenever a annihilates the unit vector ψ.
Blueprint: def:state
The Cauchy–Schwarz inequality is stated for any positive linear functional on a complex *-ring,
with no continuity, normalisation or unit. Since \omega(a^*a) and \omega(b^*b) are
non-negative reals, the right-hand side uses real parts:
open Physicslib4 GNS in
Physicslib4.GNS.cauchy_schwarz_inequality.{u_1} {A : Type u_1} [NonUnitalNonAssocRing A] [StarRing A] [Module ℂ A]
[IsScalarTower ℂ A A] [SMulCommClass ℂ A A] [StarModule ℂ A] (ω : A →ₗ[ℂ] ℂ) (hω : ∀ (a : A), 0 ≤ ω (star a * a))
(a b : A) : Complex.normSq (ω (star a * b)) ≤ (ω (star a * a)).re * (ω (star b * b)).re#check cauchy_schwarz_inequality
Physicslib4.GNS.cauchy_schwarz_inequality.{u_1} {A : Type u_1} [NonUnitalNonAssocRing A] [StarRing A] [Module ℂ A]
[IsScalarTower ℂ A A] [SMulCommClass ℂ A A] [StarModule ℂ A] (ω : A →ₗ[ℂ] ℂ) (hω : ∀ (a : A), 0 ≤ ω (star a * a))
(a b : A) : Complex.normSq (ω (star a * b)) ≤ (ω (star a * a)).re * (ω (star b * b)).re
From it, the null set N(\omega) equals \{n : \omega(b^*n) = 0 \text{ for all } b\}
(lmm1), so it is a closed linear subspace (lmm2,
nullSubmodule).
1.3.2. The GNS construction🔗
Blueprint: def:cyclic-vector, thrm:gns-construction-theorem,
thrm:separating-faithful.
🔗def
A cyclic vector Ω for a representation π of A on H: the vectors π(a)Ω, a ∈ A, are dense in H.
Every vector of H is then a limit of vectors obtained by acting on Ω with the represented
algebra, as every state of a Fock space is obtained from the vacuum by acting with creation
operators. The GNS representation of a state always has a cyclic vector (gns_construction),
and a cyclic representation reproducing a state is determined by the state up to unitary
equivalence (gns_unique).
Implementation note: a representation is a unital -homomorphism π : A →⋆ₐ[ℂ] (H →L[ℂ] H) into
the bounded operators on a complex Hilbert space H. The blueprint allows any algebra A; here A is
a unital C-algebra, the case used throughout the project.
Blueprint: def:cyclic-vector
The existence half of the theorem. Lean prints the three anonymous instance arguments as
x : NormedAddCommGroup H, x_1 : InnerProductSpace ℂ H and x_2 : CompleteSpace H; tutorial
chapter 3 reads the statement line by line and
applies it to a state.
open Physicslib4 GNS in
Physicslib4.GNS.gns_construction.{u} {A : Type u} [CStarAlgebra A] (ω : State A) :
∃ H x x_1,
∃ (x_2 : CompleteSpace H),
∃ π Ω, IsCyclicVector π Ω ∧ (∀ (a : A), ω a = inner ℂ Ω ((π a) Ω)) ∧ (ω.IsFaithful → Function.Injective ⇑π)#check gns_construction
Physicslib4.GNS.gns_construction.{u} {A : Type u} [CStarAlgebra A] (ω : State A) :
∃ H x x_1,
∃ (x_2 : CompleteSpace H),
∃ π Ω, IsCyclicVector π Ω ∧ (∀ (a : A), ω a = inner ℂ Ω ((π a) Ω)) ∧ (ω.IsFaithful → Function.Injective ⇑π)
Uniqueness: any two cyclic representations that reproduce \omega are related by a unitary U,
a linear isometric equivalence, that maps \Omega_1 to \Omega_2 and intertwines \pi_1 with
\pi_2:
open Physicslib4 GNS in
Physicslib4.GNS.gns_unique.{u_1, u_2, u_3} {A : Type u_1} [CStarAlgebra A] (ω : State A) {H₁ : Type u_2}
[NormedAddCommGroup H₁] [InnerProductSpace ℂ H₁] [CompleteSpace H₁] (π₁ : A →⋆ₐ[ℂ] H₁ →L[ℂ] H₁) (Ω₁ : H₁)
(hcyc₁ : IsCyclicVector π₁ Ω₁) (hrep₁ : ∀ (a : A), ω a = inner ℂ Ω₁ ((π₁ a) Ω₁)) {H₂ : Type u_3}
[NormedAddCommGroup H₂] [InnerProductSpace ℂ H₂] [CompleteSpace H₂] (π₂ : A →⋆ₐ[ℂ] H₂ →L[ℂ] H₂) (Ω₂ : H₂)
(hcyc₂ : IsCyclicVector π₂ Ω₂) (hrep₂ : ∀ (a : A), ω a = inner ℂ Ω₂ ((π₂ a) Ω₂)) :
∃ U, U Ω₁ = Ω₂ ∧ ∀ (a : A) (x : H₁), U ((π₁ a) x) = (π₂ a) (U x)#check gns_unique
Physicslib4.GNS.gns_unique.{u_1, u_2, u_3} {A : Type u_1} [CStarAlgebra A] (ω : State A) {H₁ : Type u_2}
[NormedAddCommGroup H₁] [InnerProductSpace ℂ H₁] [CompleteSpace H₁] (π₁ : A →⋆ₐ[ℂ] H₁ →L[ℂ] H₁) (Ω₁ : H₁)
(hcyc₁ : IsCyclicVector π₁ Ω₁) (hrep₁ : ∀ (a : A), ω a = inner ℂ Ω₁ ((π₁ a) Ω₁)) {H₂ : Type u_3}
[NormedAddCommGroup H₂] [InnerProductSpace ℂ H₂] [CompleteSpace H₂] (π₂ : A →⋆ₐ[ℂ] H₂ →L[ℂ] H₂) (Ω₂ : H₂)
(hcyc₂ : IsCyclicVector π₂ Ω₂) (hrep₂ : ∀ (a : A), ω a = inner ℂ Ω₂ ((π₂ a) Ω₂)) :
∃ U, U Ω₁ = Ω₂ ∧ ∀ (a : A) (x : H₁), U ((π₁ a) x) = (π₂ a) (U x)
For a faithful state the reproducing vector is separating, in any representation, since
\|\pi(a)\Omega\|^2 = \omega(a^*a):
open Physicslib4 GNS in
Physicslib4.GNS.separating_of_faithful.{u_1, u_2} {A : Type u_1} [CStarAlgebra A] {H : Type u_2} [NormedAddCommGroup H]
[InnerProductSpace ℂ H] [CompleteSpace H] {ω : State A} (hω : ω.IsFaithful) (π : A →⋆ₐ[ℂ] H →L[ℂ] H) (Ω : H)
(hrep : ∀ (a : A), ω a = inner ℂ Ω ((π a) Ω)) {a : A} (ha : (π a) Ω = 0) : a = 0#check separating_of_faithful
Physicslib4.GNS.separating_of_faithful.{u_1, u_2} {A : Type u_1} [CStarAlgebra A] {H : Type u_2} [NormedAddCommGroup H]
[InnerProductSpace ℂ H] [CompleteSpace H] {ω : State A} (hω : ω.IsFaithful) (π : A →⋆ₐ[ℂ] H →L[ℂ] H) (Ω : H)
(hrep : ∀ (a : A), ω a = inner ℂ Ω ((π a) Ω)) {a : A} (ha : (π a) Ω = 0) : a = 0
The GNS form, a triple whose vector is both cyclic and separating, is
exists_gns_separating.
1.3.3. Irreducibility and purity🔗
Blueprint: def:irreducible-representation, thrm:schur-lemma,
thrm:irreducible-generates-all, def:pure-state,
thrm:gns-radon-nikodym-operator, thrm:pure-iff-irreducible,
def:extreme-state, thrm:pure-iff-extreme,
thrm:state-space-weak-compact, def:von-neumann-center.
🔗def
An irreducible representation: every bounded operator commuting with all π(a) is a multiple of 1.
The operators that commute with every π(a) form the commutant π(A)'. Irreducibility asks that
π(A)' consist of the scalars c·1 only. For a representation on a Hilbert space this is
equivalent to the absence of a nontrivial closed subspace invariant under all π(a), because the
orthogonal projection onto such a subspace lies in π(A)'; the library uses the commutant form.
A state is pure exactly when its GNS representation is irreducible (isPure_iff_isIrreducible),
and π is irreducible exactly when π(A)'' is all of B(H)
(isIrreducible_iff_gnsVonNeumann_eq_univ).
Implementation note: on the zero Hilbert space every operator is 0 = 0·1, so every representation
on it is irreducible in this sense; the usual convention excludes H = 0, and results that need a
nonzero space assume it.
Blueprint: def:irreducible-representation
In the printed statements Lean writes GNS.IsIrreducible, to distinguish it from Mathlib's
IsIrreducible, irreducibility of a subset of a topological space. Irreducibility is the statement that the commutant, Mathlib's
Set.centralizer of the image, is the set scalarOperators H of multiples of \mathbf{1}:
open Physicslib4 GNS in
Physicslib4.GNS.isIrreducible_iff_centralizer.{u_1, u_2} {A : Type u_1} [CStarAlgebra A] {H₁ : Type u_2}
[NormedAddCommGroup H₁] [InnerProductSpace ℂ H₁] [CompleteSpace H₁] {π : A →⋆ₐ[ℂ] H₁ →L[ℂ] H₁} :
GNS.IsIrreducible π ↔ (Set.range ⇑π).centralizer = scalarOperators H₁#check isIrreducible_iff_centralizer
Physicslib4.GNS.isIrreducible_iff_centralizer.{u_1, u_2} {A : Type u_1} [CStarAlgebra A] {H₁ : Type u_2}
[NormedAddCommGroup H₁] [InnerProductSpace ℂ H₁] [CompleteSpace H₁] {π : A →⋆ₐ[ℂ] H₁ →L[ℂ] H₁} :
GNS.IsIrreducible π ↔ (Set.range ⇑π).centralizer = scalarOperators H₁
Equivalently, \pi(A)'' is all of B(H), because the commutant of the scalars is everything and
the centre of B(H) is the scalars:
open Physicslib4 GNS in
Physicslib4.GNS.isIrreducible_iff_gnsVonNeumann_eq_univ.{u_1, u_2} {A : Type u_1} [CStarAlgebra A] {H : Type u_2}
[NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {π : A →⋆ₐ[ℂ] H →L[ℂ] H} :
GNS.IsIrreducible π ↔ gnsVonNeumann π = Set.univ#check isIrreducible_iff_gnsVonNeumann_eq_univ
Physicslib4.GNS.isIrreducible_iff_gnsVonNeumann_eq_univ.{u_1, u_2} {A : Type u_1} [CStarAlgebra A] {H : Type u_2}
[NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {π : A →⋆ₐ[ℂ] H →L[ℂ] H} :
GNS.IsIrreducible π ↔ gnsVonNeumann π = Set.univ
🔗def
The von Neumann algebra π(A)'' generated by a representation π, as a set of operators.
The commutant S' of a set S of bounded operators is the set of operators commuting with every
element of S, and S'' = (S')' is its bicommutant. By von Neumann's density theorem every element
of π(A)'' is a strong-operator limit of elements of π(A)
(exists_forall_norm_sub_lt_of_mem_bicommutant), so π(A)'' adds to the represented observables
their limits, such as spectral projections. π is irreducible exactly when π(A)'' is all of B(H)
(isIrreducible_iff_gnsVonNeumann_eq_univ).
Implementation note: the commutant is Set.centralizer, taken in the bounded operators on H.
The name refers to the GNS representation, but π is any representation. The bundled version is
gnsVonNeumannAlgebra.
The topological Schur lemma, eq_smul_one_of_commute_of_cyclic, says that in a cyclic
representation an operator T of \pi(A)' with
\langle \Omega, T\pi(a)\Omega \rangle = c\,\langle \Omega, \pi(a)\Omega \rangle for all a equals
c\mathbf{1}. The centre of a von Neumann algebra R is
vonNeumannCenter R, and R is a factor
(IsFactor) when the centre is the scalars. For an irreducible representation the centre of
\pi(A)'' is the scalars (center_gnsVonNeumann_eq_of_isIrreducible), so it generates a factor
(isFactor_gnsVonNeumann_of_isIrreducible).
🔗def
A pure state: every positive functional dominated by ω is a scalar multiple of ω.
A positive functional ψ is dominated by ω when 0 ≤ ψ(a* a) ≤ ω(a* a) for every a ∈ A. If
ω = t ω₁ + (1 − t) ω₂ is a mixture of states with 0 < t < 1, then t ω₁ is dominated by ω, so a
pure state is not a nontrivial mixture; the converse holds too, so pure means an extreme point
of the convex set of states (isPure_iff_isExtremePoint). On the algebra of bounded operators
of a Hilbert space, the vector state a ↦ ⟨ψ, aψ⟩ is pure and a density matrix of rank two or
more is not. A state is pure exactly when its GNS representation is irreducible
(isPure_iff_isIrreducible).
Implementation note: the dominated ψ range over continuous linear functionals A →L[ℂ] ℂ, which
is no restriction since positive functionals on a C*-algebra are continuous. The inequality
ψ(a* a) ≤ ω(a* a) is in Mathlib's order on ℂ, so the difference is real and non-negative. This
order form avoids normalising the parts of a convex combination.
Blueprint: def:pure-state
The headline theorem of the section, for any cyclic representation that reproduces \omega:
open Physicslib4 GNS in
Physicslib4.GNS.isPure_iff_isIrreducible.{u_1, u_2} {A : Type u_1} [CStarAlgebra A] {H : Type u_2}
[NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {ω : State A} {π : A →⋆ₐ[ℂ] H →L[ℂ] H} {Ω : H}
(hcyc : IsCyclicVector π Ω) (hrep : ∀ (a : A), ω a = inner ℂ Ω ((π a) Ω)) : IsPure ω ↔ GNS.IsIrreducible π#check isPure_iff_isIrreducible
Physicslib4.GNS.isPure_iff_isIrreducible.{u_1, u_2} {A : Type u_1} [CStarAlgebra A] {H : Type u_2}
[NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {ω : State A} {π : A →⋆ₐ[ℂ] H →L[ℂ] H} {Ω : H}
(hcyc : IsCyclicVector π Ω) (hrep : ∀ (a : A), ω a = inner ℂ Ω ((π a) Ω)) : IsPure ω ↔ GNS.IsIrreducible π
From irreducible to pure, a dominated \psi gives the Radon–Nikodym operator
rnOp in \pi(A)', with
\psi(a) = \langle \Omega, T\pi(a)\Omega \rangle, which irreducibility makes a scalar. From pure
to irreducible, an element of \pi(A)' splits into self-adjoint parts, which rescale into
functionals dominated by \omega. With the GNS triple, a pure state therefore gives a factor
(exists_gns_factor_of_isPure) and \pi(A)'' = B(H) (exists_gns_generates_all_of_isPure).
🔗def
An extreme point of the state space: ω is not a mixture t ω₁ + (1 − t) ω₂ of two distinct states.
The states of A form a convex set: a mixture of states with weights t and 1 − t is a state
(State.convexCombo). ω is extreme when ω = t ω₁ + (1 − t) ω₂ with 0 < t < 1 forces ω₁ = ω₂,
and then both equal ω. Physically, an extreme state carries no classical uncertainty about which
state the system is in. Extremality is equivalent to purity (isPure_iff_isExtremePoint) and to
membership in Mathlib's extremePoints of the state space
(mem_extremePoints_iff_isExtremePoint).
Implementation note: the decomposition is stated pointwise, ω(a) = t ω₁(a) + (1 − t) ω₂(a) for all
a ∈ A, with real t.
Blueprint: def:extreme-state
open Physicslib4 GNS in
Physicslib4.GNS.isPure_iff_isExtremePoint.{u_1} {A : Type u_1} [CStarAlgebra A] (ω : State A) :
IsPure ω ↔ ω.IsExtremePoint#check isPure_iff_isExtremePoint
Physicslib4.GNS.isPure_iff_isExtremePoint.{u_1} {A : Type u_1} [CStarAlgebra A] (ω : State A) :
IsPure ω ↔ ω.IsExtremePoint
The proof rests on \|\varphi\| = \mathrm{Re}\,\varphi(\mathbf{1}) for positive \varphi,
which fixes the weights of a mixture. Extremality agrees with Mathlib's extremePoints of
stateSpace A
(mem_extremePoints_iff_isExtremePoint), which is convex (convex_stateSpace). In the weak-*
topology:
🔗def
The state space in the weak-* topology: the positive functionals φ on A with φ(1) = 1.
In the weak-* topology, functionals converge when their values φ(a) converge for every a: a
sequence of states converges when all expectation values do. For a positive functional
φ(1) = 1 is the same as ‖φ‖ = 1, so mathematically these are exactly the states; the library
proves that every state lies in the set (State.toWeakDual, State.toWeakDual_mem_weakStateSet),
not the converse. By the Banach–Alaoglu theorem the set is weak-* compact
(isCompact_weakStateSet), which with the Krein–Milman theorem gives the existence of pure
states; the library proves the compactness, not the existence.
Implementation note: the set lives in Mathlib's WeakDual ℂ A, whose topology is the weak-*
topology; stateSpace is the same set of functionals with the norm topology.
Blueprint: thrm:state-space-weak-compact
open Physicslib4 GNS in
Physicslib4.GNS.isCompact_weakStateSet.{u_1} {A : Type u_1} [CStarAlgebra A] : IsCompact weakStateSet#check isCompact_weakStateSet
Physicslib4.GNS.isCompact_weakStateSet.{u_1} {A : Type u_1} [CStarAlgebra A] : IsCompact weakStateSet
The proof is the Banach–Alaoglu theorem: the set is weak-* closed and lies in the unit ball.
1.3.4. Equivalence and disjointness of representations🔗
Blueprint: def:unitary-equivalence, thrm:unitary-equiv-invariants,
def:disjoint-representations, def:quasi-equivalence,
thrm:irreducible-dichotomy, thrm:pure-state-dichotomy,
thrm:commutant-von-neumann.
🔗defPhysicslib4.GNS.UnitaryEquiv.{u_1, u_2, u_3} {A : Type u_1}
[CStarAlgebra A] {H₁ : Type u_2} [NormedAddCommGroup H₁]
[InnerProductSpace ℂ H₁] [CompleteSpace H₁] {H₂ : Type u_3}
[NormedAddCommGroup H₂] [InnerProductSpace ℂ H₂] [CompleteSpace H₂]
(π₁ : A →⋆ₐ[ℂ] H₁ →L[ℂ] H₁) (π₂ : A →⋆ₐ[ℂ] H₂ →L[ℂ] H₂) : Prop Physicslib4.GNS.UnitaryEquiv.{u_1, u_2,
u_3}
{A : Type u_1} [CStarAlgebra A]
{H₁ : Type u_2} [NormedAddCommGroup H₁]
[InnerProductSpace ℂ H₁]
[CompleteSpace H₁] {H₂ : Type u_3}
[NormedAddCommGroup H₂]
[InnerProductSpace ℂ H₂]
[CompleteSpace H₂]
(π₁ : A →⋆ₐ[ℂ] H₁ →L[ℂ] H₁)
(π₂ : A →⋆ₐ[ℂ] H₂ →L[ℂ] H₂) : Prop
Unitary equivalence of representations: a unitary U : H₁ → H₂ with U π₁(a) = π₂(a) U for all a.
Two unitarily equivalent representations differ only by a change of basis of the Hilbert space,
U π₁(a) U⁻¹ = π₂(a), so they describe the same physics. It is an equivalence relation
(UnitaryEquiv.refl, UnitaryEquiv.symm, UnitaryEquiv.trans) and preserves irreducibility and
the factor property (UnitaryEquiv.isIrreducible_iff, UnitaryEquiv.isFactor_iff). The GNS
representation of a state is unique up to unitary equivalence (gns_unique), and superselection
sectors are classes of irreducible representations of the algebra of observables.
Implementation note: U is a linear isometric equivalence H₁ ≃ₗᵢ[ℂ] H₂, which for Hilbert spaces
is the same as a unitary operator, and the intertwining is U(π₁(a)x) = π₂(a)(Ux) for all x ∈ H₁.
Blueprint: def:unitary-equivalence
🔗defPhysicslib4.GNS.Intertwines.{u_1, u_2, u_3} {A : Type u_1}
[CStarAlgebra A] {H₁ : Type u_2} [NormedAddCommGroup H₁]
[InnerProductSpace ℂ H₁] [CompleteSpace H₁] {H₂ : Type u_3}
[NormedAddCommGroup H₂] [InnerProductSpace ℂ H₂] [CompleteSpace H₂]
(π₁ : A →⋆ₐ[ℂ] H₁ →L[ℂ] H₁) (π₂ : A →⋆ₐ[ℂ] H₂ →L[ℂ] H₂)
(T : H₁ →L[ℂ] H₂) : Prop Physicslib4.GNS.Intertwines.{u_1, u_2,
u_3}
{A : Type u_1} [CStarAlgebra A]
{H₁ : Type u_2} [NormedAddCommGroup H₁]
[InnerProductSpace ℂ H₁]
[CompleteSpace H₁] {H₂ : Type u_3}
[NormedAddCommGroup H₂]
[InnerProductSpace ℂ H₂]
[CompleteSpace H₂]
(π₁ : A →⋆ₐ[ℂ] H₁ →L[ℂ] H₁)
(π₂ : A →⋆ₐ[ℂ] H₂ →L[ℂ] H₂)
(T : H₁ →L[ℂ] H₂) : Prop
An intertwiner from π₁ to π₂: a bounded operator T : H₁ → H₂ with T π₁(a) = π₂(a) T for all a.
An intertwiner maps the action of A on H₁ to its action on H₂. Intertwiners form a vector space
closed under composition and adjoints (Intertwines.comp, Intertwines.adjoint); a unitary
intertwiner is a unitary equivalence. The intertwiners from π to itself are the commutant π(A)'
(intertwines_self_iff_mem_centralizer), so π is irreducible exactly when they are the scalars.
Two representations are disjoint when 0 is their only intertwiner (AreDisjoint).
Implementation note: the condition is stated pointwise, T(π₁(a)x) = π₂(a)(Tx) for all x ∈ H₁.
Blueprint: the intertwiners of def:disjoint-representations
🔗defPhysicslib4.GNS.AreDisjoint.{u_1, u_2, u_3} {A : Type u_1}
[CStarAlgebra A] {H₁ : Type u_2} [NormedAddCommGroup H₁]
[InnerProductSpace ℂ H₁] [CompleteSpace H₁] {H₂ : Type u_3}
[NormedAddCommGroup H₂] [InnerProductSpace ℂ H₂] [CompleteSpace H₂]
(π₁ : A →⋆ₐ[ℂ] H₁ →L[ℂ] H₁) (π₂ : A →⋆ₐ[ℂ] H₂ →L[ℂ] H₂) : Prop Physicslib4.GNS.AreDisjoint.{u_1, u_2,
u_3}
{A : Type u_1} [CStarAlgebra A]
{H₁ : Type u_2} [NormedAddCommGroup H₁]
[InnerProductSpace ℂ H₁]
[CompleteSpace H₁] {H₂ : Type u_3}
[NormedAddCommGroup H₂]
[InnerProductSpace ℂ H₂]
[CompleteSpace H₂]
(π₁ : A →⋆ₐ[ℂ] H₁ →L[ℂ] H₁)
(π₂ : A →⋆ₐ[ℂ] H₂ →L[ℂ] H₂) : Prop
Disjoint representations: the only intertwiner from π₁ to π₂ is 0.
Disjoint representations have nothing in common: no nonzero subrepresentation of one is
unitarily equivalent to a subrepresentation of the other. Disjointness is symmetric
(AreDisjoint.symm), and unitarily equivalent representations on a nonzero space are never disjoint
(UnitaryEquiv.not_areDisjoint). Two irreducible representations are either disjoint or
unitarily equivalent (areDisjoint_or_unitaryEquiv_of_isIrreducible), so distinct
superselection sectors give disjoint representations. Equilibrium (KMS) states of an infinite
system at different temperatures typically give disjoint representations too.
Blueprint: def:disjoint-representations
Unitarily equivalent representations on a nonzero space are not disjoint
(UnitaryEquiv.not_areDisjoint, which assumes Nontrivial H₁). For irreducible representations
the two notions are complementary: a nonzero intertwiner T between irreducibles has
T^*T and TT^* scalar, so a multiple of T is unitary.
open Physicslib4 GNS in
Physicslib4.GNS.areDisjoint_or_unitaryEquiv_of_isIrreducible.{u_1, u_2, u_3} {A : Type u_1} [CStarAlgebra A]
{H₁ : Type u_2} [NormedAddCommGroup H₁] [InnerProductSpace ℂ H₁] [CompleteSpace H₁] {H₂ : Type u_3}
[NormedAddCommGroup H₂] [InnerProductSpace ℂ H₂] [CompleteSpace H₂] {π₁ : A →⋆ₐ[ℂ] H₁ →L[ℂ] H₁}
{π₂ : A →⋆ₐ[ℂ] H₂ →L[ℂ] H₂} (h1 : GNS.IsIrreducible π₁) (h2 : GNS.IsIrreducible π₂) :
AreDisjoint π₁ π₂ ∨ UnitaryEquiv π₁ π₂#check areDisjoint_or_unitaryEquiv_of_isIrreducible
Physicslib4.GNS.areDisjoint_or_unitaryEquiv_of_isIrreducible.{u_1, u_2, u_3} {A : Type u_1} [CStarAlgebra A]
{H₁ : Type u_2} [NormedAddCommGroup H₁] [InnerProductSpace ℂ H₁] [CompleteSpace H₁] {H₂ : Type u_3}
[NormedAddCommGroup H₂] [InnerProductSpace ℂ H₂] [CompleteSpace H₂] {π₁ : A →⋆ₐ[ℂ] H₁ →L[ℂ] H₁}
{π₂ : A →⋆ₐ[ℂ] H₂ →L[ℂ] H₂} (h1 : GNS.IsIrreducible π₁) (h2 : GNS.IsIrreducible π₂) :
AreDisjoint π₁ π₂ ∨ UnitaryEquiv π₁ π₂
For pure states, applied to their GNS representations, this is
exists_gns_areDisjoint_or_unitaryEquiv_of_isPure:
the GNS representations of two pure states are unitarily equivalent (the same superselection
sector) or disjoint. Unitary equivalence
preserves irreducibility and the factor property (UnitaryEquiv.isIrreducible_iff,
UnitaryEquiv.isFactor_iff).
🔗defPhysicslib4.GNS.QuasiEquiv.{u_1, u_2, u_3} {A : Type u_1}
[CStarAlgebra A] {H₁ : Type u_2} [NormedAddCommGroup H₁]
[InnerProductSpace ℂ H₁] [CompleteSpace H₁] {H₂ : Type u_3}
[NormedAddCommGroup H₂] [InnerProductSpace ℂ H₂] [CompleteSpace H₂]
(π₁ : A →⋆ₐ[ℂ] H₁ →L[ℂ] H₁) (π₂ : A →⋆ₐ[ℂ] H₂ →L[ℂ] H₂) : Prop Physicslib4.GNS.QuasiEquiv.{u_1, u_2, u_3}
{A : Type u_1} [CStarAlgebra A]
{H₁ : Type u_2} [NormedAddCommGroup H₁]
[InnerProductSpace ℂ H₁]
[CompleteSpace H₁] {H₂ : Type u_3}
[NormedAddCommGroup H₂]
[InnerProductSpace ℂ H₂]
[CompleteSpace H₂]
(π₁ : A →⋆ₐ[ℂ] H₁ →L[ℂ] H₁)
(π₂ : A →⋆ₐ[ℂ] H₂ →L[ℂ] H₂) : Prop
Quasi-equivalence: a *-isomorphism π₁(A)'' → π₂(A)'' sending π₁(a) to π₂(a) for every a.
Quasi-equivalent representations generate the same von Neumann algebra up to isomorphism.
Mathematically, they therefore have the same normal states (the states given by density matrices),
which form the folium of a representation, so quasi-equivalence means having the same folium; they
may differ in multiplicity, as a representation and its amplification do. The library proves none of
these three facts. Quasi-equivalence is an equivalence relation (QuasiEquiv.refl,
QuasiEquiv.symm, QuasiEquiv.trans) and is coarser than unitary equivalence
(UnitaryEquiv.quasiEquiv).
Implementation note: the isomorphism is a StarAlgEquiv between the underlying *-subalgebras of
the bundled algebras gnsVonNeumannAlgebra π₁ and gnsVonNeumannAlgebra π₂; normality (weak
continuity) of the isomorphism is not required, since a *-isomorphism of von Neumann algebras is
automatically normal.
Blueprint: def:quasi-equivalence
open Physicslib4 GNS in
Physicslib4.GNS.UnitaryEquiv.quasiEquiv.{u_1, u_2, u_3} {A : Type u_1} [CStarAlgebra A] {H₁ : Type u_2}
[NormedAddCommGroup H₁] [InnerProductSpace ℂ H₁] [CompleteSpace H₁] {H₂ : Type u_3} [NormedAddCommGroup H₂]
[InnerProductSpace ℂ H₂] [CompleteSpace H₂] {π₁ : A →⋆ₐ[ℂ] H₁ →L[ℂ] H₁} {π₂ : A →⋆ₐ[ℂ] H₂ →L[ℂ] H₂}
(h : UnitaryEquiv π₁ π₂) : QuasiEquiv π₁ π₂#check UnitaryEquiv.quasiEquiv
Physicslib4.GNS.UnitaryEquiv.quasiEquiv.{u_1, u_2, u_3} {A : Type u_1} [CStarAlgebra A] {H₁ : Type u_2}
[NormedAddCommGroup H₁] [InnerProductSpace ℂ H₁] [CompleteSpace H₁] {H₂ : Type u_3} [NormedAddCommGroup H₂]
[InnerProductSpace ℂ H₂] [CompleteSpace H₂] {π₁ : A →⋆ₐ[ℂ] H₁ →L[ℂ] H₁} {π₂ : A →⋆ₐ[ℂ] H₂ →L[ℂ] H₂}
(h : UnitaryEquiv π₁ π₂) : QuasiEquiv π₁ π₂
The commutant \pi(A)', the algebra of intertwiners from \pi to itself, as a von Neumann
algebra:
🔗def
The commutant π(A)' of a representation, as a von Neumann algebra.
π(A)' consists of the bounded operators commuting with every π(a), that is, the intertwiners from
π to itself (mem_commutantVonNeumann_iff_intertwines). It is a von Neumann algebra because π(A)
is closed under adjoints and a commutant equals its own bicommutant (S''' = S'). π is
irreducible exactly when π(A)' is the scalars
(isIrreducible_iff_commutantVonNeumann_eq_scalars), and π(A)' and π(A)'' are each other's
commutants (commutant_gnsVonNeumannAlgebra, commutant_commutantVonNeumann).
Implementation note: the algebra is vonNeumannOfSelfAdjoint applied to the commutant
Set.centralizer (Set.range π), whose underlying set is again that commutant
(coe_commutantVonNeumann).
Blueprint: thrm:commutant-von-neumann
1.3.5. Direct sums and amplification🔗
Blueprint: def:direct-sum-representation, thrm:direct-sum-subrepresentation,
def:amplification, thrm:direct-sum-reducible.
🔗defPhysicslib4.GNS.directSum.{u_1, u_2, u_3} {A : Type u_1}
[CStarAlgebra A] {ι : Type u_2} {H : ι → Type u_3}
[(i : ι) → NormedAddCommGroup (H i)]
[(i : ι) → InnerProductSpace ℂ (H i)] [∀ (i : ι), CompleteSpace (H i)]
(π : (i : ι) → A →⋆ₐ[ℂ] H i →L[ℂ] H i) :
A →⋆ₐ[ℂ] ↥(lp H 2) →L[ℂ] ↥(lp H 2) Physicslib4.GNS.directSum.{u_1, u_2, u_3}
{A : Type u_1} [CStarAlgebra A]
{ι : Type u_2} {H : ι → Type u_3}
[(i : ι) → NormedAddCommGroup (H i)]
[(i : ι) → InnerProductSpace ℂ (H i)]
[∀ (i : ι), CompleteSpace (H i)]
(π : (i : ι) → A →⋆ₐ[ℂ] H i →L[ℂ] H i) :
A →⋆ₐ[ℂ] ↥(lp H 2) →L[ℂ] ↥(lp H 2)
The direct sum ⊕ᵢ πᵢ of a family of representations, acting on the Hilbert direct sum ⊕ᵢ Hᵢ.
A vector of ⊕ᵢ Hᵢ is a family x = (xᵢ) with xᵢ ∈ Hᵢ and Σᵢ ‖xᵢ‖² < ∞, and the direct sum acts
componentwise, (⊕ᵢ πᵢ)(a) x = (πᵢ(a) xᵢ)ᵢ: a block-diagonal operator with blocks πᵢ(a). It is
bounded by ‖a‖, because each πᵢ(a) is (a -homomorphism of C-algebras is contractive). Each
summand is a subrepresentation (intertwines_single), and the projection onto it lies in the
commutant (summandProj_mem_commutant), so a direct sum of two nonzero representations is
reducible (not_isIrreducible_directSum).
Implementation note: the Hilbert direct sum is Mathlib's ℓ²-space lp H 2, and the operator is
the diagonal lpDiag of the family πᵢ(a). The index type ι is arbitrary.
Blueprint: def:direct-sum-representation
🔗defPhysicslib4.GNS.amplification.{u_1, u_2, u_3} {A : Type u_1}
[CStarAlgebra A] {H₀ : Type u_2} [NormedAddCommGroup H₀]
[InnerProductSpace ℂ H₀] [CompleteSpace H₀] {ι : Type u_3}
(π : A →⋆ₐ[ℂ] H₀ →L[ℂ] H₀) :
A →⋆ₐ[ℂ] ↥(lp (fun x => H₀) 2) →L[ℂ] ↥(lp (fun x => H₀) 2) Physicslib4.GNS.amplification.{u_1, u_2,
u_3}
{A : Type u_1} [CStarAlgebra A]
{H₀ : Type u_2} [NormedAddCommGroup H₀]
[InnerProductSpace ℂ H₀]
[CompleteSpace H₀] {ι : Type u_3}
(π : A →⋆ₐ[ℂ] H₀ →L[ℂ] H₀) :
A →⋆ₐ[ℂ]
↥(lp (fun x => H₀) 2) →L[ℂ]
↥(lp (fun x => H₀) 2)
The amplification ι·π of a representation π: the direct sum of copies of π indexed by ι.
It acts on the Hilbert direct sum ℓ²(ι, H₀) of copies of H₀, by π(a) in every copy, that is, on
H₀ ⊗ ℓ²(ι) by π(a) ⊗ 1. It is π with multiplicity |ι|: π embeds in it as each summand
(amplification_intertwines_single), and with two or more copies on a nonzero space it is
reducible (not_isIrreducible_directSum).
Implementation note: amplification is directSum of the constant family. That π and ι·π are
quasi-equivalent is not proved; it needs the commutant of an amplification, (π ⊗ 1)' =
π' ⊗ B(ℓ²(ι)), which Mathlib does not provide.
Blueprint: def:amplification
The projection onto one summand commutes with the direct sum
(summandProj_mem_commutant), and it is not a scalar when its own summand and another summand
are both nonzero:
open Physicslib4 GNS in
Physicslib4.GNS.not_isIrreducible_directSum.{u_1, u_2, u_3} {A : Type u_1} [CStarAlgebra A] {ι : Type u_2}
[DecidableEq ι] {H : ι → Type u_3} [(i : ι) → NormedAddCommGroup (H i)] [(i : ι) → InnerProductSpace ℂ (H i)]
[∀ (i : ι), CompleteSpace (H i)] (π : (i : ι) → A →⋆ₐ[ℂ] H i →L[ℂ] H i) {j k : ι} (hjk : j ≠ k) {v : H j} (hv : v ≠ 0)
{w : H k} (hw : w ≠ 0) : ¬GNS.IsIrreducible (directSum π)#check not_isIrreducible_directSum
Physicslib4.GNS.not_isIrreducible_directSum.{u_1, u_2, u_3} {A : Type u_1} [CStarAlgebra A] {ι : Type u_2}
[DecidableEq ι] {H : ι → Type u_3} [(i : ι) → NormedAddCommGroup (H i)] [(i : ι) → InnerProductSpace ℂ (H i)]
[∀ (i : ι), CompleteSpace (H i)] (π : (i : ι) → A →⋆ₐ[ℂ] H i →L[ℂ] H i) {j k : ι} (hjk : j ≠ k) {v : H j} (hv : v ≠ 0)
{w : H k} (hw : w ≠ 0) : ¬GNS.IsIrreducible (directSum π)
1.3.6. Covariance🔗
Blueprint: def:state-pullback, thrm:pure-pullback-invariant,
thrm:gns-covariance, thrm:gns-covariance-unitary-equiv,
thrm:gns-sector-transport, and, for the unitary implementation,
thrm:invariant-state-gns-unitary and
thrm:invariant-state-gns-unitary-strongly-continuous, of which the theorems below are the
general form.
🔗def
The pullback ω ∘ π of a state ω on B along a unital *-homomorphism π : A → B: a ↦ ω(π(a)).
Positivity follows from π(a* a) = π(a)* π(a), and normalisation from π(1) = 1, since a positive
functional has norm equal to its value at 1. The pullback is contravariantly functorial
(State.comp_id, State.comp_comp): a *-homomorphism A → B gives a map from the states of B to
the states of A. Along a *-isomorphism Φ, purity is preserved in both directions
(isPure_comp_iff), and the GNS representation of ω ∘ Φ is that of ω composed with Φ, up to
unitary equivalence (unitaryEquiv_comp_of_gns). An example is the restriction of a global
state to a local algebra along the inclusion ι_B.
Implementation note: π enters as a continuous linear map through starAlgHomCLM, since a
-homomorphism of C-algebras is contractive. The automorphism case is also available as
State.precomp.
Blueprint: def:state-pullback
Pulling back along a *-isomorphism preserves purity in both directions:
open Physicslib4 GNS in
Physicslib4.GNS.isPure_comp_iff.{u_1, u_2} {A : Type u_1} [CStarAlgebra A] {B : Type u_2} [CStarAlgebra B]
(Φ : A ≃⋆ₐ[ℂ] B) (ω : State B) : IsPure (ω.comp Φ.toStarAlgHom) ↔ IsPure ω#check isPure_comp_iff
Physicslib4.GNS.isPure_comp_iff.{u_1, u_2} {A : Type u_1} [CStarAlgebra A] {B : Type u_2} [CStarAlgebra B]
(Φ : A ≃⋆ₐ[ℂ] B) (ω : State B) : IsPure (ω.comp Φ.toStarAlgHom) ↔ IsPure ω
The automorphism case, with State.precomp, is isPure_precomp_iff. The GNS data of
\omega \circ \Phi and of \omega correspond through a unitary: for a cyclic representation
(H_1, \pi_1, \Omega_1) of A reproducing \omega \circ \Phi and one, (H_2, \pi_2, \Omega_2),
of B reproducing \omega, there is U with U\Omega_1 = \Omega_2 and
U\pi_1(a) = \pi_2(\Phi(a))U:
open Physicslib4 GNS in
Physicslib4.GNS.exists_unitary_of_gns_comp.{u_1, u_2, u_4, u_5} {A : Type u_1} [CStarAlgebra A] {B : Type u_2}
[CStarAlgebra B] (Φ : A ≃⋆ₐ[ℂ] B) (ω : State B) {H₁ : Type u_4} [NormedAddCommGroup H₁] [InnerProductSpace ℂ H₁]
[CompleteSpace H₁] (π₁ : A →⋆ₐ[ℂ] H₁ →L[ℂ] H₁) (Ω₁ : H₁) (hcyc₁ : IsCyclicVector π₁ Ω₁)
(hrep₁ : ∀ (a : A), (ω.comp Φ.toStarAlgHom) a = inner ℂ Ω₁ ((π₁ a) Ω₁)) {H₂ : Type u_5} [NormedAddCommGroup H₂]
[InnerProductSpace ℂ H₂] [CompleteSpace H₂] (π₂ : B →⋆ₐ[ℂ] H₂ →L[ℂ] H₂) (Ω₂ : H₂) (hcyc₂ : IsCyclicVector π₂ Ω₂)
(hrep₂ : ∀ (b : B), ω b = inner ℂ Ω₂ ((π₂ b) Ω₂)) :
∃ U, U Ω₁ = Ω₂ ∧ ∀ (a : A) (x : H₁), U ((π₁ a) x) = (π₂ (Φ a)) (U x)#check exists_unitary_of_gns_comp
Physicslib4.GNS.exists_unitary_of_gns_comp.{u_1, u_2, u_4, u_5} {A : Type u_1} [CStarAlgebra A] {B : Type u_2}
[CStarAlgebra B] (Φ : A ≃⋆ₐ[ℂ] B) (ω : State B) {H₁ : Type u_4} [NormedAddCommGroup H₁] [InnerProductSpace ℂ H₁]
[CompleteSpace H₁] (π₁ : A →⋆ₐ[ℂ] H₁ →L[ℂ] H₁) (Ω₁ : H₁) (hcyc₁ : IsCyclicVector π₁ Ω₁)
(hrep₁ : ∀ (a : A), (ω.comp Φ.toStarAlgHom) a = inner ℂ Ω₁ ((π₁ a) Ω₁)) {H₂ : Type u_5} [NormedAddCommGroup H₂]
[InnerProductSpace ℂ H₂] [CompleteSpace H₂] (π₂ : B →⋆ₐ[ℂ] H₂ →L[ℂ] H₂) (Ω₂ : H₂) (hcyc₂ : IsCyclicVector π₂ Ω₂)
(hrep₂ : ∀ (b : B), ω b = inner ℂ Ω₂ ((π₂ b) Ω₂)) :
∃ U, U Ω₁ = Ω₂ ∧ ∀ (a : A) (x : H₁), U ((π₁ a) x) = (π₂ (Φ a)) (U x)
In the language of UnitaryEquiv this is
unitaryEquiv_comp_of_gns, and with it
irreducibility and the factor property transport along \Phi
(isIrreducible_iff_of_gns_comp, isFactor_iff_of_gns_comp).
The unitary implementation of a symmetry that leaves \omega invariant is
exists_gns_unitary_of_invariant.
For *-automorphisms \gamma_g of A, g in a monoid G, with
\gamma_{g'g} = \gamma_{g'} \circ \gamma_g, \gamma_1 = \mathrm{id} and
\omega \circ \gamma_g = \omega, it gives a GNS triple of \omega and unitaries U(g) with
U(g)\,\pi(a)\Omega = \pi(\gamma_g(a))\,\Omega, \quad U(g)\,\Omega = \Omega, \quad U(g'g) = U(g')\,U(g), \quad U(1) = \mathbf{1},
and U(g)\,\pi(a)\,U(g)^{-1} = \pi(\gamma_g(a)) on all of H.
exists_gns_unitaryRep_of_invariant
takes \gamma and returns U as monoid homomorphisms. When G has a topology and the matrix
coefficients g \mapsto \omega(a^*\gamma_g(b)) are continuous, g \mapsto U(g)\psi is
continuous for every \psi
(exists_gns_unitary_of_invariant_strongContinuous,
exists_gns_unitaryRep_of_invariant_strongContinuous).
These statements are long existentials over the Hilbert space and its structure, so they are
linked rather than printed.